diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index faa6e67d8358..9a09ce6163f8 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -181,6 +181,8 @@ impl KaniSession { "-Z", "mir-enable-passes=-RemoveStorageMarkers", "--check-cfg=cfg(kani)", + // Do not invoke the linker since the compiler will not generate real object files + "-Clinker=echo", ] .map(OsString::from), ); diff --git a/tests/cargo-kani/issue-3817/Cargo.toml b/tests/cargo-kani/issue-3817/Cargo.toml new file mode 100644 index 000000000000..f187c13e0705 --- /dev/null +++ b/tests/cargo-kani/issue-3817/Cargo.toml @@ -0,0 +1,17 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "issue-3817" +version = "0.1.0" +edition = "2024" +description = "Issue with linking cdylib and another shared library" + +[lib] +crate-type = ["cdylib", "rlib"] + +[dependencies] +bzip2 = "0.5.0" + +[profile.release] +lto = true diff --git a/tests/cargo-kani/issue-3817/expected b/tests/cargo-kani/issue-3817/expected new file mode 100644 index 000000000000..9c1de23bbc6e --- /dev/null +++ b/tests/cargo-kani/issue-3817/expected @@ -0,0 +1,9 @@ +Checking harness check_unreachable_extern_fn... +VERIFICATION:- SUCCESSFUL + +Checking harness check_missing_extern_fn... +Failed Checks: call to foreign "C" function `BZ2_bzCompressInit` is not currently supported by Kani. +VERIFICATION:- FAILED + +Verification failed for - check_missing_extern_fn +1 successfully verified harnesses, 1 failures, 2 total diff --git a/tests/cargo-kani/issue-3817/src/lib.rs b/tests/cargo-kani/issue-3817/src/lib.rs new file mode 100644 index 000000000000..a2bb4e0b0b22 --- /dev/null +++ b/tests/cargo-kani/issue-3817/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani can compile a crate that depends on bzip, and the analysis will only +//! fail if a missing symbol is reachable. + +use bzip2::Compression; +use bzip2::read::BzEncoder; + +#[kani::proof] +fn check_missing_extern_fn() { + // Call bzip compressor + let data: [u8; 10] = kani::any(); + let compressor = BzEncoder::new(&data[..], Compression::best()); + assert_eq!(compressor.total_in(), data.len().try_into().unwrap()); +} + +#[kani::proof] +fn check_unreachable_extern_fn() { + let positive = kani::any_where(|v: &i8| *v > 0); + if positive == 0 { + // This should be unreachable so verification should succeed. + check_missing_extern_fn(); + } +}