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