cargo kani playback generates zero test for proof #3990
Description
From https://model-checking.github.io/kani/reference/experimental/concrete-playback.html , it says
To manually compile and run the test, you can use Kani's playback subcommand:
cargo kani playback -Z concrete-playback -- ${unit_test_func_name}
But for this snippet:
#[cfg(kani)]
mod verifies {
#[kani::proof]
fn f() {
let a: u8 = kani::any();
assert_eq!(a, 1, "Not eq to 1.");
}
}and the suggested command:
$ cargo kani playback -Z concrete-playback
# or $ cargo kani playback -Z concrete-playback -- f
warning: unexpected `cfg` condition name: `kani`
--> src/lib.rs:2:7
|
2 | #[cfg(kani)]
| ^^^^
|
= help: expected names are: `docsrs`, `feature`, and `test` and 31 more
= help: consider using a Cargo feature instead
= help: or consider adding in `Cargo.toml` the `check-cfg` lint config for the lint:
[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
= help: or consider adding `println!("cargo::rustc-check-cfg=cfg(kani)");` to the top of the `build.rs`
= note: see <https://doc.rust-lang.org/nightly/rustc/check-cfg/cargo-specifics.html> for more information about checking conditional configuration
= note: `#[warn(unexpected_cfgs)]` on by default
warning: `test-kani` (lib) generated 1 warning
warning: `test-kani` (lib test) generated 1 warning (1 duplicate)
Finished `test` profile [unoptimized + debuginfo] target(s) in 0.04s
Running unittests src/lib.rs (target/x86_64-unknown-linux-gnu/debug/deps/test_kani-c36f80394abe5d8f)
running 0 tests
test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
Doc-tests test_kani
running 0 tests
test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00sno output test case to run, which can be confirmed by running target/x86_64-unknown-linux-gnu/debug/deps/test_kani-c36f80394abe5d8f --list to see 0 tests, 0 benchmarks.
BTW the commands documented are a bit confusing and incomplete:
cargo kani playback -Z concrete-playback -- ${unit_test_func_name}
- What does
unit_test_func_namemeans? The proof fn name? Or the generated test fn name likekani_concrete_playback_f_2469314071636892245trailling with numbers? - the command behaves differently from
kani ...or merecargo kaniif looked closer:
Kani Rust Verifier 0.60.0 (standalone)
warning: target feature `x87` must be enabled to ensure that the ABI of the current target can be implemented correctly
|
= note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
= note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>
warning: target feature `sse2` must be enabled to ensure that the ABI of the current target can be implemented correctly
|
= note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
= note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>
warning: 2 warnings emitted
Checking harness verifies::f...
CBMC 6.4.1 (cbmc-6.4.1)cargo kani playback -Z concrete-playback goes normally into cargo procedure with cargo diagnostics such as unexpected cfg condition name, while kani ... or cargo kani enters kani's custom sysroot procedure without cargo diagnostics any more, but with kani's target feature warnings (ref #3878 ).
kani -Z concrete-playback --concrete-playback=print
It should be kani -Z concrete-playback --concrete-playback=print path/to/file.rs for clarity.