Array creation annotation checks (#928)

Co-authored-by: Werner Dietl <wdietl@gmail.com>

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

@@ -348,7 +348,14 @@ public Void visitNewArray(NewArrayTree tree, Void p) {
                     componentType.getAnnotations(),
                     type.toString());
         }
-
+        // type already contains substituted annotations so must look at original tree annotations
+        List<? extends AnnotationMirror> annotations =
+                TreeUtils.annotationsFromArrayCreation(tree, 0);
+        if (AnnotationUtils.containsSame(annotations, NULLABLE)
+                || AnnotationUtils.containsSame(annotations, MONOTONIC_NONNULL)
+                || AnnotationUtils.containsSame(annotations, POLYNULL)) {
+            checker.reportError(tree, "nullness.on.new.array");
+        }
         return super.visitNewArray(tree, p);
     }
 

checker/src/main/java/org/checkerframework/checker/nullness/messages.properties

@@ -23,6 +23,7 @@ instanceof.nullable=instanceof is only true for a non-null expression
 instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof
 new.array.type.invalid=annotations %s may not be applied as component type for array "%s"
 nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null
+nullness.on.new.array=do not write nullness annotations on an array creation, which is always non-null
 nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null
 nullness.on.exception.parameter=do not write nullness annotations on an exception parameter, which is always non-null
 nullness.on.outer=nullness annotations are not applicable to outer types

checker/tests/nullness/ArrayCreation.java

@@ -0,0 +1,13 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class ArrayCreation {
+
+    void foo() {
+        // :: error: (nullness.on.new.array)
+        int[] o = new int @Nullable [10];
+    }
+
+    void bar() {
+        int[] @Nullable [] o = new int[10] @Nullable [];
+    }
+}

docs/CHANGELOG.md

@@ -6,6 +6,9 @@ Version 3.42.0-eisop5 (November ??, 2024)
 Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1.
 Use `-ApermitMissingJdk` instead.
 
+The Nullness Checker now reports an error if an array creation is annotated with `@Nullable`,
+as array creations are intrinsically non-null.
+
 **Implementation details:**
 
 Changed `org.checkerframework.framework.util.ContractsFromMethod` to an interface.
@@ -16,7 +19,7 @@ Make `SourceChecker#suppressWarningsString` protected to allow adaptation in sub
 
 **Closed issues:**
 
-eisop#413, eisop#777, eisop#782, eisop#982.
+eisop#413, eisop#777, eisop#782, eisop#927, eisop#982.
 
 
 Version 3.42.0-eisop4 (July 12, 2024)