-
Notifications
You must be signed in to change notification settings - Fork 262
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Enable all struct tests under regression/cbmc/
for new SMT backend
#7809
Enable all struct tests under regression/cbmc/
for new SMT backend
#7809
Conversation
5a4ac6e
to
16b0492
Compare
@@ -1,4 +1,4 @@ | |||
CORE smt-backend | |||
CORE smt-backend new-smt-backend | |||
main.c | |||
--trace --z3 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Despite the --z3
flag here, this does run with the new SMT backend when the test.pl
profile for the new-smt-backend
is run.
I have verified this locally, but I'm not sure I understand why that is - I speculate that the handling for the --incremental-smt2-solver
flag is earlier, and path dependence handles the rest, but I haven't looked too close.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That matches my understanding. The --z3
flag is ignored when --incremental-smt2-solver
is specified. Unfortunately the control flow for the solver_factory
where this is handled is not always the easiest to follow.
16b0492
to
c0f5b72
Compare
Codecov ReportAll modified lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #7809 +/- ##
========================================
Coverage 78.62% 78.63%
========================================
Files 1701 1700 -1
Lines 195975 195974 -1
========================================
+ Hits 154087 154095 +8
+ Misses 41888 41879 -9 ☔ View full report in Codecov by Sentry. |
c0f5b72
to
eadb111
Compare
ref = &var_expr.line; | ||
else | ||
ref = &other_expr.line; | ||
__CPROVER_assert(*ref != 34, "expected failure: ref == 34"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
⛏️ I am not sure this is a great test of the new SMT back end. The line
field of expr
will be at offset zero. It would be good to include taking the address of a field with a non-zero offset such as the comment
field and to check that the resulting size of the offset is as expected.
Enable all struct tests under
regression/cbmc/
for the new SMT backend (by marking them asnew-smt-backend
) and add two more regression tests for the case where the address-of operator is applied to a struct member.