Insert final assert false pass #4985
Conversation
nchong-at-aws
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
There was a problem hiding this comment.
Thank you for this instrumentation pass, it will be very useful!
Apart from the comments, please could you have a go at writing a regression test? You already wrote a few small programs while creating this patch, it should be reasonably easy to adapt them to a test somewhere under the regression/ directory.
|
@nchong-at-aws The way people usually check whether there are inconsistent assumptions is using --cover location. Is that good for your use-case? |
|
@kroening many of our proofs don't have 100% coverage, for various valid reasons. If using @nchong-at-aws's patch is thus very useful because it provides a stateless way of alerting on inconsistent assumptions. This check is also much simpler and much more black-or-white. There can be nuanced reasons for less-than-100% coverage. But it is certainly a bad sign if code instrumented with this pass successfully verifies, no doubt about it. |
|
@kroening Yes, cover is useful for seeing this problem too. This check is another way to sanity check a result. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 11c2f8a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123517019
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
|
@allredj I think this could be because I'm a first time contributor? |
|
This is now getting ready to merge -- may I suggest that you squash the commits into one. |
|
@nchong-at-aws Very probably. You can ignore the message. |
This option takes a function name (usually the test harness entry point) and inserts `assert(false)` at the end of the function body. This assertion is *expected to fail*. If it passes then this may indicate that the test harness has inconsistent assumptions. Note that there are other reasons why the assert may pass (such as insufficient loop unwind depth). It is up to the user to interpret the results.
|
@nchong-at-aws looks like this is good to go, please squash commits |
nchong-at-aws
force-pushed
the
insert-final-assert-false-pass
branch
from
11c2f8a to
639ef81
Compare
Codecov Report
@@ Coverage Diff @@
## develop #4985 +/- ##
===========================================
- Coverage 69.48% 69.24% -0.24%
===========================================
Files 1310 1311 +1
Lines 108813 108471 -342
===========================================
- Hits 75609 75112 -497
- Misses 33204 33359 +155
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 639ef81).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123735093
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
A
goto-instrumentpass that addsassert(false)to the end of a function body---usually expected to be the test harness. If verification still passes then this might indicate inconsistent assumptions. Useful as an automatic check for vacuous proofs.