Introduce @UnannnotatedFor

checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java

@@ -0,0 +1,39 @@
+package org.checkerframework.framework.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that this class has not been annotated for the given type system, even though an
+ * enclosing element is annotated for it. For example, if a package is
+ * {@code @AnnotatedFor("nullness")} but one of its classes has not been annotated with
+ * {@code @Nullable} and friends, mark that class {@code @UnannotatedFor("nullness")}. The argument
+ * to {@code UnannotatedFor} is not an annotation name, but a checker name.
+ *
+ * <p>This annotation has no effect unless the {@code
+ * -AuseConservativeDefaultsForUncheckedCode=source} command-line argument is supplied. It only
+ * subtracts from the scope of an enclosing {@link AnnotatedFor}: an element in its scope is
+ * defaulted using conservative defaults and its warnings are suppressed, as if no enclosing
+ * {@code @AnnotatedFor} were present. An {@code @AnnotatedFor} on a nested element takes effect
+ * again for that element.
+ *
+ * @checker_framework.manual #compiling-libraries Compiling partially-annotated libraries
+ */
+@Documented
+@Retention(RetentionPolicy.SOURCE)
+@Target({ElementType.TYPE, ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.PACKAGE})
+public @interface UnannotatedFor {
+    /**
+     * Returns the type systems for which the class has not been annotated. Legal arguments are any
+     * string that may be passed to the {@code -processor} command-line argument: the
+     * fully-qualified class name for the checker, or a shorthand for built-in checkers. Using the
+     * annotation with no arguments, as in {@code @UnannotatedFor({})}, has no effect.
+     *
+     * @return the type systems for which the class has not been annotated
+     * @checker_framework.manual #shorthand-for-checkers Short names for built-in checkers
+     */
+    String[] value();
+}

checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java

@@ -0,0 +1,34 @@
+package org.checkerframework.checker.test.junit;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+import java.io.File;
+import java.util.List;
+
+/** JUnit tests for the Nullness checker. */
+public class NullnessUnannotatedForTest extends CheckerFrameworkPerDirectoryTest {
+
+    /**
+     * Create a NullnessNullMarkedTest.
+     *
+     * @param testFiles the files containing test code, which will be type-checked
+     */
+    public NullnessUnannotatedForTest(List<File> testFiles) {
+        super(
+                testFiles,
+                org.checkerframework.checker.nullness.NullnessChecker.class,
+                "nullness",
+                "-AuseConservativeDefaultsForUncheckedCode=source");
+    }
+
+    /**
+     * This method returns the directory containing test code.
+     *
+     * @return the directories containing test code
+     */
+    @Parameters
+    public static String[] getTestDirs() {
+        return new String[] {"nullness-unannotatedfor"};
+    }
+}

checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java

@@ -0,0 +1,57 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.AnnotatedFor;
+import org.checkerframework.framework.qual.UnannotatedFor;
+
+public class NullnessUnannotatedForTest {
+    @AnnotatedFor("nullness")
+    class A {
+        // :: error: (assignment.type.incompatible)
+        Object o = null;
+    }
+
+    @AnnotatedFor("nullness")
+    class B {
+        @UnannotatedFor("nullness")
+        void method(@Nullable Object o) {
+            o.toString();
+        }
+    }
+
+    @AnnotatedFor("nullness")
+    class Lambdas {
+        // A lambda body is in the scope of the @UnannotatedFor method that contains it, even
+        // though a lambda is not itself a declaration.
+        @UnannotatedFor("nullness")
+        Runnable excluded(@Nullable Object o) {
+            return () -> o.toString();
+        }
+
+        Runnable included(@Nullable Object o) {
+            // :: error: (dereference.of.nullable)
+            return () -> o.toString();
+        }
+    }
+
+    @AnnotatedFor("nullness")
+    class C {
+        // @UnannotatedFor only subtracts from the enclosing scope, so a nested @AnnotatedFor takes
+        // effect again.
+        @UnannotatedFor("nullness")
+        class Excluded {
+            Object unannotated = null;
+
+            @AnnotatedFor("nullness")
+            void reannotated(@Nullable Object o) {
+                // :: error: (dereference.of.nullable)
+                o.toString();
+            }
+        }
+
+        // An @UnannotatedFor for a different checker does not exclude this class.
+        @UnannotatedFor("regex")
+        class UnannotatedForOtherChecker {
+            // :: error: (assignment.type.incompatible)
+            Object o = null;
+        }
+    }
+}

checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java

