Warn when using the top type in a pre- or post-condition annotation

[mernst]

Depends on #6254.

[jyoo980]

Thanks! I'm in favour of merging this over my work in #6409

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: c3a36eb3-bc71-4f32-92f4-bafc1208ab1e

📥 Commits

Reviewing files that changed from the base of the PR and between 1724ac1 and cd1da31.

📒 Files selected for processing (3)

• framework/tests/flow/ContractsOverridingSubtyping.java
• framework/tests/flow/Postcondition.java
• framework/tests/flow/Precondition.java

---

📝 Walkthrough

Walkthrough

Adds detection and reporting for precondition and postcondition contract annotations that use a top-level qualifier. Changes include: new tracking and detection logic in BaseTypeVisitor for pre/post-condition annotations, a new message key for top-type contract qualifiers, increased visibility and documentation for ContractsFromMethod#getQualifierEnforcedByContractAnnotation, and test additions/annotations exercising top-type contract warnings. Also removes a trailing blank line in a test resource JAIF file.

Possibly related PRs

• Make canonicalAnnotation return a non-null value #7505: Modifies the implementation and canonicalization handling of getQualifierEnforcedByContractAnnotation, which this PR also exposes and documents.

Suggested reviewers

• smillst
• msridhar

🚥 Pre-merge checks | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 45.00% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

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

Tip

Try Coding Plans. Let us write the prompt for your AI agent so you can ship faster (with fewer bugs).
Share your feedback on Discord.

---

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: 2

♻️ Duplicate comments (2)

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java (2)

2479-2488: ⚠️ Potential issue | 🟠 Major

Unsupported meta-annotations are currently treated as supported in detection set.

The set includes PreconditionAnnotation and PostconditionAnnotation, but the TODO in the warning path states qualifier extraction does not work for them. This causes silent missed warnings for those annotation types.

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`
around lines 2479 - 2488, The preAndPostConditionAnnotations set incorrectly
includes PreconditionAnnotation and PostconditionAnnotation even though
qualifier extraction for those meta-annotations is not supported; update the
preAndPostConditionAnnotations field to remove
PreconditionAnnotation.class.getName() and
PostconditionAnnotation.class.getName() (or otherwise exclude them from
detection) and add a short comment referencing the existing TODO about
unsupported qualifier extraction so they are not treated as supported and won't
silently suppress warnings; ensure the change targets the
preAndPostConditionAnnotations declaration and mentions the exact names
PreconditionAnnotation and PostconditionAnnotation so future maintainers see why
they were excluded.

---

2408-2408: ⚠️ Potential issue | 🟠 Major

Remove debug stdout from annotation visiting path.

Line 2408 prints for every visited contract annotation and will pollute compiler/test output.

🧹 Proposed fix

-      System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName, tree);

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`
at line 2408, Remove the debug stdout in BaseTypeVisitor by deleting the
System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName,
tree) call; if you need to retain diagnostic information, replace it with the
checker-framework messaging/logging mechanism (e.g.,
processingEnv.getMessager().printMessage or the project's logger) using the same
variables (anno, annoName, tree) so compiler/test output is not polluted.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`:
- Line 2418: The warning call in BaseTypeVisitor uses
checker.reportWarning(tree, "contracts.toptype", contractQualName) but the
message "contracts.toptype" expects two %s placeholders; update the
checker.reportWarning invocation to pass both formatting arguments in the
correct order (keep contractQualName and add the top-type qualifier/name
variable used in this method, e.g., topType, topQualName, or a call that obtains
the top type's qualified name) so both placeholders are filled (locate the call
site in BaseTypeVisitor and supply the second argument alongside
contractQualName).

In
`@framework/src/main/java/org/checkerframework/common/basetype/messages.properties`:
- Line 93: The diagnostic message for key contracts.toptype contains a typo —
change the word "qualifer" to "qualifier" in the message string for
contracts.toptype so the user-facing text reads "the top qualifier %s in a
contract annotation %s has no effect"; update the value associated with the
contracts.toptype property accordingly.

---

Duplicate comments:
In
`@framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java`:
- Around line 2479-2488: The preAndPostConditionAnnotations set incorrectly
includes PreconditionAnnotation and PostconditionAnnotation even though
qualifier extraction for those meta-annotations is not supported; update the
preAndPostConditionAnnotations field to remove
PreconditionAnnotation.class.getName() and
PostconditionAnnotation.class.getName() (or otherwise exclude them from
detection) and add a short comment referencing the existing TODO about
unsupported qualifier extraction so they are not treated as supported and won't
silently suppress warnings; ensure the change targets the
preAndPostConditionAnnotations declaration and mentions the exact names
PreconditionAnnotation and PostconditionAnnotation so future maintainers see why
they were excluded.
- Line 2408: Remove the debug stdout in BaseTypeVisitor by deleting the
System.out.printf("anno = %s for annoName = %s for tree = %s%n", anno, annoName,
tree) call; if you need to retain diagnostic information, replace it with the
checker-framework messaging/logging mechanism (e.g.,
processingEnv.getMessager().printMessage or the project's logger) using the same
variables (anno, annoName, tree) so compiler/test output is not polluted.

---

ℹ️ Review info

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 60f5c7f and 1724ac1.

📒 Files selected for processing (7)

• annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif
• framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java
• framework/src/main/java/org/checkerframework/common/basetype/messages.properties
• framework/src/main/java/org/checkerframework/framework/util/ContractsFromMethod.java
• framework/tests/flow/ContractsOverridingSubtyping.java
• framework/tests/flow/Postcondition.java
• framework/tests/flow/Precondition.java

💤 Files with no reviewable changes (1)

• annotation-file-utilities/src/test/resources/annotations/tests/classfile/all-annotations.jaif