Repository navigation
Document why removeAnnosFromScene skips declaration annotations - #8127
Conversation
`ASceneWrapper.removeAnnosFromScene` filters the field, return, receiver, and parameter type elements, but not `aclass.tlAnnotationsHere`. That is correct: `annosToIgnore` is populated only by `WholeProgramInferenceScenesStorage.addAnnotationsToATypeElement`, so it never holds a declaration annotation. Say so. Also record, as a TODO, that precondition and postcondition type elements are not visited even though they can hold ignorable annotations. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…o wpi-review-fix-50
|
Warning Review limit reachedNext included review available in 46 minutes. View limit detailsLimit details: You’ve used all 4 included reviews currently available. You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Review configuration: ⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (1)
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (1)
Included review availability: Your plan provides up to 4 included reviews per hour; 2 remain after this review. 📝 WalkthroughWalkthroughThe Javadoc for Priority: ⬇️ Low Merge Risk: ⚪ Minimal · up to This change clarifies annotation-removal behavior and known limitations without changing runtime behavior. No current merge-readiness risk remains. 🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
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. Comment |
The claim that this method visits only type annotations is false for formal parameters: addDeclarationAnnotationToFormalParameter stores the declaration annotation in param.type.tlAnnotationsHere, which is the set that this method removes annotations from. The removal is still safe, but because annosToIgnore records only supported type qualifiers, not because declaration annotations are unvisited. Also, the TODO said that inferred pre- and postconditions are recorded under TypeUseLocation.FIELD. That holds only for contracts about field expressions; contracts about a formal parameter or the receiver are recorded under TypeUseLocation.PARAMETER. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ASceneWrapper.removeAnnosFromScenefilters the field, return, receiver,and parameter type elements, but not
aclass.tlAnnotationsHere. That iscorrect:
annosToIgnoreis populated only byWholeProgramInferenceScenesStorage.addAnnotationsToATypeElement, so itnever holds a declaration annotation. Say so.
Also record, as a TODO, that precondition and postcondition type elements
are not visited even though they can hold ignorable annotations.