@@ -0,0 +1,12 @@
+package packageunannotatedfornullness;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.UnannotatedFor;
+
+@UnannotatedFor("nullness")
+public class Excluded {
+    void foo(@Nullable Object o) {
+        // No error: @UnannotatedFor excludes this class from the package's @AnnotatedFor scope.
+        o.toString();
+    }
+}

checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java

@@ -0,0 +1,10 @@
+package packageunannotatedfornullness;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Included {
+    void foo(@Nullable Object o) {
+        // :: error: (dereference.of.nullable)
+        o.toString();
+    }
+}

checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java

@@ -0,0 +1,4 @@
+@AnnotatedFor("nullness")
+package packageunannotatedfornullness;
+
+import org.checkerframework.framework.qual.AnnotatedFor;

docs/CHANGELOG.md

@@ -3,6 +3,13 @@ Version 3.49.5-eisop2 (June ?, 2026)
 
 **User-visible changes:**
 
+New declaration annotation `@UnannotatedFor`, which excludes a package, class, method, or
+constructor from the scope of an enclosing `@AnnotatedFor` for the given checkers. Its scope is
+defaulted using conservative defaults and its warnings are suppressed, as if no enclosing
+`@AnnotatedFor` were present; a nested `@AnnotatedFor` takes effect again. Like `@AnnotatedFor`,
+it has no effect unless `-AuseConservativeDefaultsForUncheckedCode=source` or `-AonlyAnnotatedFor`
+is supplied.
+
 The Checker Framework now issues an `annotation.on.supertype` error when an annotation supported by
 the checker is written as a main annotation on the superclass or interface in an `extends` or
 `implements` clause. Annotations on the supertype's type arguments remain permitted. A checker

docs/manual/annotating-libraries.tex

@@ -436,6 +436,16 @@
 any annotations, but that you examined the source code and verified
 that all appropriate annotations are present.
 
+The \refqualclass{framework/qual}{UnannotatedFor} annotation is the inverse:
+it excludes a package, class, method, or constructor from the scope of an
+enclosing \<@AnnotatedFor>.  For example, if a package is
+\<@AnnotatedFor("nullness")> but one class in it has not been annotated, write
+\<@UnannotatedFor("nullness")> on that class; it is then treated as unchecked
+code, exactly as if the package had no \<@AnnotatedFor>.  An \<@AnnotatedFor>
+on a nested element takes effect again for that element.
+\refqualclass{framework/qual}{UnannotatedFor}'s arguments are checker names,
+in the same format as \refqualclass{framework/qual}{AnnotatedFor}'s.
+
 \begin{sloppypar}
 Whenever you compile a class using the Checker Framework, including when
 using the \<-AuseConservativeDefaultsForUncheckedCode=source,bytecode> command-line

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java

@@ -6,6 +6,7 @@
 import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.source.SourceChecker;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
@@ -76,7 +77,8 @@ public abstract class BaseTypeChecker extends SourceChecker {
 
     /**
      * A mapping from an element to whether it is in an {@code @AnnotatedFor} scope for this checker
-     * or an upstream checker.
+     * or an upstream checker. The value is the fully-resolved answer for the element: it accounts
+     * for enclosing elements and for {@code @UnannotatedFor} exclusions.
      */
     private final IdentityHashMap<Element, Boolean> elementAnnotatedForThisCheckerOrUpstreamCache =
             new IdentityHashMap<>();
@@ -344,7 +346,10 @@ public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Eleme
                 annotatedFor != null
                         && atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor);
 
-        if (!elementAnnotatedForThisChecker) {
+        // @UnannotatedFor only subtracts from an enclosing @AnnotatedFor scope, so consult it only
+        // when this element is not itself annotated for this checker, and let it stop the walk to
+        // the enclosing element.
+        if (!elementAnnotatedForThisChecker && !isElementUnannotatedForThisChecker(elt)) {
             Element parent;
             if (elt.getKind() == ElementKind.PACKAGE) {
                 parent =
@@ -362,4 +367,19 @@ public boolean isElementAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Eleme
         elementAnnotatedForThisCheckerOrUpstreamCache.put(elt, elementAnnotatedForThisChecker);
         return elementAnnotatedForThisChecker;
     }
+
+    /**
+     * Is {@code elt} annotated with an {@code @UnannotatedFor} that applies to this checker or an
+     * upstream checker? Unlike {@link #isElementAnnotatedForThisCheckerOrUpstreamChecker}, this
+     * does not consider enclosing elements.
+     *
+     * @param elt the element to check
+     * @return true if {@code elt} is excluded from an enclosing {@code @AnnotatedFor} scope
+     */
+    private boolean isElementUnannotatedForThisChecker(Element elt) {
+        AnnotatedTypeFactory atypeFactory = getTypeFactory();
+        AnnotationMirror unannotatedFor = atypeFactory.getDeclAnnotation(elt, UnannotatedFor.class);
+        return unannotatedFor != null
+                && atypeFactory.doesUnannotatedForApplyToThisChecker(unannotatedFor);
+    }
 }

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -2841,54 +2841,47 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) {
             return true;
         }
 
