typetools/checker-framework 3.38.0 release (#601)

.editorconfig

@@ -32,11 +32,13 @@ ij_any_spaces_around_logical_operators = true
 ij_any_spaces_around_multiplicative_operators = true
 ij_any_spaces_around_relational_operators = true
 ij_any_spaces_around_shift_operators = true
+ij_java_align_multiline_parameters = false
 ij_java_if_brace_force = always
 ij_java_indent_case_from_switch = true
+ij_java_names_count_to_use_import_on_demand = 9999
+ij_java_class_count_to_use_import_on_demand = 9999
 ij_java_space_after_colon = true
 ij_java_space_before_colon = true
 ij_java_ternary_operation_signs_on_next_line = true
 ij_java_use_single_class_imports = true
 ij_java_wrap_long_lines = true
-ij_java_align_multiline_parameters = false

azure-pipelines.yml

@@ -342,6 +342,7 @@ jobs:
   container: wmdietl/cf-ubuntu-jdk11-plus:latest
   steps:
   - checkout: self
+    fetchDepth: 25
   - bash: ./checker/bin-devel/test-misc.sh
     displayName: test-misc.sh
 - job: misc_jdk17
@@ -350,6 +351,7 @@ jobs:
   container: wmdietl/cf-ubuntu-jdk17-plus:latest
   steps:
   - checkout: self
+    fetchDepth: 25
   - bash: ./checker/bin-devel/test-misc.sh
     displayName: test-misc.sh
 - job: misc_jdk_latest
@@ -361,6 +363,7 @@ jobs:
   container: wmdietl/cf-ubuntu-jdk-latest-plus:latest
   steps:
   - checkout: self
+    fetchDepth: 25
   - bash: ./checker/bin-devel/test-misc.sh
     displayName: test-misc.sh
 - job: misc_jdk_next

build.gradle

@@ -70,7 +70,7 @@ ext {
     // afu = "${annotationTools}/annotation-file-utilities"
 
     stubparser = "${parentDir}/stubparser"
-    stubparserVersion = "3.25.3"
+    stubparserVersion = "3.25.5"
     stubparserJar = "${stubparser}/javaparser-core/target/stubparser-${stubparserVersion}.jar"
 
     jtregHome = "${parentDir}/jtreg"
@@ -163,7 +163,7 @@ allprojects {
     //   * any new checkers have been added, or
     //   * backward-incompatible changes have been made to APIs or elsewhere.
     // To make a snapshot release: ./gradlew publish
-    version '3.37.0'
+    version '3.38.0'
 
     tasks.withType(JavaCompile).configureEach {
         options.fork = true
@@ -252,6 +252,7 @@ allprojects {
             // If you add any formatters to this block that require dependencies, then you must also
             // add them to spotlessPredeclare block.
             def doNotFormat = [
+                'checker/bin-devel/.plume-scripts/**',
                 'checker/tests/ainfer-*/annotated/*',
                 'dataflow/manual/examples/',
                 '**/nullness-javac-errors/*',

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java

@@ -13,7 +13,10 @@
 
 /**
  * Indicates that the method, if it terminates successfully, always invokes the given methods on the
- * given expressions. This annotation is repeatable.
+ * given expressions. This annotation is repeatable, which means that users can write more than one
+ * instance of it on the same method (users should NOT manually write an
+ * {@code @EnsuresCalledMethods.List} annotation, which the checker will create from multiple copies
+ * of this annotation automatically).
  *
  * <p>Consider the following method:
  *
@@ -61,10 +64,10 @@
     String[] methods();
 
     /**
-     * A wrapper annotation that makes the {@link EnsuresCalledMethods} annotation repeatable.
-     *
-     * <p>Programmers generally do not need to write this. It is created by Java when a programmer
-     * writes more than one {@link EnsuresCalledMethods} annotation at the same location.
+     * A wrapper annotation that makes the {@link EnsuresCalledMethods} annotation repeatable. This
+     * annotation is an implementation detail: programmers generally do not need to write this. It
+     * is created automatically by Java when a programmer writes more than one {@link
+     * EnsuresCalledMethods} annotation at the same location.
      */
     @Documented
     @Retention(RetentionPolicy.RUNTIME)

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java

@@ -1,23 +1,22 @@
 package org.checkerframework.checker.signedness.qual;
 
+import org.checkerframework.framework.qual.SubtypeOf;
+
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
 /**
- * The expression's value is in the signed positive range; that is, its most significant bit is not
- * set. The value has the same interpretation as {@code @}{@link Signed} and {@code @}{@link
+ * The expression's value is in the signed positive range; that is, its most significant bit is
+ * zero. The value has the same interpretation as {@code @}{@link Signed} and {@code @}{@link
  * Unsigned} — both interpretations are equivalent.
  *
  * <p>Programmers should rarely write {@code @SignedPositive}. Instead, the programmer should write
  * {@code @}{@link Signed} or {@code @}{@link Unsigned} to indicate how the programmer intends the
  * value to be interpreted.
  *
- * <p>Internally, this is translated to the {@code @}{@link SignednessGlb} annotation. This means
- * that programmers do not see this annotation in error messages.
- *
  * <p>{@code @SignedPositive} corresponds to {@code @}{@link
  * org.checkerframework.checker.index.qual.NonNegative NonNegative} in the Index Checker's type
  * system.
@@ -28,4 +27,5 @@
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(SignednessGlb.class)
 public @interface SignedPositive {}

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java

@@ -25,5 +25,5 @@
     TypeUseLocation.LOWER_BOUND,
     TypeUseLocation.UPPER_BOUND,
 })
-@SubtypeOf({SignedPositiveFromUnsigned.class})
+@SubtypeOf({SignedPositive.class})
 public @interface SignednessBottom {}

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java

@@ -1,7 +1,5 @@
 package org.checkerframework.checker.signedness.qual;
 
-import org.checkerframework.framework.qual.LiteralKind;
-import org.checkerframework.framework.qual.QualifierForLiterals;
 import org.checkerframework.framework.qual.SubtypeOf;
 
 import java.lang.annotation.Documented;
@@ -39,5 +37,4 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf({Unsigned.class, Signed.class})
-@QualifierForLiterals({LiteralKind.INT, LiteralKind.LONG, LiteralKind.CHAR})
 public @interface SignednessGlb {}

checker/bin-devel/count-suppressions → checker/bin-devel/count-suppression-reasons

@@ -3,7 +3,7 @@
 # This command counts the approximate frequency of each distinct reason for
 # warning suppressions, in all files under the current directory.
 # To invoke it, pass a type system name; for example:
-#   count-suppressions nullness
+#   count-suppression-reasons nullness
 # The argument to this script is actually a regular expression.
 
 # The "reason" for a warning suppression is the Java line comment after it:
@@ -62,19 +62,19 @@ fi
 # Diagnostics
 # echo "regex=${regex}"
 
-greplines=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
-countedreasons=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
+greplines=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
+countedreasons=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
 
 # These are the two types of matching lines:
 #  * "checkername" or "chekername:..."
 #    This matches occurrences within @SuppressWarnings.  The regex does not
 #    include "@SuppressWarnings" because it might appear on the previous line.
 #  * @AssumeAssertion(checkername)
 # This grep command captures a few stray lines; users should ignore them.
-# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppressions-ignore".
+# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppression-reasons-ignore".
 ${GREP} -n --recursive --include='*.java' "\"${regex}[:\"]\(.*[^;]\)\?\(\$\|//\)\|@AssumeAssertion(${regex})" \
     | grep -v "@AnnotatedFor" | grep -v "/tests/" \
-    | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppressions-ignore" > "${greplines}"
+    | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppression-reasons-ignore" > "${greplines}"
 
 total=$(wc -l < "${greplines}")
 ## Don't output a total, to avoid people using this approximate count.
@@ -87,7 +87,7 @@ cat "${greplines}" \
     | ${SED} 's/ \+$//' \
     | sort | uniq -c | sort -rg > "${countedreasons}"
 
-# Add leading percentages to `uniq -c` output.  Note that it rounds down to the nearest integer.
+# Add leading percentages to `uniq -c` output.  Note that it rounds *down* to the nearest integer.
 # (Digits afert the decimal don't make a practical difference.)
 while read -r line; do
     count=$(echo "$line" | cut -f1 -d " ");

checker/bin/query-github.sh

@@ -11,8 +11,8 @@
 # $1 is the query file, which should contain the literal string to use
 # as the github search. REQUIRED, no default.
 #
-# $2 is the number of GitHub search pages.  Default 1. Each page contains 10 results.  GitHub only returns
-# the first 1000 results, so 100 is the maximum useful number of search pages.
+# $2 is the number of GitHub search pages.  Default 1. Each page contains 10 results.  GitHub only
+# returns the first 1000 results, so 100 is the maximum useful number of search pages.
 #
 # This script outputs a list of projects. The underlying GitHub search is for code snippets, and this
 # script eliminates duplicates (i.e. different code snippets from the same project are combined into

checker/src/main/java/org/checkerframework/checker/calledmethods/builder/BuilderFrameworkSupport.java

@@ -20,7 +20,7 @@
 public interface BuilderFrameworkSupport {
 
     /**
-     * Determines if a method is a {@code toBuilder} method on a type generated by the builder
+     * Returns true if a method is a {@code toBuilder} method on a type generated by the builder
      * framework.
      *
      * @param candidateToBuilderElement a method
@@ -42,7 +42,7 @@ public interface BuilderFrameworkSupport {
     void handleToBuilderMethod(AnnotatedExecutableType toBuilderType);
 
     /**
-     * Determines if a method is a {@code build} method on a {@code Builder} type for the builder
+     * Returns true if a method is a {@code build} method on a {@code Builder} type for the builder
      * framework.
      *
      * @param candidateBuildElement a method

checker/src/main/java/org/checkerframework/checker/index/IndexUtil.java

@@ -15,7 +15,18 @@
 
 /** A collection of utility functions used by several Index Checker subcheckers. */
 public class IndexUtil {
-    /** Determines whether the type is a sequence supported by this checker. */
+
+    /** Do not instantiate IndexUtil. */
+    private IndexUtil() {
+        throw new Error("Do not instantiate IndexUtil.");
+    }
+
+    /**
+     * Returns true if the type is a sequence supported by this checker.
+     *
+     * @param type a type
+     * @return true if the type is a sequence supported by this checker
+     */
     public static boolean isSequenceType(TypeMirror type) {
         return type.getKind() == TypeKind.ARRAY || TypesUtils.isString(type);
     }

checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java

@@ -937,7 +937,7 @@ private boolean classIsAnnotated(AnnotatedTypeMirror type) {
     }
 
     /**
-     * Determines whether or not the given element overrides the named method in the named class.
+     * Returns true if the given element overrides the named method in the named class.
      *
      * @param e an element for a method
      * @param clazz the class

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java

@@ -863,9 +863,9 @@ private void updateObligationsWithInvocationResult(Set<Obligation> obligations,
     }
 
     /**
-     * Determines if the result of the given method or constructor invocation node should be tracked
-     * in {@code obligations}. In some cases, there is no need to track the result because the
-     * must-call obligations are already satisfied in some other way or there cannot possibly be
+     * Returns true if the result of the given method or constructor invocation node should be
+     * tracked in {@code obligations}. In some cases, there is no need to track the result because
+     * the must-call obligations are already satisfied in some other way or there cannot possibly be
      * must-call obligations because of the structure of the code.
      *
      * <p>Specifically, an invocation result does NOT need to be tracked if any of the following is
@@ -1505,12 +1505,17 @@ && varTrackedInObligations(obligations, (LocalVariableNode) receiver))
         AccumulationStore cmStoreBefore = typeFactory.getStoreBefore(rhs);
         AccumulationValue cmValue = cmStoreBefore == null ? null : cmStoreBefore.getValue(lhs);
         AnnotationMirror cmAnno = null;
-        if (cmValue != null) {
-            for (AnnotationMirror anno : cmValue.getAnnotations()) {
-                if (AnnotationUtils.areSameByName(
-                        anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) {
-                    cmAnno = anno;
-                    break;
+        if (cmValue != null) { // When store contains the lhs
+            Set<String> accumulatedValues = cmValue.getAccumulatedValues();
+            if (accumulatedValues != null) { // type variable or wildcard type
+                cmAnno = typeFactory.createCalledMethods(accumulatedValues.toArray(new String[0]));
+            } else {
+                for (AnnotationMirror anno : cmValue.getAnnotations()) {
+                    if (AnnotationUtils.areSameByName(
+                            anno,
+                            "org.checkerframework.checker.calledmethods.qual.CalledMethods")) {
+                        cmAnno = anno;
+                    }
                 }
             }
         }