1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
CORE dfcc-only
main.c
--dfcc main --apply-loop-contracts _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
^\[body_1.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
^\[body_2.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
^\[body_3.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
^\[incr.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
^\[main.loop_assigns.\d+\] line 73 Check assigns clause inclusion for loop .*: SUCCESS$
^\[main.loop_invariant_base.\d+\] line 73 Check invariant before entry for loop .*: SUCCESS$
^\[main.loop_invariant_step.\d+\] line 73 Check invariant after step for loop .*: SUCCESS$
^\[main.loop_step_unwinding.\d+\] line 73 Check step was unwound for loop .*: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$
^\[upperbound.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
--
This test checks assigns clause checking presence of locally declared static
variables.
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).
|
