-
Notifications
You must be signed in to change notification settings - Fork 250
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
[CONTRACTS] Refactor quantified symbol detection for loop contracts #8299
Conversation
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #8299 +/- ##
===========================================
- Coverage 78.35% 78.32% -0.04%
===========================================
Files 1721 1721
Lines 188278 188338 +60
Branches 18460 18452 -8
===========================================
- Hits 147523 147511 -12
- Misses 40755 40827 +72 ☔ View full report in Codecov by Sentry. |
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.
We don't seem to have tests for all the possible operators matched in add_quantified_variable
(ternary op?)
@@ -376,7 +376,9 @@ void add_quantified_variable( | |||
auto &unary_expression = to_unary_expr(expression); | |||
add_quantified_variable(symbol_table, unary_expression.op(), mode); | |||
} | |||
if(expression.id() == ID_notequal || expression.id() == ID_implies) | |||
if( |
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.
Would it be possible to transform forall
and exists
nodes without having to explicitly match on other irep_ids
? Maybe using exprt::visit_post
or exprt::visit_pre
?
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.
Rewrote the whole function with visit_pre
.
657328c
to
08d8491
Compare
Resolves: #8298
In loop contracts, we replace quantified variables with a tmp variable and add the tmp variable to the symbol map. However, the detection of the quantified variables is not complete now---it does not include equal expression.
This PR add equal expressions