I tried the following:
$ cargo init dummy
$ cd dummy
I added the following line to Cargo.toml
[dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }I opened src/main.rs
#[cfg(kani)]
mod harnesses {
#[kani::proof]
fn force_failure() {
assert!(kani::any());
}
}using the following command line invocation:
cargo kani --enable-unstable --concrete-playback
RUSTFLAGS="--cfg=kani" cargo +nightly test
with Kani version: 0.9.0
I expected to see this happen: Cargo runs the new test and fail.
Instead, this happened: Cargo failed to build the harness with the following error:
error[E0433]: failed to resolve: use of undeclared crate or module `kanitool`
--> src/main.rs:36:5
|
36 | #[kani::proof]
| ^^^^^^^^^^^^^^ use of undeclared crate or module `kanitool`
|
= note: this error originates in the attribute macro `kani::proof` (in Nightly builds, run with -Z macro-backtrace for more info)
I tried the following:
I added the following line to
Cargo.tomlI opened src/main.rs
using the following command line invocation:
with Kani version: 0.9.0
I expected to see this happen: Cargo runs the new test and fail.
Instead, this happened: Cargo failed to build the harness with the following error: