Skip to content

Commit e6f6970

Browse files
martin-csmartin-cs
authored
Merge pull request #5678 from jezhiggins/vsd-pointer-arithmetic
VSD pointer arithmetic, differencing, and comparisons
2 parents b65fee1 + 4844d22 commit e6f6970

File tree

78 files changed

+1451
-124
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

78 files changed

+1451
-124
lines changed

‎regression/goto-analyzer/pointer-arithmetic-simple/main.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int a[2];
6+
int *p = a;
7+
8+
++p;
9+
assert(p == &(a[1]));
10+
11+
--p;
12+
assert(p == a);
13+
}

‎regression/goto-analyzer/pointer-arithmetic-simple/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --vsd-values constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line 9 assertion p == \&\(a\[1\]\): SUCCESS
7+
^\[main.assertion.2\] line 12 assertion p == a: SUCCESS

‎regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
struct int_pair
6+
{
7+
int a;
8+
int b;
9+
};
10+
struct int_pair x[2];
11+
12+
int *pa = &(x[0].a);
13+
14+
assert(pa == &(x[0].a));
15+
assert(pa != &(x[0].a));
16+
assert(pa == &(x[0].b));
17+
assert(pa != &(x[0].b));
18+
assert(pa == &(x[1].a));
19+
assert(pa != &(x[1].a));
20+
assert(pa == &(x[1].b));
21+
assert(pa != &(x[1].b));
22+
}

‎regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-constants.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion pa == &\(x\[0\].a\): SUCCESS
7+
^\[main.assertion.2\] .* assertion pa != &\(x\[0\].a\): FAILURE
8+
^\[main.assertion.3\] .* assertion pa == &\(x\[0\].b\): FAILURE
9+
^\[main.assertion.4\] .* assertion pa != &\(x\[0\].b\): SUCCESS
10+
^\[main.assertion.5\] .* assertion pa == &\(x\[1\].a\): FAILURE
11+
^\[main.assertion.6\] .* assertion pa != &\(x\[1\].a\): SUCCESS
12+
^\[main.assertion.7\] .* assertion pa == &\(x\[1\].b\): FAILURE
13+
^\[main.assertion.8\] .* assertion pa != &\(x\[1\].b\): SUCCESS

‎regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-value-set.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion pa == &\(x\[0\].a\): SUCCESS
7+
^\[main.assertion.2\] .* assertion pa != &\(x\[0\].a\): FAILURE
8+
^\[main.assertion.3\] .* assertion pa == &\(x\[0\].b\): FAILURE
9+
^\[main.assertion.4\] .* assertion pa != &\(x\[0\].b\): SUCCESS
10+
^\[main.assertion.5\] .* assertion pa == &\(x\[1\].a\): FAILURE
11+
^\[main.assertion.6\] .* assertion pa != &\(x\[1\].a\): SUCCESS
12+
^\[main.assertion.7\] .* assertion pa == &\(x\[1\].b\): FAILURE
13+
^\[main.assertion.8\] .* assertion pa != &\(x\[1\].b\): SUCCESS

‎regression/goto-analyzer/pointer-comparison-equality-different-target/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int a[2];
6+
int b[2];
7+
int c;
8+
9+
int *p = &(a[0]);
10+
int *q = &(b[1]);
11+
int *r = &c;
12+
13+
assert(p == q);
14+
assert(p == r);
15+
assert(q == r);
16+
17+
assert(p != q);
18+
assert(p != r);
19+
assert(q != r);
20+
}

‎regression/goto-analyzer/pointer-comparison-equality-different-target/test-constants.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion p == q: FAILURE
7+
^\[main.assertion.2\] .* assertion p == r: FAILURE
8+
^\[main.assertion.3\] .* assertion q == r: FAILURE
9+
^\[main.assertion.4\] .* assertion p != q: SUCCESS
10+
^\[main.assertion.5\] .* assertion p != r: SUCCESS
11+
^\[main.assertion.6\] .* assertion q != r: SUCCESS

‎regression/goto-analyzer/pointer-comparison-equality-different-target/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-different-target/test-value-set.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-same-target-2/main.c

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 a[2];
6+
7+
int *p = &(a[0]);
8+
int *q = &(a[1]);
9+
int *r = p + 1;
10+
11+
assert(p == q || p == r);
12+
assert(q == p || q == r);
13+
14+
assert(p != q && p != r);
15+
assert(q != p && q != r);
16+
}

‎regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-constants.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion p == q || p == r: FAILURE
7+
^\[main.assertion.2\] .* assertion q == p || q == r: SUCCESS
8+
^\[main.assertion.3\] .* assertion p != q && p != r: SUCCESS
9+
^\[main.assertion.4\] .* assertion q != p && q != r: FAILURE

