diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 8edd25a668df..99f297c1c428 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -510,14 +510,15 @@ public static SideEffectAnnotation weakest() { } /** - * Indicates which side effect annotation is present on the given method. If more than one - * annotation is present, this method issues an error (if issueErrorIfMoreThanOnePresent is true) - * and returns the annotation providing the weakest guarantee. Only call with - * issueErrorIfMoreThanOnePresent == true when visiting a method definition. This prevents - * multiple errors being issued for the same method (as would occur if - * issueErrorIfMoreThanOnePresent were set to true when visiting method invocations). If no - * annotation is present, return RELEASESNOLOCKS as the default, and MAYRELEASELOCKS as the - * conservative default. + * Indicates which side effect annotation is present on the given method. Returns LOCKINGFREE + * rather than PURE or SIDEEFFECTFREE. If no annotation is present, returns RELEASESNOLOCKS as the + * default, and MAYRELEASELOCKS as the conservative default. + * + *

If more than one annotation is present, this method issues an error (if + * issueErrorIfMoreThanOnePresent is true) and returns the annotation providing the weakest + * guarantee. Only call with issueErrorIfMoreThanOnePresent == true when visiting a method + * definition. This prevents multiple errors being issued for the same method (as would occur if + * issueErrorIfMoreThanOnePresent were set to true when visiting method invocations). * * @param methodElement the method element * @param issueErrorIfMoreThanOnePresent if true, issue an error if more than one side effect @@ -536,6 +537,9 @@ public static SideEffectAnnotation weakest() { EnumSet.noneOf(SideEffectAnnotation.class); for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { if (getDeclAnnotationNoAliases(methodElement, sea.getAnnotationClass()) != null) { + if (sea == SideEffectAnnotation.PURE || sea == SideEffectAnnotation.SIDEEFFECTFREE) { + sea = SideEffectAnnotation.LOCKINGFREE; + } sideEffectAnnotationPresent.add(sea); } } @@ -548,7 +552,12 @@ public static SideEffectAnnotation weakest() { : SideEffectAnnotation.RELEASESNOLOCKS; } - if (count > 1 && issueErrorIfMoreThanOnePresent) { + if (count == 1) { + return sideEffectAnnotationPresent.iterator().next(); + } + // count > 1 + + if (issueErrorIfMoreThanOnePresent) { // TODO: Turn on after figuring out how this interacts with inherited annotations. // checker.reportError(methodElement, "multiple.sideeffect.annotations"); } 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 d34a783dec2d..1d4979cce97c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1447,12 +1447,14 @@ private void reportPurityError(String msgKeyPrefix, IPair r) { @SuppressWarnings("compilermessages") @CompilerMessageKey String msgKey = msgKeyPrefix + reason; if (reason.equals("call")) { + ExecutableElement calleeElement; if (r.first instanceof MethodInvocationTree mitree) { - checker.reportError(r.first, msgKey, mitree.getMethodSelect()); + calleeElement = TreeUtils.elementFromUse(mitree); } else { - NewClassTree nctree = (NewClassTree) r.first; - checker.reportError(r.first, msgKey, nctree.getIdentifier()); + calleeElement = TreeUtils.elementFromUse((NewClassTree) r.first); } + checker.reportError( + r.first, msgKey, calleeElement.getEnclosingElement(), calleeElement.getSimpleName()); } else { checker.reportError(r.first, msgKey); } 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 681dc1eba032..5f268f925004 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -68,15 +68,15 @@ purity.methodref=Incompatible purity declaration%nMethod in %s%n %s %s%n is no purity.overriding=Incompatible purity declaration%nMethod in %s%n %s %s%ncannot override method in %s%n %s %s purity.not.deterministic.assign.array=array assignment not allowed in deterministic method purity.not.deterministic.assign.field=field assignment not allowed in deterministic method -purity.not.deterministic.call=call to non-deterministic method %s not allowed in deterministic method +purity.not.deterministic.call=call to non-deterministic %s::%s not allowed in deterministic method purity.not.deterministic.catch=catch block not allowed in deterministic method purity.not.deterministic.object.creation=object creation not allowed in deterministic method purity.not.deterministic.not.sideeffectfree.assign.array=array assignment not allowed in deterministic side-effect-free method purity.not.deterministic.not.sideeffectfree.assign.field=field assignment not allowed in deterministic side-effect-free method -purity.not.deterministic.not.sideeffectfree.call=call to non-deterministic side-effecting %s not allowed in deterministic side-effect-free method +purity.not.deterministic.not.sideeffectfree.call=call to non-deterministic side-effecting %s::%s not allowed in deterministic side-effect-free method purity.not.sideeffectfree.assign.array=array assignment not allowed in side-effect-free method purity.not.sideeffectfree.assign.field=field assignment not allowed in side-effect-free method -purity.not.sideeffectfree.call=call to side-effecting %s not allowed in side-effect-free method +purity.not.sideeffectfree.call=call to side-effecting %s::%s not allowed in side-effect-free method purity.more.deterministic=the method %s could be declared as @Deterministic purity.more.pure=the method %s could be declared as @Pure purity.more.sideeffectfree=the method %s could be declared as @SideEffectFree diff --git a/framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java b/framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java index 90b4353e0354..f679bf572db1 100644 --- a/framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java +++ b/framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java @@ -54,6 +54,7 @@ import org.checkerframework.checker.regex.qual.Regex; import org.checkerframework.checker.signature.qual.DotSeparatedIdentifiers; import org.checkerframework.checker.signature.qual.FullyQualifiedName; +import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.stub.AnnotationFileParser; import org.checkerframework.framework.util.JavaParserUtil; import org.checkerframework.framework.util.StaticJavaParserUtil; @@ -520,6 +521,7 @@ public String insertAnnotations( * @return a negative integer, zero, or a positive integer if {@code insertion1} belongs before, * at the same position, or after {@code insertion2} respectively in the above ordering */ + @Pure private static int compareInsertions(Insertion insertion1, Insertion insertion2) { int cmp = Integer.compare(insertion1.position, insertion2.position); if (cmp == 0 && (insertion1.ownLine != insertion2.ownLine)) { diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 89899771db89..8dba22ce3539 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -396,6 +396,7 @@ public static boolean containsSameByName( * @param a2 the second annotation * @return an ordering over AnnotationMirrors based on their name and values */ + @Pure public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror a2) { int nameComparison = compareByName(a1, a2); if (nameComparison != 0) {