Skip to content

Commit 5303a9d

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6866 from NlightNFotis/smt_pointer_arithmetic_conversion_final
Add support for conversion of pointer arithmetic expressions to new SMT backend.
2 parents 0de701c + 34b2985 commit 5303a9d

20 files changed

+443
-15
lines changed

‎regression/cbmc-incr-smt2/pointer_arithmetic/addition_compound_expr.c‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <stdint.h>
2+
3+
#define NULL (void *)0
4+
5+
int main()
6+
{
7+
int32_t *a;
8+
__CPROVER_assume(a != NULL);
9+
int32_t *z = a + 2 * sizeof(int32_t);
10+
11+
__CPROVER_assert(a != z, "expected successful because of pointer arithmetic");
12+
__CPROVER_assert(a == z, "expected failure because of pointer arithmetic");
13+
}

‎regression/cbmc-incr-smt2/pointer_arithmetic/addition_compound_expr.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
addition_compound_expr.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ expected successful because of pointer arithmetic: SUCCESS
5+
\[main\.assertion\.2\] line \d+ expected failure because of pointer arithmetic: FAILURE
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This is testing the same thing as the test in addition_simple.desc, with the
11+
difference being that the addition expression here is compound, containing a
12+
more elaborate operand in the form of a multiplication containing a sizeof
13+
operator.

‎regression/cbmc-incr-smt2/pointer_arithmetic/addition_simple.c‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#define NULL (void *)0
2+
3+
int main()
4+
{
5+
int *x;
6+
int *y = x + 1;
7+
__CPROVER_assume(x != NULL);
8+
__CPROVER_assume(y != NULL);
9+
10+
__CPROVER_assert(y == x, "expected false after pointer manipulation");
11+
__CPROVER_assert(y != x, "expected true");
12+
}

‎regression/cbmc-incr-smt2/pointer_arithmetic/addition_simple.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
addition_simple.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ expected false after pointer manipulation: FAILURE
5+
\[main\.assertion\.2\] line \d+ expected true: SUCCESS
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This is testing basic pointer arithmetic by adding by incrementing a pointer's
11+
address and assigning that value to another pointer, then asserting that they
12+
don't point to the same thing.

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <stdlib.h>
2+
int main()
3+
{
4+
int *x = malloc(sizeof(int));
5+
int *y = x + 3;
6+
int z = y - x;
7+
__CPROVER_assert(y == x, "expected failure after pointer manipulation");
8+
__CPROVER_assert(z == 3, "expected successful after pointer manipulation");
9+
__CPROVER_assert(z != 3, "expected failure after pointer manipulation");
10+
}

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
pointer_subtraction.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
5+
\[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
6+
\[main\.assertion\.3\] line \d+ expected failure after pointer manipulation: FAILURE
7+
z=3
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
--
12+
This test is testing that the subtraction between two pointers (giving us the
13+
increment between the two pointers) works as it should.

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <stdlib.h>
2+
int main()
3+
{
4+
int *x = malloc(sizeof(int));
5+
float *y = x + 3;
6+
int z = y - x;
7+
__CPROVER_assert(y == x, "expected failure after pointer manipulation");
8+
__CPROVER_assert(z == 3, "expected successful after pointer manipulation");
9+
__CPROVER_assert(z != 3, "expected failure after pointer manipulation");
10+
}

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
pointer_subtraction_diff_types.c
3+
--trace
4+
^Reason: only pointers of the same object type can be subtracted.
5+
^EXIT=(134|127)$
6+
^SIGNAL=0$
7+
--
8+
--
9+
This test is for making sure that we only subtract pointers with the
10+
same underlying (base) type.

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_unsigned.c‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#define NULL (void *)0
2+
3+
int main()
4+
{
5+
int *x;
6+
unsigned int z;
7+
__CPROVER_assume(z < 3);
8+
__CPROVER_assume(z > 1);
9+
int *y = x - z;
10+
__CPROVER_assume(x != NULL);
11+
__CPROVER_assume(y != NULL);
12+
13+
__CPROVER_assert(y == x, "expected failure after pointer manipulation");
14+
__CPROVER_assert(y != x, "expected success after pointer manipulation");
15+
}

‎regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_unsigned.desc‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
pointer_subtraction_unsigned.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
5+
\[main\.assertion\.2\] line \d+ expected success after pointer manipulation: SUCCESS
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
--
10+
The test is similar to the one in `pointer_subtraction.desc`, but with different
11+
types in the subtraction operands.

0 commit comments

Comments
 (0)