Cannot use ternary operator to check null

[blackdiz]

Hi, I am doing some tests about the checker framework, but I find that using a ternary operator can't eliminate the dereference.of.nullable error and I'm not sure why.

• commands (that can be cut-and-pasted into a command shell),
  gradle build

• inputs,

public class App {
   public static void main(String[] args) {
       TernaryTest t = new TernaryTest();
       byte[] b = t.getA() != null ? t.getA().getBytes() : new byte[1];
   }

   public static class TernaryTest {
       @Nullable
       private String a;

       @Nullable
       public String getA() {
           return a;
       }
   }
}

• outputs,

/Users/luke/source-code/checker-framework-test/app/build/generated/sources/delombok/java/main/checker/framework/test/App.java:13: error: [dereference.of.nullable] dereference of possibly-null reference t.getA()
       byte[] b = t.getA() != null ? t.getA().getBytes() : new byte[1];
                                           ^

• expectation.
  I think the t.getA() != null part has checked the nullability already, but I still get the error and don't know why?

[mernst]

The Checker Framework reasons about each method individually, using only the specification (not the implementation) of methods that it calls. In particular, when analyzing the body of main, it uses the specification of getA(). In general, a method might return different values each time the method is called, and the Checker Framework makes that assumption, for soundness.

To indicate that getA() returns the same value every time it is called on the same receiver, annotate its definition with @Deterministic.

Here are two relevant sections in the Checker Framework manual:
https://checkerframework.org/manual/#purity-annotations
https://checkerframework.org/manual/#handling-warnings-step2

[blackdiz]

I see, thank you for your kind explanation. I'll just close the issue.

[mernst]

I'm glad that helped.

If you pass the -AassumeDeterministic command-line option, then the Checker Framework assumes that every method is deterministic. This is not a sound assumption, but it does handle cases like yours without the need for a @Deterministic annotation.