-
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--pointer-check | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
-win32 | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
struct_bytewise.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
FUTURE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.i | ||
--32 | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--pointer-check | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--unwind 5 | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
struct expr | ||
{ | ||
int line; | ||
char comment; | ||
}; | ||
|
||
int main(int argc, char *argv[]) | ||
{ | ||
struct expr var_expr = {42, 'a'}; | ||
struct expr other_expr = {34, 'b'}; | ||
unsigned int nondet; | ||
int *ref; | ||
if(nondet) | ||
ref = &var_expr.line; | ||
else | ||
ref = &other_expr.line; | ||
__CPROVER_assert(*ref != 34, "expected failure: ref == 34"); | ||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE new-smt-backend | ||
address_of.c | ||
|
||
\[main\.assertion\.1\] line \d+ expected failure: ref == 34: FAILURE | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^VERIFICATION FAILED$ | ||
-- | ||
-- |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
struct aux | ||
{ | ||
char comment; | ||
}; | ||
|
||
struct expr | ||
{ | ||
int line; | ||
struct aux *info; | ||
}; | ||
|
||
int main(void) | ||
{ | ||
struct aux info1 = {'a'}; | ||
struct aux info2 = {'b'}; | ||
struct expr var_expr = {42, &info1}; | ||
struct expr other_expr = {34, &info2}; | ||
unsigned int nondet; | ||
char *ref; | ||
if(nondet) | ||
ref = &var_expr.info->comment; | ||
else | ||
ref = &other_expr.info->comment; | ||
__CPROVER_assert(*ref != 'b', "expected failure: ref == 'b'"); | ||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE new-smt-backend | ||
address_of_rec.c | ||
|
||
\[main\.assertion\.1\] line \d+ expected failure: ref == 'b': FAILURE | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^VERIFICATION FAILED$ | ||
-- | ||
-- |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE gcc-only | ||
CORE gcc-only new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--pointer-check --bounds-check | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=10$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE smt-backend | ||
CORE smt-backend new-smt-backend | ||
main.c | ||
--trace --z3 | ||
^EXIT=0$ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Despite the I have verified this locally, but I'm not sure I understand why that is - I speculate that the handling for the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. That matches my understanding. The |
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^VERIFICATION SUCCESSFUL$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--bounds-check --pointer-check | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
--pointer-check --bounds-check | ||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
CORE | ||
CORE new-smt-backend | ||
main.c | ||
|
||
^EXIT=0$ | ||
|
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 ofexpr
will be at offset zero. It would be good to include taking the address of a field with a non-zero offset such as thecomment
field and to check that the resulting size of the offset is as expected.