diff --git a/regression/cbmc/address_of_struct_member/address_of.c b/regression/cbmc/address_of_struct_member/address_of.c new file mode 100644 index 00000000000..99787968b11 --- /dev/null +++ b/regression/cbmc/address_of_struct_member/address_of.c @@ -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; +} diff --git a/regression/cbmc/address_of_struct_member/test.desc b/regression/cbmc/address_of_struct_member/test.desc new file mode 100644 index 00000000000..d5dc9a41012 --- /dev/null +++ b/regression/cbmc/address_of_struct_member/test.desc @@ -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$ +-- +--