From 137224c06ca07c0f3e0cab6cadc5e3ce51689765 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 20 Mar 2025 12:23:27 -0400 Subject: [PATCH 01/15] fix 6990 --- .../resourceleak/MustCallConsistencyAnalyzer.java | 6 ++++-- checker/tests/resourceleak/DropOwning.java | 15 +++++++++++++++ 2 files changed, 19 insertions(+), 2 deletions(-) create mode 100644 checker/tests/resourceleak/DropOwning.java diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java index cee309a4dfcc..9fb92c0bd878 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -353,7 +353,7 @@ public boolean derivedFromMustCallAlias() { } /** - * Gets the must-call type associated with the given resource alias, falling on back on the + * Gets the must-call type associated with the given resource alias, falling back on the * declared type if there is no refined type for the alias in the store. * * @param alias a resource alias @@ -367,7 +367,9 @@ private static AnnotationMirror getMustCallValue( CFValue value = mcStore == null ? null : mcStore.getValue(reference); if (value != null) { AnnotationMirror result = - AnnotationUtils.getAnnotationByClass(value.getAnnotations(), MustCall.class); + mcAtf + .getQualifierHierarchy() + .findAnnotationInHierarchy(value.getAnnotations(), mcAtf.TOP); if (result != null) { return result; } diff --git a/checker/tests/resourceleak/DropOwning.java b/checker/tests/resourceleak/DropOwning.java new file mode 100644 index 000000000000..219dfd93efef --- /dev/null +++ b/checker/tests/resourceleak/DropOwning.java @@ -0,0 +1,15 @@ +// test case for https://github.com/typetools/checker-framework/issues/6990 + +import java.io.Closeable; +import org.checkerframework.checker.mustcall.qual.MustCallUnknown; +import org.checkerframework.checker.mustcall.qual.Owning; + +public class DropOwning { + + public void f(@Owning Closeable resource) { + drop(resource); + } + + // :: error: required.method.not.known + private void drop(@Owning @MustCallUnknown Object resourceCF6990) {} +} From 32e26b5c7e4b125d2ca2a9b5fc71046df45b4ab0 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Mon, 24 Mar 2025 14:34:19 -0400 Subject: [PATCH 02/15] ignore excess warning on crash test --- .../tests/ainfer-resourceleak/non-annotated/CrashForTempVar.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/ainfer-resourceleak/non-annotated/CrashForTempVar.java b/checker/tests/ainfer-resourceleak/non-annotated/CrashForTempVar.java index ed72d1603f2e..edc40f683603 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/CrashForTempVar.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/CrashForTempVar.java @@ -2,6 +2,7 @@ * Demonstrates an issue in the Checker Framework with handling the nearest enclosing element for * temporary variable declarations, leading to a crash during analysis. */ +@SuppressWarnings("all") // only check for crashes public abstract class CrashForTempVar { private final CrashForTempVar _base; From aae6acd81053a4890d11f606922e336e64817b3d Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Mon, 24 Mar 2025 14:56:59 -0400 Subject: [PATCH 03/15] annotations to remove false positives --- .../checker/initialization/InitializationStore.java | 7 +++++-- .../checker/initialization/InitializationTransfer.java | 3 ++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index 565d8b3cbfee..22367c6d5204 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -8,6 +8,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.VariableElement; +import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; import org.checkerframework.dataflow.expression.ClassName; @@ -30,8 +31,10 @@ * * @see InitializationTransfer */ -public class InitializationStore, S extends InitializationStore> - extends CFAbstractStore { +public class InitializationStore< + V extends CFAbstractValue<@MustCall({}) V>, + S extends InitializationStore<@MustCall({}) V, @MustCall({}) S>> + extends CFAbstractStore<@MustCall({}) V, @MustCall({}) S> { /** The set of fields that are initialized. */ protected final Set initializedFields; diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java index e3db178e1cab..3ea55b85657d 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java @@ -13,6 +13,7 @@ import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import javax.lang.model.util.ElementFilter; +import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; @@ -56,7 +57,7 @@ public class InitializationTransfer< V extends CFAbstractValue, T extends InitializationTransfer, - S extends InitializationStore> + S extends InitializationStore<@MustCall({}) V, @MustCall({}) S>> extends CFAbstractTransfer { protected final InitializationAnnotatedTypeFactory atypeFactory; From 0a8b1b9f0b319571e38377ee7585f233f2fe6d51 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 25 Mar 2025 16:00:52 -0700 Subject: [PATCH 04/15] Add Javadoc --- .../checker/initialization/InitializationStore.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index 22367c6d5204..3fc2b9435c76 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -29,6 +29,8 @@ * A store that extends {@code CFAbstractStore} and additionally tracks which fields of the 'self' * reference have been initialized. * + * @param the type of values in the abstract store + * @param the type of teh abstract store * @see InitializationTransfer */ public class InitializationStore< From c6e6d94371a81dcf436dc880ec11a04a2baafe52 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Fri, 18 Jul 2025 11:00:29 -0400 Subject: [PATCH 05/15] Update checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- .../checker/initialization/InitializationStore.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index 3fc2b9435c76..95a0eea86bd3 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -30,7 +30,7 @@ * reference have been initialized. * * @param the type of values in the abstract store - * @param the type of teh abstract store + * @param the type of the abstract store * @see InitializationTransfer */ public class InitializationStore< From 0b0d74f3f26c9dd1d7d1b24fdf1eab185975a483 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 24 Jul 2025 13:41:18 -0400 Subject: [PATCH 06/15] add suppressions and annotations to AFU --- .../src/main/java/org/checkerframework/afu/annotator/Main.java | 1 + .../org/checkerframework/afu/scenelib/el/TypeASTMapper.java | 1 + .../java/org/checkerframework/afu/scenelib/io/ASTPath.java | 1 + .../java/org/checkerframework/afu/scenelib/util/SceneOps.java | 1 + .../afu/scenelib/util/coll/LinkedHashKeyedSet.java | 1 + .../checkerframework/afu/scenelib/util/coll/VivifyingMap.java | 3 ++- 6 files changed, 7 insertions(+), 1 deletion(-) diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java index 833b2a9e57e7..fc06d6295937 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java @@ -195,6 +195,7 @@ public class Main { // TODO: remove this. public static boolean temporaryDebug = false; + @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private static ElementVisitor classFilter = new ElementVisitor() { Void filter(VivifyingMap vm0, VivifyingMap vm1) { diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/TypeASTMapper.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/TypeASTMapper.java index 8da0bc1e9013..c952a33b4756 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/TypeASTMapper.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/el/TypeASTMapper.java @@ -22,6 +22,7 @@ * * @param common supertype of the AST nodes */ +@SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources public abstract class TypeASTMapper { /** Constructs a {@link TypeASTMapper}. A {@link TypeASTMapper} stores no state. */ protected TypeASTMapper() {} diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java index b2e1536a0c14..5a66a26d9f91 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/io/ASTPath.java @@ -1433,6 +1433,7 @@ public String toString() { * * @param type of stack elements */ +@SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources class ImmutableStack { // The stack is implemented as a linked list: diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java index 0d27057d4499..3e2f96748966 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java @@ -289,6 +289,7 @@ public Void visitElement(AElement minuend, Pair eltPair) { * Calculates difference between {@code minuend} and first component of {@code eltPair}, adding * results to second component of {@code eltPair}. */ + @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private void visitElements( VivifyingMap minuend, VivifyingMap subtrahend, VivifyingMap difference) { if (minuend != null) { diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java index f20dd9d0859b..b723361f1b65 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/LinkedHashKeyedSet.java @@ -10,6 +10,7 @@ * A simple implementation of {@link KeyedSet} backed by an insertion-order {@link * java.util.LinkedHashMap} and its {@link java.util.LinkedHashMap#values() value collection}. */ +@SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources public class LinkedHashKeyedSet extends AbstractSet implements KeyedSet { private final Keyer keyer; diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java index d3e06819bc15..27e40a2dd679 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java @@ -2,6 +2,7 @@ import java.util.Iterator; import java.util.Map; +import org.checkerframework.checker.mustcall.qual.MustCall; /** * A {@link VivifyingMap} is a map with two additional methods: @@ -12,7 +13,7 @@ *
  • {@link #prune} removes empty values * */ -public abstract class VivifyingMap extends WrapperMap { +public abstract class VivifyingMap extends WrapperMap { /** * Constructs a new {@link VivifyingMap} backed by the given map. All reads and writes to this * {@link VivifyingMap} go through to the backing map. However, since the {@link VivifyingMap} From 182fcd6c26e6b3d8339d6f2ac2103fd7363124d4 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 1 Jun 2026 17:27:19 -0700 Subject: [PATCH 07/15] Javadoc --- .../java/org/checkerframework/afu/annotator/Main.java | 1 + .../checkerframework/afu/scenelib/util/SceneOps.java | 11 +++++++++-- .../afu/scenelib/util/coll/VivifyingMap.java | 3 +++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java index b89291d18032..982e32fd2889 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java @@ -199,6 +199,7 @@ private Main() { // TODO: remove this. public static boolean temporaryDebug = false; + /** Does the work of {@link #filteredScene}. */ @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private static ElementVisitor classFilter = new ElementVisitor() { diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java index 3e2f96748966..fb86e944f138 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java @@ -286,8 +286,15 @@ public Void visitElement(AElement minuend, Pair eltPair) { } /** - * Calculates difference between {@code minuend} and first component of {@code eltPair}, adding - * results to second component of {@code eltPair}. + * Calculates difference between {@code minuend} and {@code subtrahend}, adding results to {@code + * difference}. + * + * @param minuend the first argument to diff + * @param subtrahend the second argument + * @param difference side-effected to add elements that are in {@code minuend} but not in {@code + * subtrahend} + * @param the type of keys + * @param the type of values */ @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private void visitElements( diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java index 3c03083640f4..2661148ce458 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/coll/VivifyingMap.java @@ -12,6 +12,9 @@ * empty value and returns that. *
  • {@link #prune} removes empty values * + * + * @param the type of keys + * @param the type of values */ public abstract class VivifyingMap extends WrapperMap { /** From e4a8a1159dd135554a5f9e0efff34d0fb24547fb Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 1 Jun 2026 19:26:26 -0700 Subject: [PATCH 08/15] Javadoc --- .../org/checkerframework/afu/annotator/Main.java | 12 +++--------- .../checkerframework/afu/scenelib/util/SceneOps.java | 2 +- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java index 982e32fd2889..008a63308180 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java @@ -186,19 +186,19 @@ private Main() { // Debugging options go below here. + /** Print progress information. */ @OptionGroup("Debugging options") @Option("-v Verbose (print progress information)") public static boolean verbose = false; + /** Print debug information. */ @Option("Debug (print debug information)") public static boolean debug = false; + /** Print the stack if an error is thrown. */ @Option("Print error stack") public static boolean print_error_stack = false; - // TODO: remove this. - public static boolean temporaryDebug = false; - /** Does the work of {@link #filteredScene}. */ @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private static ElementVisitor classFilter = @@ -582,12 +582,6 @@ public static void main(String[] args) throws IOException { IndexFileSpecification spec = new IndexFileSpecification(jaifFile); try { List parsedSpec = spec.parse(); - if (temporaryDebug) { - System.out.printf("parsedSpec (size %d):%n", parsedSpec.size()); - for (Insertion insertion : parsedSpec) { - System.out.printf(" %s, isInserted=%s%n", insertion, insertion.isInserted()); - } - } AScene scene = spec.getScene(); parsedSpec.sort( (Insertion i1, Insertion i2) -> { diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java index fb86e944f138..b6a274435d8c 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/scenelib/util/SceneOps.java @@ -294,7 +294,7 @@ public Void visitElement(AElement minuend, Pair eltPair) { * @param difference side-effected to add elements that are in {@code minuend} but not in {@code * subtrahend} * @param the type of keys - * @param the type of values + * @param the type of values */ @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private void visitElements( From 02c7d3a9248b58c0a496fc50e68b9b99041c58c6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 2 Jun 2026 06:58:39 -0700 Subject: [PATCH 09/15] Reinstate debugging flag --- .../java/org/checkerframework/afu/annotator/Main.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java index 008a63308180..c449bc94250c 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java @@ -199,6 +199,10 @@ private Main() { @Option("Print error stack") public static boolean print_error_stack = false; + /** Debugging flag. */ + // TODO: remove this. + public static boolean temporaryDebug = false; + /** Does the work of {@link #filteredScene}. */ @SuppressWarnings("resourceleak:required.method.not.known") // Not relevant to resources private static ElementVisitor classFilter = @@ -582,6 +586,12 @@ public static void main(String[] args) throws IOException { IndexFileSpecification spec = new IndexFileSpecification(jaifFile); try { List parsedSpec = spec.parse(); + if (temporaryDebug) { + System.out.printf("parsedSpec (size %d):%n", parsedSpec.size()); + for (Insertion insertion : parsedSpec) { + System.out.printf(" %s, isInserted=%s%n", insertion, insertion.isInserted()); + } + } AScene scene = spec.getScene(); parsedSpec.sort( (Insertion i1, Insertion i2) -> { From 3ad4cbbcc8e35498b07c2698357a4174237caa7b Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 2 Jun 2026 07:25:39 -0700 Subject: [PATCH 10/15] Grammar tweak --- .../checker/rlccalledmethods/messages.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties index a9df3c247117..84ccf4a4affd 100644 --- a/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/rlccalledmethods/messages.properties @@ -9,4 +9,4 @@ mustcallalias.out.of.scope=This @MustCallAlias parameter might go out of scope w mustcallalias.method.return.and.param=@MustCallAlias annotations must appear in pairs (one on a return type and one on a parameter type).%nBut %s owning.override.param=Incompatible ownership for parameter %s.%nfound : no ownership annotation or @NotOwning%nrequired: @Owning%nConsequence: method %s in %s cannot override method %s in %s owning.override.return=Incompatible ownership for return.%nfound : no ownership annotation or @Owning%nrequired: @NotOwning%nConsequence: method %s in %s cannot override method %s in %s -required.method.not.known=The checker cannot determine the must call methods of %s or any of its aliases, so it could not determine if they were called. Typically, this error indicates that you need to write an @MustCall annotation (often on an unconstrained generic type).%nThe type of object is: %s.%nReason for going out of scope: %s +required.method.not.known=The checker cannot determine the must-call methods of %s or any of its aliases, so it could not determine if they were called. Typically, this error indicates that you need to write an @MustCall annotation (often on an unconstrained generic type).%nThe type of object is: %s.%nReason for going out of scope: %s From c0935758522c8ec8bc97a056fc986be076676a54 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Tue, 2 Jun 2026 13:18:49 -0400 Subject: [PATCH 11/15] add must call annotations to InitializationVisitor --- .../checker/initialization/InitializationVisitor.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java index 5cdade6e2df0..ede685ad2a37 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java @@ -20,6 +20,7 @@ import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.VariableElement; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; +import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.nullness.NullnessChecker; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; @@ -49,9 +50,9 @@ * safe initialization should be tracked. For an example, see the {@link NullnessChecker}. */ public class InitializationVisitor< - Factory extends InitializationAnnotatedTypeFactory, + Factory extends InitializationAnnotatedTypeFactory, Value extends CFAbstractValue, - Store extends InitializationStore> + Store extends InitializationStore> extends BaseTypeVisitor { /** The annotation formatter. */ From 5117277dc9817e9b344f3e0861f1846a2d8c8449 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Tue, 2 Jun 2026 13:35:43 -0400 Subject: [PATCH 12/15] finish annotating InitializationVisitor --- .../checker/initialization/InitializationVisitor.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java index 5907029df361..b40aeef032a2 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java @@ -50,9 +50,10 @@ * safe initialization should be tracked. For an example, see the {@link NullnessChecker}. */ public class InitializationVisitor< - Factory extends InitializationAnnotatedTypeFactory, - Value extends CFAbstractValue, - Store extends InitializationStore> + Factory extends + InitializationAnnotatedTypeFactory<@MustCall({}) Value, @MustCall({}) Store, ?, ?>, + Value extends CFAbstractValue<@MustCall({}) Value>, + Store extends InitializationStore<@MustCall({}) Value, @MustCall({}) Store>> extends BaseTypeVisitor { /** The annotation formatter. */ From 86ae6ae8e271b00f0e66627a05cd3c0742e55b01 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 2 Jun 2026 10:59:31 -0700 Subject: [PATCH 13/15] Javadoc --- .../checker/initialization/InitializationVisitor.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java index f57a2f881138..8cdcc4b193b5 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java @@ -47,6 +47,10 @@ * The visitor for the freedom-before-commitment type-system. The freedom-before-commitment * type-system and this class are abstract and need to be combined with another type-system whose * safe initialization should be tracked. For an example, see the {@link NullnessChecker}. + * + * @param the type of the annotated type factory + * @param the type of values in the store + * @param the type of the store */ public class InitializationVisitor< Factory extends InitializationAnnotatedTypeFactory, From 7429f787572a8274d5e69329a8703486c616c2f2 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 2 Jun 2026 12:13:16 -0700 Subject: [PATCH 14/15] Add redundant `messages.properties` file --- .../java/org/checkerframework/checker/regex/util/RegexUtil.java | 1 + .../checkerframework/checker/resourceleak/messages.properties | 1 + 2 files changed, 2 insertions(+) create mode 100644 checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties diff --git a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java index 03c2be9ab007..48e8c33003db 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java @@ -449,6 +449,7 @@ public static boolean noStringMatchesAnyRegex( * @param iterable an iterable * @return a list of the results of applying {@code f} to the elements of {@code iterable} */ + @SuppressWarnings("resourceleak:required.method.not.known") // list elements public static < @KeyForBottom FROM extends @Nullable @UnknownKeyFor Object, @KeyForBottom TO extends @Nullable @UnknownKeyFor Object> diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties new file mode 100644 index 000000000000..b22c9c095dca --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties @@ -0,0 +1 @@ +required.method.not.known=The checker cannot determine the must-call methods of %s or any of its aliases, so it could not determine if they were called. Typically, this error indicates that you need to write an @MustCall annotation (often on an unconstrained generic type).%nThe type of object is: %s.%nReason for going out of scope: %s From cdd7e3e6fdbdefbb3d1af783030562bcedf52134 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 5 Jun 2026 14:36:59 -0700 Subject: [PATCH 15/15] Formatting --- .../main/java/org/checkerframework/afu/annotator/Main.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java index d272f0461db9..a984c58fc2a0 100644 --- a/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java +++ b/annotation-file-utilities/src/main/java/org/checkerframework/afu/annotator/Main.java @@ -205,8 +205,10 @@ private Main() { public static boolean temporaryDebug = false; /** Does the work of {@link #filteredScene}. */ - @SuppressWarnings({"resourceleak:required.method.not.known", // Not relevant to resources - "PMD.UseDiamondOperator"}) + @SuppressWarnings({ + "resourceleak:required.method.not.known", // Not relevant to resources + "PMD.UseDiamondOperator" + }) private static ElementVisitor classFilter = new ElementVisitor() { Void filter(VivifyingMap vm0, VivifyingMap vm1) {