1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
CORE dfcc-only
main.c
--dfcc main --replace-call-with-contract bar --apply-loop-contracts _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[main.loop_assigns.\d+\] line 33 Check assigns clause inclusion for loop .*: SUCCESS$
^\[main.loop_invariant_base.\d+\] line 33 Check invariant before entry for loop .*: SUCCESS$
^\[main.loop_invariant_step.\d+\] line 33 Check invariant after step for loop .*: SUCCESS$
^\[main.loop_step_unwinding.\d+\] line 33 Check step was unwound for loop .*: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
^\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion j == 9: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
--
This test checks assigns clause checking presence of locally declared static
variables and loops.
We observe that the local static variables declared within the loop's
scope are correctly gathered and added to the write set,
and are havoced (body_1 and body_2 do not return 0 anymore after the loop).
|
