Kani fails when feature is missing from dependency #4544
Description
For a Cargo workspace with two members:
mylib— a library with no featuresmytests— a test crate with an optional dependency onmylibgated by the
use_mylibfeature
cargo kani --workspace --features <feature> fails when a workspace member does not
declare the requested feature, even though cargo test --workspace --features <feature>
handles this case correctly.
Workspace structure:
.
├── Cargo.toml
├── mylib
│ ├── Cargo.toml
│ └── src
│ └── lib.rs
└── mytests
├── Cargo.toml
└── src
└── lib.rs
Cargo.toml:
[workspace]
resolver = "2"
members = ["mylib", "mytests"]mylib/Cargo.toml:
[package]
name = "mylib"
version = "0.1.0"
edition = "2021"mylib/src/lib.rs:
pub fn add(a: u32, b: u32) -> u32 {
a + b
}mytests/Cargo.toml:
[package]
name = "mytests"
version = "0.1.0"
edition = "2021"
[features]
use_mylib = ["dep:mylib"]
[dependencies]
mylib = { path = "../mylib", optional = true }mytests/src/lib.rs:
#[cfg(feature = "use_mylib")]
pub fn add_wrapper(a: u32, b: u32) -> u32 {
mylib::add(a, b)
}
#[cfg(kani)]
mod proofs {
#[kani::proof]
fn check_add() {
let a: u32 = kani::any();
let b: u32 = kani::any();
kani::assume(a <= 1000);
kani::assume(b <= 1000);
#[cfg(feature = "use_mylib")]
{
let result = super::add_wrapper(a, b);
assert!(result == a + b);
}
}
}
#[cfg(test)]
mod tests {
#[test]
fn test_add() {
#[cfg(feature = "use_mylib")]
assert_eq!(super::add_wrapper(2, 3), 5);
}
}Reproduction
# Works: cargo test silently ignores the missing feature for mylib
cargo test --workspace --features use_mylib
# Fails: cargo kani errors because mylib doesn't have use_mylib
cargo kani --workspace --features use_mylibError
error: the package 'mylib' does not contain this feature: use_mylib
help: package with the missing feature: mytests
error: Failed to execute cargo (exit status: 101). Found 0 compilation errors.
Expected behavior
cargo kani --workspace --features use_mylib should behave like
cargo test --workspace --features use_mylib — apply the feature to packages that
declare it and silently skip packages that don't.