Ensure that reachability includes `free` when using `assigns` contracts

[JustusAdam]

When enforcing assigns contracts CBMC expects the presence of a function free, whether or not any heap allocation is used. The current workaround is to include let _ = Box::new(()) in the harness to force free to be included in the emitted GOTO code.

I assume the problem lies in the reachability analysis which does not include free since no memory is ever deallocated from the heap. One option to fix it is to force the inclusion of free in the reachability if a contract is used.

[celinval]

Isn't free a C function? The reachability algorithm only collects Rust functions.

[celinval]

This could be related to CBMC slicing though. Not sure.

[JustusAdam]

Hmm, we could ask or try to create a minimal CBMC example that uses an assigns clause but does not malloc and see if that reproduces the problem.