1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
CORE
main.c
--enforce-contract f1 --enforce-contract f2 --enforce-contract f3 _ --no-standard-checks
^EXIT=10$
^SIGNAL=0$
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?1\] is assignable: SUCCESS$
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?2\] is assignable: SUCCESS$
^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$
^\[f2.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$
^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$
^\[f3.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
^VERIFICATION FAILED$
--
--
Checks whether CBMC properly evaluates write set of members
from the same object. In this case, we have a dynamic object
as one of the struct members.
|