‎regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-value-set.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-same-target/main.c

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 a[2];
6+
7+
int *p = &(a[0]);
8+
int *q = &(a[1]);
9+
int *r = p + 1;
10+
11+
assert(p == q);
12+
assert(r == q);
13+
14+
assert(p != q);
15+
assert(r != q);
16+
}

‎regression/goto-analyzer/pointer-comparison-equality-same-target/test-constants.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion p == q: FAILURE
7+
^\[main.assertion.2\] .* assertion r == q: SUCCESS
8+
^\[main.assertion.3\] .* assertion p != q: SUCCESS
9+
^\[main.assertion.4\] .* assertion r != q: FAILURE

‎regression/goto-analyzer/pointer-comparison-equality-same-target/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-same-target/test-value-set.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-struct-members/main.c

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
struct int_pair
6+
{
7+
int a;
8+
int b;
9+
};
10+
struct int_pair x = {0, 1};
11+
12+
int *pa = &(x.a);
13+
14+
assert(pa == &(x.a));
15+
assert(pa != &(x.a));
16+
17+
int *pb = &(x.b);
18+
assert(pb == &(x.a));
19+
assert(pb != &(x.a));
20+
21+
struct int_pair y = {0, 1.0};
22+
assert(pa == &(y.a));
23+
assert(pa != &(y.a));
24+
25+
int *pb = &(x.b);
26+
assert(pb == &(y.a));
27+
assert(pb != &(y.a));
28+
}

‎regression/goto-analyzer/pointer-comparison-equality-struct-members/test-constants.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion pa == &\(x.a\): SUCCESS
7+
^\[main.assertion.2\] .* assertion pa != &\(x.a\): FAILURE
8+
^\[main.assertion.3\] .* assertion pb == &\(x.a\): FAILURE
9+
^\[main.assertion.4\] .* assertion pb != &\(x.a\): SUCCESS
10+
^\[main.assertion.5\] .* assertion pa == &\(y.a\): FAILURE
11+
^\[main.assertion.6\] .* assertion pa != &\(y.a\): SUCCESS
12+
^\[main.assertion.7\] .* assertion pb == &\(y.a\): FAILURE
13+
^\[main.assertion.8\] .* assertion pb != &\(y.a\): SUCCESS

‎regression/goto-analyzer/pointer-comparison-equality-struct-members/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-equality-struct-members/test-value-set.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-pointers value-set --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] .* assertion pa == &\(x.a\): SUCCESS
7+
^\[main.assertion.2\] .* assertion pa != &\(x.a\): FAILURE
8+
^\[main.assertion.3\] .* assertion pb == &\(x.a\): FAILURE
9+
^\[main.assertion.4\] .* assertion pb != &\(x.a\): SUCCESS
10+
^\[main.assertion.5\] .* assertion pa == &\(y.a\): FAILURE
11+
^\[main.assertion.6\] .* assertion pa != &\(y.a\): SUCCESS
12+
^\[main.assertion.7\] .* assertion pb == &\(y.a\): FAILURE
13+
^\[main.assertion.8\] .* assertion pb != &\(y.a\): SUCCESS

‎regression/goto-analyzer/pointer-comparison-inequality-different-target/main.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int a[2];
6+
int b[2];
7+
8+
int *p = &(a[0]);
9+
int *q = &(b[1]);
10+
11+
// p and q point to different base objects so these
12+
// comparisons are undefined. Consequently we evaluate
13+
// them as UNKNOWN
14+
assert(p <= q);
15+
assert(p < q);
16+
assert(p >= q);
17+
assert(p > q);
18+
19+
assert(q <= p);
20+
assert(q < p);
21+
assert(q >= p);
22+
assert(q > p);
23+
}

‎regression/goto-analyzer/pointer-comparison-inequality-different-target/test-constants.desc

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

‎regression/goto-analyzer/pointer-comparison-inequality-different-target/test-top-bottom.desc

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

‎regression/goto-analyzer/pointer-comparison-inequality-different-target/test-value-set.desc

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

‎regression/goto-analyzer/pointer-comparison-inequality-same-target/main.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int a[2];
6+
7+
int *p = &(a[0]);
8+
int *q = &(a[1]);
9+
10+
assert(p <= a);
11+
assert(p < a);
12+
assert(p >= a);
13+
assert(p > a);
14+
15+
assert(p <= q);
16+
assert(p < q);
17+
assert(p >= q);
18+
assert(p > q);
19+
20+
assert(q <= p);
21+
assert(q < p);
22+
assert(q >= p);
23+
assert(q > p);
24+
}

0 commit comments

Comments
 (0)