Nullness checker fails to handle freshly instantiated value inside a for-loop

[GoogleCodeExporter]

Attached is a simple reproducer java class, where a lazily instantiated field 
is initialized with some values directly after an if-block in which it is 
instantiated.

Nullness checker reports a possibly-null dereference right after the field is 
initialized but ONLY IF the field is used inside a for-loop:

In another words, this is considered OK:

if (this.field == null) { this.field = new ...; }

this.field.use(); // <-- this is ok.

but this is considered an error:

if (this.field == null) { this.field = new ...; }

for(int i = 0; i < 10; ++i) this.field.use(); // <-- this is reported as error

What steps will reproduce the problem?
1. Use the attached Main.java file.
2. $CHECKERFRAMEWORK/bin/java -processor 
org.checkerframework.checker.nullness.NullnessChecker Main.java

What is the expected output? What do you see instead?
    No errors, because IMHO the field can never be null at the reported position.

What version of the product are you using? On what operating system?
    1.8.11

Original issue reported on code.google.com by metl...@gmail.com on 3 Apr 2015 at 10:07

Attachments:

• Main.java

[GoogleCodeExporter]

I tried reproducing this issue, but neither release 1.8.11 nor trunk give a 
warning for Main.java. Can you check your test case?

However, I think an error should be raised, and I created Issue 425 with a 
reproduction without for loop.

Original comment by wdi...@gmail.com on 4 Apr 2015 at 2:53

• Changed state: Accepted

[GoogleCodeExporter]

Sorry, in my attempts to minimize the test case I apparently got lost and 
mightily confused :)

I'm attaching a new reproducer that should illustrate the issue.

Run with 1.8.11:
$CHECKER_HOME/checker/bin/javac -processor NullnessChecker Issue424.java

Original comment by metl...@gmail.com on 7 Apr 2015 at 5:33

Attachments:

• Issue424.java