Add support for incremental SMT traces containing C_bool #6628
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
thomasspriggs
requested review from
chris-ryder,
NlightNFotis,
peterschrammel and
TGWDB
as code owners
thomasspriggs
force-pushed
the
tas/smt2_c_bool
branch
from
38c8b73 to
5a5bd84
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6628 +/- ##
========================================
Coverage 76.64% 76.65%
========================================
Files 1579 1580 +1
Lines 181487 181560 +73
========================================
+ Hits 139109 139168 +59
- Misses 42378 42392 +14
Continue to review full report at Codecov.
|
TGWDB
approved these changes
Feb 2, 2022
thomasspriggs
force-pushed
the
tas/smt2_c_bool
branch
from
5a5bd84 to
a9f78e6
Compare
NlightNFotis
reviewed
Feb 2, 2022
| int x, y; | ||
| bool equal = x == y; | ||
| __CPROVER_assert(equal, "Assert of integer equality."); | ||
| __CPROVER_assert(!equal, "Assert of not integer equality."); |
There was a problem hiding this comment.
⛏️ What does not integer equality mean? Do you mean inequality in this context?
There was a problem hiding this comment.
I mean the not operator is being applied to the result of testing for integer equality. This is equivalent to testing for inequality with the != operator, so the distinction is not really important here. The main purpose of this assertion is to ensure that the output traces include instances where equal is assigned a true value and equal is assigned a false value.
An "unsupported type" invariant violation would previously have been encountered when attempting to generate traces featuring `c_bool_typet`. This is due to `c_bool_typet` not being castable to `integer_bitvector_typet`.
The following commit is adding an include which will cause the updated version of clang-format to re-order the includes. Doing the reorder in advance will make it clear which include is added.
thomasspriggs
force-pushed
the
tas/smt2_c_bool
branch
from
a9f78e6 to
a638644
Compare
NlightNFotis
approved these changes
Feb 2, 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.
An "unsupported type" invariant violation would previously have been
encountered when attempting to generate traces featuring
c_bool_typet.This is due to
c_bool_typetnot being castable tointeger_bitvector_typet.