Stub linker to avoid missing symbols errors

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),
         );

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

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

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();
+    }
+}