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 00000000000..414926abc38 --- /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). + * + *
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();
+}
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 35819c3aa37..cbdefc3b031 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", 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(
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index f599801da15..c4caa9b72c2 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 2a414ac2883..ba8b010357c 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 228df9f8942..f6777d18740 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 =
@@ -1528,6 +1534,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);
@@ -6018,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 unannotatedForAnno an {@link UnannotatedFor} annotation
+ * @return whether {@code anno} applies to this checker
+ */
+ public boolean doesUnannotatedForApplyToThisChecker(AnnotationMirror unannotatedForAnno) {
+ List