Incorrect nullness inference for array constructors

[GoogleCodeExporter]

Is this a known issue? I couldn't find documentation for it.

=== Test.java ===
class Test {
  public static void main(String[] args) {
    String array[] = new String[3];
    array[0].length(); // NPE here
  }
}
===

$ ~/jsr308/checker-framework-1.9.1/checker/bin/javac -version -processor 
org.checkerframework.checker.nullness.NullnessChecker Test.java 
javac 1.8.0-jsr308-1.9.1

# compiles cleanly

$ java Test
Exception in thread "main" java.lang.NullPointerException
    at Test.main(Test.java:4)

Original issue reported on code.google.com by cus...@google.com on 14 May 2015 at 6:59

[GoogleCodeExporter]

Thanks for this report!
The manual describes a similar situation at:

http://types.cs.washington.edu/checker-framework/current/checker-framework-manua
l.html#nullness-arrays

This definitely worked as described at some point, but obviously broke and no 
test case caught the issue.

Original comment by wdi...@gmail.com on 15 May 2015 at 5:35

• Changed state: Accepted
• Added labels: Priority-High
• Removed labels: Priority-Medium

[GoogleCodeExporter]

I've now looked at the code and see that this check is guarded by a
-Aarrays:forbidnonnullcomponents
flag.
However, that flag doesn't work: it violates a javac flag naming convention.
The code mentions Issues 154 and 322 as references.

We should decide whether to document the flag or switch the default (and add a 
flag for the current, unsound, behavior?).

Original comment by wdi...@gmail.com on 15 May 2015 at 6:02

[GoogleCodeExporter]

I think we should definitely document the flag.  This means:
 * rename the flag to obey javac naming conventions
 * document the flag in section 3.3.4, "Nullness and arrays"
 * mention the flag in section 2.2.1, "Summary of command-line options"

What should the name be, and what should the default be?

I am inclined to default the Checker Framework to sound behavior, and require a 
user to suppress the warnings (easy, because there is a unique key 
"new.array.type.invalid") or pass a command-line argument to suppress 
"new.array.type.invalid" warnings.

Here are some possibilities for the name of the flag:
  -AignoreUnitializedArrays
  -ApermitUnitializedArrays
  -AignoreNullArrayElements
  -AsuppressWarnings=new.array.type.invalid

Original comment by michael.ernst@gmail.com on 22 May 2015 at 9:00