Enable verification of code that uses C-FFI

[danielsn]

Requested feature: Enable verification of code that uses C-FFI Use case: Any code that has mixed language calls, and the user wants to verify Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/nomicon/ffi.html

Test case:

<code>