1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
CORE
main.c
--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
^\[foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$
^\[foo.assigns.\d+\] line 11 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
^\[bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$
^\[bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$
^\[bar.assigns.\d+\] line 19 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
^\[baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$
^\[baz.assigns.\d+\] line 25 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Checks whether contract enforcement works with functions that deallocate memory.
We had problems before when freeing a variable, but still keeping it on
the writable set, which lead to deallocated variables issues.
Now, if a memory is deallocated, we remove it from the our freely assignable set.
|
