Skip to content

Commit 2c486c8

Browse files
author
Remi Delmas
committed
Add regression tests for is_fresh and pointer_in_range.
Tests the behaviour of predicates in disjunctions in assume contexts: - in requires clauses in enforce mode, - in ensures clauses in replace mode.
1 parent 740d1f4 commit 2c486c8

File tree

16 files changed

+414
-22
lines changed

16 files changed

+414
-22
lines changed

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

+14
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

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
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$
5+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
6+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
7+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
8+
^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
9+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
10+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
11+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
12+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
13+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
14+
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
15+
^EXIT=10$
16+
^SIGNAL=0$
17+
^VERIFICATION FAILED$
18+
--
19+
--
20+
This test checks that when `__CPROVER_is_fresh` is disjunctions,
21+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
22+
and no object gets allocated, and pointers remains undefined.

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

+20-8
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,30 @@
1-
void foo(int *x)
1+
#include <stdlib.h>
2+
void foo(int *x, int *y)
23
// clang-format off
34
__CPROVER_requires(
4-
/* Case A -- pointer is valid */
5-
__CPROVER_is_fresh(x, sizeof(*x))
6-
/* Case B -- pointer is invalid */
7-
|| 1)
8-
__CPROVER_assigns(*x)
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)
910
// clang-format on
1011
{
11-
*x = 0;
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+
}
1223
}
1324

1425
void main()
1526
{
1627
int *x;
17-
foo(x);
28+
int *y;
29+
foo(x, y);
1830
}

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

+22-14
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,30 @@
11
CORE dfcc-only
22
main.c
33
--dfcc main --enforce-contract foo
4-
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
5-
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
6-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
7-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
8-
^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
9-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
10-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
11-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
12-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
13-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
14-
^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
4+
^\[foo.assertion.\d+\] line 13 assertion 0: FAILURE$
5+
^\[foo.assigns.\d+\] line 14 Check that \*x is assignable: SUCCESS$
6+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: dead object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 14 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[foo.assertion.\d+\] line 16 assertion 0: FAILURE$
13+
^\[foo.assertion.\d+\] line 17 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[foo.assigns.\d+\] line 18 Check that \*y is assignable: SUCCESS$
15+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: dead object in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 18 dereference failure: invalid integer address in \*y: SUCCESS$
1521
^EXIT=10$
1622
^SIGNAL=0$
1723
^VERIFICATION FAILED$
1824
--
1925
--
20-
This test checks that when __CPROVER_is_fresh is disjunctions,
21-
the goto model accepts traces where __CPROVER_is_fresh evaluates to false
22-
and no object gets allocated, and pointers remains undefined.
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

+15
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

+17
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: FAILURE$
5+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: FAILURE$
6+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: FAILURE$
7+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: FAILURE$
8+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: FAILURE$
9+
^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: FAILURE$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_is_fresh` is disjunctions,
16+
the program accepts models where `__CPROVER_is_fresh` evaluates to false
17+
and no object gets allocated, and pointers remains undefined.

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

+41
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

+30
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 25 assertion 0: FAILURE$
5+
^\[bar.assigns.\d+\] line 26 Check that \*x is assignable: SUCCESS$
6+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer NULL in \*x: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer invalid in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: deallocated dynamic object in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: dead object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer outside object bounds in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line 26 dereference failure: invalid integer address in \*x: SUCCESS$
12+
^\[bar.assertion.\d+\] line 28 assertion 0: FAILURE$
13+
^\[bar.assertion.\d+\] line 29 assertion x == \(\(.*\)NULL\): SUCCESS$
14+
^\[bar.assigns.\d+\] line 30 Check that \*y is assignable: SUCCESS$
15+
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer NULL in \*y: SUCCESS$
16+
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer invalid in \*y: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: deallocated dynamic object in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: dead object in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer outside object bounds in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line 30 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

+16
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

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
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$
5+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
6+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
7+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
8+
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
9+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer NULL in \*y: FAILURE$
10+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer invalid in \*y: FAILURE$
11+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: deallocated dynamic object in \*y: FAILURE$
12+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: dead object in \*y: FAILURE$
13+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*y: FAILURE$
14+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: invalid integer address in \*y: FAILURE$
15+
^EXIT=10$
16+
^SIGNAL=0$
17+
^VERIFICATION FAILED$
18+
--
19+
--
20+
This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions,
21+
the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
22+
false the target pointer of the predicate remains undefined.

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

+34
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

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
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+
^SIGNAL=0$
24+
^VERIFICATION FAILED$
25+
--
26+
--
27+
Illustrates the behaviour of `__CPROVER_pointer_in_range_dfcc` under disjunctions in assume contexts.
28+
The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null,
29+
or `x` is null and `y` is in range of `a`. The function `foo` branches on `y == NULL`.
30+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
31+
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

+30
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

+17
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 24 dereference failure: pointer NULL in \*x: FAILURE$
5+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: FAILURE$
6+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: FAILURE$
7+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: FAILURE$
8+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: FAILURE$
9+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: FAILURE$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions,
16+
the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
17+
false the target pointer remains undefined.

0 commit comments

Comments
 (0)