1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
CORE
main.c
--apply-loop-contracts
^EXIT=10$
^SIGNAL=0$
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$
^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$
^VERIFICATION FAILED$
--
This test is expected to fail because it modifies a variable within a loop,
but attempts to check that it is "effectively constant" without asserting so
within the loop invariant.
The current implementation of `check_apply_invariant` correctly havocs all
variables that are modified within the loop.
The fact that a variable is "effectively constant" within a loop must be
established using an appropriate clause in the invariant.
|
