JSpecify mode: a `@Nullable Object[]` passed to an unmarked method's `@NonNull Object[]` parameter is not reported

Open
  • Is something wrong?
#2,044 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
55/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
java
Domain
devtools, testing-qa

Research direction

Start by reading the JSpecify handling for unmarked code and the related #1488 report; the payload identifies the array element type as the failing case. Reproduce the missing diagnostic with a CompilationTestHelper test using the provided Lib and Test examples and flags. Done means the test reports the incompatible nullable-to-non-null array argument while preserving the return-type diagnostic.

Written by the indexing model from the issue text.

Description

false negative jspecify

With JSpecify mode on, passing an array with @Nullable elements to a parameter declared with @NonNull elements is reported when the callee is annotated code, and is not reported when the callee is unannotated or @NullUnmarked. The restrictive annotation on the return type of the same unmarked class is honored: assigning its @Nullable Object[] result to an Object[] local is reported.

Versions: NullAway master at e91ea4bcf and the 0.14.2 release give the same result. Error Prone 2.50.0, JDK 21.0.9. Flags: -XepOpt:NullAway:AnnotatedPackages=com.uber -XepOpt:NullAway:JSpecifyMode=true -XDaddTypeAnnotationsToSymbol=true, and the same with -XepOpt:NullAway:JSpecifyExperimental=true added.

Code sample. I ran it as a CompilationTestHelper test with makeTestHelperWithArgs, without // BUG: markers, so the helper lists every diagnostic.

package foo.unannotated;
public class Lib {
  public static void takes(@org.jspecify.annotations.NonNull Object[] a) {}
  public static @org.jspecify.annotations.Nullable Object[] gives() { return new Object[1]; }
}

package com.uber;
import foo.unannotated.Lib;
import org.jspecify.annotations.Nullable;
public class Test {
  void pass(@Nullable Object[] arr) {
    Lib.takes(arr);
  }
  Object[] ret() {
    Object[] r = Lib.gives();
    return r;
  }
}

Expected: a diagnostic on line 6 (Lib.takes(arr)), as there is when Lib is in com.uber:

/Test.java:6: warning: [NullAway] incompatible types: @Nullable Object [] cannot be converted to Object []

The JSpecify spec gives a type usage annotated @NonNull the MINUS_NULL nullness operator before it consults the null-marked scope ("Augmented type of a type usage appearing in code"), so the element type of takes's parameter is non-null in unmarked code too. NullAway already applies this to the return type on line 9.

Actual: with Lib in foo.unannotated, and with Lib as a @NullUnmarked class in com.uber, in both flag configurations and both versions:

/Test.java:9: warning: [NullAway] incompatible types: @Nullable Object [] cannot be converted to Object []

Line 6 gets no diagnostic. With Lib as annotated code in com.uber, lines 6 and 9 are both reported.

#1488 reports the same kind of gap for a restrictive annotation on a type argument (Foo<@NonNull T>) of an @NullUnmarked method's parameter; this one is the array element type. Found while checking array types for #1028.

Dominant language
Java
Stars
4.1k
Forks
379
Avg merge
1d 2h
Merged PRs (30d)
106

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from uber/NullAway

All issues in uber/NullAway

Similar issues

More Java issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.