Update jdk-21 from typetools/jdk up to the Checker Framework 3.55.0 release

src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java

@@ -6,6 +6,7 @@
 import org.checkerframework.framework.qual.TypeUseLocation;
 
 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;
@@ -21,7 +22,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({}) // empty target prevents programmers from writing this in a program
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf({FenumTop.class})
 @DefaultQualifierInHierarchy
 @DefaultFor(TypeUseLocation.EXCEPTION_PARAMETER)

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

@@ -20,7 +20,7 @@
  * <pre>
  * {@literal @}Format({GENERAL, INT}) String f = "String '%s' has length %d";
  *
- *  String.format(f, "Example", 7);
+ * String.format(f, "Example", 7);
  * </pre>
  *
  * </blockquote>

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

@@ -14,7 +14,7 @@
  * different lengths.
  *
  * <p>The <a
- * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/String.html#charAt(int)">
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#charAt(int)">
  * {@code String.charAt(int)}</a> method is declared as
  *
  * <pre>{@code

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

@@ -11,7 +11,7 @@
  * sequence's length.
  *
  * <p>The <a
- * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Arrays.html#binarySearch(java.lang.Object%5B%5D,int,int,java.lang.Object)">
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/util/Arrays.html#binarySearch(java.lang.Object%5B%5D,int,int,java.lang.Object)">
  * {@code Arrays.binarySearch}</a> method is declared as
  *
  * <pre>{@code
@@ -34,7 +34,10 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 public @interface IndexOrHigh {
     /**
-     * Sequences that the annotated expression is a valid index for or is equal to the lengeth of.
+     * Sequences that the annotated expression is a valid index for or is equal to the length of.
+     *
+     * @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/IndexOrLow.java

@@ -10,13 +10,13 @@
  * An integer that is either -1 or is a valid index for each of the given sequences.
  *
  * <p>The <a
- * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/String.html#indexOf(java.lang.String)">
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#indexOf(java.lang.String)">
  * {@code String.indexOf(String)}</a> method is declared as
  *
  * <pre><code>
- *   class String {
+ *  class String {
  *    {@literal @}IndexOrLow("this") int indexOf(String str) { ... }
- *   }
+ *  }
  * </code></pre>
  *
  * <p>Writing {@code @IndexOrLow("arr")} is equivalent to writing {@link

src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java

@@ -4,6 +4,7 @@
 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;
@@ -20,7 +21,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf(LockPossiblyHeld.class) // This is the bottom type in this hierarchy
 @InvisibleQualifier
 public @interface LockHeld {}

src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java

@@ -10,6 +10,7 @@
 import org.checkerframework.framework.qual.TypeUseLocation;
 
 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;
@@ -25,7 +26,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @InvisibleQualifier
 @SubtypeOf({})
 @DefaultQualifierInHierarchy

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

@@ -19,19 +19,19 @@
  * effect:
  *
  * <pre><code>
- *   {@literal @}EnsuresNonEmpty("ids")
- *   void addId(String id) {
- *     ids.add(id);
- *   }
+ *  {@literal @}EnsuresNonEmpty("ids")
+ *  void addId(String id) {
+ *    ids.add(id);
+ *  }
  * </code></pre>
  *
  * It can also be used for a method that fails if a given value is empty, indicating that the
  * argument is non-empty if the method returns normally:
  *
  * <pre><code>
- *   /** Throws an exception if the argument is empty. *&#47;
- *   {@literal @}EnsuresNonEmpty("#1")
- *   void useTheMap(Map&lt;T, U&gt; arg) { ... }
+ *  /** Throws an exception if the argument is empty. *&#47;
+ *  {@literal @}EnsuresNonEmpty("#1")
+ *  void useTheMap(Map&lt;T, U&gt; arg) { ... }
  * </code></pre>
  *
  * @see NonEmpty

src/java.base/share/classes/org/checkerframework/checker/nullness/qual/AssertNonNullIfNonNull.java

@@ -15,11 +15,11 @@
  * <p>Here is an example use:
  *
  * <pre><code>
- *    {@literal @}AssertNonNullIfNonNull("id")
- *    {@literal @}Pure
- *     public @Nullable Long getId() {
- *         return id;
- *     }
+ *  {@literal @}AssertNonNullIfNonNull("id")
+ *  {@literal @}Pure
+ *  public @Nullable Long getId() {
+ *    return id;
+ *  }
  * </code></pre>
  *
  * Note the direction of the implication. This annotation says that if the result is non-null, then

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

@@ -16,19 +16,19 @@
  * <p>This postcondition annotation is useful for methods that construct a present Optional:
  *
  * <pre><code>
- *   {@literal @}EnsuresPresent("optStr")
- *   void initialize() {
- *     optStr = Optional.of("abc");
- *   }
+ *  {@literal @}EnsuresPresent("optStr")
+ *  void initialize() {
+ *    optStr = Optional.of("abc");
+ *  }
  * </code></pre>
  *
  * It can also be used for a method that fails if a given Optional value is empty, indicating that
  * the argument is present if the method returns normally:
  *
  * <pre><code>
- *   /** Throws an exception if the argument is empty. *&#47;
- *   {@literal @}EnsuresPresent("#1")
- *   void useTheOptional(Optional&lt;T&gt; arg) { ... }
+ *  /** Throws an exception if the argument is empty. *&#47;
+ *  {@literal @}EnsuresPresent("#1")
+ *  void useTheOptional(Optional&lt;T&gt; arg) { ... }
  * </code></pre>
  *
  * @see Present

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

@@ -22,7 +22,7 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({}) // empty target prevents programmers from writing this in a program
 @InvisibleQualifier
-@SubtypeOf(org.checkerframework.checker.regex.qual.UnknownRegex.class)
+@SubtypeOf(UnknownRegex.class)
 public @interface PartialRegex {
 
     /**

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

@@ -23,6 +23,6 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.LOWER_BOUND, TypeUseLocation.UPPER_BOUND})
 @InvisibleQualifier
-@SubtypeOf({Regex.class, org.checkerframework.checker.regex.qual.PartialRegex.class})
+@SubtypeOf({Regex.class, PartialRegex.class})
 @DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
 public @interface RegexBottom {}

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

@@ -4,6 +4,7 @@
 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;
@@ -18,7 +19,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({}) // empty target prevents programmers from writing this in a program
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf({})
 @DefaultQualifierInHierarchy
 public @interface SignatureUnknown {}

src/java.base/share/classes/org/checkerframework/checker/signedness/qual/Signed.java

@@ -33,16 +33,9 @@
             TypeKind.FLOAT,
             TypeKind.DOUBLE
         },
-        types = {
-            java.lang.Byte.class,
-            java.lang.Integer.class,
-            java.lang.Long.class,
-            java.lang.Short.class,
-            java.lang.Float.class,
-            java.lang.Double.class
-        },
+        types = {Byte.class, Integer.class, Long.class, Short.class, Float.class, Double.class},
         value = TypeUseLocation.EXCEPTION_PARAMETER)
 @UpperBoundFor(
         typeKinds = {TypeKind.FLOAT, TypeKind.DOUBLE},
-        types = {java.lang.Float.class, java.lang.Double.class})
+        types = {Float.class, Double.class})
 public @interface Signed {}

src/java.base/share/classes/org/checkerframework/checker/signedness/qual/Unsigned.java

@@ -24,8 +24,8 @@
 @SubtypeOf({UnknownSignedness.class})
 @DefaultFor(
         typeKinds = {TypeKind.CHAR},
-        types = {java.lang.Character.class})
+        types = {Character.class})
 @UpperBoundFor(
         typeKinds = {TypeKind.CHAR},
-        types = {java.lang.Character.class})
+        types = {Character.class})
 public @interface Unsigned {}

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

@@ -5,6 +5,7 @@
 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;
@@ -22,7 +23,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({})
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @DefaultQualifierInHierarchy
 @SubtypeOf({LeakedToResult.class})
 @InvisibleQualifier

src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java

@@ -4,6 +4,7 @@
 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;
@@ -22,7 +23,7 @@
  */
 @Documented
 @Retention(RetentionPolicy.SOURCE) // don't store in class file
-@Target({}) // empty target prevents programmers from writing this in a program.
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @InvisibleQualifier
 @SubtypeOf({})
 public @interface Unqualified {}

src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java

@@ -13,7 +13,7 @@
  * Java regular expressions. If an expression's type has this annotation, then at run time, the
  * expression evaluates to a string that matches none of the regular expressions. Matching is via
  * the <a
- * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches</a>
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches</a>
  * method, which matches against the entire string (it does not look for a match against a
  * substring).
  *

src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java

@@ -15,7 +15,7 @@
  *
  * <p>IntRangeFromGTENegativeOne annotations derived from GTENegativeOne annotations are used to
  * create IntRange annotations, but IntRangeFromGTENegativeOne annotations are not checked when they
- * appear on the left hand side of expressions. Therefore, the Index Checker MUST be run on any code
+ * appear on the left-hand side of expressions. Therefore, the Index Checker MUST be run on any code
  * with @GTENegativeOne annotations on the left-hand side of expressions, since the Value Checker
  * will derive information from them but not check them.
  *

src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java

@@ -15,7 +15,7 @@
  *
  * <p>IntRangeFromNonNegative annotations derived from NonNegative annotations are used to create
  * IntRange annotations, but IntRangeFromNonNegative annotations are not checked when they appear on
- * the left hand side of expressions. Therefore, the Index Checker MUST be run on any code
+ * the left-hand side of expressions. Therefore, the Index Checker MUST be run on any code
  * with @NonNegative annotations on the left-hand side of expressions, since the Value Checker will
  * derive information from them but not check them.
  *

src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java

@@ -14,10 +14,10 @@
  * annotation.
  *
  * <p>IntRangeFromPositive annotations derived from Positive annotations are used to create IntRange
- * annotations, but IntRangeFromPositive annotations are not checked when they appear on the left
- * hand side of expressions. Therefore, the Index Checker MUST be run on any code with @Positive
- * annotations on the left-hand side of expressions, since the Value Checker will derive information
- * from them but not check them.
+ * annotations, but IntRangeFromPositive annotations are not checked when they appear on the
+ * left-hand side of expressions. Therefore, the Index Checker MUST be run on any code
+ * with @Positive annotations on the left-hand side of expressions, since the Value Checker will
+ * derive information from them but not check them.
  *
  * <p>It is an error to write this annotation directly. {@code @Positive} or {@code IntRange(from =
  * 1, to = Integer.MAX_VALUE)} should always be written instead. This annotation is not retained in

src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java

@@ -13,7 +13,7 @@
  * Java regular expressions. If an expression's type has this annotation, then at run time, the
  * expression evaluates to a string that matches at least one of the regular expressions. Matching
  * is via the <a
- * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches</a>
+ * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#matches(java.lang.String)">java.lang.String#matches</a>
  * method, which matches against the entire string (it does not look for a match against a
  * substring).
  *

src/java.base/share/classes/org/checkerframework/framework/qual/EnsuresQualifierIf.java

@@ -18,10 +18,10 @@
  * <p>Here is an example use:
  *
  * <pre><code>
- *   {@literal @}EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class)
- *    boolean isOdd(int p1, int p2) {
- *        return p1 % 2 == 1;
- *    }
+ *  {@literal @}EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class)
+ *   boolean isOdd(int p1, int p2) {
+ *     return p1 % 2 == 1;
+ *   }
  * </code></pre>
  *
  * <p>This annotation is only applicable to methods with a boolean return type.

src/java.base/share/classes/org/checkerframework/framework/qual/PostconditionAnnotation.java

@@ -31,8 +31,8 @@
  * org.checkerframework.common.value.qual.MinLen} qualifier:
  *
  * <pre><code>
