CONTRACTS: add doc for loop assigns inference #8516
Conversation
qinheping
requested review from
tautschnig,
feliperodri and
remi-delmas-3000
as code owners
|
Paste @rod-chapman's comment in qinheping#4 here:
|
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #8516 +/- ##
========================================
Coverage 78.84% 78.84%
========================================
Files 1728 1728
Lines 198775 198766 -9
Branches 18406 18385 -21
========================================
Hits 156719 156719
+ Misses 42056 42047 -9 ☔ View full report in Codecov by Sentry. 🚨 Try these New Features:
|
|
|
||
| When loop invariant clauses are specified but loop assigns are not, CBMC will infer | ||
| loop assigns clauses and use them to apply loop contracts. The idea of the inference | ||
| is to include all the left hand side of assignments in the loop. |
There was a problem hiding this comment.
@rod-chapman 's comment in qinheping#4
What if a reference is taken as a r-value. i.e. a function call that contains f(&x, b) - is that an assign to x?
We inline f and check if there is any assignment to targets aliasing x in the inlined body. See incr function in test_loop_assigns_inference as an example.
| 3. assigns targets widening. | ||
|
|
||
| We do the function inlining first so that we can infer those assigns targets | ||
| hidden in the function call, for example, `j` is assigned to in `set_j`. |
There was a problem hiding this comment.
@rod-chapman 's comment in qinheping#4
What if the body of a called unit is not available, but that unit does have contracts, and --replace-all-with-contract has been specified? If you can't inline what happens? Can you get the info you need from the contract of the called unit alone?
Good point. As a next step, we will use functions' assigns for those with contracts instead of inlining them.
This PR add an example, explanation, and limitation of the loop assigns inference used in DFCC contracts.