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
|
KNOWNBUG
main.c
--apply-loop-contracts
^EXIT=10$
^SIGNAL=0$
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
^\[main.assertion.1\] .* assertion __CPROVER_same_object(old_data123, &(data\[1\]\[2\]\[3\])): SUCCESS$
^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
^VERIFICATION FAILED$
--
--
Test case related to issue #6020: it checks that dynamically allocated multi
dimensional arrays are correctly havoced when enforcing invariant contracts.
The `__CPROVER_same_object(old_data123, &(data[1][2][3]))` assertion is expected
to pass -- we should not mistakenly havoc the allocations, just their values.
However, the `data[1][2][3] == 0` assertion is expected to fail since `data`
is havoced.
Blocked on #6326:
The assigns clause in this case would have an entire 3D space,
and some of it must be re-established, to the original objects
but with different values at certain locations, by the loop invariant.
However, currently we cannot restrict same_object for pointers
within loop invariants.
|