-        boolean foundAnnotatedFor = false;
+        // The innermost declaration enclosing path.  The @AnnotatedFor scope question is asked
+        // about it once, after the loop.
+        Element innermostDecl = null;
 
         // iterate through the path; continue until path contains no declarations
         for (TreePath declPath = TreePathUtil.enclosingDeclarationPath(path);
                 declPath != null;
                 declPath = TreePathUtil.enclosingDeclarationPath(declPath.getParentPath())) {
             Tree decl = declPath.getLeaf();
 
+            Element elt;
             if (decl instanceof VariableTree) {
-                Element elt = TreeUtils.elementFromDeclaration((VariableTree) decl);
-                if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) {
-                    return true;
-                }
+                elt = TreeUtils.elementFromDeclaration((VariableTree) decl);
             } else if (decl instanceof MethodTree) {
-                Element elt = TreeUtils.elementFromDeclaration((MethodTree) decl);
-                if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) {
-                    return true;
-                }
-
-                if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) {
-                    foundAnnotatedFor = true;
-                }
+                elt = TreeUtils.elementFromDeclaration((MethodTree) decl);
             } else if (TreeUtils.classTreeKinds().contains(decl.getKind())) {
-                // A class tree
-                Element elt = TreeUtils.elementFromDeclaration((ClassTree) decl);
-                if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) {
-                    return true;
-                }
-
-                if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) {
-                    foundAnnotatedFor = true;
-                }
-                Element packageElement = elt.getEnclosingElement();
-                if (packageElement != null && packageElement.getKind() == ElementKind.PACKAGE) {
-                    if (hasSuppressWarningsAnnotationForErrorKey(packageElement, errKey)) {
-                        return true;
-                    }
-                    if (!foundAnnotatedFor
-                            && isElementAnnotatedForThisCheckerOrUpstreamChecker(packageElement)) {
-                        foundAnnotatedFor = true;
-                    }
-                }
+                elt = TreeUtils.elementFromDeclaration((ClassTree) decl);
             } else {
                 throw new BugInCF("Unexpected declaration kind: " + decl.getKind() + " " + decl);
             }
+
+            if (hasSuppressWarningsAnnotationForErrorKey(elt, errKey)) {
+                return true;
+            }
+            if (innermostDecl == null) {
+                innermostDecl = elt;
+            }
+
+            Element packageElement = elt.getEnclosingElement();
+            if (packageElement != null
+                    && packageElement.getKind() == ElementKind.PACKAGE
+                    && hasSuppressWarningsAnnotationForErrorKey(packageElement, errKey)) {
+                return true;
+            }
         }
 
-        if (foundAnnotatedFor) {
+        // Ask only about the innermost declaration:
+        // isElementAnnotatedForThisCheckerOrUpstreamChecker already resolves the enclosing scope,
+        // and asking about an enclosing element separately would ignore an @UnannotatedFor that
+        // excludes the innermost declaration from that scope.
+        if (isElementAnnotatedForThisCheckerOrUpstreamChecker(innermostDecl)) {
             return false;
         } else if (useConservativeDefaultsSource || onlyAnnotatedFor) {
             // If we got this far without hitting an @AnnotatedFor and returning
@@ -2955,17 +2948,16 @@ public boolean shouldSuppressWarnings(Element elt, String errKey) {
             return true;
         }
 
-        boolean foundAnnotatedFor = false;
         for (Element currElt = elt; currElt != null; currElt = currElt.getEnclosingElement()) {
             if (hasSuppressWarningsAnnotationForErrorKey(currElt, errKey)) {
                 return true;
             }
-            if (!foundAnnotatedFor && isElementAnnotatedForThisCheckerOrUpstreamChecker(currElt)) {
-                foundAnnotatedFor = true;
-            }
         }
 
-        if (foundAnnotatedFor) {
+        // Ask only about elt: isElementAnnotatedForThisCheckerOrUpstreamChecker already resolves
+        // the enclosing scope, and asking about an enclosing element separately would ignore an
+        // @UnannotatedFor that excludes elt from that scope.
+        if (isElementAnnotatedForThisCheckerOrUpstreamChecker(elt)) {
             return false;
         } else if (useConservativeDefaultsSource || onlyAnnotatedFor) {
             // If we got this far without hitting an @AnnotatedFor and returning