search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.26k stars 94 forks source link

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

Open JustusAdam opened 1 year ago

JustusAdam commented 1 year ago

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 commented 9 months ago

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

celinval commented 9 months ago

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

JustusAdam commented 9 months ago

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.