1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
CORE
main.c
--apply-loop-contracts _ --no-standard-checks
^EXIT=10$
^SIGNAL=0$
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
^\[main.\d+\] .* Check that loop instrumentation was not truncated: SUCCESS$
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
^\[main.assigns.\d+\] .* Check that i is valid: SUCCESS$
^\[main.assigns.\d+\] .* Check that __CPROVER_object_upto\(\(.*\)b->data, \(.*\)5\) is valid: SUCCESS$
^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data, (4|8).*, TRUE\) is valid: SUCCESS$
^\[main.assigns.\d+\] .* Check that b->data is assignable: SUCCESS$
^\[main.assigns.\d+\] .* Check that \*b->data is assignable: SUCCESS$
^\[main.assertion.\d+\] .* assertion b->data == start: FAILURE$
^\[main.assertion.\d+\] .* assertion start <= b->data && b->data <= end: SUCCESS$
^VERIFICATION FAILED$
--
--
This test checks that __CPROVER_typed_target(ptr) is supported in loop contracts
for pointer typed targets and gets translated to
__CPROVER_assignable(address_of(ptr), sizeof(ptr), TRUE).
|
