kani fails to compile a crate but cargo can build it

[lrobidou]

I would like to use kani, but it fails to build one of my dependencies (needletail), even though cargo build runs fine.
Step to reproduce:

git clone https://github.com/onecodex/needletail
cd needletail
cargo build  # OK

However, kani fails to build:

cargo kani
# Kani Rust Verifier 0.57.0 (cargo plugin)
# [...]
# error: linking with `cc` failed: exit status: 1
#  = note: rust-lld: error: version script assignment of 'global' to symbol 'bz_internal_error' failed: symbol not defined
          collect2: error: ld returned 1 exit
# error: could not compile `needletail` (lib) due to 1 previous error
# error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

Note: when I remove bzip2 from the dependencies of needletail, kani works fine, but I don't need to do it for cargo build.

Is there a difference in linking between cargo build and cargo kani?

[carolynzech]

Hi @lrobidou,
I can't reproduce this error on my machine (ARM64 Mac):

cmzech@80a9971b5e20 ~ % git clone https://github.com/onecodex/needletail
Cloning into 'needletail'...
remote: Enumerating objects: 1076, done.
remote: Counting objects: 100% (171/171), done.
remote: Compressing objects: 100% (92/92), done.
remote: Total 1076 (delta 107), reused 84 (delta 79), pack-reused 905 (from 1)
Receiving objects: 100% (1076/1076), 652.41 KiB | 11.65 MiB/s, done.
Resolving deltas: 100% (600/600), done.
cmzech@80a9971b5e20 ~ % cd needletail 
cmzech@80a9971b5e20 needletail % cargo build
    Updating crates.io index
     Locking 193 packages to latest compatible versions
      Adding bio v1.6.0 (available: v2.0.3)
      Adding bzip2 v0.4.4 (available: v0.5.0)
      Adding pyo3 v0.21.2 (available: v0.23.3)
   Compiling libc v0.2.169
   Compiling shlex v1.3.0
   Compiling pkg-config v0.3.31
   Compiling zstd-safe v7.2.1
   Compiling adler2 v2.0.0
   Compiling cfg-if v1.0.0
   Compiling memchr v2.7.4
   Compiling bytecount v0.6.8
   Compiling crc32fast v1.4.2
   Compiling miniz_oxide v0.8.2
   Compiling buffer-redux v1.0.2
   Compiling flate2 v1.0.35
   Compiling jobserver v0.1.32
   Compiling cc v1.2.7
   Compiling zstd-sys v2.0.13+zstd.1.5.6
   Compiling liblzma-sys v0.3.11
   Compiling bzip2-sys v0.1.11+1.0.8
   Compiling bzip2 v0.4.4
   Compiling liblzma v0.3.5
   Compiling zstd v0.13.2
   Compiling needletail v0.6.1 (/Users/cmzech/needletail)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 6.46s
cmzech@80a9971b5e20 needletail % cargo kani
Kani Rust Verifier 0.57.0 (cargo plugin)
   Compiling libc v0.2.169
   Compiling shlex v1.3.0
   Compiling pkg-config v0.3.31
   Compiling zstd-safe v7.2.1
   Compiling adler2 v2.0.0
   Compiling cfg-if v1.0.0
   Compiling memchr v2.7.4
   Compiling bytecount v0.6.8
   Compiling crc32fast v1.4.2
   Compiling miniz_oxide v0.8.2
   Compiling buffer-redux v1.0.2
   Compiling flate2 v1.0.35
   Compiling jobserver v0.1.32
   Compiling cc v1.2.7
   Compiling zstd-sys v2.0.13+zstd.1.5.6
   Compiling liblzma-sys v0.3.11
   Compiling bzip2-sys v0.1.11+1.0.8
   Compiling bzip2 v0.4.4
   Compiling liblzma v0.3.5
   Compiling zstd v0.13.2
   Compiling needletail v0.6.1 (/Users/cmzech/needletail)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 4.66s
No proof harnesses (functions with #[kani::proof]) were found to verify.
cmzech@80a9971b5e20 needletail % 

Would you mind sharing:

• Your setup (what OS/architecture you're running on)
• The result of running cargo kani --debug

so we can try to dig into this problem? Thanks!