havoc call return value when replacing a call by its contract #6502
Conversation
remi-delmas-3000
force-pushed
the
contract-replacement-havoc-return-value
branch
2 times, most recently
from
af08b3f to
cbc1f68
Compare
…act. This was not done previously and could result in vacuous proofs when multiple calls to a same function were replaced in a same scope.
remi-delmas-3000
force-pushed
the
contract-replacement-havoc-return-value
branch
from
cbc1f68 to
320a9f8
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6502 +/- ##
========================================
Coverage 76.08% 76.08%
========================================
Files 1548 1548
Lines 166387 166399 +12
========================================
+ Hits 126591 126603 +12
Misses 39796 39796
Continue to review full report at Codecov.
|
remi-delmas-3000
added
aws
| @@ -0,0 +1,23 @@ | |||
| int cmp(int i1, int i2) | |||
There was a problem hiding this comment.
Random place for comment: can you please add "Fixes: #6483" to the commit message so that the issue is auto-resolved once this PR is merged?
There was a problem hiding this comment.
I'll go ahead and merge anyway, so this is just for future reference.
| @@ -23,6 +23,7 @@ Date: February 2016 | |||
| #include <goto-instrument/havoc_utils.h> | |||
|
|
|||
| #include <goto-programs/goto_inline.h> | |||
| #include <goto-programs/goto_program.h> | |||
There was a problem hiding this comment.
I don't think this is strictly necessary? (Even the remove_skip.h will already drag in this header.)
This PR adds havoc instructions for the return value of function call when it gets replaced by the function's contract.
This havocking was missing previously and could result in vacuous instances when a same function was replaced more than once in a same scope (e.g. in loops), and the same return value variable was subjected to a superposition of post-conditions that can be contradicting each other.