From af94341c57903d4ccf572076e09c1a7053401d3f Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Wed, 14 Aug 2024 22:49:42 -0400
Subject: [PATCH 01/10] No bytecode storage flag first

---
 docs/CHANGELOG.md                                             | 2 ++
 .../org/checkerframework/framework/source/SourceChecker.java  | 4 ++++
 .../checkerframework/framework/type/AnnotatedTypeFactory.java | 4 ++++
 3 files changed, 10 insertions(+)

diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index f599801da15d..c4caa9b72c2d 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -3,6 +3,8 @@ Version 3.42.0-eisop5 (July ?, 2024)
 
 **User-visible changes:**
 
+The new command-line argument '-AnoBytecodeStorage' allows the option to not store defaulted annotations in bytecode.
+
 Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1.
 Use `-ApermitMissingJdk` instead.
 
diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
index 2a414ac2883b..ba8b010357c1 100644
--- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
+++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
@@ -187,6 +187,10 @@
     // org.checkerframework.framework.source.SourceChecker.useConservativeDefault
     "useConservativeDefaultsForUncheckedCode",
 
+    // Whether to store defaulted annotations in bytecode.
+    // org.checkerframework.framework.type.AnnotatedTypeFactory.postProcessClassTree
+    "noBytecodeStorage",
+
     // Whether to assume sound concurrent semantics or
     // simplified sequential semantics
     // org.checkerframework.framework.flow.CFAbstractTransfer.sequentialSemantics
diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index 228df9f89428..75fe6f784329 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -1528,6 +1528,10 @@ public void preProcessClassTree(ClassTree classTree) {}
      * to override this method if storing defaulted types is not desirable.
      */
     public void postProcessClassTree(ClassTree tree) {
+        if (!checker.hasOption("noBytecodeStorage")) {
+            TypesIntoElements.store(processingEnv, this, tree);
+            DeclarationsIntoElements.store(processingEnv, this, tree);
+        }
         TypesIntoElements.store(processingEnv, this, tree);
         DeclarationsIntoElements.store(processingEnv, this, tree);
 

From e6e83f96e9ebe4410dad39e4a89a9527e5d8446b Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Thu, 15 Aug 2024 00:10:10 -0400
Subject: [PATCH 02/10] Add UnannotatedFor qualifier

---
 .../framework/qual/UnannotatedFor.java        | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java

diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java
new file mode 100644
index 000000000000..414926abc388
--- /dev/null
+++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java
@@ -0,0 +1,27 @@
+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 and this annotation is
+ * used to exclude package, class or method which already in {@code @Annotatedfor} scope. In the
+ * scope of {@code UnannotatedFor}, the source code and bytecode should use conservative default if
+ * the command-line argument {@code -AuseConservativeDefaultsForUncheckedCode=source} is supplied
+ * while other package, class or method in {@code @Annotatedfor} scope is defaulted normally
+ * (typically using the CLIMB-to-top rule).
+ *
+ * <p>For example, mark a package as @Annotatedfor("nullness") will indicate that the package has
+ * been annotated with nullness annotation but some classes or methods in the package is not
+ * annotated, then mark the class or method with @UnannotatedFor("nullness") to exclude them from
+ * the scope of @Annotatedfor("nullness").
+ */
+@Documented
+@Retention(RetentionPolicy.SOURCE)
+@Target({ElementType.TYPE, ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.PACKAGE})
+public @interface UnannotatedFor {
+    String[] value();
+}

From 315cb00195dca8a31f7406b39f2d1270f496507f Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Thu, 15 Aug 2024 23:47:31 -0400
Subject: [PATCH 03/10] Don't apply conservative defaults if this element is in
 the scope of Unannotatedfor

---
 .../util/defaults/QualifierDefaults.java      | 57 +++++++++++++++++--
 1 file changed, 53 insertions(+), 4 deletions(-)

diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
index a7b7c149fe8a..47ad2268b2c1 100644
--- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
+++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
@@ -16,6 +16,7 @@
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.DefaultQualifier;
 import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
@@ -123,6 +124,12 @@ public class QualifierDefaults {
     /** A mapping of Element &rarr; Whether or not that element is AnnotatedFor this type system. */
     private final IdentityHashMap<Element, Boolean> elementAnnotatedFors = new IdentityHashMap<>();
 
+    /**
+     * A mapping of Element &rarr; Whether or not that element is UnannotatedFor this type system.
+     */
+    private final IdentityHashMap<Element, Boolean> elementUnannotatedFors =
+            new IdentityHashMap<>();
+
     /** CLIMB locations whose standard default is top for a given type system. */
     public static final List<TypeUseLocation> STANDARD_CLIMB_DEFAULTS_TOP =
             Collections.unmodifiableList(
@@ -660,12 +667,13 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
                     atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor);
         }
 
+        // If the element is not Annotatedfor this checker, check if the parent is.
         if (!elementAnnotatedForThisChecker) {
             Element parent;
             if (elt.getKind() == ElementKind.PACKAGE) {
                 // TODO: should AnnotatedFor apply to subpackages??
-                // elt.getEnclosingElement() on a package is null; therefore,
-                // use the dedicated method.
+                // elt.getEnclosingElement() on a package is null if module does not exist;
+                // therefore, use the dedicated method.
                 parent = ElementUtils.parentPackage((PackageElement) elt, elements);
             } else {
                 parent = elt.getEnclosingElement();
@@ -681,6 +689,45 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
         return elementAnnotatedForThisChecker;
     }
 
+    /**
+     * Returns whether the element is UnannotatedFor this checker.
+     *
+     * @param elt the element
+     * @return whether the element is UnannotatedFor this checker
+     */
+    private boolean isElementUnannotatedForThisChecker(Element elt) {
+        boolean elementUnannotatedForThisChecker = false;
+
+        if (elt == null) {
+            throw new BugInCF(
+                    "Call of QualifierDefaults.isElementUnannotatedForThisChecker with null");
+        }
+
+        if (elementUnannotatedFors.containsKey(elt)) {
+            return elementUnannotatedFors.get(elt);
+        }
+
+        AnnotationMirror UnannotatedFor = atypeFactory.getDeclAnnotation(elt, UnannotatedFor.class);
+
+        if (UnannotatedFor != null) {
+            elementUnannotatedForThisChecker =
+                    atypeFactory.doesAnnotatedForApplyToThisChecker(UnannotatedFor);
+        }
+
+        // If the element is not Unannotatedfor this checker, check if the parent is. Only get the
+        // parent for enclosing elements, not for packages.
+        if (!elementUnannotatedForThisChecker) {
+            Element parent = elt.getEnclosingElement();
+            if (parent != null && isElementUnannotatedForThisChecker(parent)) {
+                elementUnannotatedForThisChecker = true;
+            }
+        }
+
+        elementAnnotatedFors.put(elt, elementUnannotatedForThisChecker);
+
+        return elementUnannotatedForThisChecker;
+    }
+
     /**
      * Returns the defaults that apply to the given Element, considering defaults from enclosing
      * Elements.
@@ -809,7 +856,8 @@ public boolean applyConservativeDefaults(Element annotationScope) {
                         && !isFromStubFile;
         if (isBytecode) {
             return useConservativeDefaultsBytecode
-                    && !isElementAnnotatedForThisChecker(annotationScope);
+                    && (!isElementAnnotatedForThisChecker(annotationScope)
+                            || isElementUnannotatedForThisChecker(annotationScope));
         } else if (isFromStubFile) {
             // TODO: Types in stub files not annotated for a particular checker should be
             // treated as unchecked bytecode.  For now, all types in stub files are treated as
@@ -818,7 +866,8 @@ public boolean applyConservativeDefaults(Element annotationScope) {
             // be treated like unchecked code except for methods in the scope of an @AnnotatedFor.
             return false;
         } else if (useConservativeDefaultsSource) {
-            return !isElementAnnotatedForThisChecker(annotationScope);
+            return !isElementAnnotatedForThisChecker(annotationScope)
+                    || isElementUnannotatedForThisChecker(annotationScope);
         }
         return false;
     }

From d0e4a0307d973e4f6e3e02219642974f36c96c48 Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Thu, 15 Aug 2024 23:57:19 -0400
Subject: [PATCH 04/10] Add aliasing for JSpecify scope annotation

---
 .../NullnessNoInitAnnotatedTypeFactory.java    | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
index 35819c3aa379..e920e7fb473a 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
@@ -32,8 +32,10 @@
 import org.checkerframework.dataflow.expression.ThisReference;
 import org.checkerframework.dataflow.util.NodeUtils;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
+import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.DefaultQualifier;
 import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFormatter;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -393,10 +395,26 @@ public NullnessNoInitAnnotatedTypeFactory(BaseTypeChecker checker) {
                                     new TypeUseLocation[] {TypeUseLocation.UPPER_BOUND})
                             .setValue("applyToSubpackages", false)
                             .build();
+            AnnotationMirror annotatedForNullness =
+                    new AnnotationBuilder(processingEnv, AnnotatedFor.class)
+                            .setValue("value", "nullness")
+                            .build();
+            AnnotationMirror unannotatedForNullness =
+                    new AnnotationBuilder(processingEnv, UnannotatedFor.class)
+                            .setValue("value", "nullness")
+                            .build();
             addAliasedDeclAnnotation(
                     "org.jspecify.annotations.NullMarked",
                     DefaultQualifier.class.getCanonicalName(),
                     nullMarkedDefaultQual);
+            addAliasedDeclAnnotation(
+                    "org.jspecify.annotations.NullMarked",
+                    AnnotatedFor.class.getCanonicalName(),
+                    annotatedForNullness);
+            addAliasedDeclAnnotation(
+                    "org.jspecify.annotations.NullUnmarked",
+                    UnannotatedFor.class.getCanonicalName(),
+                    unannotatedForNullness);
 
             // 2022-11-17: Deprecated old package location, remove after some grace period
             addAliasedDeclAnnotation(

From 40828d676799c4967d714a0c279bc00f29da3dbb Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Fri, 16 Aug 2024 01:15:45 -0400
Subject: [PATCH 05/10] Commit for fixing crash bugs b.c. incorrect method
 invoking

---
 .../NullnessNoInitAnnotatedTypeFactory.java   |  4 +--
 .../framework/type/AnnotatedTypeFactory.java  | 27 +++++++++++++++++++
 .../util/defaults/QualifierDefaults.java      | 16 +++++++----
 3 files changed, 40 insertions(+), 7 deletions(-)

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
index e920e7fb473a..cbdefc3b031e 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
@@ -397,11 +397,11 @@ public NullnessNoInitAnnotatedTypeFactory(BaseTypeChecker checker) {
                             .build();
             AnnotationMirror annotatedForNullness =
                     new AnnotationBuilder(processingEnv, AnnotatedFor.class)
-                            .setValue("value", "nullness")
+                            .setValue("value", new String[] {"nullness"})
                             .build();
             AnnotationMirror unannotatedForNullness =
                     new AnnotationBuilder(processingEnv, UnannotatedFor.class)
-                            .setValue("value", "nullness")
+                            .setValue("value", new String[] {"nullness"})
                             .build();
             addAliasedDeclAnnotation(
                     "org.jspecify.annotations.NullMarked",
diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index 75fe6f784329..266e440a7cce 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -52,6 +52,7 @@
 import org.checkerframework.framework.qual.InheritedAnnotation;
 import org.checkerframework.framework.qual.NoQualifierParameter;
 import org.checkerframework.framework.qual.RequiresQualifier;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.source.SourceChecker;
 import org.checkerframework.framework.stub.AnnotationFileElementTypes;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
@@ -203,6 +204,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
     /** The AnnotatedFor.value argument/element. */
     protected final ExecutableElement annotatedForValueElement;
 
+    /** The UnannotatedFor.value argument/element. */
+    protected final ExecutableElement unannotatedForValueElement;
+
     /** The EnsuresQualifier.expression field/element. */
     protected final ExecutableElement ensuresQualifierExpressionElement;
 
@@ -708,6 +712,8 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) {
 
         annotatedForValueElement =
                 TreeUtils.getMethod(AnnotatedFor.class, "value", 0, processingEnv);
+        unannotatedForValueElement =
+                TreeUtils.getMethod(UnannotatedFor.class, "value", 0, processingEnv);
         ensuresQualifierExpressionElement =
                 TreeUtils.getMethod(EnsuresQualifier.class, "expression", 0, processingEnv);
         ensuresQualifierListValueElement =
@@ -6022,6 +6028,27 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA
         return false;
     }
 
+    /**
+     * Does {@code anno}, which is an {@link org.checkerframework.framework.qual.UnannotatedFor}
+     * annotation, apply to this checker?
+     *
+     * @param annotatedForAnno an {@link UnannotatedFor} annotation
+     * @return whether {@code anno} applies to this checker
+     */
+    public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedFor) {
+        List<String> unannotatedForCheckers =
+                AnnotationUtils.getElementValueArray(
+                        unannotatedFor, unannotatedForValueElement, String.class);
+        for (String unannoForChecker : unannotatedForCheckers) {
+            if (checker.getUpstreamCheckerNames().contains(unannoForChecker)
+                    || CheckerMain.matchesFullyQualifiedProcessor(
+                            unannoForChecker, checker.getUpstreamCheckerNames(), true)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
     /**
      * Get the {@code expression} field/element of the given contract annotation.
      *
diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
index 47ad2268b2c1..c7242e3d22d3 100644
--- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
+++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
@@ -711,19 +711,25 @@ private boolean isElementUnannotatedForThisChecker(Element elt) {
 
         if (UnannotatedFor != null) {
             elementUnannotatedForThisChecker =
-                    atypeFactory.doesAnnotatedForApplyToThisChecker(UnannotatedFor);
+                    atypeFactory.doesUnannotatedForApplyToThisChecker(UnannotatedFor);
         }
 
-        // If the element is not Unannotatedfor this checker, check if the parent is. Only get the
-        // parent for enclosing elements, not for packages.
         if (!elementUnannotatedForThisChecker) {
-            Element parent = elt.getEnclosingElement();
+            Element parent;
+            if (elt.getKind() == ElementKind.PACKAGE) {
+                // elt.getEnclosingElement() on a package is null if module does not exist;
+                // therefore, use the dedicated method.
+                parent = ElementUtils.parentPackage((PackageElement) elt, elements);
+            } else {
+                parent = elt.getEnclosingElement();
+            }
+
             if (parent != null && isElementUnannotatedForThisChecker(parent)) {
                 elementUnannotatedForThisChecker = true;
             }
         }
 
-        elementAnnotatedFors.put(elt, elementUnannotatedForThisChecker);
+        elementUnannotatedFors.put(elt, elementUnannotatedForThisChecker);
 
         return elementUnannotatedForThisChecker;
     }

From 8b1380fbe12ca0ab24a920c7e846142a56b115ae Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Fri, 16 Aug 2024 23:30:59 -0400
Subject: [PATCH 06/10] Fix java doc

---
 .../framework/type/AnnotatedTypeFactory.java                | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index 266e440a7cce..f6777d187405 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -6032,13 +6032,13 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA
      * Does {@code anno}, which is an {@link org.checkerframework.framework.qual.UnannotatedFor}
      * annotation, apply to this checker?
      *
-     * @param annotatedForAnno an {@link UnannotatedFor} annotation
+     * @param unannotatedForAnno an {@link UnannotatedFor} annotation
      * @return whether {@code anno} applies to this checker
      */
-    public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedFor) {
+    public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedForAnno) {
         List<String> unannotatedForCheckers =
                 AnnotationUtils.getElementValueArray(
-                        unannotatedFor, unannotatedForValueElement, String.class);
+                        unannotatedForAnno, unannotatedForValueElement, String.class);
         for (String unannoForChecker : unannotatedForCheckers) {
             if (checker.getUpstreamCheckerNames().contains(unannoForChecker)
                     || CheckerMain.matchesFullyQualifiedProcessor(

From 7387ef2bb67e23a840c7db6600bc49677a0d1282 Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Fri, 27 Jun 2025 21:52:53 -0400
Subject: [PATCH 07/10] Revert aliasing

---
 .../NullnessNoInitAnnotatedTypeFactory.java    | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
index 1505f7a793b4..5da576329b08 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java
@@ -32,10 +32,8 @@
 import org.checkerframework.dataflow.expression.ThisReference;
 import org.checkerframework.dataflow.util.NodeUtils;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
-import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.DefaultQualifier;
 import org.checkerframework.framework.qual.TypeUseLocation;
-import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
@@ -408,26 +406,10 @@ public NullnessNoInitAnnotatedTypeFactory(BaseTypeChecker checker) {
                                     new TypeUseLocation[] {TypeUseLocation.UPPER_BOUND})
                             .setValue("applyToSubpackages", false)
                             .build();
-            AnnotationMirror annotatedForNullness =
-                    new AnnotationBuilder(processingEnv, AnnotatedFor.class)
-                            .setValue("value", new String[] {"nullness"})
-                            .build();
-            AnnotationMirror unannotatedForNullness =
-                    new AnnotationBuilder(processingEnv, UnannotatedFor.class)
-                            .setValue("value", new String[] {"nullness"})
-                            .build();
             addAliasedDeclAnnotation(
                     "org.jspecify.annotations.NullMarked",
                     DefaultQualifier.class.getCanonicalName(),
                     nullMarkedDefaultQual);
-            addAliasedDeclAnnotation(
-                    "org.jspecify.annotations.NullMarked",
-                    AnnotatedFor.class.getCanonicalName(),
-                    annotatedForNullness);
-            addAliasedDeclAnnotation(
-                    "org.jspecify.annotations.NullUnmarked",
-                    UnannotatedFor.class.getCanonicalName(),
-                    unannotatedForNullness);
 
             // 2022-11-17: Deprecated old package location, remove after some grace period
             addAliasedDeclAnnotation(

From bba08aaf6b6e82be56b6fcf0060f094552635327 Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Fri, 27 Jun 2025 21:54:56 -0400
Subject: [PATCH 08/10] Revert no bytecode storage

---
 docs/CHANGELOG.md                                             | 2 --
 .../org/checkerframework/framework/source/SourceChecker.java  | 4 ----
 .../checkerframework/framework/type/AnnotatedTypeFactory.java | 4 ----
 3 files changed, 10 deletions(-)

diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index d4bbc27a085a..a4f0239d940c 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -316,8 +316,6 @@ Version 3.42.0-eisop5 (December 20, 2024)
 
 **User-visible changes:**
 
-The new command-line argument '-AnoBytecodeStorage' allows the option to not store defaulted annotations in bytecode.
-
 Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1.
 Use `-ApermitMissingJdk` instead.
 
diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
index c57f38c727c9..f8e4c6a00052 100644
--- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
+++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
@@ -201,10 +201,6 @@
     // org.checkerframework.framework.source.SourceChecker.useConservativeDefault
     "useConservativeDefaultsForUncheckedCode",
 
-    // Whether to store defaulted annotations in bytecode.
-    // org.checkerframework.framework.type.AnnotatedTypeFactory.postProcessClassTree
-    "noBytecodeStorage",
-
     // Whether to assume sound concurrent semantics or
     // simplified sequential semantics
     // org.checkerframework.framework.flow.CFAbstractTransfer.sequentialSemantics
diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index da7c9a1d59ca..56d5f0014868 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -1536,10 +1536,6 @@ public void preProcessClassTree(ClassTree classTree) {}
      * to override this method if storing defaulted types is not desirable.
      */
     public void postProcessClassTree(ClassTree tree) {
-        if (!checker.hasOption("noBytecodeStorage")) {
-            TypesIntoElements.store(processingEnv, this, tree);
-            DeclarationsIntoElements.store(processingEnv, this, tree);
-        }
         TypesIntoElements.store(processingEnv, this, tree);
         DeclarationsIntoElements.store(processingEnv, this, tree);
 

From df8723b81954d454d1b3c3bc1c5727cf922b9a30 Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Sat, 28 Jun 2025 01:41:11 -0400
Subject: [PATCH 09/10] Add unannotatedfor annotation. TODO: check for conflict

---
 .../junit/NullnessUnannotatedForTest.java     |  34 ++++++
 .../NullnessUnannotatedForTest.java           |  18 +++
 .../framework/source/SourceChecker.java       |  23 +++-
 .../util/defaults/QualifierDefaults.java      | 111 ++++++++++--------
 4 files changed, 129 insertions(+), 57 deletions(-)
 create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java
 create mode 100644 checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java

diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessUnannotatedForTest.java
new file mode 100644
index 000000000000..349d36de2a2f
--- /dev/null
+++ b/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"};
+    }
+}
diff --git a/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java
new file mode 100644
index 000000000000..4223a9251ffa
--- /dev/null
+++ b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java
@@ -0,0 +1,18 @@
+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() {
+            Object o = null;
+        }
+    }
+}
diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
index f8e4c6a00052..ee5bd007366c 100644
--- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
+++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
@@ -33,6 +33,7 @@
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.common.reflection.MethodValChecker;
 import org.checkerframework.framework.qual.AnnotatedFor;
+import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.util.CheckerMain;
 import org.checkerframework.framework.util.OptionConfiguration;
@@ -481,6 +482,12 @@ public abstract class SourceChecker extends AbstractTypeProcessor implements Opt
     public static final @CompilerMessageKey String UNNEEDED_SUPPRESSION_KEY =
             "unneeded.suppression";
 
+    /**
+     * The message key emitted when AnnotatedFor and UnannotatedFor on the same element has same
+     * value.
+     */
+    public static final @CompilerMessageKey String ANNOTATEDFOR_CONFLICT = "annotatedfor.conflict";
+
     /** File name of the localized messages. */
     protected static final String MSGS_FILE = "messages.properties";
 
@@ -2988,11 +2995,11 @@ private boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt
             return false;
         }
 
-        AnnotatedFor anno = elt.getAnnotation(AnnotatedFor.class);
-
-        String[] userAnnotatedFors = (anno == null ? null : anno.value());
-
-        if (userAnnotatedFors != null) {
+        AnnotatedFor annotatedFor = elt.getAnnotation(AnnotatedFor.class);
+        UnannotatedFor unannotatedFor = elt.getAnnotation(UnannotatedFor.class);
+        String[] userAnnotatedFors = (annotatedFor == null ? null : annotatedFor.value());
+        String[] userUnannotatedFors = (unannotatedFor == null ? null : unannotatedFor.value());
+        if (userAnnotatedFors != null || userUnannotatedFors != null) {
             List<@FullyQualifiedName String> upstreamCheckerNames = getUpstreamCheckerNames();
 
             for (String userAnnotatedFor : userAnnotatedFors) {
@@ -3001,6 +3008,12 @@ private boolean isAnnotatedForThisCheckerOrUpstreamChecker(@Nullable Element elt
                     return true;
                 }
             }
+            for (String userUnannotatedFor : userUnannotatedFors) {
+                if (CheckerMain.matchesCheckerOrSubcheckerFromList(
+                        userUnannotatedFor, upstreamCheckerNames)) {
+                    return false;
+                }
+            }
         }
 
         return false;
diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
index a7570f9aed72..23c69f8f9741 100644
--- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
+++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java
@@ -16,7 +16,6 @@
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.DefaultQualifier;
 import org.checkerframework.framework.qual.TypeUseLocation;
-import org.checkerframework.framework.qual.UnannotatedFor;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
@@ -63,7 +62,7 @@
  *
  * <p>Type variable uses have two possible defaults. If flow sensitive type refinement is enabled,
  * unannotated top-level type variable uses receive the same default as local variables. All other
- * type variable uses are defaulted using the {@code TYPE_VARIABLE_USE} default.
+ * type variable uses are defaulted using the {@code TYPE_VARIABLE_USE} defaul1t.
  *
  * <pre>{@code
  * <T> void method(USE T tIn) {
@@ -650,6 +649,7 @@ private void applyDefaults(Tree tree, AnnotatedTypeMirror type) {
 
     private boolean isElementAnnotatedForThisChecker(Element elt) {
         boolean elementAnnotatedForThisChecker = false;
+        boolean elementUnAnnotatedForThisChecker = false;
 
         if (elt == null) {
             throw new BugInCF(
@@ -661,14 +661,21 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
         }
 
         AnnotationMirror annotatedFor = atypeFactory.getDeclAnnotation(elt, AnnotatedFor.class);
+        AnnotationMirror unannotatedFor =
+                atypeFactory.getDeclAnnotation(
+                        elt, org.checkerframework.framework.qual.UnannotatedFor.class);
 
         if (annotatedFor != null) {
             elementAnnotatedForThisChecker =
                     atypeFactory.doesAnnotatedForApplyToThisChecker(annotatedFor);
         }
 
-        // If the element is not Annotatedfor this checker, check if the parent is.
-        if (!elementAnnotatedForThisChecker) {
+        if (unannotatedFor != null) {
+            elementUnAnnotatedForThisChecker =
+                    atypeFactory.doesUnannotatedForApplyToThisChecker(unannotatedFor);
+        }
+
+        if (!elementAnnotatedForThisChecker && !elementUnAnnotatedForThisChecker) {
             Element parent;
             if (elt.getKind() == ElementKind.PACKAGE) {
                 // TODO: should AnnotatedFor apply to subpackages??
@@ -685,54 +692,56 @@ private boolean isElementAnnotatedForThisChecker(Element elt) {
         }
 
         elementAnnotatedFors.put(elt, elementAnnotatedForThisChecker);
+        elementUnannotatedFors.put(elt, elementUnAnnotatedForThisChecker);
 
         return elementAnnotatedForThisChecker;
     }
 
-    /**
-     * Returns whether the element is UnannotatedFor this checker.
-     *
-     * @param elt the element
-     * @return whether the element is UnannotatedFor this checker
-     */
-    private boolean isElementUnannotatedForThisChecker(Element elt) {
-        boolean elementUnannotatedForThisChecker = false;
-
-        if (elt == null) {
-            throw new BugInCF(
-                    "Call of QualifierDefaults.isElementUnannotatedForThisChecker with null");
-        }
-
-        if (elementUnannotatedFors.containsKey(elt)) {
-            return elementUnannotatedFors.get(elt);
-        }
-
-        AnnotationMirror UnannotatedFor = atypeFactory.getDeclAnnotation(elt, UnannotatedFor.class);
-
-        if (UnannotatedFor != null) {
-            elementUnannotatedForThisChecker =
-                    atypeFactory.doesUnannotatedForApplyToThisChecker(UnannotatedFor);
-        }
-
-        if (!elementUnannotatedForThisChecker) {
-            Element parent;
-            if (elt.getKind() == ElementKind.PACKAGE) {
-                // elt.getEnclosingElement() on a package is null if module does not exist;
-                // therefore, use the dedicated method.
-                parent = ElementUtils.parentPackage((PackageElement) elt, elements);
-            } else {
-                parent = elt.getEnclosingElement();
-            }
-
-            if (parent != null && isElementUnannotatedForThisChecker(parent)) {
-                elementUnannotatedForThisChecker = true;
-            }
-        }
-
-        elementUnannotatedFors.put(elt, elementUnannotatedForThisChecker);
-
-        return elementUnannotatedForThisChecker;
-    }
+    //    /**
+    //     * Returns whether the element is UnannotatedFor this checker.
+    //     *
+    //     * @param elt the element
+    //     * @return whether the element is UnannotatedFor this checker
+    //     */
+    //    private boolean isElementUnannotatedForThisChecker(Element elt) {
+    //        boolean elementUnannotatedForThisChecker = false;
+    //
+    //        if (elt == null) {
+    //            throw new BugInCF(
+    //                    "Call of QualifierDefaults.isElementUnannotatedForThisChecker with null");
+    //        }
+    //
+    //        if (elementUnannotatedFors.containsKey(elt)) {
+    //            return elementUnannotatedFors.get(elt);
+    //        }
+    //
+    //        AnnotationMirror UnannotatedFor = atypeFactory.getDeclAnnotation(elt,
+    // UnannotatedFor.class);
+    //
+    //        if (UnannotatedFor != null) {
+    //            elementUnannotatedForThisChecker =
+    //                    atypeFactory.doesUnannotatedForApplyToThisChecker(UnannotatedFor);
+    //        }
+    //
+    //        if (!elementUnannotatedForThisChecker) {
+    //            Element parent;
+    //            if (elt.getKind() == ElementKind.PACKAGE) {
+    //                // elt.getEnclosingElement() on a package is null if module does not exist;
+    //                // therefore, use the dedicated method.
+    //                parent = ElementUtils.parentPackage((PackageElement) elt, elements);
+    //            } else {
+    //                parent = elt.getEnclosingElement();
+    //            }
+    //
+    //            if (parent != null && isElementUnannotatedForThisChecker(parent)) {
+    //                elementUnannotatedForThisChecker = true;
+    //            }
+    //        }
+    //
+    //        elementUnannotatedFors.put(elt, elementUnannotatedForThisChecker);
+    //
+    //        return elementUnannotatedForThisChecker;
+    //    }
 
     /**
      * Returns the defaults that apply to the given Element, considering defaults from enclosing
@@ -862,8 +871,7 @@ public boolean applyConservativeDefaults(Element annotationScope) {
                         && !isFromStubFile;
         if (isBytecode) {
             return useConservativeDefaultsBytecode
-                    && (!isElementAnnotatedForThisChecker(annotationScope)
-                            || isElementUnannotatedForThisChecker(annotationScope));
+                    && !isElementAnnotatedForThisChecker(annotationScope);
         } else if (isFromStubFile) {
             // TODO: Types in stub files not annotated for a particular checker should be
             // treated as unchecked bytecode.  For now, all types in stub files are treated as
@@ -872,8 +880,7 @@ public boolean applyConservativeDefaults(Element annotationScope) {
             // be treated like unchecked code except for methods in the scope of an @AnnotatedFor.
             return false;
         } else if (useConservativeDefaultsSource) {
-            return !isElementAnnotatedForThisChecker(annotationScope)
-                    || isElementUnannotatedForThisChecker(annotationScope);
+            return !isElementAnnotatedForThisChecker(annotationScope);
         }
         return false;
     }

From 1da609ad57c37fb51f5abfe697436071008d7161 Mon Sep 17 00:00:00 2001
From: Aosen Xiong <aosen.xiong@uwaterloo.ca>
Date: Sat, 29 Aug 2026 18:56:14 -0400
Subject: [PATCH 10/10] Make @UnannotatedFor exclude an element from an
 enclosing @AnnotatedFor scope

@UnannotatedFor was defined and given an AnnotatedTypeFactory helper, but its
effect was implemented in QualifierDefaults.isElementAnnotatedForThisChecker,
which #1331 removed.  Implement it in the lookup that replaced it,
BaseTypeChecker.isElementAnnotatedForThisCheckerOrUpstreamChecker, so that it
governs both conservative defaults and warning suppression.

@AnnotatedFor is tested first, so @UnannotatedFor is purely subtractive: it
stops the walk to the enclosing element, and never overrides an explicit
@AnnotatedFor on the same element.  A nested @AnnotatedFor takes effect again.

Both shouldSuppressWarnings overloads accumulated the @AnnotatedFor answer over
every enclosing declaration, and the TreePath overload additionally asked about
the enclosing package.  That defeated the exclusion: an @UnannotatedFor class in
an @AnnotatedFor package was defaulted as unchecked code but still had its
warnings reported.  Ask isElementAnnotatedForThisCheckerOrUpstreamChecker once,
about the innermost declaration; it already resolves enclosing scopes, so the
per-level query was redundant work even before this change.

Only one cache is needed.  The element's cached boolean is the fully-resolved
scope answer, including @UnannotatedFor exclusions.

Also mirror doesUnannotatedForApplyToThisChecker on its @AnnotatedFor sibling,
and correct the @UnannotatedFor javadoc, which claimed an effect on bytecode
although the annotation has source retention.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .../framework/qual/UnannotatedFor.java        | 32 ++++++---
 .../NullnessUnannotatedForTest.java           | 41 ++++++++++-
 .../Excluded.java                             | 12 ++++
 .../Included.java                             | 10 +++
 .../package-info.java                         |  4 ++
 docs/CHANGELOG.md                             |  7 ++
 docs/manual/annotating-libraries.tex          | 10 +++
 .../common/basetype/BaseTypeChecker.java      | 24 ++++++-
 .../framework/source/SourceChecker.java       | 68 ++++++++-----------
 .../framework/type/AnnotatedTypeFactory.java  | 11 +--
 10 files changed, 163 insertions(+), 56 deletions(-)
 create mode 100644 checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java
 create mode 100644 checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java
 create mode 100644 checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java

diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java
index 414926abc388..0a87d8937406 100644
--- a/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java
+++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/UnannotatedFor.java
@@ -7,21 +7,33 @@
 import java.lang.annotation.Target;
 
 /**
- * Indicates that this class has not been annotated for the given type system and this annotation is
- * used to exclude package, class or method which already in {@code @Annotatedfor} scope. In the
- * scope of {@code UnannotatedFor}, the source code and bytecode should use conservative default if
- * the command-line argument {@code -AuseConservativeDefaultsForUncheckedCode=source} is supplied
- * while other package, class or method in {@code @Annotatedfor} scope is defaulted normally
- * (typically using the CLIMB-to-top rule).
+ * 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>For example, mark a package as @Annotatedfor("nullness") will indicate that the package has
- * been annotated with nullness annotation but some classes or methods in the package is not
- * annotated, then mark the class or method with @UnannotatedFor("nullness") to exclude them from
- * the scope of @Annotatedfor("nullness").
+ * <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();
 }
diff --git a/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java
index 4223a9251ffa..9bdac0219f37 100644
--- a/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java
+++ b/checker/tests/nullness-unannotatedfor/NullnessUnannotatedForTest.java
@@ -1,3 +1,4 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.UnannotatedFor;
 
@@ -11,7 +12,45 @@ class A {
     @AnnotatedFor("nullness")
     class B {
         @UnannotatedFor("nullness")
-        void method() {
+        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;
         }
     }
diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Excluded.java
new file mode 100644
index 000000000000..210fbb470aca
--- /dev/null
+++ b/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();
+    }
+}
diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/Included.java
new file mode 100644
index 000000000000..7d80b73b621c
--- /dev/null
+++ b/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();
+    }
+}
diff --git a/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java
new file mode 100644
index 000000000000..3ea907dc08b6
--- /dev/null
+++ b/checker/tests/nullness-unannotatedfor/packageunannotatedfornullness/package-info.java
@@ -0,0 +1,4 @@
+@AnnotatedFor("nullness")
+package packageunannotatedfornullness;
+
+import org.checkerframework.framework.qual.AnnotatedFor;
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index 63142b582161..7de904121552 100644
--- a/docs/CHANGELOG.md
+++ b/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
diff --git a/docs/manual/annotating-libraries.tex b/docs/manual/annotating-libraries.tex
index b6ce89dc8fd8..acce944cf7d6 100644
--- a/docs/manual/annotating-libraries.tex
+++ b/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
diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java
index ae058151e952..79d94c089ebd 100644
--- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java
+++ b/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);
+    }
 }
diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
index b28eae57f77a..d8163658f40b 100644
--- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
+++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java
@@ -2841,7 +2841,9 @@ 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);
@@ -2849,46 +2851,37 @@ public boolean shouldSuppressWarnings(TreePath path, String errKey) {
                 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
diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index a1e48e94b20e..ed0e5bc2c653 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -6881,20 +6881,21 @@ public boolean doesAnnotatedForApplyToThisChecker(AnnotationMirror annotatedForA
     }
 
     /**
-     * Does {@code anno}, which is an {@link org.checkerframework.framework.qual.UnannotatedFor}
-     * annotation, apply to this checker?
+     * Does {@code unannotatedForAnno}, which is an {@link UnannotatedFor} annotation, apply to this
+     * checker?
      *
      * @param unannotatedForAnno an {@link UnannotatedFor} annotation
-     * @return whether {@code anno} applies to this checker
+     * @return whether {@code unannotatedForAnno} applies to this checker
      */
     public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedForAnno) {
         List<String> unannotatedForCheckers =
                 AnnotationUtils.getElementValueArray(
                         unannotatedForAnno, unannotatedForValueElement, String.class);
+        List<@FullyQualifiedName String> upstreamCheckerNames = checker.getUpstreamCheckerNames();
         for (String unannoForChecker : unannotatedForCheckers) {
-            if (checker.getUpstreamCheckerNames().contains(unannoForChecker)
+            if (upstreamCheckerNames.contains(unannoForChecker)
                     || CheckerMain.matchesFullyQualifiedProcessor(
-                            unannoForChecker, checker.getUpstreamCheckerNames(), true)) {
+                            unannoForChecker, upstreamCheckerNames, true)) {
                 return true;
             }
         }