From 9a54c36a2e5ba2911aa8cdfb10d72a9e1f01f0ab Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 5 Aug 2026 02:51:00 -0400 Subject: [PATCH 1/7] Add @EnsuresInitialized postcondition --- .../qual/EnsuresInitialized.java | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java new file mode 100644 index 00000000000..2a969bb3f3d --- /dev/null +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -0,0 +1,51 @@ +package org.checkerframework.checker.initialization.qual; + +import org.checkerframework.framework.qual.InheritedAnnotation; +import org.checkerframework.framework.qual.PostconditionAnnotation; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Repeatable; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * A method postcondition annotation that guarantees that a field is initialized (assigned a value) + * after the method terminates successfully. + * + *

Note: This is an initialization checker postcondition, distinct from {@link + * org.checkerframework.common.initializedfields.qual.EnsuresInitializedFields} which is used by the + * standalone Initialized Fields Checker. + * + * @checker_framework.manual #initialization-checker Initialization Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@PostconditionAnnotation(qualifier = Initialized.class) +@InheritedAnnotation +@Repeatable(EnsuresInitialized.List.class) +public @interface EnsuresInitialized { + /** + * The Java expressions that are initialized upon successful method termination. + * + * @return the Java expressions that are initialized + */ + String[] value(); + + /** A wrapper annotation that makes the {@link EnsuresInitialized} annotation repeatable. */ + @Documented + @Retention(RetentionPolicy.RUNTIME) + @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) + @PostconditionAnnotation(qualifier = Initialized.class) + @InheritedAnnotation + public static @interface List { + /** + * Return the repeatable annotations. + * + * @return the repeatable annotations + */ + EnsuresInitialized[] value(); + } +} From 2e9f1556237ab6795f5847910ab6044704d3fbf2 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 5 Aug 2026 03:07:43 -0400 Subject: [PATCH 2/7] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- .../checker/initialization/qual/EnsuresInitialized.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java index 2a969bb3f3d..b632ca18e71 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -11,8 +11,8 @@ import java.lang.annotation.Target; /** - * A method postcondition annotation that guarantees that a field is initialized (assigned a value) - * after the method terminates successfully. + * A method postcondition annotation that guarantees that the given Java expressions are {@link + * Initialized} after the method terminates successfully. * *

Note: This is an initialization checker postcondition, distinct from {@link * org.checkerframework.common.initializedfields.qual.EnsuresInitializedFields} which is used by the From b41175922f98c9d10e69d6d589811d3986b0286e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 5 Aug 2026 18:35:05 -0400 Subject: [PATCH 3/7] Apply suggestion from @aosen-xiong --- .../checker/initialization/qual/EnsuresInitialized.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java index b632ca18e71..ca770cc84ff 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -27,10 +27,11 @@ @InheritedAnnotation @Repeatable(EnsuresInitialized.List.class) public @interface EnsuresInitialized { - /** + /** * The Java expressions that are initialized upon successful method termination. * * @return the Java expressions that are initialized + * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions */ String[] value(); From bf89058b4469c36ead930c63eed93f06a82879b9 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 5 Aug 2026 20:05:46 -0400 Subject: [PATCH 4/7] Fix indentation of the EnsuresInitialized value() Javadoc The Javadoc comment on value() was indented five spaces instead of four, so check-jdk-consistency.sh reported a difference against the checker-qual copy and failed the misc CI job. Co-Authored-By: Claude Opus 5 (1M context) --- .../checker/initialization/qual/EnsuresInitialized.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java index ca770cc84ff..0c51f241bb0 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -27,7 +27,7 @@ @InheritedAnnotation @Repeatable(EnsuresInitialized.List.class) public @interface EnsuresInitialized { - /** + /** * The Java expressions that are initialized upon successful method termination. * * @return the Java expressions that are initialized From 76dc666b5948fe9a667db74953507fa465ef73a6 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 6 Aug 2026 10:53:48 -0400 Subject: [PATCH 5/7] Sync EnsuresInitialized.java from checker-framework --- .../checker/initialization/qual/EnsuresInitialized.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java index 0c51f241bb0..158f3e20bd6 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -14,7 +14,7 @@ * A method postcondition annotation that guarantees that the given Java expressions are {@link * Initialized} after the method terminates successfully. * - *

Note: This is an initialization checker postcondition, distinct from {@link + *

Note: This is an Initialization Checker postcondition, distinct from {@link * org.checkerframework.common.initializedfields.qual.EnsuresInitializedFields} which is used by the * standalone Initialized Fields Checker. * From edb7b7a93768866acc864fbfadcf11ad0550e0bd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 27 Aug 2026 21:05:14 -0400 Subject: [PATCH 6/7] Sync EnsuresInitialized.java Javadoc from checker-framework Picks up the Javadoc clarification added in eisop/checker-framework#1918: when the annotation is useful, that it is trivially true on an already @Initialized receiver, and to prefer @EnsuresNonNull when a nullness guarantee is also wanted. check-jdk-consistency.sh requires this file to be identical to the checker-qual copy. --- .../initialization/qual/EnsuresInitialized.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java index 158f3e20bd6..811c76c137a 100644 --- a/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java +++ b/src/java.base/share/classes/org/checkerframework/checker/initialization/qual/EnsuresInitialized.java @@ -14,6 +14,16 @@ * A method postcondition annotation that guarantees that the given Java expressions are {@link * Initialized} after the method terminates successfully. * + *

This annotation is useful when a method initializes a field of an object that is currently + * {@link UnderInitialization} (or {@link UnknownInitialization}). It tells the Initialization + * Checker that the field has been assigned a value. + * + *

If the receiver is already fully {@link Initialized}, this annotation provides no new + * information and is trivially true. If you also want to guarantee that a reference field is not + * null (for the Nullness Checker), use {@link + * org.checkerframework.checker.nullness.qual.EnsuresNonNull} instead, which implies initialization + * but also provides a nullness guarantee. + * *

Note: This is an Initialization Checker postcondition, distinct from {@link * org.checkerframework.common.initializedfields.qual.EnsuresInitializedFields} which is used by the * standalone Initialized Fields Checker. From 1365b466eec057e9d81080cbff5b23188fb33b71 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 30 Aug 2026 18:16:51 -0400 Subject: [PATCH 7/7] Empty commit to re-run CI