From 0fc6a61fa7e268c76c6f8aec3636308598ccd08e Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 29 Jan 2024 21:28:38 -0800 Subject: [PATCH 1/8] Issue error if top is used in a contract annotation --- .../ConditionalPostconditionAnnotation.java | 5 +- .../qual/PostconditionAnnotation.java | 5 +- .../qual/PreconditionAnnotation.java | 9 ++- .../CalledMethodsAnnotatedTypeFactory.java | 12 +-- .../calledmethods/CalledMethodsTransfer.java | 3 +- .../calledmethods/CalledMethodsVisitor.java | 3 +- .../ResourceLeakAnnotatedTypeFactory.java | 7 +- .../resourceleak/ResourceLeakVisitor.java | 8 +- .../common/basetype/BaseTypeVisitor.java | 18 +++-- .../common/basetype/messages.properties | 2 + ...InitializedFieldsAnnotatedTypeFactory.java | 6 +- .../framework/flow/CFAbstractTransfer.java | 7 +- .../framework/util/Contract.java | 20 +++-- .../framework/util/ContractsFromMethod.java | 77 +++++++++++++++---- .../javacutil/TypeSystemError.java | 6 +- 15 files changed, 134 insertions(+), 54 deletions(-) diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java index 9b7feb69237..4e28a675003 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java @@ -66,7 +66,10 @@ @Target({ElementType.ANNOTATION_TYPE}) public @interface ConditionalPostconditionAnnotation { /** - * The qualifier that will be established as a postcondition. + * The qualifier that will be established as a postcondition. There is no point using the top + * qualifier, which would have no effect because every expression has the top type (and possibly + * some more refined type). Establishing more refined types is the point of a pre- or + * post-condition annotation. * *

This element is analogous to {@link EnsuresQualifierIf#qualifier()}. */ diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java index 67bb434e848..1deebf8c53f 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/PostconditionAnnotation.java @@ -61,7 +61,10 @@ @Target({ElementType.ANNOTATION_TYPE}) public @interface PostconditionAnnotation { /** - * The qualifier that will be established as a postcondition. + * The qualifier that will be established as a postcondition. There is no point using the top + * qualifier, which would have no effect because every expression has the top type (and possibly + * some more refined type). Establishing more refined types is the point of a pre- or + * post-condition annotation. * *

This element is analogous to {@link EnsuresQualifier#qualifier()}. */ diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java index 95af23ec376..38b274c8996 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java @@ -56,6 +56,13 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.ANNOTATION_TYPE}) public @interface PreconditionAnnotation { - /** The qualifier that must be established as a precondition. */ + /** + * The qualifier that must be established as a precondition. There is no point using the top + * qualifier, which would have no effect because every expression has the top type (and possibly + * some more refined type). Establishing more refined types is the point of a pre- or + * post-condition annotation. + * + *

This element is analogous to {@link RequiresQualifier#qualifier()}. + */ Class qualifier(); } diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java index a81c7d39dc7..f137c98b6f1 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java @@ -2,6 +2,7 @@ import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.MethodTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; import java.util.ArrayList; @@ -483,7 +484,7 @@ public boolean isIgnoredExceptionType(TypeMirror exceptionType) { * and can be freely modified by callers */ public Set getExceptionalPostconditions( - ExecutableElement methodOrConstructor) { + ExecutableElement methodOrConstructor, MethodTree methodDecl) { Set result = new LinkedHashSet<>(); parseEnsuresCalledMethodOnExceptionListAnnotation( @@ -496,8 +497,9 @@ public Set getExceptionalPostconditions( } /** - * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link - * EnsuresCalledMethodsOnException.List} annotation and stores the results in out. + * Helper for {@link #getExceptionalPostconditions(ExecutableElement, MethodTree)} that parses a + * {@link EnsuresCalledMethodsOnException.List} annotation and stores the results in out + * . * * @param annotation the annotation * @param out the output collection @@ -521,8 +523,8 @@ private void parseEnsuresCalledMethodOnExceptionListAnnotation( } /** - * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link - * EnsuresCalledMethodsOnException} annotation and stores the results in out. + * Helper for {@link #getExceptionalPostconditions(ExecutableElement, MethodTree)} that parses a + * {@link EnsuresCalledMethodsOnException} annotation and stores the results in out. * * @param annotation the annotation * @param out the output collection diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java index c9132bc1b2e..fb0dadcd1ef 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -268,7 +268,8 @@ private void handleEnsuresCalledMethodsOnException( Map exceptionalStores) { Types types = atypeFactory.getProcessingEnv().getTypeUtils(); for (EnsuresCalledMethodOnExceptionContract postcond : - ((CalledMethodsAnnotatedTypeFactory) atypeFactory).getExceptionalPostconditions(method)) { + ((CalledMethodsAnnotatedTypeFactory) atypeFactory) + .getExceptionalPostconditions(method, null)) { JavaExpression e; try { e = diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java index 45fb2988780..89a57ba7a4f 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java @@ -66,7 +66,8 @@ public Void visitMethod(MethodTree tree, Void p) { } } for (EnsuresCalledMethodOnExceptionContract postcond : - ((CalledMethodsAnnotatedTypeFactory) atypeFactory).getExceptionalPostconditions(elt)) { + ((CalledMethodsAnnotatedTypeFactory) atypeFactory) + .getExceptionalPostconditions(elt, tree)) { checkExceptionalPostcondition(postcond, tree); } return super.visitMethod(tree, p); diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index 243ed1bdbe8..c0ea018c6f5 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -2,6 +2,7 @@ import com.google.common.collect.BiMap; import com.google.common.collect.HashBiMap; +import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; import java.lang.annotation.Annotation; import java.util.Arrays; @@ -445,9 +446,9 @@ public boolean hasOwning(Element elt) { @Override public Set getExceptionalPostconditions( - ExecutableElement methodOrConstructor) { + ExecutableElement methodOrConstructor, MethodTree methodDecl) { Set result = - super.getExceptionalPostconditions(methodOrConstructor); + super.getExceptionalPostconditions(methodOrConstructor, methodDecl); // This override is a sneaky way to satisfy a few subtle design constraints: // 1. The RLC requires destructors to close the class's @Owning fields even on exception @@ -475,7 +476,7 @@ public Set getExceptionalPostconditions( if (isMustCallMethod(methodOrConstructor)) { Set normalPostconditions = - getContractsFromMethod().getPostconditions(methodOrConstructor); + getContractsFromMethod().getPostconditions(methodOrConstructor, methodDecl); for (Contract.Postcondition normalPostcondition : normalPostconditions) { for (String method : getCalledMethods(normalPostcondition.annotation)) { result.add( diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index 617acaac5ea..e0ab6e4bc46 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -280,9 +280,11 @@ private void checkMustCallAliasAnnoMismatch( String message = isMustCallAliasAnnotationOnParameter ? String.format( - "there is no @MustCallAlias annotation on %s, even though the parameter %s is annotated with @MustCallAlias", + "there is no @MustCallAlias annotation on %s, even though the parameter %s is" + + " annotated with @MustCallAlias", locationOfCheck, paramWithMustCallAliasAnno) - : "no parameter has a @MustCallAlias annotation, even though the return type is annotated with @MustCallAlias"; + : "no parameter has a @MustCallAlias annotation, even though the return type is" + + " annotated with @MustCallAlias"; checker.reportWarning(tree, "mustcallalias.method.return.and.param", message); } } @@ -539,7 +541,7 @@ private void checkOwningField(VariableElement field) { } Set exceptionalPostconds = - rlTypeFactory.getExceptionalPostconditions(siblingMethod); + rlTypeFactory.getExceptionalPostconditions(siblingMethod, null); for (EnsuresCalledMethodOnExceptionContract postcond : exceptionalPostconds) { if (expressionEqualsField(postcond.getExpression(), field)) { unsatisfiedMustCallObligationsOfOwningField.remove( 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 2296eb06587..b720efcbd27 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1284,7 +1284,8 @@ private void checkContractsAtMethodDeclaration( ExecutableElement methodElement, List formalParamNames, boolean abstractMethod) { - Set contracts = atypeFactory.getContractsFromMethod().getContracts(methodElement); + Set contracts = + atypeFactory.getContractsFromMethod().getContracts(methodElement, methodTree); if (contracts.isEmpty()) { return; @@ -1823,7 +1824,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { // check precondition annotations checkPreconditions( - tree, atypeFactory.getContractsFromMethod().getPreconditions(invokedMethodElement)); + tree, atypeFactory.getContractsFromMethod().getPreconditions(invokedMethodElement, null)); if (TreeUtils.isSuperConstructorCall(tree)) { checkSuperConstructorCall(tree); @@ -4040,8 +4041,8 @@ private void checkPreAndPostConditions() { ContractsFromMethod contractsUtils = atypeFactory.getContractsFromMethod(); // Check preconditions - Set superPre = contractsUtils.getPreconditions(overridden.getElement()); - Set subPre = contractsUtils.getPreconditions(overrider.getElement()); + Set superPre = contractsUtils.getPreconditions(overridden.getElement(), null); + Set subPre = contractsUtils.getPreconditions(overrider.getElement(), null); Set> superPre2 = parseAndLocalizeContracts(superPre, overridden); Set> subPre2 = @@ -4051,8 +4052,9 @@ private void checkPreAndPostConditions() { checkContractsSubset(overriderType, overriddenType, subPre2, superPre2, premsg); // Check postconditions - Set superPost = contractsUtils.getPostconditions(overridden.getElement()); - Set subPost = contractsUtils.getPostconditions(overrider.getElement()); + Set superPost = + contractsUtils.getPostconditions(overridden.getElement(), null); + Set subPost = contractsUtils.getPostconditions(overrider.getElement(), null); Set> superPost2 = parseAndLocalizeContracts(superPost, overridden); Set> subPost2 = @@ -4063,9 +4065,9 @@ private void checkPreAndPostConditions() { // Check conditional postconditions Set superCPost = - contractsUtils.getConditionalPostconditions(overridden.getElement()); + contractsUtils.getConditionalPostconditions(overridden.getElement(), null); Set subCPost = - contractsUtils.getConditionalPostconditions(overrider.getElement()); + contractsUtils.getConditionalPostconditions(overrider.getElement(), null); // consider only 'true' postconditions Set superCPostTrue = filterConditionalPostconditions(superCPost, true); Set subCPostTrue = filterConditionalPostconditions(subCPost, true); 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 effc8dbfe12..2376d71713a 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -122,3 +122,5 @@ anno.on.irrelevant=Annotation %s is not applicable to %s%s redundant.anno=Annotation %s is redundant: it's the same as the default at this location type.inference.failed=type inference crashed: %s + +contract.top.qualifier=a top qualifer %s in a contract annotation %s has no effect diff --git a/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java index 02548ba4e0e..2ae14db9dc8 100644 --- a/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java @@ -1,5 +1,6 @@ package org.checkerframework.common.initializedfields; +import com.sun.source.tree.MethodTree; import com.sun.source.tree.VariableTree; import java.lang.reflect.InvocationTargetException; import java.util.ArrayList; @@ -125,8 +126,9 @@ public InitializedFieldsContractsFromMethod(GenericAnnotatedTypeFactory getPostconditions(ExecutableElement executableElement) { - Set result = super.getPostconditions(executableElement); + public Set getPostconditions( + ExecutableElement executableElement, MethodTree methodDecl) { + Set result = super.getPostconditions(executableElement, methodDecl); // Only process methods defined in source code being type-checked. if (declarationFromElement(executableElement) != null) { diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index dac4e2e19db..42e18ebcbf5 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -495,7 +495,8 @@ protected void addInformationFromPreconditions( MethodTree methodDeclTree, ExecutableElement methodElement) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); - Set preconditions = contractsUtils.getPreconditions(methodElement); + Set preconditions = + contractsUtils.getPreconditions(methodElement, methodDeclTree); StringToJavaExpression stringToJavaExpr = stringExpr -> StringToJavaExpression.atMethodBody(stringExpr, methodDeclTree, analysis.checker); @@ -1070,7 +1071,7 @@ protected void processPostconditions( ExecutableElement executableElement, ExpressionTree invocationTree) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); - Set postconditions = contractsUtils.getPostconditions(executableElement); + Set postconditions = contractsUtils.getPostconditions(executableElement, null); processPostconditionsAndConditionalPostconditions( invocationNode, invocationTree, store, null, postconditions); } @@ -1093,7 +1094,7 @@ protected void processConditionalPostconditions( S elseStore) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); Set conditionalPostconditions = - contractsUtils.getConditionalPostconditions(methodElement); + contractsUtils.getConditionalPostconditions(methodElement, null); processPostconditionsAndConditionalPostconditions( invocationNode, invocationTree, thenStore, elseStore, conditionalPostconditions); } diff --git a/framework/src/main/java/org/checkerframework/framework/util/Contract.java b/framework/src/main/java/org/checkerframework/framework/util/Contract.java index a69da26a177..7b26fd603ea 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/Contract.java +++ b/framework/src/main/java/org/checkerframework/framework/util/Contract.java @@ -18,7 +18,8 @@ /** * A contract represents an annotation on an expression. It is a precondition, postcondition, or - * conditional postcondition. + * conditional postcondition. It can arise from a programmer-written annotation, by inheriting an + * annotation, and possibly via other mechanisms. * * @see Precondition * @see Postcondition @@ -73,13 +74,22 @@ public enum Kind { /** Used for constructing error messages. */ public final String errorKey; - /** The meta-annotation identifying annotations of this kind. */ + /** + * The meta-annotation identifying annotations of this kind: PreconditionAnnotation, + * PostconditionAnnotation, or ConditionalPostconditionAnnotation. + */ public final Class metaAnnotation; - /** The built-in framework qualifier for this contract. */ + /** + * The built-in framework qualifier for this contract: RequiresQualifier, EnsuresQualifier, or + * EnsuresQualifierIf. + */ public final Class frameworkContractClass; - /** The built-in framework qualifier for repeated occurrences of this contract. */ + /** + * The built-in framework qualifier for repeated occurrences of this contract: + * RequiresQualifier.List, EnsuresQualifier.List, or EnsuresQualifierIf.List. + */ public final Class frameworkContractListClass; /** @@ -125,7 +135,7 @@ private Contract( } /** - * Creates a new Contract. + * Creates a new {@code Contract}. * * @param kind precondition, postcondition, or conditional postcondition * @param expressionString the Java expression that should have a type qualifier 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 3ca9bf322bb..cad74ecd79e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -1,5 +1,6 @@ package org.checkerframework.framework.util; +import com.sun.source.tree.MethodTree; import java.util.Collections; import java.util.HashMap; import java.util.LinkedHashSet; @@ -23,6 +24,7 @@ import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypeSystemError; import org.plumelib.util.IPair; /** @@ -60,13 +62,14 @@ public ContractsFromMethod(GenericAnnotatedTypeFactory factory) { * Returns all the contracts on method or constructor {@code executableElement}. * * @param executableElement the method or constructor whose contracts to retrieve + * @param methodDecl the method declaration * @return the contracts on {@code executableElement} */ - public Set getContracts(ExecutableElement executableElement) { + public Set getContracts(ExecutableElement executableElement, MethodTree methodDecl) { Set contracts = new LinkedHashSet<>(); - contracts.addAll(getPreconditions(executableElement)); - contracts.addAll(getPostconditions(executableElement)); - contracts.addAll(getConditionalPostconditions(executableElement)); + contracts.addAll(getPreconditions(executableElement, methodDecl)); + contracts.addAll(getPostconditions(executableElement, methodDecl)); + contracts.addAll(getConditionalPostconditions(executableElement, methodDecl)); return contracts; } @@ -76,8 +79,10 @@ public Set getContracts(ExecutableElement executableElement) { * @param executableElement the method whose contracts to return * @return the precondition contracts on {@code executableElement} */ - public Set getPreconditions(ExecutableElement executableElement) { - return getContracts(executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class); + public Set getPreconditions( + ExecutableElement executableElement, @Nullable MethodTree methodDecl) { + return getContractsOfKind( + executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class, methodDecl); } /** @@ -86,9 +91,10 @@ public Set getPreconditions(ExecutableElement executableE * @param executableElement the method whose contracts to return * @return the postcondition contracts on {@code executableElement} */ - public Set getPostconditions(ExecutableElement executableElement) { - return getContracts( - executableElement, Contract.Kind.POSTCONDITION, Contract.Postcondition.class); + public Set getPostconditions( + ExecutableElement executableElement, @Nullable MethodTree methodDecl) { + return getContractsOfKind( + executableElement, Contract.Kind.POSTCONDITION, Contract.Postcondition.class, methodDecl); } /** @@ -98,11 +104,12 @@ public Set getPostconditions(ExecutableElement executabl * @return the conditional postcondition contracts on {@code methodElement} */ public Set getConditionalPostconditions( - ExecutableElement methodElement) { - return getContracts( + ExecutableElement methodElement, @Nullable MethodTree methodDecl) { + return getContractsOfKind( methodElement, Contract.Kind.CONDITIONALPOSTCONDITION, - Contract.ConditionalPostcondition.class); + Contract.ConditionalPostcondition.class, + methodDecl); } /// Helper methods @@ -115,18 +122,25 @@ public Set getConditionalPostconditions( * @param executableElement the method whose contracts to return * @param kind the kind of contracts to retrieve * @param clazz the class to determine the return type + * @param methodDecl the declaration of executableElement, or null * @return the contracts on {@code executableElement} */ - private Set getContracts( - ExecutableElement executableElement, Contract.Kind kind, Class clazz) { + private Set getContractsOfKind( + ExecutableElement executableElement, + Contract.Kind kind, + Class clazz, + @Nullable MethodTree methodDecl) { Set result = new LinkedHashSet<>(); + // Check for a single framework-defined contract annotation. + // The result is RequiresQualifier, EnsuresQualifier, or EnsuresQualifierIf. AnnotationMirror frameworkContractAnno = factory.getDeclAnnotation(executableElement, kind.frameworkContractClass); result.addAll(getContract(kind, frameworkContractAnno, clazz)); // Check for a framework-defined wrapper around contract annotations. // The result is RequiresQualifier.List, EnsuresQualifier.List, or EnsuresQualifierIf.List. + // Add its elements to `result`. AnnotationMirror frameworkContractListAnno = factory.getDeclAnnotation(executableElement, kind.frameworkContractListClass); if (frameworkContractListAnno != null) { @@ -137,18 +151,47 @@ private Set getContracts( } } - // Check for type-system specific annotations. + // At this point, `result` contains only framework-defined contract annotations. + Set tops = factory.getQualifierHierarchy().getTopAnnotations(); + for (T contract : result) { + AnnotationMirror anno = contract.annotation; + if (AnnotationUtils.containsSame(tops, anno)) { + // TODO: Unfortunately, TypeSystemError does not permit giving a tree at which to issue the + // error. Obtain the file and line number from the tree, and print them here. + // TODO: Issue a warning on the annotation itself rather than on the method declaration. + // This requires iterating over the annotation trees on the method declaration to determine + // which one led tho the given AnnotationMirror. + throw new TypeSystemError( + "Contract annotation %s on method %s uses the top qualifier %s, which has no effect.", + contract.contractAnnotation, methodDecl.getName(), anno); + } + } + + // Check for type-system specific annotations. These are the annotations that are + // meta-annotated by `kind.metaAnnotation`, which is PreconditionAnnotation, + // PostconditionAnnotation, or ConditionalPostconditionAnnotation. List> declAnnotations = factory.getDeclAnnotationWithMetaAnnotation(executableElement, kind.metaAnnotation); for (IPair r : declAnnotations) { AnnotationMirror anno = r.first; - // contractAnno is the meta-annotation on anno. + // contractAnno is the meta-annotation on anno, such as PreconditionAnnotation, + // PostconditionAnnotation, or ConditionalPostconditionAnnotation. AnnotationMirror contractAnno = r.second; AnnotationMirror enforcedQualifier = getQualifierEnforcedByContractAnnotation(contractAnno, anno); if (enforcedQualifier == null) { continue; } + if (AnnotationUtils.containsSame(tops, enforcedQualifier)) { + // TODO: issue a warning on the annotation itself rather than on the method declaration. + // This requires iterating over the annotation trees on the method declaration to determine + // which one led tho the given AnnotationMirror. + + factory + .getChecker() + .reportError(methodDecl, "contract.top.qualifier", enforcedQualifier, contractAnno); + } + List expressions = factory.getContractExpressions(kind, anno); Collections.sort(expressions); Boolean ensuresQualifierIfResult = factory.getEnsuresQualifierIfResult(kind, anno); @@ -169,7 +212,7 @@ private Set getContracts( * @param the type of {@link Contract} to return * @param kind the kind of {@code contractAnnotation} * @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, {@link - * EnsuresQualifierIf}, or null + * EnsuresQualifierIf}, or null; TODO: document when a client would pass null * @param clazz the class to determine the return type * @return the contracts expressed by the given annotation, or the empty set if the argument is * null diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java index a6de9d49c70..5743e99fc85 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java @@ -4,11 +4,11 @@ import org.checkerframework.checker.nullness.qual.Nullable; /** - * Exception type indicating a mistake by a type system built using the Checker Framework. For + * Exception type indicating a mistake in a type system built using the Checker Framework. For * example, misusing a meta-annotation on a qualifier. * - *

To indicate a bug in the framework, use {@link BugInCF}. To indicate that an end user made a - * mistake, use {@link UserError}. + *

To indicate a bug in the framework, use {@link BugInCF}. To indicate that an end user (a + * programmer running a type-checker) made a mistake, use {@link UserError}. */ @SuppressWarnings("serial") public class TypeSystemError extends RuntimeException { From 4f5e623ef11e2f03ede48591247f4f71dbc10794 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 29 Jan 2024 22:01:52 -0800 Subject: [PATCH 2/8] Add tests --- .../common/basetype/messages.properties | 3 +- .../framework/source/SourceChecker.java | 4 ++- .../framework/util/ContractsFromMethod.java | 28 +++++++++++-------- .../flow/ContractsOverridingSubtyping.java | 6 ++++ framework/tests/flow/Postcondition.java | 12 ++++++++ framework/tests/flow/Precondition.java | 5 ++++ 6 files changed, 44 insertions(+), 14 deletions(-) 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 2376d71713a..21f750adf7e 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 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. @@ -122,5 +123,3 @@ anno.on.irrelevant=Annotation %s is not applicable to %s%s redundant.anno=Annotation %s is redundant: it's the same as the default at this location type.inference.failed=type inference crashed: %s - -contract.top.qualifier=a top qualifer %s in a contract annotation %s has no effect 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 f7bf5301fac..295cc23db46 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -1182,8 +1182,10 @@ private void report( messager.printMessage(kind, messageText, (Element) source); } else if (source instanceof Tree) { printOrStoreMessage(kind, messageText, (Tree) source, currentRoot); + } else if (source == null) { + messager.printMessage(kind, messageText); } else { - throw new BugInCF("invalid position source, class=" + source.getClass()); + throw new BugInCF("invalid position source of class " + source.getClass() + ": " + source); } } 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 cad74ecd79e..ae1201da560 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -156,14 +156,19 @@ private Set getContractsOfKind( for (T contract : result) { AnnotationMirror anno = contract.annotation; if (AnnotationUtils.containsSame(tops, anno)) { - // TODO: Unfortunately, TypeSystemError does not permit giving a tree at which to issue the - // error. Obtain the file and line number from the tree, and print them here. - // TODO: Issue a warning on the annotation itself rather than on the method declaration. + // TODO: issue a warning on the annotation itself rather than on the method declaration. // This requires iterating over the annotation trees on the method declaration to determine // which one led tho the given AnnotationMirror. - throw new TypeSystemError( - "Contract annotation %s on method %s uses the top qualifier %s, which has no effect.", - contract.contractAnnotation, methodDecl.getName(), anno); + if (methodDecl != null) { + String methodString = " on method " + methodDecl.getName(); + factory + .getChecker() + .reportError( + methodDecl, + "contracts.toptype", + anno, + contract.contractAnnotation + methodString); + } } } @@ -183,13 +188,14 @@ private Set getContractsOfKind( continue; } if (AnnotationUtils.containsSame(tops, enforcedQualifier)) { - // TODO: issue a warning on the annotation itself rather than on the method declaration. + // TODO: Unfortunately, TypeSystemError does not permit giving a tree at which to issue the + // error. Obtain the file and line number from the tree, and print them here. + // TODO: Issue a warning on the annotation itself rather than on the method declaration. // This requires iterating over the annotation trees on the method declaration to determine // which one led tho the given AnnotationMirror. - - factory - .getChecker() - .reportError(methodDecl, "contract.top.qualifier", enforcedQualifier, contractAnno); + throw new TypeSystemError( + "Contract annotation %s on method %s uses the top qualifier %s, which has no effect.", + contractAnno, methodDecl.getName(), enforcedQualifier); } List expressions = factory.getContractExpressions(kind, anno); diff --git a/framework/tests/flow/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java index cf29e15c9c1..59105f867ee 100644 --- a/framework/tests/flow/ContractsOverridingSubtyping.java +++ b/framework/tests/flow/ContractsOverridingSubtyping.java @@ -13,6 +13,7 @@ static class Base { void requiresOdd() {} @RequiresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) void requiresUnqual() {} @EnsuresQualifier(expression = "f", qualifier = Odd.class) @@ -21,6 +22,7 @@ void ensuresOdd() { } @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) void ensuresUnqual() {} @EnsuresQualifierIf(expression = "f", result = true, qualifier = Odd.class) @@ -30,6 +32,7 @@ boolean ensuresIfOdd() { } @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) + // :: warning: (contracts.toptype) boolean ensuresIfUnqual() { return true; } @@ -39,6 +42,7 @@ static class Derived extends Base { @Override @RequiresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) void requiresOdd() {} @Override @@ -48,6 +52,7 @@ void requiresUnqual() {} @Override @EnsuresQualifier(expression = "f", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) // :: error: (contracts.postcondition.override) void ensuresOdd() { f = g; @@ -61,6 +66,7 @@ void ensuresUnqual() { @Override @EnsuresQualifierIf(expression = "f", result = true, qualifier = Unqualified.class) + // :: warning: (contracts.toptype) // :: error: (contracts.conditional.postcondition.true.override) boolean ensuresIfOdd() { f = g; diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index 5f8cbd303e7..26d4a5803ad 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 ***** */ + @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) + void noOpForTesting() {} + + @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) + boolean isF1NotSet() { + return f1 == null; + } } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 367076e5d1f..f78ed542214 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 0e1c6bb1938243827ea869905ee7c1447a8dd71b Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 30 Jan 2024 00:04:05 -0800 Subject: [PATCH 3/8] Remove MethodTree argument --- .../CalledMethodsAnnotatedTypeFactory.java | 12 +++--- .../calledmethods/CalledMethodsTransfer.java | 3 +- .../calledmethods/CalledMethodsVisitor.java | 3 +- .../ResourceLeakAnnotatedTypeFactory.java | 7 ++-- .../resourceleak/ResourceLeakVisitor.java | 2 +- .../nullness/PreconditionFieldNotInStore.java | 1 + .../common/basetype/BaseTypeVisitor.java | 18 ++++---- ...InitializedFieldsAnnotatedTypeFactory.java | 6 +-- .../framework/flow/CFAbstractTransfer.java | 7 ++-- .../framework/util/ContractsFromMethod.java | 41 ++++++++----------- framework/tests/flow/Precondition.java | 2 +- 11 files changed, 42 insertions(+), 60 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java index f137c98b6f1..a81c7d39dc7 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java @@ -2,7 +2,6 @@ import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodInvocationTree; -import com.sun.source.tree.MethodTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; import java.util.ArrayList; @@ -484,7 +483,7 @@ public boolean isIgnoredExceptionType(TypeMirror exceptionType) { * and can be freely modified by callers */ public Set getExceptionalPostconditions( - ExecutableElement methodOrConstructor, MethodTree methodDecl) { + ExecutableElement methodOrConstructor) { Set result = new LinkedHashSet<>(); parseEnsuresCalledMethodOnExceptionListAnnotation( @@ -497,9 +496,8 @@ public Set getExceptionalPostconditions( } /** - * Helper for {@link #getExceptionalPostconditions(ExecutableElement, MethodTree)} that parses a - * {@link EnsuresCalledMethodsOnException.List} annotation and stores the results in out - * . + * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link + * EnsuresCalledMethodsOnException.List} annotation and stores the results in out. * * @param annotation the annotation * @param out the output collection @@ -523,8 +521,8 @@ private void parseEnsuresCalledMethodOnExceptionListAnnotation( } /** - * Helper for {@link #getExceptionalPostconditions(ExecutableElement, MethodTree)} that parses a - * {@link EnsuresCalledMethodsOnException} annotation and stores the results in out. + * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link + * EnsuresCalledMethodsOnException} annotation and stores the results in out. * * @param annotation the annotation * @param out the output collection diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java index fb0dadcd1ef..c9132bc1b2e 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -268,8 +268,7 @@ private void handleEnsuresCalledMethodsOnException( Map exceptionalStores) { Types types = atypeFactory.getProcessingEnv().getTypeUtils(); for (EnsuresCalledMethodOnExceptionContract postcond : - ((CalledMethodsAnnotatedTypeFactory) atypeFactory) - .getExceptionalPostconditions(method, null)) { + ((CalledMethodsAnnotatedTypeFactory) atypeFactory).getExceptionalPostconditions(method)) { JavaExpression e; try { e = diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java index 89a57ba7a4f..45fb2988780 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsVisitor.java @@ -66,8 +66,7 @@ public Void visitMethod(MethodTree tree, Void p) { } } for (EnsuresCalledMethodOnExceptionContract postcond : - ((CalledMethodsAnnotatedTypeFactory) atypeFactory) - .getExceptionalPostconditions(elt, tree)) { + ((CalledMethodsAnnotatedTypeFactory) atypeFactory).getExceptionalPostconditions(elt)) { checkExceptionalPostcondition(postcond, tree); } return super.visitMethod(tree, p); diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index c0ea018c6f5..243ed1bdbe8 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -2,7 +2,6 @@ import com.google.common.collect.BiMap; import com.google.common.collect.HashBiMap; -import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; import java.lang.annotation.Annotation; import java.util.Arrays; @@ -446,9 +445,9 @@ public boolean hasOwning(Element elt) { @Override public Set getExceptionalPostconditions( - ExecutableElement methodOrConstructor, MethodTree methodDecl) { + ExecutableElement methodOrConstructor) { Set result = - super.getExceptionalPostconditions(methodOrConstructor, methodDecl); + super.getExceptionalPostconditions(methodOrConstructor); // This override is a sneaky way to satisfy a few subtle design constraints: // 1. The RLC requires destructors to close the class's @Owning fields even on exception @@ -476,7 +475,7 @@ public Set getExceptionalPostconditions( if (isMustCallMethod(methodOrConstructor)) { Set normalPostconditions = - getContractsFromMethod().getPostconditions(methodOrConstructor, methodDecl); + getContractsFromMethod().getPostconditions(methodOrConstructor); for (Contract.Postcondition normalPostcondition : normalPostconditions) { for (String method : getCalledMethods(normalPostcondition.annotation)) { result.add( diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index e0ab6e4bc46..2998e3abff0 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -541,7 +541,7 @@ private void checkOwningField(VariableElement field) { } Set exceptionalPostconds = - rlTypeFactory.getExceptionalPostconditions(siblingMethod, null); + rlTypeFactory.getExceptionalPostconditions(siblingMethod); for (EnsuresCalledMethodOnExceptionContract postcond : exceptionalPostconds) { if (expressionEqualsField(postcond.getExpression(), field)) { unsatisfiedMustCallObligationsOfOwningField.remove( diff --git a/checker/tests/nullness/PreconditionFieldNotInStore.java b/checker/tests/nullness/PreconditionFieldNotInStore.java index 4c1aa59fe4c..3447cd7eb5b 100644 --- a/checker/tests/nullness/PreconditionFieldNotInStore.java +++ b/checker/tests/nullness/PreconditionFieldNotInStore.java @@ -11,6 +11,7 @@ class PreconditionFieldNotInStore { @org.checkerframework.framework.qual.RequiresQualifier( expression = {"this.filename"}, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) + // :: warning: (contracts.toptype) @org.checkerframework.checker.nullness.qual.NonNull String getIndentString() { return "indentString"; } 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 b720efcbd27..2296eb06587 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1284,8 +1284,7 @@ private void checkContractsAtMethodDeclaration( ExecutableElement methodElement, List formalParamNames, boolean abstractMethod) { - Set contracts = - atypeFactory.getContractsFromMethod().getContracts(methodElement, methodTree); + Set contracts = atypeFactory.getContractsFromMethod().getContracts(methodElement); if (contracts.isEmpty()) { return; @@ -1824,7 +1823,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { // check precondition annotations checkPreconditions( - tree, atypeFactory.getContractsFromMethod().getPreconditions(invokedMethodElement, null)); + tree, atypeFactory.getContractsFromMethod().getPreconditions(invokedMethodElement)); if (TreeUtils.isSuperConstructorCall(tree)) { checkSuperConstructorCall(tree); @@ -4041,8 +4040,8 @@ private void checkPreAndPostConditions() { ContractsFromMethod contractsUtils = atypeFactory.getContractsFromMethod(); // Check preconditions - Set superPre = contractsUtils.getPreconditions(overridden.getElement(), null); - Set subPre = contractsUtils.getPreconditions(overrider.getElement(), null); + Set superPre = contractsUtils.getPreconditions(overridden.getElement()); + Set subPre = contractsUtils.getPreconditions(overrider.getElement()); Set> superPre2 = parseAndLocalizeContracts(superPre, overridden); Set> subPre2 = @@ -4052,9 +4051,8 @@ private void checkPreAndPostConditions() { checkContractsSubset(overriderType, overriddenType, subPre2, superPre2, premsg); // Check postconditions - Set superPost = - contractsUtils.getPostconditions(overridden.getElement(), null); - Set subPost = contractsUtils.getPostconditions(overrider.getElement(), null); + Set superPost = contractsUtils.getPostconditions(overridden.getElement()); + Set subPost = contractsUtils.getPostconditions(overrider.getElement()); Set> superPost2 = parseAndLocalizeContracts(superPost, overridden); Set> subPost2 = @@ -4065,9 +4063,9 @@ private void checkPreAndPostConditions() { // Check conditional postconditions Set superCPost = - contractsUtils.getConditionalPostconditions(overridden.getElement(), null); + contractsUtils.getConditionalPostconditions(overridden.getElement()); Set subCPost = - contractsUtils.getConditionalPostconditions(overrider.getElement(), null); + contractsUtils.getConditionalPostconditions(overrider.getElement()); // consider only 'true' postconditions Set superCPostTrue = filterConditionalPostconditions(superCPost, true); Set subCPostTrue = filterConditionalPostconditions(subCPost, true); diff --git a/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java index 2ae14db9dc8..02548ba4e0e 100644 --- a/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/initializedfields/InitializedFieldsAnnotatedTypeFactory.java @@ -1,6 +1,5 @@ package org.checkerframework.common.initializedfields; -import com.sun.source.tree.MethodTree; import com.sun.source.tree.VariableTree; import java.lang.reflect.InvocationTargetException; import java.util.ArrayList; @@ -126,9 +125,8 @@ public InitializedFieldsContractsFromMethod(GenericAnnotatedTypeFactory getPostconditions( - ExecutableElement executableElement, MethodTree methodDecl) { - Set result = super.getPostconditions(executableElement, methodDecl); + public Set getPostconditions(ExecutableElement executableElement) { + Set result = super.getPostconditions(executableElement); // Only process methods defined in source code being type-checked. if (declarationFromElement(executableElement) != null) { diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 42e18ebcbf5..dac4e2e19db 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -495,8 +495,7 @@ protected void addInformationFromPreconditions( MethodTree methodDeclTree, ExecutableElement methodElement) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); - Set preconditions = - contractsUtils.getPreconditions(methodElement, methodDeclTree); + Set preconditions = contractsUtils.getPreconditions(methodElement); StringToJavaExpression stringToJavaExpr = stringExpr -> StringToJavaExpression.atMethodBody(stringExpr, methodDeclTree, analysis.checker); @@ -1071,7 +1070,7 @@ protected void processPostconditions( ExecutableElement executableElement, ExpressionTree invocationTree) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); - Set postconditions = contractsUtils.getPostconditions(executableElement, null); + Set postconditions = contractsUtils.getPostconditions(executableElement); processPostconditionsAndConditionalPostconditions( invocationNode, invocationTree, store, null, postconditions); } @@ -1094,7 +1093,7 @@ protected void processConditionalPostconditions( S elseStore) { ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod(); Set conditionalPostconditions = - contractsUtils.getConditionalPostconditions(methodElement, null); + contractsUtils.getConditionalPostconditions(methodElement); processPostconditionsAndConditionalPostconditions( invocationNode, invocationTree, thenStore, elseStore, conditionalPostconditions); } 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 ae1201da560..cf4b3a56ef4 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -1,6 +1,5 @@ package org.checkerframework.framework.util; -import com.sun.source.tree.MethodTree; import java.util.Collections; import java.util.HashMap; import java.util.LinkedHashSet; @@ -62,14 +61,13 @@ public ContractsFromMethod(GenericAnnotatedTypeFactory factory) { * Returns all the contracts on method or constructor {@code executableElement}. * * @param executableElement the method or constructor whose contracts to retrieve - * @param methodDecl the method declaration * @return the contracts on {@code executableElement} */ - public Set getContracts(ExecutableElement executableElement, MethodTree methodDecl) { + public Set getContracts(ExecutableElement executableElement) { Set contracts = new LinkedHashSet<>(); - contracts.addAll(getPreconditions(executableElement, methodDecl)); - contracts.addAll(getPostconditions(executableElement, methodDecl)); - contracts.addAll(getConditionalPostconditions(executableElement, methodDecl)); + contracts.addAll(getPreconditions(executableElement)); + contracts.addAll(getPostconditions(executableElement)); + contracts.addAll(getConditionalPostconditions(executableElement)); return contracts; } @@ -79,10 +77,9 @@ public Set getContracts(ExecutableElement executableElement, MethodTre * @param executableElement the method whose contracts to return * @return the precondition contracts on {@code executableElement} */ - public Set getPreconditions( - ExecutableElement executableElement, @Nullable MethodTree methodDecl) { + public Set getPreconditions(ExecutableElement executableElement) { return getContractsOfKind( - executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class, methodDecl); + executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class); } /** @@ -91,10 +88,9 @@ public Set getPreconditions( * @param executableElement the method whose contracts to return * @return the postcondition contracts on {@code executableElement} */ - public Set getPostconditions( - ExecutableElement executableElement, @Nullable MethodTree methodDecl) { + public Set getPostconditions(ExecutableElement executableElement) { return getContractsOfKind( - executableElement, Contract.Kind.POSTCONDITION, Contract.Postcondition.class, methodDecl); + executableElement, Contract.Kind.POSTCONDITION, Contract.Postcondition.class); } /** @@ -104,12 +100,11 @@ public Set getPostconditions( * @return the conditional postcondition contracts on {@code methodElement} */ public Set getConditionalPostconditions( - ExecutableElement methodElement, @Nullable MethodTree methodDecl) { + ExecutableElement methodElement) { return getContractsOfKind( methodElement, Contract.Kind.CONDITIONALPOSTCONDITION, - Contract.ConditionalPostcondition.class, - methodDecl); + Contract.ConditionalPostcondition.class); } /// Helper methods @@ -122,14 +117,10 @@ public Set getConditionalPostconditions( * @param executableElement the method whose contracts to return * @param kind the kind of contracts to retrieve * @param clazz the class to determine the return type - * @param methodDecl the declaration of executableElement, or null * @return the contracts on {@code executableElement} */ private Set getContractsOfKind( - ExecutableElement executableElement, - Contract.Kind kind, - Class clazz, - @Nullable MethodTree methodDecl) { + ExecutableElement executableElement, Contract.Kind kind, Class clazz) { Set result = new LinkedHashSet<>(); // Check for a single framework-defined contract annotation. @@ -159,12 +150,12 @@ private Set getContractsOfKind( // TODO: issue a warning on the annotation itself rather than on the method declaration. // This requires iterating over the annotation trees on the method declaration to determine // which one led tho the given AnnotationMirror. - if (methodDecl != null) { - String methodString = " on method " + methodDecl.getName(); + if (executableElement != null) { + String methodString = " on method " + executableElement.getSimpleName(); factory .getChecker() - .reportError( - methodDecl, + .reportWarning( + executableElement, "contracts.toptype", anno, contract.contractAnnotation + methodString); @@ -195,7 +186,7 @@ private Set getContractsOfKind( // which one led tho the given AnnotationMirror. throw new TypeSystemError( "Contract annotation %s on method %s uses the top qualifier %s, which has no effect.", - contractAnno, methodDecl.getName(), enforcedQualifier); + contractAnno, executableElement.getSimpleName(), enforcedQualifier); } List expressions = factory.getContractExpressions(kind, anno); diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index f78ed542214..754ae8a92e8 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) @RequiresQualifier(expression = "f1", qualifier = Unqualified.class) + // :: warning: (contracts.toptype) void noOpForTesting() {} } From 4155568a614c4b4a2b05f8ac831a3a4af2bd3404 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 30 Jan 2024 00:16:04 -0800 Subject: [PATCH 4/8] Undo changes --- .../common/basetype/messages.properties | 2 +- .../framework/source/SourceChecker.java | 2 -- .../org/checkerframework/framework/util/Contract.java | 3 +-- .../framework/util/ContractsFromMethod.java | 10 ++++++---- 4 files changed, 8 insertions(+), 9 deletions(-) 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 21f750adf7e..6aca35b12a6 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 qualifer %s in a contract annotation %s has no effect +contracts.toptype=the top qualifer %s in 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. 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 295cc23db46..21900fb3116 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -1182,8 +1182,6 @@ private void report( messager.printMessage(kind, messageText, (Element) source); } else if (source instanceof Tree) { printOrStoreMessage(kind, messageText, (Tree) source, currentRoot); - } else if (source == null) { - messager.printMessage(kind, messageText); } else { throw new BugInCF("invalid position source of class " + source.getClass() + ": " + source); } diff --git a/framework/src/main/java/org/checkerframework/framework/util/Contract.java b/framework/src/main/java/org/checkerframework/framework/util/Contract.java index 7b26fd603ea..3883adc4ecd 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/Contract.java +++ b/framework/src/main/java/org/checkerframework/framework/util/Contract.java @@ -18,8 +18,7 @@ /** * A contract represents an annotation on an expression. It is a precondition, postcondition, or - * conditional postcondition. It can arise from a programmer-written annotation, by inheriting an - * annotation, and possibly via other mechanisms. + * conditional postcondition. * * @see Precondition * @see Postcondition 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 cf4b3a56ef4..dbb95cd9779 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -124,10 +124,12 @@ private Set getContractsOfKind( Set result = new LinkedHashSet<>(); // Check for a single framework-defined contract annotation. - // The result is RequiresQualifier, EnsuresQualifier, or EnsuresQualifierIf. + // The result is RequiresQualifier, EnsuresQualifier, EnsuresQualifierIf, or null. AnnotationMirror frameworkContractAnno = factory.getDeclAnnotation(executableElement, kind.frameworkContractClass); - result.addAll(getContract(kind, frameworkContractAnno, clazz)); + if (frameworkContractAnno != null) { + result.addAll(getContract(kind, frameworkContractAnno, clazz)); + } // Check for a framework-defined wrapper around contract annotations. // The result is RequiresQualifier.List, EnsuresQualifier.List, or EnsuresQualifierIf.List. @@ -208,8 +210,8 @@ private Set getContractsOfKind( * * @param the type of {@link Contract} to return * @param kind the kind of {@code contractAnnotation} - * @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, {@link - * EnsuresQualifierIf}, or null; TODO: document when a client would pass null + * @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, or {@link + * EnsuresQualifierIf} * @param clazz the class to determine the return type * @return the contracts expressed by the given annotation, or the empty set if the argument is * null From f95f5a51b7f4eebf3ef29700bb2c024fee1700fa Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 30 Jan 2024 00:32:50 -0800 Subject: [PATCH 5/8] Undo changes --- .../framework/source/SourceChecker.java | 2 +- .../framework/util/Contract.java | 17 ++++--------- .../framework/util/ContractsFromMethod.java | 24 +++++++------------ .../javacutil/TypeSystemError.java | 6 ++--- 4 files changed, 17 insertions(+), 32 deletions(-) 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 21900fb3116..f7bf5301fac 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -1183,7 +1183,7 @@ private void report( } else if (source instanceof Tree) { printOrStoreMessage(kind, messageText, (Tree) source, currentRoot); } else { - throw new BugInCF("invalid position source of class " + source.getClass() + ": " + source); + throw new BugInCF("invalid position source, class=" + source.getClass()); } } diff --git a/framework/src/main/java/org/checkerframework/framework/util/Contract.java b/framework/src/main/java/org/checkerframework/framework/util/Contract.java index 3883adc4ecd..a69da26a177 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/Contract.java +++ b/framework/src/main/java/org/checkerframework/framework/util/Contract.java @@ -73,22 +73,13 @@ public enum Kind { /** Used for constructing error messages. */ public final String errorKey; - /** - * The meta-annotation identifying annotations of this kind: PreconditionAnnotation, - * PostconditionAnnotation, or ConditionalPostconditionAnnotation. - */ + /** The meta-annotation identifying annotations of this kind. */ public final Class metaAnnotation; - /** - * The built-in framework qualifier for this contract: RequiresQualifier, EnsuresQualifier, or - * EnsuresQualifierIf. - */ + /** The built-in framework qualifier for this contract. */ public final Class frameworkContractClass; - /** - * The built-in framework qualifier for repeated occurrences of this contract: - * RequiresQualifier.List, EnsuresQualifier.List, or EnsuresQualifierIf.List. - */ + /** The built-in framework qualifier for repeated occurrences of this contract. */ public final Class frameworkContractListClass; /** @@ -134,7 +125,7 @@ private Contract( } /** - * Creates a new {@code Contract}. + * Creates a new Contract. * * @param kind precondition, postcondition, or conditional postcondition * @param expressionString the Java expression that should have a type qualifier 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 dbb95cd9779..dffef845900 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java +++ b/framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java @@ -78,8 +78,7 @@ public Set getContracts(ExecutableElement executableElement) { * @return the precondition contracts on {@code executableElement} */ public Set getPreconditions(ExecutableElement executableElement) { - return getContractsOfKind( - executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class); + return getContracts(executableElement, Contract.Kind.PRECONDITION, Contract.Precondition.class); } /** @@ -89,7 +88,7 @@ public Set getPreconditions(ExecutableElement executableE * @return the postcondition contracts on {@code executableElement} */ public Set getPostconditions(ExecutableElement executableElement) { - return getContractsOfKind( + return getContracts( executableElement, Contract.Kind.POSTCONDITION, Contract.Postcondition.class); } @@ -101,7 +100,7 @@ public Set getPostconditions(ExecutableElement executabl */ public Set getConditionalPostconditions( ExecutableElement methodElement) { - return getContractsOfKind( + return getContracts( methodElement, Contract.Kind.CONDITIONALPOSTCONDITION, Contract.ConditionalPostcondition.class); @@ -119,7 +118,7 @@ public Set getConditionalPostconditions( * @param clazz the class to determine the return type * @return the contracts on {@code executableElement} */ - private Set getContractsOfKind( + private Set getContracts( ExecutableElement executableElement, Contract.Kind kind, Class clazz) { Set result = new LinkedHashSet<>(); @@ -127,9 +126,7 @@ private Set getContractsOfKind( // The result is RequiresQualifier, EnsuresQualifier, EnsuresQualifierIf, or null. AnnotationMirror frameworkContractAnno = factory.getDeclAnnotation(executableElement, kind.frameworkContractClass); - if (frameworkContractAnno != null) { - result.addAll(getContract(kind, frameworkContractAnno, clazz)); - } + result.addAll(getContract(kind, frameworkContractAnno, clazz)); // Check for a framework-defined wrapper around contract annotations. // The result is RequiresQualifier.List, EnsuresQualifier.List, or EnsuresQualifierIf.List. @@ -165,15 +162,12 @@ private Set getContractsOfKind( } } - // Check for type-system specific annotations. These are the annotations that are - // meta-annotated by `kind.metaAnnotation`, which is PreconditionAnnotation, - // PostconditionAnnotation, or ConditionalPostconditionAnnotation. + // Check for type-system specific annotations. List> declAnnotations = factory.getDeclAnnotationWithMetaAnnotation(executableElement, kind.metaAnnotation); for (IPair r : declAnnotations) { AnnotationMirror anno = r.first; - // contractAnno is the meta-annotation on anno, such as PreconditionAnnotation, - // PostconditionAnnotation, or ConditionalPostconditionAnnotation. + // contractAnno is the meta-annotation on anno. AnnotationMirror contractAnno = r.second; AnnotationMirror enforcedQualifier = getQualifierEnforcedByContractAnnotation(contractAnno, anno); @@ -210,8 +204,8 @@ private Set getContractsOfKind( * * @param the type of {@link Contract} to return * @param kind the kind of {@code contractAnnotation} - * @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, or {@link - * EnsuresQualifierIf} + * @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, {@link + * EnsuresQualifierIf}, or null * @param clazz the class to determine the return type * @return the contracts expressed by the given annotation, or the empty set if the argument is * null diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java index 5743e99fc85..a6de9d49c70 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypeSystemError.java @@ -4,11 +4,11 @@ import org.checkerframework.checker.nullness.qual.Nullable; /** - * Exception type indicating a mistake in a type system built using the Checker Framework. For + * Exception type indicating a mistake by a type system built using the Checker Framework. For * example, misusing a meta-annotation on a qualifier. * - *

To indicate a bug in the framework, use {@link BugInCF}. To indicate that an end user (a - * programmer running a type-checker) made a mistake, use {@link UserError}. + *

To indicate a bug in the framework, use {@link BugInCF}. To indicate that an end user made a + * mistake, use {@link UserError}. */ @SuppressWarnings("serial") public class TypeSystemError extends RuntimeException { From 84dfc628a321240e361d04538d5e53098230e145 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 30 Jan 2024 10:45:09 -0800 Subject: [PATCH 6/8] Add Javadoc --- .../checkerframework/framework/qual/PreconditionAnnotation.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java index 38b274c8996..f1cdec923b4 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java @@ -63,6 +63,8 @@ * post-condition annotation. * *

This element is analogous to {@link RequiresQualifier#qualifier()}. + * + * @return the qualifier that must be established as a precondition */ Class qualifier(); } From b6f0b7911b0dbed3ff945f29fc7e4c6202960be7 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 4 Mar 2026 07:56:29 -0800 Subject: [PATCH 7/8] Put error message key in brackets --- checker/tests/nullness/PreconditionFieldNotInStore.java | 2 +- framework/tests/flow/Postcondition.java | 4 ++-- framework/tests/flow/Precondition.java | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/checker/tests/nullness/PreconditionFieldNotInStore.java b/checker/tests/nullness/PreconditionFieldNotInStore.java index 3447cd7eb5b..2d9d2d813c2 100644 --- a/checker/tests/nullness/PreconditionFieldNotInStore.java +++ b/checker/tests/nullness/PreconditionFieldNotInStore.java @@ -11,7 +11,7 @@ class PreconditionFieldNotInStore { @org.checkerframework.framework.qual.RequiresQualifier( expression = {"this.filename"}, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] @org.checkerframework.checker.nullness.qual.NonNull String getIndentString() { return "indentString"; } diff --git a/framework/tests/flow/Postcondition.java b/framework/tests/flow/Postcondition.java index f1b6439f59e..7fff9d4c5e0 100644 --- a/framework/tests/flow/Postcondition.java +++ b/framework/tests/flow/Postcondition.java @@ -316,11 +316,11 @@ void t6(@Odd String p1, @ValueTypeAnno String p2) { /** *** errors for invalid postconditions ***** */ @EnsuresQualifier(expression = "f1", qualifier = Unqualified.class) - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] void noOpForTesting() {} @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Unqualified.class) - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] boolean isF1NotSet() { return f1 == null; } diff --git a/framework/tests/flow/Precondition.java b/framework/tests/flow/Precondition.java index 0326ea18da5..92d66754b00 100644 --- a/framework/tests/flow/Precondition.java +++ b/framework/tests/flow/Precondition.java @@ -162,6 +162,6 @@ void t5(@Odd String p1, String p2, @ValueTypeAnno String p3) { } @RequiresQualifier(expression = "f1", qualifier = Unqualified.class) - // :: warning: (contracts.toptype) + // :: warning: [contracts.toptype] void noOpForTesting() {} } From 8462ad64ee138b365fddd21e85246ee1719bb47a Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 21 May 2026 20:09:13 -0700 Subject: [PATCH 8/8] Tweak error 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 7ffad12b82a..b6debebf4f3 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 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.