Skip to content

Commit 62e5320

Browse files
committed
Test confirming dereferencing a pointer to an indeterminate value
Test uses intervals. Value-sets should also work but we can't write that test yet as we needs more work on asserting value-set equality.
1 parent 7d483d4 commit 62e5320

File tree

4 files changed

+37
-0
lines changed

4 files changed

+37
-0
lines changed
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int unknown;
6+
int a = 10;
7+
8+
int *p = &a;
9+
10+
if(unknown)
11+
a = 15;
12+
13+
int q = *p;
14+
15+
assert(q == a);
16+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
4+
^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom
4+
^\[main.assertion.1\] line 15 assertion q == a: UNKNOWN
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set
4+
^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--

0 commit comments

Comments
 (0)