The nullness checker should not allow @NonNull for uninitialized array elements

[GoogleCodeExporter]

When I run the nullness checker on a class with the following method, the 
checker doesn't report any errors:

  static Object[] createObjects() {
    @NonNull Object [] oa = new @NonNull Object[10];
    return oa;
  }

However, as explained in section 3.3.4 "Nullness and arrays" of the checker 
framework manual, the nullness checker should report an error because the 
elements of the "oa" array are null.

What version of the product are you using? On what operating system?
checker framework 1.8.0, linux

Original issue reported on code.google.com by reprogra...@gmail.com on 26 Apr 2014 at 2:48

[GoogleCodeExporter]

At the moment this check is turned off by default.
One needs to provide the -Alint=arrays:forbidnonnullcomponents option to turn 
this check on.
The manual doesn't document this flag, which is an issue we should fix.
Alternatively, we should discuss whether the default should be to enable this 
check and whether we want an option to turn off the check.

I assume the reason we have this option is to avoid many false positives, 
created by the common pattern of first creating an array and then immediately 
initializing all fields (see Issue 154).

Original comment by wdi...@gmail.com on 10 May 2014 at 10:06

• Changed state: Accepted