From fade1aa75582092739ef3840bf17f431806ad18f Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Feb 2026 12:21:34 -0800 Subject: [PATCH 1/7] Annotate `lineSeparator()` with `@Regex` (cherry picked from commit 26442c476c5f97a8734dd54687d4199ba04e33df) --- src/java.base/share/classes/java/lang/System.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/java.base/share/classes/java/lang/System.java b/src/java.base/share/classes/java/lang/System.java index 19439ccff41..6aea0892ef4 100644 --- a/src/java.base/share/classes/java/lang/System.java +++ b/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; } From 50d791ba22838f250c4fc3f1d85a274da3df172d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Feb 2026 09:34:27 -0800 Subject: [PATCH 2/7] Must call `disconnect()` on `HttpURLConnection` (cherry picked from commit cb73e18027c9e31d3f089f5693f1afd1e22e35b4) --- src/java.base/share/classes/java/net/HttpURLConnection.java | 5 +++++ .../classes/sun/net/www/protocol/http/HttpURLConnection.java | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/java.base/share/classes/java/net/HttpURLConnection.java b/src/java.base/share/classes/java/net/HttpURLConnection.java index 9f7779dd011..ada97c4f54b 100644 --- a/src/java.base/share/classes/java/net/HttpURLConnection.java +++ b/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 */ diff --git a/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java b/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java index 6280cc1c826..cf75165b839 100644 --- a/src/java.base/share/classes/sun/net/www/protocol/http/HttpURLConnection.java +++ b/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"; From eba5ba267019385be0ac9eb077c6409be887670c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 10 Feb 2026 08:59:46 -0800 Subject: [PATCH 3/7] Update Claude settings (cherry picked from commit 9f4904f5f397053729bdecdebf6c8f7dcb2ef454) --- .claude/settings.json | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 .claude/settings.json diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 00000000000..1ca8b047bc6 --- /dev/null +++ b/.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": [] + } +} From bca6d2b2655044551ee0d7cafb185f151a981e82 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 4 Feb 2026 11:08:46 -0800 Subject: [PATCH 4/7] CodeRabbit configuration (cherry picked from commit 363610bb063fdff9fc558f739efa964eba19fdd7) --- .coderabbit.yaml | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 .coderabbit.yaml diff --git a/.coderabbit.yaml b/.coderabbit.yaml new file mode 100644 index 00000000000..64605043b7d --- /dev/null +++ b/.coderabbit.yaml @@ -0,0 +1,45 @@ +# 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: + 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" From 04dcccc0fa62939e5f449fe8e62aef7e6d3f0e01 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 11 Feb 2026 07:02:33 -0800 Subject: [PATCH 5/7] Whitespace fixes, thanks to Daniel Gao From c5729f3b3cdf08be8734d4bd00406ead35dd7da2 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 9 Feb 2026 15:13:32 -0800 Subject: [PATCH 6/7] Update `.coderabbit.yaml` (cherry picked from commit 03d12f315444de037422e557e5ac1710ad4b4734) --- .coderabbit.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.coderabbit.yaml b/.coderabbit.yaml index 64605043b7d..bcd9365ae43 100644 --- a/.coderabbit.yaml +++ b/.coderabbit.yaml @@ -19,6 +19,7 @@ reviews: - "!**/.idea/**" - "!**/node_modules/**" auto_review: + auto_pause_after_reviewed_commits: 0 ignore_title_keywords: - "wip" - "draft" From ba3413bc0b5894a62caec1f3792e6293bc2c5bd9 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Sat, 3 Oct 2026 01:22:55 -0400 Subject: [PATCH 7/7] Match the qualifier files to Checker Framework 3.54.0 The JDK consistency check requires identical qualifier files; 3.54.0 changed their Javadoc and removed @Target({}) from some qualifiers. Co-Authored-By: Claude Sonnet 5.5 --- .../checker/fenum/qual/FenumUnqualified.java | 3 ++- .../org/checkerframework/checker/index/qual/IndexFor.java | 2 +- .../checkerframework/checker/index/qual/IndexOrHigh.java | 7 +++++-- .../checkerframework/checker/index/qual/IndexOrLow.java | 2 +- .../org/checkerframework/checker/lock/qual/LockHeld.java | 3 ++- .../checker/lock/qual/LockPossiblyHeld.java | 3 ++- .../checker/signature/qual/SignatureUnknown.java | 3 ++- .../common/aliasing/qual/MaybeLeaked.java | 3 ++- .../common/subtyping/qual/Unqualified.java | 3 ++- .../common/value/qual/DoesNotMatchRegex.java | 2 +- .../common/value/qual/IntRangeFromGTENegativeOne.java | 2 +- .../common/value/qual/IntRangeFromNonNegative.java | 2 +- .../common/value/qual/IntRangeFromPositive.java | 8 ++++---- .../checkerframework/common/value/qual/MatchesRegex.java | 2 +- 14 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java b/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java index d516e69de09..247342a0707 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/fenum/qual/FenumUnqualified.java +++ b/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) diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java index 3a0a4a7d1ed..13320e03a64 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java +++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexFor.java @@ -14,7 +14,7 @@ * different lengths. * *

The + * href="https://docs.oracle.com/en/java/javase/25/docs/api/java.base/java/lang/String.html#charAt(int)"> * {@code String.charAt(int)} method is declared as * *

{@code
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
index c91497e94aa..31c222dc3aa 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
@@ -11,7 +11,7 @@
  * sequence's length.
  *
  * 

The + * 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} method is declared as * *

{@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();
 }
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java
index e4cd74d2b6d..594a6b3bb14 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrLow.java
+++ b/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.
  *
  * 

The + * 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)} method is declared as * *


diff --git a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java
index 4d8af9898f8..eb402825340 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockHeld.java
+++ b/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 {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java b/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java
index 0cc89dae203..bf7b1095c40 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java
+++ b/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
diff --git a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java
index a74c04d84fe..ef46ecb04bb 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/SignatureUnknown.java
+++ b/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 {}
diff --git a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java b/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java
index 0d421fc3242..09a951be1f7 100644
--- a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/MaybeLeaked.java
+++ b/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
diff --git a/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java b/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java
index ab339ca71ea..0a71f75c51a 100644
--- a/src/java.base/share/classes/org/checkerframework/common/subtyping/qual/Unqualified.java
+++ b/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 {}
diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java
index 8fb1c2667e1..1c7c7756d4e 100644
--- a/src/java.base/share/classes/org/checkerframework/common/value/qual/DoesNotMatchRegex.java
+++ b/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 java.lang.String#matches
+ * 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
  * method, which matches against the entire string (it does not look for a match against a
  * substring).
  *
diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
index c1cbd3a1673..405a048e3cf 100644
--- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
+++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromGTENegativeOne.java
@@ -15,7 +15,7 @@
  *
  * 

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. * diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java index ecce8296e88..cf393bc52bb 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java +++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromNonNegative.java @@ -15,7 +15,7 @@ * *

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. * diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java index f1cfc6084f3..09a176785a7 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java +++ b/src/java.base/share/classes/org/checkerframework/common/value/qual/IntRangeFromPositive.java @@ -14,10 +14,10 @@ * annotation. * *

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. * *

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 diff --git a/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java b/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java index 49fa1377a88..5282daa65e4 100644 --- a/src/java.base/share/classes/org/checkerframework/common/value/qual/MatchesRegex.java +++ b/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 java.lang.String#matches + * 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 * method, which matches against the entire string (it does not look for a match against a * substring). *