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 --apply-loop-contracts
^EXIT=10$
^SIGNAL=0$
^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$
^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$
^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$
^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: SUCCESS$
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
^VERIFICATION FAILED$
--
--
This test (taken from #6021) shows the need for assigns clauses on loops.
The alias analysis in this case returns `unknown`,
and so we must manually annotate an assigns clause on the loop.
Note that the annotated assigns clause in this case us an underapproximation,
per the current semantics of the assigns clause -- it must model ALL memory
being assigned to by the loop, not just a single symbolic iteration so we expect
this to fail.
|
