Handle the InitializationChecker as upstream checker (#991)

Co-authored-by: Werner Dietl <wdietl@gmail.com>
eisop · Dec 9, 2024 · c31ab6a · c31ab6a
1 parent 101aae1
commit c31ab6a
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 5 deletions.
diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java
@@ -12,6 +12,7 @@
 import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.signature.qual.FullyQualifiedName;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 
 import java.util.ArrayList;
@@ -87,6 +88,20 @@ public InitializationChecker() {}
      */
     public abstract Class<? extends BaseTypeChecker> getTargetCheckerClass();
 
+    /**
+     * Also handle {@code AnnotatedFor} annotations for this checker. See {@link
+     * InitializationFieldAccessSubchecker#getUpstreamCheckerNames()} and the two implementations
+     * should be kept in sync.
+     */
+    @Override
+    public List<@FullyQualifiedName String> getUpstreamCheckerNames() {
+        if (upstreamCheckerNames == null) {
+            super.getUpstreamCheckerNames();
+            upstreamCheckerNames.add(InitializationChecker.class.getName());
+        }
+        return upstreamCheckerNames;
+    }
+
     @Override
     public NavigableSet<String> getSuppressWarningsPrefixes() {
         NavigableSet<String> result = super.getSuppressWarningsPrefixes();

diff --git a/...java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java b/...java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java
@@ -25,7 +25,11 @@ public class InitializationFieldAccessSubchecker extends BaseTypeChecker {
     /** Default constructor for InitializationFieldAccessSubchecker. */
     public InitializationFieldAccessSubchecker() {}
 
-    /** Also handle {@code AnnotatedFor} annotations for the {@link InitializationChecker}. */
+    /**
+     * Also handle {@code AnnotatedFor} annotations for the {@link InitializationChecker}. See
+     * {@link InitializationChecker#getUpstreamCheckerNames()} and the two implementations should be
+     * kept in sync.
+     */
     @Override
     public List<@FullyQualifiedName String> getUpstreamCheckerNames() {
         if (upstreamCheckerNames == null) {

diff --git a/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java b/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java
@@ -34,12 +34,13 @@ Object unannotatedFor(Object test) {
 
     @AnnotatedFor("nullness")
     void foo(@Initialized AnnotatedForNullness this) {
-        // Expect an error because conservative defaults are applied to `unannotatedFor` and it
-        // expects a @FBCBottom @KeyForBottom @Nonull Object.
+        // Expect two [argument.type.incompatible] errors in KeyForChecker and InitilizationChecker
+        // because conservative defaults are applied to `unannotatedFor` and it expects a @FBCBottom
+        // @KeyForBottom @Nonull Object.
         // ::error: (argument.type.incompatible)
         unannotatedFor(initializedField);
-        // Expect an error because conservative defaults are applied to `annotatedForInitialization`
-        // for hierarchies other than the Initialization Checker and
+        // Expect an error in KeyForChecker because conservative defaults are applied to
+        // `annotatedForInitialization` for hierarchies other than the Initialization Checker and
         // it expects an @Initialized @KeyForBottom @Nonull Object.
         // ::error: (argument.type.incompatible)
         annotatedForInitialization(initializedField);
@@ -52,4 +53,24 @@ void foo(@Initialized AnnotatedForNullness this) {
         annotatedForNullness(initializedField);
         annotatedForNullnessAndInitialization(initializedField);
     }
+
+    @AnnotatedFor("initialization")
+    void bar() {
+        // Expect an error in InitilizationChecker because conservative defaults are applied to
+        // `unannotatedFor` and it expects a @FBCBottom @UnknownKeyFor @Nonull Object.
+        // ::error: (argument.type.incompatible)
+        unannotatedFor(initializedField);
+        // Do not expect an error because the warning is suppressed other than initialzation
+        // hierarchy when conservative defaults are applied to source code and it expects an
+        // @Initialized @KeyForBottom @Nonull Object.
+        annotatedForInitialization(initializedField);
+        // Do not expect an error when conservative defaults are applied to
+        // `annotatedForInitialization` for hierarchies other than the Initialization Checker and
+        // it expects an @Initialized @KeyForBottom @Nonull Object.
+        annotatedForInitialization(initializedKeyForBottomField);
+        // Do not expect an error because these are AnnotatedFor("nullness") and these expect
+        // @Initialized @UnknownKeyFor @Nonnull Object.
+        annotatedForNullness(initializedField);
+        annotatedForNullnessAndInitialization(initializedField);
+    }
 }