CORE dfcc-only
main.c
--no-malloc-may-fail --dfcc main --enforce-contract foo
^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
This tests shows that using is_fresh without malloc failure modes active and
without imposing a limit on the size parameter results in failures:
1. in the contracts library because the addressable range of the allocated object
cannot be represented without pointer overflow
2. in the assigns clause checking because the assignable range cannot be represented
3. in pointer overflow checks generated by CBMC pointer checks