Skip to content

Fix interaction between @NotOnlyInitialized and @UnderInitialization #7426

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
PraneethKulukuri26 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix interaction between @NotOnlyInitialized and @UnderInitialization #7426

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 7 additions & 10 deletions .../java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -512,16 +512,13 @@ protected void setSelfTypeInInitializationCode(
// - if the class is final, this is @Initialized
// - otherwise, this is @UnderInitialization(CurrentClass) as
// there might still be subclasses that need initialization.
if (areAllFieldsInitializedOnly(enclosingClass)) {
Store store = getStoreBefore(tree);
if (store != null
&& getUninitializedInvariantFields(store, path, false, Collections.emptyList())
.isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
Store store = getStoreBefore(tree);
if (store != null
&& getUninitializedInvariantFields(store, path, false, Collections.emptyList()).isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
}

Expand Down
13 changes: 13 additions & 0 deletions checker/tests/nullness/InitializationNotOnlyInitialized.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// @test
// @summary Reproduce incorrect interaction between @NotOnlyInitialized and @UnderInitialization
// @compile
import org.checkerframework.checker.initialization.qual.*;
import org.checkerframework.checker.nullness.qual.*;

class Parent {
@NonNull String parentField;

Parent() {
parentField = "parent";
}
}
Comment on lines +1 to +13
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai bot Dec 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ 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.

Loading