Skip to content

Commit 53e2aa4

Browse files
committed
Add regression test for pointer address being found in the trace in new SMT backend.
The difference is that the previous test was effectively exercising NULL and any other pointer value (1, for instance) whereas this one specifically matches the decimal value of 0xDEADBEEF.
1 parent 49645bc commit 53e2aa4

File tree

2 files changed

+20
-0
lines changed

2 files changed

+20
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int *a;
4+
int *b;
5+
__CPROVER_assume(a == 0xDEADBEEF);
6+
7+
__CPROVER_assert(a != b, "should fail as b can also be assigned 0xDEADBEEF");
8+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
pointer_values_2.c
3+
--trace --slice-formula
4+
\[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE
5+
a=\(signed int \*\)3735928559
6+
b=\(signed int \*\)3735928559
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
3735928559 is the decimal value of the hex constant 0xDEADBEEF that
12+
the pointer is assumed to point to in this example.

0 commit comments

Comments
 (0)