Update checker-qual.jar

src/java.base/share/classes/org/checkerframework/checker/builder/qual/CalledMethods.java

@@ -21,7 +21,7 @@
   /**
    * The names of methods that have definitely been called.
    *
-   * @return the names of methods that have definetely been called
+   * @return the names of methods that have definitely been called
    */
   String[] value();
 }

src/java.base/share/classes/org/checkerframework/checker/formatter/qual/ConversionCategory.java

@@ -96,7 +96,7 @@ public enum ConversionCategory {
 
   /**
    * Use if no object of any type can be passed as parameter. In this case, the only legal value is
-   * null. This is seldomly needed, and indicates an error in most cases. For example:
+   * null. This is seldom needed, and indicates an error in most cases. For example:
    *
    * <pre>
    *   format("Test %1$f %1$d", null);
@@ -107,8 +107,8 @@ public enum ConversionCategory {
   NULL(null),
 
   /**
-   * Use if a parameter is not used by the formatter. This is seldomly needed, and indicates an
-   * error in most cases. For example:
+   * Use if a parameter is not used by the formatter. This is seldom needed, and indicates an error
+   * in most cases. For example:
    *
    * <pre>
    *   format("Test %1$s %3$s", "a","unused","b");
@@ -187,8 +187,9 @@ public enum ConversionCategory {
    * The conversion categories that have a corresponding conversion character. This lacks UNUSED,
    * TIME_AND_INT, etc.
    */
-  private static final ConversionCategory[] conversionCategoriesWithChar =
-      new ConversionCategory[] {GENERAL, CHAR, INT, FLOAT, TIME};
+  private static final ConversionCategory[] conversionCategoriesWithChar = {
+    GENERAL, CHAR, INT, FLOAT, TIME
+  };
 
   /**
    * Converts a conversion character to a category. For example:
@@ -210,6 +211,13 @@ public static ConversionCategory fromConversionChar(char c) {
     throw new IllegalArgumentException("Bad conversion character " + c);
   }
 
+  /**
+   * Converts an array to a set.
+   *
+   * @param a an array
+   * @param <E> the type of array and set elements
+   * @return a set containing the array's elements
+   */
   private static <E> Set<E> arrayToSet(E[] a) {
     return new HashSet<>(Arrays.asList(a));
   }
@@ -219,11 +227,12 @@ public static boolean isSubsetOf(ConversionCategory a, ConversionCategory b) {
   }
 
   /** Conversion categories that need to be considered by {@link #intersect}. */
-  private static final ConversionCategory[] conversionCategoriesForIntersect =
-      new ConversionCategory[] {CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL};
+  private static final ConversionCategory[] conversionCategoriesForIntersect = {
+    CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL
+  };
 
   /**
-   * Returns the intersection of two categories. This is seldomly needed.
+   * Returns the intersection of two categories. This is seldom needed.
    *
    * <blockquote>
    *
@@ -266,15 +275,16 @@ public static ConversionCategory intersect(ConversionCategory a, ConversionCateg
         return v;
       }
     }
-    throw new RuntimeException();
+    throw new RuntimeException("Could not compute intersect(" + a + ", " + b + ")");
   }
 
   /** Conversion categories that need to be considered by {@link #union}. */
-  private static final ConversionCategory[] conversionCategoriesForUnion =
-      new ConversionCategory[] {NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME};
+  private static final ConversionCategory[] conversionCategoriesForUnion = {
+    NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME
+  };
 
   /**
-   * Returns the union of two categories. This is seldomly needed.
+   * Returns the union of two categories. This is seldom needed.
    *
    * <blockquote>
    *
@@ -346,7 +356,7 @@ public boolean isAssignableFrom(Class<?> argType) {
   @Pure
   @Override
   public String toString() {
-    StringBuilder sb = new StringBuilder();
+    StringBuilder sb = new StringBuilder(32);
     sb.append(name());
     sb.append(" conversion category");
 
@@ -358,7 +368,7 @@ public String toString() {
     for (Class<?> cls : types) {
       sj.add(cls.getSimpleName());
     }
-    sb.append(" ");
+    sb.append(' ');
     sb.append(sj);
 
     return sb.toString();

src/java.base/share/classes/org/checkerframework/checker/formatter/qual/FormatBottom.java

@@ -21,5 +21,5 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @SubtypeOf({Format.class, InvalidFormat.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface FormatBottom {}

src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java

@@ -64,8 +64,7 @@ public enum I18nConversionCategory {
   }
 
   /** Used by {@link #stringToI18nConversionCategory}. */
-  private static final I18nConversionCategory[] namedCategories =
-      new I18nConversionCategory[] {DATE, NUMBER};
+  private static final I18nConversionCategory[] namedCategories = {DATE, NUMBER};
 
   /**
    * Creates a conversion cagetogry from a string name.
@@ -90,6 +89,13 @@ public static I18nConversionCategory stringToI18nConversionCategory(String strin
     throw new IllegalArgumentException("Invalid format type " + string);
   }
 
+  /**
+   * Converts an array to a set.
+   *
+   * @param a an array
+   * @param <E> the type of array and set elements
+   * @return a set containing the array's elements
+   */
   private static <E> Set<E> arrayToSet(E[] a) {
     return new HashSet<>(Arrays.asList(a));
   }
@@ -104,8 +110,7 @@ public static boolean isSubsetOf(I18nConversionCategory a, I18nConversionCategor
   }
 
   /** Conversion categories that need to be considered by {@link #intersect}. */
-  private static final I18nConversionCategory[] conversionCategoriesForIntersect =
-      new I18nConversionCategory[] {DATE, NUMBER};
+  private static final I18nConversionCategory[] conversionCategoriesForIntersect = {DATE, NUMBER};
 
   /**
    * Returns the intersection of the two given I18nConversionCategories.
@@ -147,7 +152,7 @@ public static I18nConversionCategory intersect(
         return v;
       }
     }
-    throw new RuntimeException();
+    throw new RuntimeException("Could not compute intersect(" + a + ", " + b + ")");
   }
 
   /**

src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nFormatBottom.java

@@ -22,5 +22,5 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @SubtypeOf({I18nFormat.class, I18nInvalidFormat.class, I18nFormatFor.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface I18nFormatBottom {}

src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java

@@ -33,6 +33,11 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 public @interface IndexOrHigh {
-  /** The annotated expression is a valid index for, or is equal to the length of, each sequence. */
+  /**
+   * The annotated expression is a valid index for, or is equal to the length of, each sequence.
+   *
+   * @return sequences that the annotated expression is a valid index for or is equal to the length
+   *     of
+   */
   String[] value();
 }

