diff --git a/checker/tests/nullness/flow/PurityError.java b/checker/tests/nullness/flow/VoidMethodIsDeterministic.java similarity index 73% rename from checker/tests/nullness/flow/PurityError.java rename to checker/tests/nullness/flow/VoidMethodIsDeterministic.java index 61819c9a8ebc..62b20f0b0ec3 100644 --- a/checker/tests/nullness/flow/PurityError.java +++ b/checker/tests/nullness/flow/VoidMethodIsDeterministic.java @@ -1,13 +1,12 @@ import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; -public class PurityError { +public class VoidMethodIsDeterministic { @SideEffectFree void method() {} @Pure Object method2() { - // :: error: [purity.not.deterministic.call] method(); return ""; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java index f6ebe763de54..94be3589dcfe 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -20,6 +20,7 @@ import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; import org.checkerframework.dataflow.qual.Deterministic; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; @@ -260,7 +261,10 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void ignore) { // Avoid computation if not necessary ? detAndSeFree : PurityUtils.getPurityKinds(annoProvider, elt); - boolean det = assumeDeterministic || purityKinds.contains(Pure.Kind.DETERMINISTIC); + boolean det = + assumeDeterministic + || purityKinds.contains(Pure.Kind.DETERMINISTIC) + || elt.getReturnType().getKind() == TypeKind.VOID; boolean seFree = assumeSideEffectFree || purityKinds.contains(Pure.Kind.SIDE_EFFECT_FREE); if (!det && !seFree) { purityResult.addNotBothReason(tree, "call"); 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 adddb59542d5..6e404219653f 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -63,8 +63,8 @@ unallowed.access=access of the field (%s) is not permitted on receiver of type ( cast.redundant=Redundant cast;%ntype : %s # TODO: The call.{constructor,method} messages should take an argument indicating which method or constructor is the problem -purity.deterministic.constructor=a constructor cannot be deterministic -purity.deterministic.void.method=a method without return value cannot be deterministic +purity.deterministic.constructor=a constructor cannot be annotated @Deterministic +purity.deterministic.void.method=a method without return value cannot be annotated @Deterministic purity.methodref=Incompatible purity declaration%nMethod in %s%n %s%n is not a valid method reference for method in %s%n %s%nfound : %s%nrequired: %s purity.overriding=Incompatible purity declaration%nMethod in %s%n %s%n cannot override method in %s%n %s%nfound : %s%nrequired: %s purity.not.deterministic.assign.array=array assignment not allowed in deterministic method diff --git a/framework/tests/purity-suggestions/SideEffectFreeVoidMethod.java b/framework/tests/purity-suggestions/SideEffectFreeVoidMethod.java new file mode 100644 index 000000000000..ce75fd71deef --- /dev/null +++ b/framework/tests/purity-suggestions/SideEffectFreeVoidMethod.java @@ -0,0 +1,21 @@ +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +public class SideEffectFreeVoidMethod { + + int size; + + @Pure + private int getOrNull(int index) { + assertIndexInBounds(index, "getOrNull"); + return 22; + } + + @SideEffectFree + private void assertIndexInBounds(int index, String method) { + if (index < 0 || index >= size) { + throw new IndexOutOfBoundsException( + method + "(" + index + ",...) called on ArrayMap of size " + size); + } + } +} diff --git a/release.gradle b/release.gradle index fd518862afb3..7f45d1baebfd 100644 --- a/release.gradle +++ b/release.gradle @@ -9,7 +9,7 @@ ext { // * any new checkers have been added, or // * backward-incompatible changes have been made to APIs or elsewhere. // To make a snapshot release, version should end in "-SNAPSHOT", then: ./gradlew publish - releaseVersion = "4.1.0" + releaseVersion = "4.1.1-SNAPSHOT" releaseVersionRegex = "\\d\\.\\d+\\.\\d+(?:\\.\\d)?"