From a9e22bd233e92f4a0553084d380a5ec07746c62a Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 21 Jan 2024 17:07:12 -0800 Subject: [PATCH 1/7] Warn when using the top type in a pre- or post-condition annotation --- .../common/basetype/BaseTypeVisitor.java | 48 +++++++++++++++++-- .../common/basetype/messages.properties | 1 + .../framework/util/ContractsFromMethod.java | 2 +- .../flow/ContractsOverridingSubtyping.java | 6 +++ framework/tests/flow/Postcondition.java | 12 +++++ framework/tests/flow/Precondition.java | 5 ++ 6 files changed, 70 insertions(+), 4 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 519b1a944b13..176736b336f2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -59,6 +59,7 @@ import java.util.Map; import java.util.Set; import java.util.StringJoiner; +import java.util.TreeSet; import java.util.Vector; import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; @@ -101,6 +102,11 @@ import org.checkerframework.framework.flow.CFAbstractStore; import org.checkerframework.framework.flow.CFAbstractValue; import org.checkerframework.framework.qual.DefaultQualifier; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.qual.EnsuresQualifierIf; +import org.checkerframework.framework.qual.PostconditionAnnotation; +import org.checkerframework.framework.qual.PreconditionAnnotation; +import org.checkerframework.framework.qual.RequiresQualifier; import org.checkerframework.framework.qual.Unused; import org.checkerframework.framework.source.DiagMessage; import org.checkerframework.framework.source.SourceVisitor; @@ -2234,16 +2240,29 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { return null; } - TypeElement anno = (TypeElement) TreeInfo.symbol((JCTree) tree.getAnnotationType()); + TypeElement annoType = (TypeElement) TreeInfo.symbol((JCTree) tree.getAnnotationType()); - Name annoName = anno.getQualifiedName(); + Name annoName = annoType.getQualifiedName(); if (annoName.contentEquals(DefaultQualifier.class.getName()) || annoName.contentEquals(SuppressWarnings.class.getName())) { // Skip these two annotations, as we don't care about the arguments to them. return null; } - List methods = ElementFilter.methodsIn(anno.getEnclosedElements()); + if (isPreOrPostConditionAnnotation(annoName)) { + AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree); + AnnotationMirror qualifier = + atypeFactory.getContractsFromMethod().getQualifierEnforcedByContractAnnotation(anno); + if (qualifier != null) { + AnnotationMirror topForQualifier = qualHierarchy.getTopAnnotation(qualifier); + if (AnnotationUtils.areSame(qualifier, topForQualifier)) { + Name contractQualName = qualifier.getAnnotationType().asElement().getSimpleName(); + checker.reportWarning(tree, "contracts.toptype", contractQualName); + } + } + } + + List methods = ElementFilter.methodsIn(annoType.getEnclosedElements()); // Mapping from argument simple name to its annotated type. Map annoTypes = ArrayMap.newArrayMapOrHashMap(methods.size()); for (ExecutableElement meth : methods) { @@ -2299,6 +2318,29 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { return null; } + /** Pre- and post-condition annotations that take a qualifier as an argument. */ + private TreeSet preAndPostConditionAnnotations = + new TreeSet<>( + // In Java 9+, use `List.of()`. + Arrays.asList( + PreconditionAnnotation.class.getName(), + PostconditionAnnotation.class.getName(), + RequiresQualifier.class.getName(), + EnsuresQualifier.class.getName(), + EnsuresQualifierIf.class.getName())); + + /** + * Returns true if the given annotation name matches that of a pre- or post-condition annotation + * or meta-annotation that takes a qualifier as an argument. + * + * @param annotationName an annotation name + * @return true iff the annotation name matches that of a pre- or post-condition annotation + */ + private boolean isPreOrPostConditionAnnotation(Name annotationName) { + String annoName = annotationName.toString(); + return preAndPostConditionAnnotations.contains(annoName); + } + /** * If the computation of the type of the ConditionalExpressionTree in * org.checkerframework.framework.type.TypeFromTree.TypeFromExpression.visitConditionalExpression(ConditionalExpressionTree, diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index effc8dbfe12f..fa8f8c7b3a10 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -88,6 +88,7 @@ flowexpr.parse.context.not.determined=could not determine the context at '%s' wi flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned) contracts.precondition=precondition of %s is not satisfied.%nfound : %s%nrequired: %s contracts.postcondition=postcondition of %s is not satisfied.%nfound : %s%nrequired: %s +contracts.toptype=the top type %s has no effect contracts.conditional.postcondition=conditional postcondition is not satisfied when %s returns %s.%nfound : %s%nrequired: %s contracts.conditional.postcondition.returntype=this annotation is only valid for methods with return type 'boolean' # Same text for "override" and "methodref", but different key. diff --git a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java index 5d527785d022..e5a75b750a79 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -210,7 +210,7 @@ private Set getContract( * @param contractAnno a pre- or post-condition annotation, such as {@code @RequiresQualifier} * @return the type annotation specified in {@code contractAnno.qualifier} */ - private @Nullable AnnotationMirror getQualifierEnforcedByContractAnnotation( + public @Nullable AnnotationMirror getQualifierEnforcedByContractAnnotation( AnnotationMirror contractAnno) { return getQualifierEnforcedByContractAnnotation(contractAnno, null, null); } diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index cf29e15c9c1a..62b7f36aa822 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -12,6 +12,7 @@ static class Base { @RequiresQualifier(expression = "f", qualifier = Odd.class) void requiresOdd() {} + // :: warning: (contracts.toptype) @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresUnqual() {} @@ -20,6 +21,7 @@ void ensuresOdd() { f = g; } + // :: warning: (contracts.toptype) @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) void ensuresUnqual() {} @@ -29,6 +31,7 @@ boolean ensuresIfOdd() { return true; } + // :: warning: (contracts.toptype) @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) boolean ensuresIfUnqual() { return true; @@ -38,6 +41,7 @@ boolean ensuresIfUnqual() { static class Derived extends Base { @Override + // :: warning: (contracts.toptype) @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresOdd() {} @@ -47,6 +51,7 @@ void requiresOdd() {} void requiresUnqual() {} @Override + // :: warning: (contracts.toptype) @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) // :: error: (contracts.postcondition.override) void ensuresOdd() { @@ -60,6 +65,7 @@ void ensuresUnqual() { } @Override + // :: warning: (contracts.toptype) @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) // :: error: (contracts.conditional.postcondition.true.override) boolean ensuresIfOdd() { diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index 5f8cbd303e74..2f0f17657715 100644 --- a/framework/tests/flow/Postcondition.java +++ b/framework/tests/flow/Postcondition.java @@ -1,3 +1,4 @@ +import org.checkerframework.common.subtyping.qual.Unqualified; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.qual.EnsuresQualifier; import org.checkerframework.framework.qual.EnsuresQualifierIf; @@ -312,4 +313,15 @@ void t6(@Odd String p1, @ValueTypeAnno String p2) { @Odd String l6 = f1; } } + + /** *** errors for invalid postconditions ***** */ + // :: warning: (contracts.toptype) + @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class) + void noOpForTesting() {} + + // :: warning: (contracts.toptype) + @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class) + boolean isF1NotSet() { + return f1 == null; + } } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 367076e5d1f9..f78ed5422149 100644 --- a/framework/tests/flow/Precondition.java +++ b/framework/tests/flow/Precondition.java @@ -1,3 +1,4 @@ +import org.checkerframework.common.subtyping.qual.Unqualified; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.qual.RequiresQualifier; import org.checkerframework.framework.test.*; @@ -159,4 +160,8 @@ void t5(@Odd String p1, String p2, @ValueTypeAnno String p3) { // :: error: (flowexpr.parse.error) error2(); } + + // :: warning: (contracts.toptype) + @RequiresQualifier(expression = "f1", qualifier = Unqualified.class) + void noOpForTesting() {} } From bb633db693bc827920990f5489f65f37b2f13553 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 22 Jan 2024 00:47:46 -0800 Subject: [PATCH 2/7] Add TODO about `@PreconditionAnnotation` and `@PostconditionAnnotation` --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 4 ++++ .../checkerframework/framework/util/ContractsFromMethod.java | 3 ++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 176736b336f2..829447247bdc 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2251,6 +2251,10 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { if (isPreOrPostConditionAnnotation(annoName)) { AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree); + System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName, tree); + // TODO: `getQualifierEnforcedByContractAnnotation` does not work for @PreconditionAnnotation + // or @PostconditionAnnotation. Should I extend the method to handle that, or should I put + // the logic here and avoid calling the method? AnnotationMirror qualifier = atypeFactory.getContractsFromMethod().getQualifierEnforcedByContractAnnotation(anno); if (qualifier != null) { diff --git a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java index e5a75b750a79..5b0adac24dd0 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -207,7 +207,8 @@ private Set getContract( * Returns the annotation mirror as specified by the {@code qualifier} element in {@code * contractAnno}. May return null. * - * @param contractAnno a pre- or post-condition annotation, such as {@code @RequiresQualifier} + * @param contractAnno a pre- or post-condition annotation, such as {@code @RequiresQualifier}. + * Does not work for {@code PreconditionAnnotation} or {@code PostconditionAnnotation}. * @return the type annotation specified in {@code contractAnno.qualifier} */ public @Nullable AnnotationMirror getQualifierEnforcedByContractAnnotation( From d6224a70687b16fa86443335f7f674729f567391 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 17 Mar 2024 21:21:56 -0700 Subject: [PATCH 3/7] Expand warning message --- .../org/checkerframework/common/basetype/messages.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index fa8f8c7b3a10..21f750adf7e7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -88,7 +88,7 @@ flowexpr.parse.context.not.determined=could not determine the context at '%s' wi flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned) contracts.precondition=precondition of %s is not satisfied.%nfound : %s%nrequired: %s contracts.postcondition=postcondition of %s is not satisfied.%nfound : %s%nrequired: %s -contracts.toptype=the top type %s has no effect +contracts.toptype=the top qualifer %s in a contract annotation %s has no effect contracts.conditional.postcondition=conditional postcondition is not satisfied when %s returns %s.%nfound : %s%nrequired: %s contracts.conditional.postcondition.returntype=this annotation is only valid for methods with return type 'boolean' # Same text for "override" and "methodref", but different key. From cd1da31a0d7411128b6a758bb22aea571949830a Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 4 Mar 2026 07:36:30 -0800 Subject: [PATCH 4/7] Put error message key in brackets --- .../tests/flow/ContractsOverridingSubtyping.java | 12 ++++++------ framework/tests/flow/Postcondition.java | 4 ++-- framework/tests/flow/Precondition.java | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index 5da4bded3819..0c32ee76b85c 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -12,7 +12,7 @@ static class Base { @RequiresQualifier(expression = "f", qualifier = Odd.class) void requiresOdd() {} - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresUnqual() {} @@ -21,7 +21,7 @@ void ensuresOdd() { f = g; } - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) void ensuresUnqual() {} @@ -31,7 +31,7 @@ boolean ensuresIfOdd() { return true; } - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) boolean ensuresIfUnqual() { return true; @@ -41,7 +41,7 @@ boolean ensuresIfUnqual() { static class Derived extends Base { @Override - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresOdd() {} @@ -51,7 +51,7 @@ void requiresOdd() {} void requiresUnqual() {} @Override - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) // :: error: [contracts.postcondition.override] void ensuresOdd() { @@ -65,7 +65,7 @@ void ensuresUnqual() { } @Override - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) // :: error: [contracts.conditional.postcondition.true.override] boolean ensuresIfOdd() { diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index edccaacc451a..cc3a9c3b534c 100644 --- a/framework/tests/flow/Postcondition.java +++ b/framework/tests/flow/Postcondition.java @@ -315,11 +315,11 @@ void t6(@Odd String p1, @ValueTypeAnno String p2) { } /** *** errors for invalid postconditions ***** */ - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class) void noOpForTesting() {} - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class) boolean isF1NotSet() { return f1 == null; diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 4c4134547cc8..d789e885629e 100644 --- a/framework/tests/flow/Precondition.java +++ b/framework/tests/flow/Precondition.java @@ -161,7 +161,7 @@ void t5(@Odd String p1, String p2, @ValueTypeAnno String p3) { error2(); } - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @RequiresQualifier(expression = "f1", qualifier = Unqualified.class) void noOpForTesting() {} } From 0b14148e8e8807db0ae11c9fbe6aa1c2ebcc4233 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 2 May 2026 19:20:18 -0700 Subject: [PATCH 5/7] Move warning suppression --- .../common/basetype/BaseTypeVisitor.java | 3 +-- .../common/basetype/messages.properties | 2 +- .../tests/flow/ContractsOverridingSubtyping.java | 12 ++++++------ 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 32075e9ffad2..f60505e55c32 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2467,8 +2467,7 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { /** Pre- and post-condition annotations that take a qualifier as an argument. */ private TreeSet preAndPostConditionAnnotations = new TreeSet<>( - // In Java 9+, use `List.of()`. - Arrays.asList( + List.of( PreconditionAnnotation.class.getName(), PostconditionAnnotation.class.getName(), RequiresQualifier.class.getName(), diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 977c71f7d0a8..b6debebf4f32 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -90,7 +90,7 @@ flowexpr.parse.context.not.determined=could not determine the context at '%s' wi flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned) contracts.precondition=precondition of %s is not satisfied.%nfound : %s%nrequired: %s contracts.postcondition=postcondition of %s is not satisfied.%nfound : %s%nrequired: %s -contracts.toptype=the top qualifer %s in a contract annotation %s has no effect +contracts.toptype=the top qualifer %s has no effect in contract annotation %s contracts.conditional.postcondition=conditional postcondition is not satisfied when %s returns %s.%nfound : %s%nrequired: %s contracts.conditional.postcondition.returntype=this annotation is only valid for methods with return type 'boolean' # Same text for "override" and "methodref", but different key. diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index 0c32ee76b85c..de69d8e504b0 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -12,8 +12,8 @@ static class Base { @RequiresQualifier(expression = "f", qualifier = Odd.class) void requiresOdd() {} - // :: warning: [contracts.toptype] @RequiresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: [contracts.toptype] void requiresUnqual() {} @EnsuresQualifier(expression = "f", qualifier = Odd.class) @@ -21,8 +21,8 @@ void ensuresOdd() { f = g; } - // :: warning: [contracts.toptype] @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: [contracts.toptype] void ensuresUnqual() {} @EnsuresQualifierIf(expression = "f", result = true, qualifier = Odd.class) @@ -31,8 +31,8 @@ boolean ensuresIfOdd() { return true; } - // :: warning: [contracts.toptype] @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) + // :: warning: [contracts.toptype] boolean ensuresIfUnqual() { return true; } @@ -41,8 +41,8 @@ boolean ensuresIfUnqual() { static class Derived extends Base { @Override - // :: warning: [contracts.toptype] @RequiresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: [contracts.toptype] void requiresOdd() {} @Override @@ -51,8 +51,8 @@ void requiresOdd() {} void requiresUnqual() {} @Override - // :: warning: [contracts.toptype] @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: [contracts.toptype] // :: error: [contracts.postcondition.override] void ensuresOdd() { f = g; @@ -65,8 +65,8 @@ void ensuresUnqual() { } @Override - // :: warning: [contracts.toptype] @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) + // :: warning: [contracts.toptype] // :: error: [contracts.conditional.postcondition.true.override] boolean ensuresIfOdd() { f = g; From e23c6972fa628398bf1a51870978e56f8244e2f6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 2 May 2026 19:44:48 -0700 Subject: [PATCH 6/7] Fix number of arguments to format method --- .../common/basetype/BaseTypeVisitor.java | 10 +++++----- .../tests/flow/ContractsOverridingSubtyping.java | 12 ++++++------ 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index f60505e55c32..6d8a25f50ecc 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2395,17 +2395,17 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { if (isPreOrPostConditionAnnotation(annoName)) { AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree); - System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName, tree); - // TODO: `getQualifierEnforcedByContractAnnotation` does not work for @PreconditionAnnotation - // or @PostconditionAnnotation. Should I extend the method to handle that, or should I put - // the logic here and avoid calling the method? + // TODO: `getQualifierEnforcedByContractAnnotation` does not work for user-defined contract + // annotations defined with @PreconditionAnnotation or @PostconditionAnnotation. Should I + // extend the method to handle that, or should I put the logic here and avoid calling the + // method? AnnotationMirror qualifier = atypeFactory.getContractsFromMethod().getQualifierEnforcedByContractAnnotation(anno); if (qualifier != null) { AnnotationMirror topForQualifier = qualHierarchy.getTopAnnotation(qualifier); if (AnnotationUtils.areSame(qualifier, topForQualifier)) { Name contractQualName = qualifier.getAnnotationType().asElement().getSimpleName(); - checker.reportWarning(tree, "contracts.toptype", contractQualName); + checker.reportWarning(tree, "contracts.toptype", contractQualName, tree); } } } diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index de69d8e504b0..0c32ee76b85c 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -12,8 +12,8 @@ static class Base { @RequiresQualifier(expression = "f", qualifier = Odd.class) void requiresOdd() {} - @RequiresQualifier(expression = "f", qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresUnqual() {} @EnsuresQualifier(expression = "f", qualifier = Odd.class) @@ -21,8 +21,8 @@ void ensuresOdd() { f = g; } - @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) void ensuresUnqual() {} @EnsuresQualifierIf(expression = "f", result = true, qualifier = Odd.class) @@ -31,8 +31,8 @@ boolean ensuresIfOdd() { return true; } - @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) boolean ensuresIfUnqual() { return true; } @@ -41,8 +41,8 @@ boolean ensuresIfUnqual() { static class Derived extends Base { @Override - @RequiresQualifier(expression = "f", qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @RequiresQualifier(expression = "f", qualifier = Unqualified.class) void requiresOdd() {} @Override @@ -51,8 +51,8 @@ void requiresOdd() {} void requiresUnqual() {} @Override - @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) // :: error: [contracts.postcondition.override] void ensuresOdd() { f = g; @@ -65,8 +65,8 @@ void ensuresUnqual() { } @Override - @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) // :: warning: [contracts.toptype] + @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) // :: error: [contracts.conditional.postcondition.true.override] boolean ensuresIfOdd() { f = g; From f04ff9f145b300c81ea3cbc003c1a65b3dafcf0d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 2 May 2026 20:07:20 -0700 Subject: [PATCH 7/7] Fixes --- .../common/basetype/BaseTypeVisitor.java | 12 ++++-------- .../common/basetype/messages.properties | 2 +- .../framework/util/ContractsFromMethod.java | 5 ++++- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6d8a25f50ecc..2c6f78d6d8c0 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -108,8 +108,6 @@ import org.checkerframework.framework.qual.EnsuresQualifier; import org.checkerframework.framework.qual.EnsuresQualifierIf; import org.checkerframework.framework.qual.HasQualifierParameter; -import org.checkerframework.framework.qual.PostconditionAnnotation; -import org.checkerframework.framework.qual.PreconditionAnnotation; import org.checkerframework.framework.qual.RequiresQualifier; import org.checkerframework.framework.qual.Unused; import org.checkerframework.framework.source.DiagMessage; @@ -2393,12 +2391,10 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { return null; } + // This logic is not in BaseTypeVisitor#checkContractsAtMethodDeclaration because that method + // apears to also check implicit annotations. if (isPreOrPostConditionAnnotation(annoName)) { AnnotationMirror anno = TreeUtils.annotationFromAnnotationTree(tree); - // TODO: `getQualifierEnforcedByContractAnnotation` does not work for user-defined contract - // annotations defined with @PreconditionAnnotation or @PostconditionAnnotation. Should I - // extend the method to handle that, or should I put the logic here and avoid calling the - // method? AnnotationMirror qualifier = atypeFactory.getContractsFromMethod().getQualifierEnforcedByContractAnnotation(anno); if (qualifier != null) { @@ -2468,8 +2464,6 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { private TreeSet preAndPostConditionAnnotations = new TreeSet<>( List.of( - PreconditionAnnotation.class.getName(), - PostconditionAnnotation.class.getName(), RequiresQualifier.class.getName(), EnsuresQualifier.class.getName(), EnsuresQualifierIf.class.getName())); @@ -2483,6 +2477,8 @@ public Void visitAnnotation(AnnotationTree tree, Void p) { */ private boolean isPreOrPostConditionAnnotation(Name annotationName) { String annoName = annotationName.toString(); + // TODO: This method should also return true for any annotation that is meta-annotated with + // @PreconditionAnnotation or @PostconditionAnnotation. return preAndPostConditionAnnotations.contains(annoName); } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index b6debebf4f32..48557b71f224 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -90,7 +90,7 @@ flowexpr.parse.context.not.determined=could not determine the context at '%s' wi flowexpr.parameter.not.final=parameter %s in '%s' is not effectively final (i.e., it gets re-assigned) contracts.precondition=precondition of %s is not satisfied.%nfound : %s%nrequired: %s contracts.postcondition=postcondition of %s is not satisfied.%nfound : %s%nrequired: %s -contracts.toptype=the top qualifer %s has no effect in contract annotation %s +contracts.toptype=the top qualifier %s has no effect in contract annotation %s contracts.conditional.postcondition=conditional postcondition is not satisfied when %s returns %s.%nfound : %s%nrequired: %s contracts.conditional.postcondition.returntype=this annotation is only valid for methods with return type 'boolean' # Same text for "override" and "methodref", but different key. diff --git a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java index 5dd54e370bfa..f4f169140497 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -263,12 +263,15 @@ private Set getContract( @Nullable AnnotationMirror argumentAnno, @Nullable Map argumentRenaming) { + // This method returns null for user-defined contract annotations defined with + // @PreconditionAnnotation or @PostconditionAnnotation. TODO: extend the method to handle that. + @SuppressWarnings("deprecation") // permitted for use in the framework Name c = AnnotationUtils.getElementValueClassName(contractAnno, "qualifier", false); AnnotationMirror anno; if (argumentAnno == null || argumentRenaming.isEmpty()) { - // If there are no arguments, use factory method that allows caching + // If there are no arguments, use factory method that allows caching. anno = AnnotationBuilder.fromName(factory.getElementUtils(), c); } else { AnnotationBuilder builder = new AnnotationBuilder(factory.getProcessingEnv(), c);