src/java.base/share/classes/org/checkerframework/checker/index/qual/LengthOf.java

@@ -13,7 +13,7 @@
  * detail that may change in the future, when this type may be used to implement more precise
  * refinements.
  *
- * <p>The usual use case for the {@code LengthOf} annotation is in the defintions of custom
+ * <p>The usual use case for the {@code LengthOf} annotation is in the definitions of custom
  * collections. Consider the signature of java.lang.String#length():
  *
  * <pre>

src/java.base/share/classes/org/checkerframework/checker/interning/qual/InternedDistinct.java

@@ -25,5 +25,5 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf(Interned.class)
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface InternedDistinct {}

src/java.base/share/classes/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java

@@ -71,7 +71,7 @@
   /**
    * A wrapper annotation that makes the {@link EnsuresNonEmptyIf} annotation repeatable.
    *
-   * <p>Programmers generally do not need to write ths. It is created by Java when a programmer
+   * <p>Programmers generally do not need to write this. It is created by Java when a programmer
    * writes more than one {@link EnsuresNonEmptyIf} annotation at the same location.
    */
   @Retention(RetentionPolicy.RUNTIME)

src/java.base/share/classes/org/checkerframework/checker/optional/qual/RequiresPresent.java

@@ -63,7 +63,7 @@
 public @interface RequiresPresent {
 
   /**
-   * The Java expressions that that need to be {@link Present}.
+   * The Java expressions that need to be {@link Present}.
    *
    * @return the Java expressions that need to be {@link Present}
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions

src/java.base/share/classes/org/checkerframework/checker/regex/qual/RegexBottom.java

@@ -23,5 +23,5 @@
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @InvisibleQualifier
 @SubtypeOf({Regex.class, PartialRegex.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface RegexBottom {}

src/java.base/share/classes/org/checkerframework/checker/signature/qual/BinaryName.java

@@ -9,7 +9,7 @@
 
 /**
  * Represents a binary name as defined in the <a
- * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">Java Language
+ * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">Java Language
  * Specification, section 13.1</a>.
  *
  * <p>For example, in

src/java.base/share/classes/org/checkerframework/checker/signature/qual/CanonicalName.java

@@ -12,11 +12,10 @@
  * Every canonical name is a fully-qualified name, but not every fully-qualified name is a canonical
  * name.
  *
- * <p><a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-6.html#jls-6.7">JLS section
+ * <p><a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-6.html#jls-6.7">JLS section
  * 6.7</a> gives the following example:
  *
  * <blockquote>
- *
  * The difference between a fully qualified name and a canonical name can be seen in code such as:
  *
  * <pre>{@code
@@ -27,7 +26,6 @@
  *
  * Both {@code p.O1.I} and {@code p.O2.I} are fully qualified names that denote the member class
  * {@code I}, but only {@code p.O1.I} is its canonical name.
- *
  * </blockquote>
  *
  * Given a character sequence that is a fully-qualified name, there is no way to know whether or not

src/java.base/share/classes/org/checkerframework/checker/signature/qual/FullyQualifiedName.java

@@ -10,7 +10,7 @@
 /**
  * A sequence of dot-separated identifiers, followed by any number of array square brackets.
  * Represents a fully-qualified name as defined in the <a
- * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-6.html#jls-6.7">Java Language
+ * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-6.html#jls-6.7">Java Language
  * Specification, section 6.7</a>.
  *
  * <p>Examples:

src/java.base/share/classes/org/checkerframework/checker/sqlquotes/qual/SqlQuotesBottom.java

@@ -23,5 +23,5 @@
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @InvisibleQualifier
 @SubtypeOf({SqlEvenQuotes.class, SqlOddQuotes.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface SqlQuotesBottom {}

src/java.base/share/classes/org/checkerframework/common/aliasing/qual/NonLeaked.java

@@ -21,7 +21,7 @@
  */
 
 // This is a type qualifier because of a Checker Framework limitation (Issue 383), but its hierarchy
-// is ignored. Once the stub parser gets updated to read non-type-qualifiers annotations on stub
+// is ignored. Once the stub parser gets updated to store non-type-qualifier annotations from stub
 // files, this annotation won't be a type qualifier anymore.
 
 @Documented

src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassBound.java

@@ -19,7 +19,7 @@
 @SubtypeOf({UnknownClass.class})
 public @interface ClassBound {
   /**
-   * The <a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary
+   * The <a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary
    * name</a> of the class or classes that upper-bound the values of this Class object.
    */
   String[] value();

src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassVal.java

@@ -22,7 +22,7 @@
   /**
    * The name of the type that this Class object represents. The name is a "fully-qualified binary
    * name" ({@link org.checkerframework.checker.signature.qual.FqBinaryName}): a primitive or <a
-   * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary name</a>,
+   * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary name</a>,
    * possibly followed by some number of array brackets.
    *
    * @return the name of the type that this Class object represents

src/java.base/share/classes/org/checkerframework/common/reflection/qual/MethodVal.java

@@ -24,7 +24,7 @@
 @SubtypeOf({UnknownMethod.class})
 public @interface MethodVal {
   /**
-   * The <a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary
+   * The <a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary
    * name</a> of the class that declares this method.
    */
   String[] className();

src/java.base/share/classes/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java

@@ -23,6 +23,6 @@
 @SubtypeOf({})
 @DefaultQualifierInHierarchy
 @QualifierForLiterals(LiteralKind.NULL)
-@DefaultFor(value = TypeUseLocation.LOWER_BOUND)
+@DefaultFor(TypeUseLocation.LOWER_BOUND)
 @InvisibleQualifier
 public @interface UnknownThis {}

src/java.base/share/classes/org/checkerframework/dataflow/qual/Pure.java

@@ -25,13 +25,4 @@
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
-public @interface Pure {
-  /** The type of purity. */
-  public static enum Kind {
-    /** The method has no visible side effects. */
-    SIDE_EFFECT_FREE,
-
-    /** The method returns exactly the same value when called in the same environment. */
-    DETERMINISTIC
-  }
-}
+public @interface Pure {}

src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectFree.java

@@ -12,8 +12,8 @@
  *
  * <p>Only the visible side effects are important. The method is allowed to cache the answer to a
  * computationally expensive query, for instance. It is also allowed to modify newly-created
- * objects, and a constructor is side-effect-free if it does not modify any objects that existed
- * before it was called.
+ * objects. A constructor is side-effect-free if it does not modify any objects that existed before
+ * it was called in ways that are externally visible.
  *
  * <p>This annotation is important to pluggable type-checking because if some fact about an object
  * is known before a call to such a method, then the fact is still known afterwards, even if the

src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectsOnly.java

@@ -8,22 +8,44 @@
 import org.checkerframework.framework.qual.JavaExpression;
 
 /**
- * A method annotated with the declaration annotation {@code @SideEffectsOnly("A", "B")} changes the
- * value of at most the expressions A and B. All other expressions have the same value before and
- * after a call to the method.
+ * A method annotated with the declaration annotation {@code @SideEffectsOnly({"A", "B"})} changes
+ * the value of at most the expressions A and B. No other expression is directly modified by the
+ * method. Absent aliasing, no other expression has a different value after a call to the method.
+ * But checking of this annotation (under {@code -AcheckPurityAnnotations}) treats two expressions
+ * as possibly aliased only when an assignment relating them appears in the method body.
  *
- * @checker_framework.manual #type-refinement-purity Specifying side effects
+ * <p>This annotation is inherited by subtypes, just as if it were meta-annotated with
+ * {@code @InheritedAnnotation}.
+ *
+ * <p>On a constructor, this annotation constrains what the constructor modifies besides the object
+ * being constructed. Assigning to the new object's own fields is always permitted and need not be
+ * listed, because the object did not exist before the call; writing {@code this} in the annotation
+ * is legal but has no additional effect. At a {@code new} expression, the expressions that are
+ * reached through {@code this} are ignored, because the object being constructed did not exist
+ * before the call. A constructor's annotation does not yet affect type refinement at {@code new}
+ * expressions.
+ *
+ * @checker_framework.manual #side-effects-only-checking Checking {@code @SideEffectsOnly}
  */
+// @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on
+// "framework" project.
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface SideEffectsOnly {
   /**
    * An upper bound on the expressions that this method might change the value of.
    *
+   * <p>Each expression must denote the same location every time it is evaluated: it must be a
+   * variable, a field access, an array access, a literal, a class name, or a call to a {@link Pure}
+   * method, recursively. A {@code @Pure} method returns the same value every time it is called with
+   * the same arguments, so a call to one qualifies so long as its receiver and its arguments do. An
+   * expression such as {@code "#1.getList()"}, where {@code getList} is not {@code @Pure}, may
+   * denote a different value each time it is evaluated, so no method body could satisfy it.
+   *
    * @return the Java expressions that the annotated method might side-effect
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
   @JavaExpression
-  public String[] value();
+  String[] value();
 }