Type refinement and anonymous classes

[GoogleCodeExporter]

The following code should be safe, but the nullness checker still emits an 
error.

I understand the issues with @Nullable fields in general, but in the case where 
the field is also final or @MonotonicNonNull, shouldn't the null checks 
guarantee that all subsequent accesses are safe?

===
import org.checkerframework.checker.nullness.qual.*;

class Test {

  @MonotonicNonNull Object field1 = null;
  final @Nullable Object field2 = null;

  void m() {
    if (field1 != null) {
      new Object() {
        void f() {
          field1.toString(); // dereference of possibly-null reference
        }
      };
    }
  }

  void n() {
    if (field2 != null) {
      new Object() {
        void f() {
          field2.toString(); // dereference of possibly-null reference
        }
      };
    }
  }
}
===

$ ~/jsr308/checker-framework-1.8.11/checker/bin/javac -version -processor 
org.checkerframework.checker.nullness.NullnessChecker Test.java
javac 1.8.0-jsr308-1.8.11
Test.java:12: error: [dereference.of.nullable] dereference of possibly-null 
reference field1
          field1.toString(); // dereference of possibly-null reference
          ^
Test.java:22: error: [dereference.of.nullable] dereference of possibly-null 
reference field2
          field2.toString(); // dereference of possibly-null reference
          ^
2 errors

Original issue reported on code.google.com by cus...@google.com on 14 Mar 2015 at 2:29

• Merged into: #266

[GoogleCodeExporter]

I agree with your analysis.  This looks like an imprecision in the dataflow 
analysis.
I have added your test case as file
checker-framework/checker/tests/nullness/Issue411.java .  It's currently 
skipped to avoid breaking the build.

Original comment by michael.ernst@gmail.com on 16 Mar 2015 at 2:44

• Changed state: Accepted
• Added labels: Dataflow

[GoogleCodeExporter]

Isn't this the same as Issue 266 
(https://code.google.com/p/checker-framework/issues/detail?id=266)?

Original comment by wdi...@gmail.com on 16 Mar 2015 at 8:37

[GoogleCodeExporter]

You're right, although the other bug doesn't mention @MonotonicNonNull. Sorry 
for the duplicate.

Original comment by cus...@google.com on 16 Mar 2015 at 8:48

[GoogleCodeExporter]

I'm merging the issues.
Testing for @MonotonicNonNull should be done, but should come for free once the 
Store has the correct information.
Issue 266 has a simple workaround. Are you running into this issue a lot? 
Should this issue get a higher priority?

Original comment by wdi...@gmail.com on 16 Mar 2015 at 8:53

• Changed state: Duplicate

[GoogleCodeExporter]

I'm merging the issues.
Testing for @MonotonicNonNull should be done, but should come for free once the 
Store has the correct information.
Issue 266 has a simple workaround. Are you running into this issue a lot? 
Should this issue get a higher priority?

Original comment by wdi...@gmail.com on 16 Mar 2015 at 8:53

[GoogleCodeExporter]

There was one report recently, I wouldn't say its high priority. Having to use 
workarounds (even if they're simple) can be discouraging to people trying to 
adopt the tool, though.

Original comment by cus...@google.com on 16 Mar 2015 at 9:02