Skip to content

Commit bb3307a

Browse files
author
Remi Delmas
committed
CONTRACTS: at most one predicate occurence per pointer
Ensures that at most one pointer predicate is positively asserted/assumed per pointer. Before, `is_fresh(p, n) && is_fresh(p, n)` would fail in assertion contexts as expected but pass in assumption contexts by allocating twice.
1 parent 309c77c commit bb3307a

File tree

9 files changed

+456
-1
lines changed

9 files changed

+456
-1
lines changed

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_enforce_fail/main.c

+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
int nondet_int();
2+
void foo(
3+
int *in,
4+
int *in1,
5+
int *in2,
6+
int *in3,
7+
int *in4,
8+
int *in5,
9+
int *in6,
10+
int **out1,
11+
int **out2,
12+
int **out3,
13+
int **out4,
14+
int **out5,
15+
int **out6)
16+
// clang-format off
17+
__CPROVER_requires(__CPROVER_is_fresh(in, sizeof(int)))
18+
__CPROVER_requires(__CPROVER_is_fresh(in1, sizeof(int)) && __CPROVER_pointer_in_range_dfcc(in, in1, in))
19+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in2, in) && __CPROVER_is_fresh(in2, sizeof(int)))
20+
__CPROVER_requires(__CPROVER_is_fresh(in3, sizeof(int)) && __CPROVER_pointer_equals(in3, in))
21+
__CPROVER_requires(__CPROVER_pointer_equals(in4, in) && __CPROVER_is_fresh(in4, sizeof(int)))
22+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in5, in) && __CPROVER_pointer_equals(in5, in))
23+
__CPROVER_requires(__CPROVER_pointer_equals(in6, in) && __CPROVER_pointer_in_range_dfcc(in, in6, in))
24+
__CPROVER_requires(__CPROVER_is_fresh(out1, sizeof(int *)))
25+
__CPROVER_requires(__CPROVER_is_fresh(out2, sizeof(int *)))
26+
__CPROVER_requires(__CPROVER_is_fresh(out3, sizeof(int *)))
27+
__CPROVER_requires(__CPROVER_is_fresh(out4, sizeof(int *)))
28+
__CPROVER_requires(__CPROVER_is_fresh(out5, sizeof(int *)))
29+
__CPROVER_requires(__CPROVER_is_fresh(out6, sizeof(int *)))
30+
__CPROVER_assigns(*out1, *out2, *out3, *out4, *out5, *out6)
31+
__CPROVER_ensures(__CPROVER_is_fresh(*out1, sizeof(int)) && __CPROVER_pointer_in_range_dfcc(in, *out1, in))
32+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out2, in) && __CPROVER_is_fresh(*out2, sizeof(int)))
33+
__CPROVER_ensures(__CPROVER_is_fresh(*out3, sizeof(int)) && __CPROVER_pointer_equals(*out3, in))
34+
__CPROVER_ensures(__CPROVER_pointer_equals(*out4, in) && __CPROVER_is_fresh(*out4, sizeof(int)))
35+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out5, in) && __CPROVER_pointer_equals(*out5, in))
36+
__CPROVER_ensures(__CPROVER_pointer_equals(*out6, in) && __CPROVER_pointer_in_range_dfcc(in, *out6, in))
37+
// clang-format on
38+
{
39+
int *tmp1 = malloc(sizeof(int));
40+
__CPROVER_assume(tmp1);
41+
*out1 = nondet_int() ? tmp1 : in;
42+
43+
int *tmp2 = malloc(sizeof(int));
44+
__CPROVER_assume(tmp2);
45+
*out2 = nondet_int() ? tmp2 : in;
46+
47+
int *tmp3 = malloc(sizeof(int));
48+
__CPROVER_assume(tmp3);
49+
*out3 = nondet_int() ? tmp3 : in;
50+
51+
int *tmp4 = malloc(sizeof(int));
52+
__CPROVER_assume(tmp4);
53+
*out4 = nondet_int() ? tmp4 : in;
54+
55+
*out5 = in;
56+
57+
*out6 = in;
58+
}
59+
60+
int main()
61+
{
62+
int *in, *in1, *in2, *in3, *in4, *in5, *in6;
63+
int **out1, **out2, **out3, **out4, **out5, **out6;
64+
foo(in, in1, in2, in3, in4, in5, in6, out1, out2, out3, out4, out5, out6);
65+
return 0;
66+
}

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_enforce_fail/test.desc

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo _ --arrays-uf-always --slice-formula
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: FAILURE$
5+
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: FAILURE$
6+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assume context: FAILURE$
7+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assert context: FAILURE$
8+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate in assume context: FAILURE$
9+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate in assert context: FAILURE$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
Tests that the analysis fails when a same pointer is the target of multiple
16+
pointer predicates at the same time.
17+
18+
We test all 6 pairwise combinations of is_fresh, poitner_equals,
19+
pointer_in_range_dfcc in mode assume-requires/assert-ensures.

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_enforce_pass/main.c

