Fix interaction between @NotOnlyInitialized and @UnderInitialization

[PraneethKulukuri26]

Fixes #7373

This PR fixes an incorrect interaction between @NotOnlyInitialized and
@UnderInitialization that caused a spurious method.invocation error.

The initialization refinement now relies solely on invariant-field
initialization, which matches the Checker Framework documentation.

Testing:

• ./gradlew NullnessTest

[coderabbitai]

📝 Walkthrough

Walkthrough

This pull request modifies the initialization type checking logic in the Checker Framework. The primary change updates InitializationAnnotatedTypeFactory.java to replace a field-based guard with a store-based evaluation that checks for uninitialized invariant fields. When the store is valid and contains no uninitialized invariant fields, the annotation is set to either INITIALIZED for final classes or an UnderInitialization annotation for other classes. Additionally, a new test file InitializationNotOnlyInitialized.java is introduced to validate the interaction between @NotOnlyInitialized and @UnderInitialization annotations.

Pre-merge checks and finishing touches

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 50.00% which is insufficient. The required threshold is 80.00%.	You can run @coderabbitai generate docstrings to improve docstring coverage.

✅ Passed checks (2 passed)

Check name	Status	Explanation
Linked Issues check	✅ Passed	The PR correctly addresses issue #7373 by fixing the initialization refinement logic to rely solely on invariant-field initialization, ensuring @this is recognized as @UnderInitialization(current class) after all non-null fields are assigned.
Out of Scope Changes check	✅ Passed	All changes are directly scoped to fixing the @NotOnlyInitialized and @UnderInitialization interaction: the InitializationAnnotatedTypeFactory modification refines initialization logic, and the new test file verifies the fix.

✨ Finishing touches

• 📝 Generate docstrings

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 1

📜 Review details

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between f976a6b and e8e9526.

📒 Files selected for processing (2)

• checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java (1 hunks)
• checker/tests/nullness/InitializationNotOnlyInitialized.java (1 hunks)

🧰 Additional context used

🧠 Learnings (2)

📓 Common learnings

Learnt from: mernst
Repo: typetools/checker-framework PR: 7354
File: annotation-file-utilities/tests/LocalMultipleManyMethodsShifted.java:14-14
Timestamp: 2025-11-02T02:18:00.536Z
Learning: In the Checker Framework repository, when doing refactoring PRs (such as preferring isEmpty() over size() comparisons), test files should not be changed. Tests should remain stable to preserve their exact patterns for annotation processing and bytecode verification purposes.

📚 Learning: 2025-10-22T20:41:01.112Z

Learnt from: kelloggm
Repo: typetools/checker-framework PR: 7166
File: checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java:128-136
Timestamp: 2025-10-22T20:41:01.112Z
Learning: In checker/src/main/java/org/checkerframework/checker/collectionownership/CollectionOwnershipAnnotatedTypeFactory.java, prefer instance fields over static state for analysis caches (e.g., maps keyed by Tree/Block). There is at most one ATF per running checker, so static mutable fields are discouraged.

Applied to files:

• checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java

🔇 Additional comments (1)

checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java (1)

515-523: The code change appears correct for the stated PR objective.

The call to getUninitializedInvariantFields(store, path, false, Collections.emptyList()).isEmpty() correctly checks whether all invariant fields are initialized in the given store without applying any receiver annotation filters. This aligns with the PR goal to rely solely on invariant-field initialization. No evidence suggests this parameter choice is problematic.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

Test appears incomplete and doesn't validate the fix.

Based on issue #7373 and the PR objectives, the test should demonstrate:

1. A class with both @NotOnlyInitialized and @NonNull fields
2. A private method that should be callable on this
3. A constructor that assigns both fields, then calls the private method
4. Verification that the method call succeeds without producing the spurious method.invocation error

The current test only defines a parent class with a single @NonNull field and doesn't exercise the interaction between @NotOnlyInitialized and @UnderInitialization.

🔎 Suggested test expansion

 class Parent {
   @NonNull String parentField;
+  @NotOnlyInitialized Object notOnlyInitField;

   Parent() {
     parentField = "parent";
+    notOnlyInitField = new Object();
+    helperMethod();  // This should not produce an error after the fix
+  }
+
+  private void helperMethod() {
+    // Method that requires @UnderInitialization(Parent) or better
   }
 }

🤖 Prompt for AI Agents

In checker/tests/nullness/InitializationNotOnlyInitialized.java around lines 1
to 13, the test is incomplete: it only defines a Parent with a @NonNull field
but does not exercise the interaction between @NotOnlyInitialized and
@UnderInitialization or verify that a private method call in a constructor after
initializing fields does not produce a spurious method.invocation error. Update
the file to add a subclass that declares a @NotOnlyInitialized @NonNull field, a
second @NonNull field, a private method that uses those fields, and a
constructor that assigns both fields and then calls the private method (ensuring
the constructor parameter is annotated @UnderInitialization(ClassName.class) if
needed); the test should compile without errors to confirm the method call is
allowed. Ensure the new code is included in the test harness so the compile run
will fail if the spurious method.invocation error reappears.

[PraneethKulukuri26]

The failures in misc_jdk25 appear to be from the documentation build
(HeVeA/LaTeX warnings such as unsupported commands and undefined citations).

These failures are unrelated to this PR’s changes; all checker, inference,
and junit tests pass.

I believe this is an environment-related docs issue in CI rather than a
regression caused by this change.