Can this be used to test C code (CFFI)?

[Ragarnoy]

Hi,
We're looking for a solution to reliably test C code from Rust, would your macros work with extern functions?

[xldenis]

Not in the way you likely would like them to. With creusot you can reason about Rust code which calls into C, so long as you can provide a trusted specification for that C code. However, Creusot has no way of reasoning about the C code itself, all it can see is the Rust.

If you are looking to prove properties about C code I would recommend checking out tools such as Frama-C, or VeriFast.