1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
CORE
main.c
--apply-loop-contracts
^EXIT=10$
^SIGNAL=0$
^\[main\.\d+\] .* Check loop invariant before entry: UNKNOWN$
^\[main\.\d+\] .* Check that loop invariant is preserved: UNKNOWN$
^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
^\[main.assigns.\d+\] line 22 Check that t->x is assignable: UNKNOWN$
^\[main.assigns.\d+\] line 25 Check that t->x is assignable: UNKNOWN$
^\[main.assertion.1\] .* assertion .*: FAILURE$
^VERIFICATION FAILED$
--
--
This test checks that members of typedef'd and dynamically allocated structs
are correctly havoced when enforcing loop invariants.
The assertion is expected to fail when `t->x` is correctly havoced (so would be
set to a nondet value).
However, it `t->x` is not havoced then it stays at value `0` and would satisfy
the assertion when the loop is replaced by a single nondet iteration.
|