- * {@literal @}PostconditionAnnotation(qualifier = MinLen.class)
- * {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+ *  {@literal @}PostconditionAnnotation(qualifier = MinLen.class)
+ *  {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
  *  public {@literal @}interface EnsuresMinLen {
  *    String[] value();
  *    {@literal @}QualifierArgument("value")
@@ -47,7 +47,7 @@
  * {@code @MinLen(2)} upon return.
  *
  * <pre><code>
- * {@literal @}EnsuresMinLen(value = "field", targetValue = 2")
+ *  {@literal @}EnsuresMinLen(value = "field", targetValue = 2)
  *  public void setField(String argument) {
  *    field = "(" + argument + ")";
  *  }

src/java.base/share/classes/org/checkerframework/framework/qual/PreconditionAnnotation.java

@@ -27,12 +27,12 @@
  * org.checkerframework.common.value.qual.MinLen} qualifier:
  *
  * <pre><code>
- * {@literal @}PreconditionAnnotation(qualifier = MinLen.class)
- * {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
- * public {@literal @}interface RequiresMinLen {
- *   String[] value();
- *   {@literal @}QualifierArgument("value")
- *   int targetValue() default 0;
+ *  {@literal @}PreconditionAnnotation(qualifier = MinLen.class)
+ *  {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+ *  public {@literal @}interface RequiresMinLen {
+ *    String[] value();
+ *    {@literal @}QualifierArgument("value")
+ *    int targetValue() default 0;
  * </code></pre>
  *
  * The {@code value} element holds the expressions to which the qualifier applies and {@code
@@ -43,10 +43,10 @@
  * {@code @MinLen(2)} upon entry.
  *
  * <pre><code>
- * {@literal @}RequiresMinLen(value = "field", targetValue = 2")
- * public char getThirdCharacter() {
- *   return field.charAt(2);
- * }
+ *  {@literal @}RequiresMinLen(value = "field", targetValue = 2")
+ *  public char getThirdCharacter() {
+ *    return field.charAt(2);
+ *  }
  * </code></pre>
  *
  * @see RequiresQualifier