Treat void methods as deterministic

checker/tests/nullness/flow/PurityError.java → 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 "";
   }

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");

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

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);
+    }
+  }
+}

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)?"