Update from typetools/jdk up to the Checker Framework 3.54.0 release

.claude/settings.json

@@ -0,0 +1,22 @@
+{
+  "enabledPlugins": {
+    "rust-analyzer-lsp@claude-plugins-official": true
+  }
+  "permissions": {
+    "allow": [
+      "WebFetch(domain:checkerframework.org)",
+      "Bash(mkdir:*)",
+      "Bash(./gradlew:*)",
+      "Bash(git -C /home/mernst/research/types/checker-framework-fork-mernst-branch-override-order diff master..override-order --stat)"
+      "Bash(git -C /home/mernst/research/types/checker-framework-fork-mernst-branch-override-order log master..override-order --oneline)",
+      "Bash(java:*)",
+      "Bash(javac:*)",
+      "Bash(ls)",
+      "Bash(timeout 300 ./gradlew:*)",
+      "Bash(./x.py check:*)",
+      "Read(//scratch/mernst/**)"
+    ],
+    "deny": [],
+    "ask": []
+  }
+}

.coderabbit.yaml

@@ -0,0 +1,46 @@
+# yaml-language-server: $schema=https://coderabbit.ai/integrations/schema.v2.json
+
+language: "en-US"
+
+reviews:
+  profile: "assertive"
+  high_level_summary: false
+  review_status: false
+  collapse_walkthrough: true
+  changed_files_summary: false
+  sequence_diagrams: false
+  estimate_code_review_effort: false
+  in_progress_fortune: false
+  poem: false
+  path_filters:
+    - "!**/build/**"
+    - "!**/out/**"
+    - "!**/.gradle/**"
+    - "!**/.idea/**"
+    - "!**/node_modules/**"
+  auto_review:
+    auto_pause_after_reviewed_commits: 0
+    ignore_title_keywords:
+      - "wip"
+      - "draft"
+    ignore_usernames:
+      - "dependabot"
+      - "dependabot[bot]"
+      - "mend"
+      - "renovate"
+      - "renovate[bot]"
+  pre_merge_checks:
+    title:
+      mode: "off"
+    description:
+      mode: "off"
+
+chat:
+  art: false
+
+knowledge_base:
+  code_guidelines:
+    enabled: true
+    filePatterns:
+      - "**/.cursorrules"
+      - "**/CODING_STANDARDS.md"

src/java.base/share/classes/java/lang/System.java

@@ -31,6 +31,7 @@
 import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
+import org.checkerframework.checker.regex.qual.Regex;
 import org.checkerframework.checker.signedness.qual.PolySigned;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
@@ -112,7 +113,7 @@
  *
  * @since   1.0
  */
-@AnnotatedFor({"index", "interning", "lock", "mustcall", "nullness", "signedness"})
+@AnnotatedFor({"index", "interning", "lock", "mustcall", "nullness", "regex", "signedness"})
 public final @UsesObjectEquals class System {
     /* Register the natives via the static initializer.
      *
@@ -854,7 +855,7 @@ public static Properties getProperties() {
      * @since 1.7
      */
     @Pure
-    public static String lineSeparator() {
+    public static @Regex String lineSeparator() {
         return lineSeparator;
     }
 

src/java.base/share/classes/java/net/HttpURLConnection.java

@@ -25,6 +25,9 @@
 
 package java.net;
 
+import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
+import org.checkerframework.framework.qual.AnnotatedFor;
+
 import java.io.InputStream;
 import java.io.IOException;
 import java.security.Permission;
@@ -66,6 +69,8 @@
  * @see     java.net.HttpURLConnection#disconnect()
  * @since 1.1
  */
+@AnnotatedFor("mustcall")
+@InheritableMustCall("disconnect")
 public abstract class HttpURLConnection extends URLConnection {
     /* instance variables */
 

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/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,7 +10,7 @@
  * 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>

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/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/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/sun/net/www/protocol/http/HttpURLConnection.java

@@ -25,6 +25,9 @@
 
 package sun.net.www.protocol.http;
 
+import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
+import org.checkerframework.framework.qual.AnnotatedFor;
+
 import java.security.PrivilegedAction;
 import java.util.Arrays;
 import java.net.URL;
@@ -97,6 +100,8 @@
  */
 
 
+@AnnotatedFor("mustcall")
+@InheritableMustCall("disconnect")
 public class HttpURLConnection extends java.net.HttpURLConnection {
 
     static final String HTTP_CONNECT = "CONNECT";