+61
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
int nondet_int();
2+
void foo(
3+
int *in,
4+
int *in1,
5+
int *in2,
6+
int *in3,
7+
int *in4,
8+
int *in5,
9+
int *in6,
10+
int **out1,
11+
int **out2,
12+
int **out3,
13+
int **out4,
14+
int **out5,
15+
int **out6)
16+
// clang-format off
17+
__CPROVER_requires(__CPROVER_is_fresh(in, sizeof(int)))
18+
__CPROVER_requires(__CPROVER_is_fresh(in1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, in1, in))
19+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in2, in) || __CPROVER_is_fresh(in2, sizeof(int)))
20+
__CPROVER_requires(__CPROVER_is_fresh(in3, sizeof(int)) || __CPROVER_pointer_equals(in3, in))
21+
__CPROVER_requires(__CPROVER_pointer_equals(in4, in) || __CPROVER_is_fresh(in4, sizeof(int)))
22+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in5, in) || __CPROVER_pointer_equals(in5, in))
23+
__CPROVER_requires(__CPROVER_pointer_equals(in6, in) || __CPROVER_pointer_in_range_dfcc(in, in6, in))
24+
__CPROVER_requires(__CPROVER_is_fresh(out1, sizeof(int *)))
25+
__CPROVER_requires(__CPROVER_is_fresh(out2, sizeof(int *)))
26+
__CPROVER_requires(__CPROVER_is_fresh(out3, sizeof(int *)))
27+
__CPROVER_requires(__CPROVER_is_fresh(out4, sizeof(int *)))
28+
__CPROVER_requires(__CPROVER_is_fresh(out5, sizeof(int *)))
29+
__CPROVER_requires(__CPROVER_is_fresh(out6, sizeof(int *)))
30+
__CPROVER_assigns(*out1, *out2, *out3, *out4, *out5, *out6)
31+
__CPROVER_ensures(__CPROVER_is_fresh(*out1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, *out1, in))
32+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out2, in) || __CPROVER_is_fresh(*out2, sizeof(int)))
33+
__CPROVER_ensures(__CPROVER_is_fresh(*out3, sizeof(int)) || __CPROVER_pointer_equals(*out3, in))
34+
__CPROVER_ensures(__CPROVER_pointer_equals(*out4, in) || __CPROVER_is_fresh(*out4, sizeof(int)))
35+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out5, in) || __CPROVER_pointer_equals(*out5, in))
36+
__CPROVER_ensures(__CPROVER_pointer_equals(*out6, in) || __CPROVER_pointer_in_range_dfcc(in, *out6, in))
37+
// clang-format on
38+
{
39+
int *tmp1 = malloc(sizeof(int));
40+
__CPROVER_assume(tmp1);
41+
*out1 = nondet_int() ? tmp1 : in;
42+
int *tmp2 = malloc(sizeof(int));
43+
__CPROVER_assume(tmp2);
44+
*out2 = nondet_int() ? tmp2 : in;
45+
int *tmp3 = malloc(sizeof(int));
46+
__CPROVER_assume(tmp3);
47+
*out3 = nondet_int() ? tmp3 : in;
48+
int *tmp4 = malloc(sizeof(int));
49+
__CPROVER_assume(tmp4);
50+
*out4 = nondet_int() ? tmp4 : in;
51+
*out5 = in;
52+
*out6 = in;
53+
}
54+
55+
int main()
56+
{
57+
int *in, *in1, *in2, *in3, *in4, *in5, *in6;
58+
int **out1, **out2, **out3, **out4, **out5, **out6;
59+
foo(in, in1, in2, in3, in4, in5, in6, out1, out2, out3, out4, out5, out6);
60+
return 0;
61+
}

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_enforce_pass/test.desc

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo _ --arrays-uf-always --slice-formula
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS$
5+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: SUCCESS$
6+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assume context: SUCCESS$
7+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assert context: SUCCESS$
8+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate in assume context: SUCCESS$
9+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate in assert context: SUCCESS$
10+
^EXIT=0$
11+
^SIGNAL=0$
12+
^VERIFICATION SUCCESSFUL$
13+
--
14+
--
15+
Tests that a same pointer can be the target of multiple pointer predicates as
16+
long as they do not apply at the same time.
17+
18+
We test all 6 pairwise combinations of is_fresh, poitner_equals,
19+
pointer_in_range_dfcc in mode assume-requires/assert-ensures.

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_replace_fail/main.c

