-
Notifications
You must be signed in to change notification settings - Fork 431
Refine upper bound for startsWith/endsWith #7447
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.
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
base: master
Are you sure you want to change the base?
Refine upper bound for startsWith/endsWith #7447
Conversation
📝 WalkthroughWalkthroughAdds cached lookups for three String methods as private fields initialized in the constructor via TreeUtils and imports ExpressionTree, ExecutableElement, and TreeUtils. Overrides processConditionalPostconditions to handle String.startsWith(String) and String.endsWith(String): when receiver and argument are resolvable, creates a LessThanLengthOf qualifier (offset -1) for the receiver and, if insertable, inserts a corresponding refinement for argument.length() into the then-branch CFStore while still calling super. Tests add endsWith-based cases, remove a prior suppression, and add negative tests. Docs update the contributors list with additional names. 🚥 Pre-merge checks | ✅ 1✅ Passed checks (1 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing touches
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In
`@checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundTransfer.java`:
- Around line 754-796: The code unconditionally calls
thenStore.insertValue(argLengthExpr, anno) inside
processConditionalPostconditions for startsWith/endsWith; guard this with
CFAbstractStore.canInsertJavaExpression(argLengthExpr) (same pattern used in
visitLengthAccess) so you only call thenStore.insertValue(...) when
canInsertJavaExpression(argLengthExpr) returns true, preserving existing checks
(unknowns/determinism) and avoiding attempts to insert non-insertable
expressions.
checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundTransfer.java
Show resolved
Hide resolved
a0e8db9 to
781c9de
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@docs/manual/contributors.tex`:
- Around line 154-155: The contributor list has "Zhiping Cai, shubhamk0205." out
of alphabetical order; move the "shubhamk0205" entry from the end into the
correct alphabetized position among the other "Shubham …" contributors (so the
list remains alphabetically ordered) and ensure punctuation/spacing
(comma/period) matches the surrounding entries (e.g., keep the trailing period
only at the end of the full list).
781c9de to
2ff72bb
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@checker/tests/index/StartsEndsWith.java`:
- Around line 30-40: The comment above removeSuffix should be expanded to
clearly state this test intentionally demonstrates a checker limitation:
although endsWith(suffix) implies suffix.length() <= methodName.length(), the
checker cannot prove the arithmetic upper bound used in methodName.substring(0,
methodName.length() - suffix.length()), so the test expects an error; update the
comment to state that this is a known limitation test for arithmetic expression
refinement and mention the targeted expression (methodName.length() -
suffix.length()) and the expected diagnostic on the substring call.
♻️ Duplicate comments (1)
docs/manual/contributors.tex (1)
154-156: Alphabetical order is broken and duplicate entry exists."Shubham Kapoor" should be inserted alphabetically near line 134 (after "Shubham Raj" or before "Sidney Monteiro"). Also, "shubhamk0205" appears to be a GitHub handle—if this is the same person as "Shubham Kapoor," only one entry is needed. If they are different contributors, "shubhamk0205" should also be placed alphabetically (or converted to a real name for consistency with the rest of the list).
2ff72bb to
694943a
Compare
|
@mernst the fix causes |
|
Please
Now, CI for this pull request will use it and should no longer fail. Thanks. |
solves #5201
previously , code checked
if (methodName.startsWith(prefix))we know by intuition that prefix length is less than or equal to method length . but the checker doesnt know this and gives us a false warning .to solve this when the code calls this method and returns true , then our code tells checker that prefix length is less or equal to the method length and doesnt give us warning .
also i have removed suppress warning annotation .