1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
CORE
main.c
--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
^\[f1.assigns.\d+\] line 4 Check that \*x1 is valid: SUCCESS$
^\[f1.assigns.\d+\] line 4 Check that \*y1 is valid: SUCCESS$
^\[f1.assigns.\d+\] line 4 Check that \*z1 is valid: SUCCESS$
^\[f2.assigns.\d+\] line 9 Check that \*x2 is valid: SUCCESS$
^\[f2.assigns.\d+\] line 9 Check that \*y2 is valid: SUCCESS$
^\[f2.assigns.\d+\] line 9 Check that \*z2 is valid: SUCCESS$
^\[f3.assigns.\d+\] line 14 Check that \*x3 is valid: SUCCESS$
^\[f3.assigns.\d+\] line 14 Check that \*y3 is valid: SUCCESS$
^\[f3.assigns.\d+\] line 15 Check that \*z3 is valid: SUCCESS$
^\[f3.assigns.\d+\] line 17 Check that \*x3 is assignable: SUCCESS$
^\[f3.assigns.\d+\] line 18 Check that \*y3 is assignable: SUCCESS$
^\[f3.assigns.\d+\] line 19 Check that \*z3 is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
--
This test checks that verification succeeds when assigns clauses are respected through multiple function calls.
|
