CORE
main.c
--apply-loop-contracts --pointer-check _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
^\[main.assigns.\d+] .* Check that \*data is assignable: SUCCESS$
^\[main.assigns.\d+] .* Check that i is assignable: SUCCESS$
^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
--
This test checks that modifications to deref-ed pointers are correctly handled.
In such cases, pointers should not be havoc'ed, only the value should be.