Skip to content

Commit a8f6aa4

Browse files
author
Remi Delmas
committed
Add tests for pointer predicates under disjunctions in assume contexts
1 parent e979772 commit a8f6aa4

File tree

16 files changed

+429
-0
lines changed

16 files changed

+429
-0
lines changed

‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
void foo(int *x)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) || 1)
4+
__CPROVER_assigns(*x)
5+
// clang-format on
6+
{
7+
*x = 0;
8+
}
9+
10+
void main()
11+
{
12+
int *x;
13+
foo(x);
14+
}

‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: (FAILURE|UNKNOWN)$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (FAILURE|UNKNOWN)
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (FAILURE|UNKNOWN)$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (FAILURE|UNKNOWN)
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (FAILURE|UNKNOWN)
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (FAILURE|UNKNOWN)
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (FAILURE|UNKNOWN)$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
19+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
20+
and no object gets allocated, and pointers remain invalid.

‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <stdlib.h>
2+
void foo(int *x, int *y)
3+
// clang-format off
4+
__CPROVER_requires(
5+
(__CPROVER_is_fresh(x, sizeof(*x)) && y == NULL) ||
6+
(x == NULL && __CPROVER_is_fresh(y, sizeof(*y)))
7+
)
8+
__CPROVER_assigns(y == NULL: *x)
9+
__CPROVER_assigns(x == NULL: *y)
10+
// clang-format on
11+
{
12+
if(y == NULL)
13+
{
14+
assert(0);
15+
*x = 0;
16+
}
17+
else
18+
{
19+
assert(0);
20+
assert(x == NULL);
21+
*y = 0;
22+
}
23+
}
24+
25+
void main()
26+
{
27+
int *x;
28+
int *y;
29+
foo(x, y);
30+
}

‎regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
5+
^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
6+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
13+
^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
15+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
21+
^EXIT=10$
22+
^SIGNAL=0$
23+
^VERIFICATION FAILED$
24+
--
25+
--
26+
Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
27+
The precondition of `foo` describes a disjunction of cases, either `x` is fresh and `y` is null,
28+
or `x` is null and `y` is fresh. The function `foo` branches on `y == NULL`.
29+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
30+
that both cases of the disjunction expressed in the requires clause are reachable.

‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int *foo()
2+
// clang-format off
3+
__CPROVER_ensures(
4+
__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)) || 1);
5+
// clang-format on
6+
7+
void bar()
8+
{
9+
int *x = foo();
10+
*x = 0; //expected to fail
11+
}
12+
void main()
13+
{
14+
bar();
15+
}

‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
5+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
6+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
7+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
8+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
9+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_is_fresh` is used in disjunctions,
16+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
17+
and no object gets allocated, and pointers remain invalid.

‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#include <stdlib.h>
2+
typedef struct
3+
{
4+
int *x;
5+
int *y;
6+
} ret_t;
7+
8+
ret_t foo()
9+
// clang-format off
10+
__CPROVER_ensures((
11+
__CPROVER_is_fresh(__CPROVER_return_value.x, sizeof(int)) &&
12+
__CPROVER_return_value.y == NULL
13+
) || (
14+
__CPROVER_return_value.x == NULL &&
15+
__CPROVER_is_fresh(__CPROVER_return_value.y, sizeof(int))
16+
))
17+
// clang-format on
18+
;
19+
20+
void bar()
21+
{
22+
ret_t ret = foo();
23+
int *x = ret.x;
24+
int *y = ret.y;
25+
if(y == NULL)
26+
{
27+
assert(0);
28+
*x = 0;
29+
}
30+
else
31+
{
32+
assert(0);
33+
assert(x == NULL);
34+
*y = 0;
35+
}
36+
}
37+
38+
void main()
39+
{
40+
bar();
41+
}

‎regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
5+
^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
6+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
13+
^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
15+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
21+
^EXIT=10$
22+
^SIGNAL=0$
23+
^VERIFICATION FAILED$
24+
--
25+
--
26+
Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts.
27+
The postcondition of `foo` describes a disjunction of cases: either `x` is fresh and `y` is null,
28+
or `x` is null and `y` is fresh. The function `bar` branches on `y == NULL`.
29+
The test succeeds if the two `assert(0)` are falsifiable, which which shows that
30+
both cases of the disjunction expressed in the ensures clause of `foo` are reachable.

‎regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, 8*sizeof(int)))
4+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(x, y, x+7) || 1)
5+
__CPROVER_assigns(*y)
6+
// clang-format on
7+
{
8+
*y = 0;
9+
}
10+
11+
void main()
12+
{
13+
int *x;
14+
int *y;
15+
foo(x, y);
16+
}

‎regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
19+
the program accepts models where `__CPROVER_pointer_equals` evaluates to
20+
false and the target pointer remains invalid.

‎regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdlib.h>
2+
void foo(int *a, int *x, int *y)
3+
// clang-format off
4+
__CPROVER_requires(__CPROVER_is_fresh(a, 8*sizeof(int)))
5+
__CPROVER_requires(
6+
(__CPROVER_pointer_in_range_dfcc(a, x, a+7) && y == NULL) ||
7+
(x == NULL && __CPROVER_pointer_in_range_dfcc(a, y, a+7))
8+
)
9+
__CPROVER_assigns(y == NULL: *x)
10+
__CPROVER_assigns(x == NULL: *y)
11+
// clang-format on
12+
{
13+
if(y == NULL)
14+
{
15+
assert(0);
16+
assert(__CPROVER_same_object(a, x));
17+
*x = 0;
18+
}
19+
else
20+
{
21+
assert(0);
22+
assert(x == NULL);
23+
assert(__CPROVER_same_object(a, y));
24+
*y = 0;
25+
}
26+
}
27+
28+
void main()
29+
{
30+
int *a;
31+
int *x;
32+
int *y;
33+
foo(a, x, y);
34+
}

‎regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
5+
^\[foo.assertion.\d+\] line 16 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
6+
^\[foo.assigns.\d+\] line 17 Check that \*x is assignable: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: dead object in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
14+
^\[foo.assertion.\d+\] line 22 assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[foo.assertion.\d+\] line 23 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
16+
^\[foo.assigns.\d+\] line 24 Check that \*y is assignable: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*y: SUCCESS$
21+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*y: SUCCESS$
23+
^EXIT=10$
24+
^SIGNAL=0$
25+
^VERIFICATION FAILED$
26+
--
27+
--
28+
Illustrates the behaviour of `__CPROVER_pointer_in_range_dfcc` under disjunctions in assume contexts.
29+
The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null,
30+
or `x` is null and `y` is in range of `a`. The function `foo` branches on `y == NULL`.
31+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
32+
that both cases of the disjunction expressed in the requires clause are reachable.

‎regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
2+
typedef struct
3+
{
4+
int *a;
5+
int *x;
6+
} ret_t;
7+
8+
ret_t foo()
9+
// clang-format off
10+
__CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, 8*sizeof(int)))
11+
__CPROVER_ensures(
12+
__CPROVER_pointer_in_range_dfcc(
13+
__CPROVER_return_value.a,
14+
__CPROVER_return_value.x,
15+
__CPROVER_return_value.a + 7
16+
) || 1)
17+
// clang-format on
18+
;
19+
20+
void bar()
21+
{
22+
ret_t ret = foo();
23+
int *x = ret.x;
24+
*x = 0; //expected to fail
25+
}
26+
27+
void main()
28+
{
29+
bar();
30+
}

‎regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
5+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
6+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
7+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
8+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
9+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_pointer_in_range_dfcc` is used in disjunctions,
16+
the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
17+
false and the target pointer remains invalid.

0 commit comments

Comments
 (0)