FFI stubbing for libc crate only works if libc crate is imported via feature(rustc_private)
#2673
Comments
|
The workaround provided in #2686 for a similar issue (importing the stubbing target by alias and stubbing our that alias) also works in this case: #[allow(unused)]
mod stubs {
use libc::{c_int, c_long};
pub unsafe extern "C" fn sysconf(_input: c_int) -> c_long {
1
}
}
use libc::sysconf as sysconf_alias;
#[kani::proof]
#[kani::stub(sysconf_alias, stubs::sysconf)]
fn verify_sysconf_stub() {
assert_eq!(1, unsafe{ libc::sysconf(libc::_SC_PAGE_SIZE) });
}leads to |
|
Mhh, instead trying to stub out I tried mod stubs {
pub unsafe extern "C" fn clock_gettime(_clock_id: libc::clockid_t, tp: *mut libc::timespec) -> libc::c_int {
unsafe {
(*tp).tv_sec = kani::any();
(*tp).tv_nsec = kani::any();
}
0
}
}
#[kani::proof]
#[kani::stub(libc::clock_gettime, stubs::clock_gettime)]
fn verify_clock_gettime_stub() {
let i = std::time::Instant::now();
}and running I think this also is a result of the standard library using a "special" version of libc. I tried to match my libc crate version to the version the standard library was compiled against (and also tried all libc versions since 0.2.141), to no avail :(. Using the |
|
Right, so I found a workaround... ish For some reason, rustc's libc is not a drop-in-replacement for crates.io libc, so just doing |
|
I think the problem here might be related to different versions of the same crate. The libc you are pulling from crates.io might not have the same version as the one that rustc_private points to, hence the mismatched type. Your workaround makes sense to me, so you can clearly pinpoint which one you are trying to stub. That said, I think we are mishandling this case, and we should fix that. Let us know if you are blocked though. |
I tried this code:
using the following command line invocation:
with Kani version: 0.34.0
I expected to see this happen: sysconf to be successfully stubbed and verification to succeed
Instead, this happened: sysconf was not stubbed out, and instead the CMBC model was used. Because of this, verification failed with
If I remove
libcfrom myCargo.tomland instead putat the top of my file, verification succeeds as expected. This is why the integration test added for the FFI stubbing feature added in #2658 passes.
The text was updated successfully, but these errors were encountered: