Skip to content

Commit f0ab57e

Browse files
feliperodrifeliperodri
authored
Merge pull request #6327 from feliperodri/free-assigns
No need to track write set with temporary variables
2 parents 318101f + 43f0f89 commit f0ab57e

File tree

31 files changed

+155
-171
lines changed

31 files changed

+155
-171
lines changed

‎regression/contracts/assigns_enforce_17/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-all-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.\d+\] line \d+ assertion x \=\= 0\: SUCCESS$
6+
^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
--

‎regression/contracts/assigns_enforce_structs_04/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--enforce-all-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
7-
^\[f2.\d+\] line \d+ Check that p\-\>x is assignable\: FAILURE$
8-
^\[f3.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
9-
^\[f4.\d+\] line \d+ Check that p is assignable\: FAILURE$
6+
^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
7+
^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
8+
^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
9+
^\[f4.\d+\] line \d+ Check that p is assignable: FAILURE$
1010
^VERIFICATION FAILED$
1111
--
1212
--

‎regression/contracts/assigns_enforce_structs_05/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--enforce-all-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
7-
^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)0\] is assignable\: SUCCESS$
8-
^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)1\] is assignable\: SUCCESS$
9-
^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)2\] is assignable\: SUCCESS$
6+
^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
7+
^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$
8+
^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$
9+
^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$
1010
^VERIFICATION FAILED$
1111
--
1212
--

‎regression/contracts/assigns_enforce_structs_06/test.desc

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ main.c
33
--enforce-all-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: SUCCESS$
7-
^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)1\] is assignable\: SUCCESS$
8-
^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)2\] is assignable\: SUCCESS$
9-
^\[f1.\d+\] line \d+ Check that p\-\>size is assignable\: FAILURE$
10-
^\[f2.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
11-
^\[f2.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
12-
^\[f3.\d+\] line \d+ Check that p\-\>buf is assignable\: SUCCESS$
13-
^\[f3.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
6+
^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
7+
^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$
8+
^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$
9+
^\[f1.\d+\] line \d+ Check that p->size is assignable: FAILURE$
10+
^\[f2.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
11+
^\[f2.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
12+
^\[f3.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$
13+
^\[f3.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
1414
^VERIFICATION FAILED$
1515
--
1616
--

‎regression/contracts/assigns_enforce_structs_07/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <assert.h>
2+
#include <stdint.h>
3+
#include <stdlib.h>
4+
5+
struct pair
6+
{
7+
uint8_t *buf;
8+
size_t size;
9+
};
10+
11+
struct pair_of_pairs
12+
{
13+
struct pair *p;
14+
};
15+
16+
void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
17+
{
18+
p->buf[0] = 0;
19+
}
20+
21+
void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
22+
{
23+
pp->p->buf[0] = 0;
24+
}
25+
26+
int main()
27+
{
28+
struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
29+
f1(p);
30+
struct pair_of_pairs *pp = malloc(sizeof(*pp));
31+
f2(pp);
32+
33+
return 0;
34+
}

‎regression/contracts/assigns_enforce_structs_07/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts _ --pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
7+
^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
8+
^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$
9+
^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$
10+
^VERIFICATION FAILED$
11+
--
12+
--
13+
Checks whether CBMC properly evaluates write set of members
14+
from invalid objects. In this case, they are not writable.

‎regression/contracts/assigns_replace_07/main.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#include <assert.h>
2+
#include <stdint.h>
3+
#include <stdlib.h>
4+
5+
struct pair
6+
{
7+
uint8_t *buf;
8+
size_t size;
9+
};
10+
11+
void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
12+
__CPROVER_ensures(p->buf[0] == 0)
13+
{
14+
p->buf[0] = 0;
15+
}
16+
17+
int main()
18+
{
19+
struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
20+
f1(p);
21+
// clang-format off
22+
assert(p != NULL ==> p->buf[0] == 0);
23+
// clang-format on
24+
return 0;
25+
}

‎regression/contracts/assigns_replace_07/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts _ --pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
7+
^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$
8+
^VERIFICATION FAILED$
9+
--
10+
--
11+
Checks whether CBMC properly evaluates write set of members
12+
from invalid objects. In this case, they are not writable.

‎regression/contracts/assigns_type_checking_valid_cases/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
7-
^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
8-
^\[foo10.\d+\] line \d+ Check that buffer\-\>aux\.allocated is assignable: SUCCESS$
7+
^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
8+
^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$
99
^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
1010
^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
1111
^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
@@ -14,10 +14,10 @@ main.c
1414
^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
1515
^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
1616
^\[foo5.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$
17-
^\[foo6.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
18-
^\[foo6.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
19-
^\[foo7.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
20-
^\[foo7.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
17+
^\[foo6.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$
18+
^\[foo6.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
19+
^\[foo7.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$
20+
^\[foo7.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
2121
^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$
2222
^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$
2323
^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$

‎regression/contracts/assigns_validity_pointer_01/test.desc

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,6 @@ ASSUME .*::tmp_if_expr\$\d
1616
IF ¬\(z ≠ NULL\) THEN GOTO \d
1717
ASSIGN .*::tmp_if_expr\$\d := \(\*z = 7 \? true : false\)
1818
ASSUME .*::tmp_if_expr\$\d
19-
// foo
20-
ASSUME \*.*::tmp_cc\$\d > 0
21-
ASSERT \*.*::tmp_cc\$\d = 3
2219
--
2320
\[3\] file main\.c line 6 assertion: FAILURE
2421
--

0 commit comments

Comments
 (0)