CORE dfcc-only
main.c
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
^\[foo.assigns.\d+\] line \d+ Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
This test checks that assuming is_fresh(ptr, size) with a non-deterministic size
checks that size < __CPROVER_max_malloc_size and then assumes it.
This guarantees that the address `ptr + size` can always be computed and
represented without offset bits overflowing into the object bits in the pointer
model used by CBMC.