goto-symex: print status note and conditional warning for self-loops #6624
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
tautschnig
requested review from
kroening,
peterschrammel and
romainbrenguier
as code owners
Unless CBMC is invoked with --no-self-loops-to-assumptions, self-loops are replaced by assumptions. This commit now introduces a status output that such replacement is happening, and also a warning when --unwinding-assertions is set: as the loop is replaced by an assumption, no unwinding assertions can possible be generated. This behaviour may be unexpected by the user, and we should therefore let them know what is going on. Fixes: diffblue#6433
tautschnig
force-pushed
the
features/self-loop-status-output
branch
from
59a738e to
3f03433
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6624 +/- ##
========================================
Coverage 76.64% 76.64%
========================================
Files 1579 1579
Lines 181479 181487 +8
========================================
+ Hits 139101 139109 +8
Misses 42378 42378
Continue to review full report at Codecov.
|
peterschrammel
approved these changes
Feb 1, 2022
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.
Unless CBMC is invoked with --no-self-loops-to-assumptions, self-loops
are replaced by assumptions. This commit now introduces a status output
that such replacement is happening, and also a warning when
--unwinding-assertions is set: as the loop is replaced by an assumption,
no unwinding assertions can possible be generated. This behaviour may be
unexpected by the user, and we should therefore let them know what is
going on.
Fixes: #6433