Skip to content

Commit

Permalink
Include --check-cfg=cfg(kani) in the rust flags to avoid a warning …
Browse files Browse the repository at this point in the history
…about an unknown `cfg`. (rust-lang#3187)

Starting with the 2024-05-05 toolchain (and the upcoming Rust 1.80
release), the `unexpected_cfgs` lint has been turned on by default. As a
result, running `cargo kani` on a crate that has a `#[cfg(kani)]`
results in a warning (see rust-lang#3186). To avoid this warning, this PR adds
`--check-cfg=cfg(kani)` to `RUSTFLAGS` when Kani invokes `cargo`.

Call-outs: On such packages, doing a `cargo build` will also result in
this warning, unless:
```rust
println!("cargo::rustc-check-cfg=cfg(kani)");
```
is added to the package's `build.rs` file. However, this warning would
only occur with `cargo build` if the package uses the 2024-05-05
toolchain (or newer), or the Rust version used in the package is
upgraded to 1.80 (when it's released at the end of July 2024). Since
we're likely to release a new version of Kani sooner than the 1.80
release, this PR mitigates the issue that is more likely to impact users
(a warning from `cargo kani`).

Resolves rust-lang#3186 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored May 16, 2024
1 parent 33b7d85 commit 9b9e473
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 0 deletions.
1 change: 1 addition & 0 deletions kani-driver/src/call_single_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,7 @@ impl KaniSession {
"panic_abort_tests=yes",
"-Z",
"mir-enable-passes=-RemoveStorageMarkers",
"--check-cfg=cfg(kani)",
]
.map(OsString::from),
);
Expand Down
9 changes: 9 additions & 0 deletions tests/cargo-kani/unexpected_cfgs/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

[package]
name = "unexpected_cfgs"
version = "0.1.0"
edition = "2021"

[dependencies]
1 change: 1 addition & 0 deletions tests/cargo-kani/unexpected_cfgs/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
VERIFICATION:- SUCCESSFUL
19 changes: 19 additions & 0 deletions tests/cargo-kani/unexpected_cfgs/src/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This test checks that the `unexpected_cfgs` lint (enabled by default as of
// the 2024-05-05 toolchain) does not cause `cargo kani` to emit warnings when
// the code has `#[cfg(kani)]`. Kani avoids the warning by adding
// `--check-cfg=cfg(kani)` to the rust flags.

#![deny(unexpected_cfgs)]

fn main() {}

#[cfg(kani)]
mod kani_checks {
#[kani::proof]
fn check_unexpected_cfg() {
assert_eq!(1, 1);
}
}

0 comments on commit 9b9e473

Please sign in to comment.