Skip to content

Commit 43306d9

Browse files
jezhigginsjezhiggins
committed
value-set pointer differences
1 parent 8d11943 commit 43306d9

19 files changed

+243
-15
lines changed

‎regression/goto-analyzer/pointer-difference-simple/test-constants.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,4 @@ main.c
33
--variable-sensitivity --vsd-pointers constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] line 10 assertion v == 1: SUCCESS
7-
6+
^\[main.assertion.1\] .* assertion v == 1: SUCCESS

‎regression/goto-analyzer/pointer-difference-simple/test-top-bottom.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers top-bottom --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion v == 1: UNKNOWN

‎regression/goto-analyzer/pointer-difference-simple/test-value-set.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion v == 1: SUCCESS

‎regression/goto-analyzer/pointer-differences-non-det/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int non_det;
6+
int array[5];
7+
array[0] = 1;
8+
array[1] = 2;
9+
array[2] = 4;
10+
array[3] = 8;
11+
array[4] = 16;
12+
13+
int *p = array;
14+
if(non_det)
15+
++p;
16+
int *q = array + 4;
17+
if(non_det)
18+
--q;
19+
20+
int offset = (q - p);
21+
assert(offset == 1);
22+
assert(offset == 2);
23+
assert(offset == 3);
24+
assert(offset == 4);
25+
assert(offset == 5);
26+
27+
assert(offset >= 2 && offset <= 4);
28+
29+
assert(offset != 1);
30+
assert(offset != 2);
31+
assert(offset != 3);
32+
assert(offset != 4);
33+
assert(offset != 5);
34+
}

‎regression/goto-analyzer/pointer-differences-non-det/test-constants.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion offset == 1: UNKNOWN$
7+
^\[main.assertion.2\] .* assertion offset == 2: UNKNOWN$
8+
^\[main.assertion.3\] .* assertion offset == 3: UNKNOWN$
9+
^\[main.assertion.4\] .* assertion offset == 4: UNKNOWN$
10+
^\[main.assertion.5\] .* assertion offset == 5: UNKNOWN$
11+
^\[main.assertion.6\] .* assertion offset >= 2 && offset <= 4: UNKNOWN$
12+
^\[main.assertion.7\] .* assertion offset != 1: UNKNOWN$
13+
^\[main.assertion.8\] .* assertion offset != 2: UNKNOWN$
14+
^\[main.assertion.9\] .* assertion offset != 3: UNKNOWN$
15+
^\[main.assertion.10\] .* assertion offset != 4: UNKNOWN$
16+
^\[main.assertion.11\] .* assertion offset != 5: UNKNOWN$

‎regression/goto-analyzer/pointer-differences-non-det/test-top-bottom.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers top-bottom --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion offset == 1: UNKNOWN$
7+
^\[main.assertion.2\] .* assertion offset == 2: UNKNOWN$
8+
^\[main.assertion.3\] .* assertion offset == 3: UNKNOWN$
9+
^\[main.assertion.4\] .* assertion offset == 4: UNKNOWN$
10+
^\[main.assertion.5\] .* assertion offset == 5: UNKNOWN$
11+
^\[main.assertion.6\] .* assertion offset >= 2 && offset <= 4: UNKNOWN$
12+
^\[main.assertion.7\] .* assertion offset != 1: UNKNOWN$
13+
^\[main.assertion.8\] .* assertion offset != 2: UNKNOWN$
14+
^\[main.assertion.9\] .* assertion offset != 3: UNKNOWN$
15+
^\[main.assertion.10\] .* assertion offset != 4: UNKNOWN$
16+
^\[main.assertion.11\] .* assertion offset != 5: UNKNOWN$

‎regression/goto-analyzer/pointer-differences-non-det/test-value-set-constants.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --vsd-values constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion offset == 1: UNKNOWN$
7+
^\[main.assertion.2\] .* assertion offset == 2: UNKNOWN$
8+
^\[main.assertion.3\] .* assertion offset == 3: UNKNOWN$
9+
^\[main.assertion.4\] .* assertion offset == 4: UNKNOWN$
10+
^\[main.assertion.5\] .* assertion offset == 5: UNKNOWN$
11+
^\[main.assertion.6\] .* assertion offset >= 2 && offset <= 4: UNKNOWN$
12+
^\[main.assertion.7\] .* assertion offset != 1: UNKNOWN$
13+
^\[main.assertion.8\] .* assertion offset != 2: UNKNOWN$
14+
^\[main.assertion.9\] .* assertion offset != 3: UNKNOWN$
15+
^\[main.assertion.10\] .* assertion offset != 4: UNKNOWN$
16+
^\[main.assertion.11\] .* assertion offset != 5: UNKNOWN$

‎regression/goto-analyzer/pointer-differences-non-det/test-value-set-intervals.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --vsd-values intervals --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion offset == 1: FAILURE
7+
^\[main.assertion.2\] .* assertion offset == 2: UNKNOWN
8+
^\[main.assertion.3\] .* assertion offset == 3: UNKNOWN
9+
^\[main.assertion.4\] .* assertion offset == 4: UNKNOWN
10+
^\[main.assertion.5\] .* assertion offset == 5: FAILURE
11+
^\[main.assertion.6\] .* assertion offset >= 2 && offset <= 4: SUCCESS
12+
^\[main.assertion.7\] .* assertion offset != 1: SUCCESS
13+
^\[main.assertion.8\] .* assertion offset != 2: UNKNOWN
14+
^\[main.assertion.9\] .* assertion offset != 3: UNKNOWN
15+
^\[main.assertion.10\] .* assertion offset != 4: UNKNOWN
16+
^\[main.assertion.11\] .* assertion offset != 5: SUCCESS

‎regression/goto-analyzer/pointer-differences-non-det/test-value-set-value-set.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --vsd-values set-of-constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion offset == 1: FAILURE
7+
^\[main.assertion.2\] .* assertion offset == 2: UNKNOWN$
8+
^\[main.assertion.3\] .* assertion offset == 3: UNKNOWN$
9+
^\[main.assertion.4\] .* assertion offset == 4: UNKNOWN$
10+
^\[main.assertion.5\] .* assertion offset == 5: FAILURE
11+
^\[main.assertion.6\] .* assertion offset >= 2 && offset <= 4: SUCCESS
12+
^\[main.assertion.7\] .* assertion offset != 1: SUCCESS
13+
^\[main.assertion.8\] .* assertion offset != 2: UNKNOWN$
14+
^\[main.assertion.9\] .* assertion offset != 3: UNKNOWN$
15+
^\[main.assertion.10\] .* assertion offset != 4: UNKNOWN$
16+
^\[main.assertion.11\] .* assertion offset != 5: SUCCESS

‎regression/goto-analyzer/pointer-differences/test-top-bottom.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers top-bottom --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line 16 assertion offset == 4: UNKNOWN$
7+
^\[main.assertion.2\] line 18 assertion offset == 3: UNKNOWN$
8+
^\[main.assertion.3\] line 20 assertion offset == 1: UNKNOWN$
9+
^\[main.assertion.4\] line 22 assertion offset == 0: UNKNOWN$
10+
^\[main.assertion.5\] line 26 assertion offset == 2: UNKNOWN$
11+
^\[main.assertion.6\] line 27 assertion q == p: UNKNOWN$
12+
^\[main.assertion.7\] line 30 assertion offset == 0: UNKNOWN$

0 commit comments

Comments
 (0)