A predicate to validate all pointer derefs in an expression AST #6365
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
SaswatPadhi
requested review from
kroening,
remi-delmas-3000,
feliperodri and
jimgrundy
SaswatPadhi
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel and
tautschnig
as code owners
SaswatPadhi
force-pushed
the
chain-validate
branch
from
f97776b to
a5ec09d
Compare
SaswatPadhi
changed the title
SaswatPadhi
force-pushed
the
chain-validate
branch
from
a5ec09d to
c211860
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6365 +/- ##
===========================================
+ Coverage 75.90% 75.91% +0.01%
===========================================
Files 1515 1517 +2
Lines 164005 164024 +19
===========================================
+ Hits 124484 124515 +31
+ Misses 39521 39509 -12
Continue to review full report at Codecov.
|
|
This should not go into |
feliperodri
requested changes
Sep 27, 2021
jimgrundy
reviewed
Sep 27, 2021
| { | ||
| binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]}; | ||
| equality_conjunctions[i] = | ||
| and_exprt(equality_conjunctions[i - 1], component_i_equality); |
There was a problem hiding this comment.
The lack of test coverage reported for this loop body seems concerning.
src/goto-instrument/havoc_utils.cpp
Outdated
| append_safe_havoc_code_for_expr(source_location, ns, expr, dest, [&]() { | ||
| append_object_havoc_code_for_expr(source_location, expr, dest); | ||
| }); | ||
| continue; |
There was a problem hiding this comment.
Lack of test coverage on this conditional is a concern
There was a problem hiding this comment.
Good point. We do have a test case for multi-dimensional decreases clauses, and it seems to be working as expected. I can take a closer look at it, but I will probably split any fixes (if needed) into a separate PR, and keep this one only about validity checking.
In this change, we move two of the "static" functions within contracts.cpp to utils.cpp (a new file in contracts module). We also fix the #include dependence -- assigns should not #include contracts.h, it should be the other way round.
SaswatPadhi
force-pushed
the
chain-validate
branch
4 times, most recently
from
76babcb to
59bfc73
Compare
SaswatPadhi
force-pushed
the
chain-validate
branch
from
59bfc73 to
10dc391
Compare
peterschrammel
approved these changes
Sep 29, 2021
+ checking containment in assigns clause verification + havocing only valid memory locations in assigns clause replacement + havocing only valid memory locations in loop contract application + creating history snapshots only for valid `old` expressions
SaswatPadhi
force-pushed
the
chain-validate
branch
from
10dc391 to
fcca0e5
Compare
4 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is useful for:
oldexpressionsThe feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).