Reachability analysis cannot see through FFI

model-checking / kani

Kani Rust Verifier

https://model-checking.github.io/kani

Apache License 2.0

2.26k stars 94 forks source link

Open tautschnig opened 5 months ago

tautschnig commented 5 months ago

See https://github.com/model-checking/kani/pull/3253#discussion_r1635382569 for an example of a test that fails when we don't directly use in Rust the function that is otherwise only invoked from C code. We might consider marking all functions with attribute no_mangle reachable.

celinval commented 4 months ago

We should only do that if -Z c-ffi is enabled though.