+89
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
int nondet_int();
2+
void foo(
3+
int *in,
4+
int *in1,
5+
int *in2,
6+
int *in3,
7+
int *in4,
8+
int *in5,
9+
int *in6,
10+
int **out1,
11+
int **out2,
12+
int **out3,
13+
int **out4,
14+
int **out5,
15+
int **out6)
16+
// clang-format off
17+
__CPROVER_requires(__CPROVER_is_fresh(in, sizeof(int)))
18+
__CPROVER_requires(__CPROVER_is_fresh(in1, sizeof(int)) && __CPROVER_pointer_in_range_dfcc(in, in1, in))
19+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in2, in) && __CPROVER_is_fresh(in2, sizeof(int)))
20+
__CPROVER_requires(__CPROVER_is_fresh(in3, sizeof(int)) && __CPROVER_pointer_equals(in3, in))
21+
__CPROVER_requires(__CPROVER_pointer_equals(in4, in) && __CPROVER_is_fresh(in4, sizeof(int)))
22+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in5, in) && __CPROVER_pointer_equals(in5, in))
23+
__CPROVER_requires(__CPROVER_pointer_equals(in6, in) && __CPROVER_pointer_in_range_dfcc(in, in6, in))
24+
__CPROVER_requires(__CPROVER_is_fresh(out1, sizeof(int *)))
25+
__CPROVER_requires(__CPROVER_is_fresh(out2, sizeof(int *)))
26+
__CPROVER_requires(__CPROVER_is_fresh(out3, sizeof(int *)))
27+
__CPROVER_requires(__CPROVER_is_fresh(out4, sizeof(int *)))
28+
__CPROVER_requires(__CPROVER_is_fresh(out5, sizeof(int *)))
29+
__CPROVER_requires(__CPROVER_is_fresh(out6, sizeof(int *)))
30+
__CPROVER_assigns(*out1, *out2, *out3, *out4, *out5, *out6)
31+
__CPROVER_ensures(__CPROVER_is_fresh(*out1, sizeof(int)) && __CPROVER_pointer_in_range_dfcc(in, *out1, in))
32+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out2, in) && __CPROVER_is_fresh(*out2, sizeof(int)))
33+
__CPROVER_ensures(__CPROVER_is_fresh(*out3, sizeof(int)) && __CPROVER_pointer_equals(*out3, in))
34+
__CPROVER_ensures(__CPROVER_pointer_equals(*out4, in) && __CPROVER_is_fresh(*out4, sizeof(int)))
35+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out5, in) && __CPROVER_pointer_equals(*out5, in))
36+
__CPROVER_ensures(__CPROVER_pointer_equals(*out6, in) && __CPROVER_pointer_in_range_dfcc(in, *out6, in))
37+
// clang-format on
38+
{
39+
int *tmp1 = malloc(sizeof(int));
40+
__CPROVER_assume(tmp1);
41+
*out1 = nondet_int() ? tmp1 : in;
42+
43+
int *tmp2 = malloc(sizeof(int));
44+
__CPROVER_assume(tmp2);
45+
*out2 = nondet_int() ? tmp2 : in;
46+
47+
int *tmp3 = malloc(sizeof(int));
48+
__CPROVER_assume(tmp3);
49+
*out3 = nondet_int() ? tmp3 : in;
50+
51+
int *tmp4 = malloc(sizeof(int));
52+
__CPROVER_assume(tmp4);
53+
*out4 = nondet_int() ? tmp4 : in;
54+
55+
*out5 = in;
56+
57+
*out6 = in;
58+
}
59+
60+
void bar()
61+
// clang-format off
62+
__CPROVER_requires(1)
63+
__CPROVER_assigns()
64+
__CPROVER_ensures(1)
65+
// clang-format on
66+
{
67+
int in, in1, in2, in3, in4, in5, in6;
68+
int *out1, *out2, *out3, *out4, *out5, *out6;
69+
foo(
70+
&in,
71+
nondet_bool() ? &in : &in1,
72+
nondet_bool() ? &in : &in2,
73+
nondet_bool() ? &in : &in3,
74+
nondet_bool() ? &in : &in4,
75+
&in,
76+
&in,
77+
&out1,
78+
&out2,
79+
&out3,
80+
&out4,
81+
&out5,
82+
&out6);
83+
}
84+
85+
int main()
86+
{
87+
bar();
88+
return 0;
89+
}

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_replace_fail/test.desc

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo _ --arrays-uf-always --slice-formula
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: FAILURE$
5+
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: FAILURE$
6+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assume context: FAILURE$
7+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assert context: FAILURE$
8+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate in assume context: FAILURE$
9+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate in assert context: FAILURE$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
Tests that the analysis fails when a same pointer is the target of multiple
16+
pointer predicates at the same time.
17+
18+
We test all 6 pairwise combinations of is_fresh, poitner_equals,
19+
pointer_in_range_dfcc in mode assume-requires/assert-ensures.

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_replace_pass/main.c

+84
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
int nondet_int();
2+
void foo(
3+
int *in,
4+
int *in1,
5+
int *in2,
6+
int *in3,
7+
int *in4,
8+
int *in5,
9+
int *in6,
10+
int **out1,
11+
int **out2,
12+
int **out3,
13+
int **out4,
14+
int **out5,
15+
int **out6)
16+
// clang-format off
17+
__CPROVER_requires(__CPROVER_is_fresh(in, sizeof(int)))
18+
__CPROVER_requires(__CPROVER_is_fresh(in1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, in1, in))
19+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in2, in) || __CPROVER_is_fresh(in2, sizeof(int)))
20+
__CPROVER_requires(__CPROVER_is_fresh(in3, sizeof(int)) || __CPROVER_pointer_equals(in3, in))
21+
__CPROVER_requires(__CPROVER_pointer_equals(in4, in) || __CPROVER_is_fresh(in4, sizeof(int)))
22+
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in5, in) || __CPROVER_pointer_equals(in5, in))
23+
__CPROVER_requires(__CPROVER_pointer_equals(in6, in) || __CPROVER_pointer_in_range_dfcc(in, in6, in))
24+
__CPROVER_requires(__CPROVER_is_fresh(out1, sizeof(int *)))
25+
__CPROVER_requires(__CPROVER_is_fresh(out2, sizeof(int *)))
26+
__CPROVER_requires(__CPROVER_is_fresh(out3, sizeof(int *)))
27+
__CPROVER_requires(__CPROVER_is_fresh(out4, sizeof(int *)))
28+
__CPROVER_requires(__CPROVER_is_fresh(out5, sizeof(int *)))
29+
__CPROVER_requires(__CPROVER_is_fresh(out6, sizeof(int *)))
30+
__CPROVER_assigns(*out1, *out2, *out3, *out4, *out5, *out6)
31+
__CPROVER_ensures(__CPROVER_is_fresh(*out1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, *out1, in))
32+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out2, in) || __CPROVER_is_fresh(*out2, sizeof(int)))
33+
__CPROVER_ensures(__CPROVER_is_fresh(*out3, sizeof(int)) || __CPROVER_pointer_equals(*out3, in))
34+
__CPROVER_ensures(__CPROVER_pointer_equals(*out4, in) || __CPROVER_is_fresh(*out4, sizeof(int)))
35+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out5, in) || __CPROVER_pointer_equals(*out5, in))
36+
__CPROVER_ensures(__CPROVER_pointer_equals(*out6, in) || __CPROVER_pointer_in_range_dfcc(in, *out6, in))
37+
// clang-format on
38+
{
39+
int *tmp1 = malloc(sizeof(int));
40+
__CPROVER_assume(tmp1);
41+
*out1 = nondet_int() ? tmp1 : in;
42+
int *tmp2 = malloc(sizeof(int));
43+
__CPROVER_assume(tmp2);
44+
*out2 = nondet_int() ? tmp2 : in;
45+
int *tmp3 = malloc(sizeof(int));
46+
__CPROVER_assume(tmp3);
47+
*out3 = nondet_int() ? tmp3 : in;
48+
int *tmp4 = malloc(sizeof(int));
49+
__CPROVER_assume(tmp4);
50+
*out4 = nondet_int() ? tmp4 : in;
51+
*out5 = in;
52+
*out6 = in;
53+
}
54+
55+
void bar()
56+
// clang-format off
57+
__CPROVER_requires(1)
58+
__CPROVER_assigns()
59+
__CPROVER_ensures(1)
60+
// clang-format on
61+
{
62+
int in, in1, in2, in3, in4, in5, in6;
63+
int *out1, *out2, *out3, *out4, *out5, *out6;
64+
foo(
65+
&in,
66+
nondet_bool() ? &in : &in1,
67+
nondet_bool() ? &in : &in2,
68+
nondet_bool() ? &in : &in3,
69+
nondet_bool() ? &in : &in4,
70+
&in,
71+
&in,
72+
&out1,
73+
&out2,
74+
&out3,
75+
&out4,
76+
&out5,
77+
&out6);
78+
}
79+
80+
int main()
81+
{
82+
bar();
83+
return 0;
84+
}

Diff for: ‎regression/contracts-dfcc/test_pointer_pred_unique_replace_pass/test.desc

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo _ --arrays-uf-always --slice-formula
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: SUCCESS$
5+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: SUCCESS$
6+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assume context: SUCCESS$
7+
^\[__CPROVER_contracts_pointer_equals.assertion.\d+\] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assert context: SUCCESS$
8+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate in assume context: SUCCESS$
9+
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+\] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate in assert context: SUCCESS$
10+
^EXIT=0$
11+
^SIGNAL=0$
12+
^VERIFICATION SUCCESSFUL$
13+
--
14+
--
15+
Tests that a same pointer can be the target of multiple pointer predicates as
16+
long as they do not apply at the same time.
17+
18+
Tests all 6 pairwise combinations of is_fresh, pointer_equals,
19+
pointer_in_range_dfcc in mode assert-requires/assume-ensures.

0 commit comments

Comments
 (0)