generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 135
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.
Description
As of the nightly-2024-05-05 toolchain, using #[cfg(kani)] in a crate results in a warning, e.g.
fn main() { }
#[cfg(kani)]
mod kani_checks {
#[kani::proof]
fn check() {
assert_eq!(1, 1);
}
}using the following command line invocation:
cargo kani
with Kani version:
$ cargo kani
Kani Rust Verifier 0.51.0 (cargo plugin)
Compiling kani_cfg v0.1.0 (/home/ubuntu/examples/kani_cfg)
warning: unexpected `cfg` condition name: `kani`
--> src/main.rs:3:7
|
3 | #[cfg(kani)]
| ^^^^
|
= help: expected names are: `clippy`, `debug_assertions`, `doc`, `docsrs`, `doctest`, `feature`, `miri`, `overflow_checks`, `panic`, `proc_macro`, `relocation_model`, `rustfmt`, `sanitize`, `sanitizer_cfi_generalize_pointers`, `sanitizer_cfi_normalize_integers`, `target_abi`, `target_arch`, `target_endian`, `target_env`, `target_family`, `target_feature`, `target_has_atomic`, `target_has_atomic_equal_alignment`, `target_has_atomic_load_store`, `target_os`, `target_pointer_width`, `target_thread_local`, `target_vendor`, `test`, `ub_checks`, `unix`, `windows`
= help: consider using a Cargo feature instead or adding `println!("cargo::rustc-check-cfg=cfg(kani)");` to the top of the `build.rs`
= note: see <https://doc.rust-lang.org/nightly/cargo/reference/build-scripts.html#rustc-check-cfg> for more information about checking conditional configuration
= note: `#[warn(unexpected_cfgs)]` on by default
warning: 1 warning emitted
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.06s
Checking harness kani_checks::check...References:
https://blog.rust-lang.org/2024/05/06/check-cfg.html
rust-lang/rust#124800
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.