Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Using #[cfg(kani)] results in a warning #3186

Closed
zhassan-aws opened this issue May 15, 2024 · 1 comment · Fixed by #3187
Closed

Using #[cfg(kani)] results in a warning #3186

zhassan-aws opened this issue May 15, 2024 · 1 comment · Fixed by #3187
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@zhassan-aws
Copy link
Contributor

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

@zhassan-aws zhassan-aws added the [C] Bug This is a bug. Something isn't working. label May 15, 2024
@zhassan-aws
Copy link
Contributor Author

This change silences the warning when running cargo kani:

diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 07899c8c489..90b3f3a58d2 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -133,6 +133,7 @@ pub fn kani_rustc_flags(&self) -> Vec<OsString> {
                 "panic_abort_tests=yes",
                 "-Z",
                 "mir-enable-passes=-RemoveStorageMarkers",
+                "--check-cfg=cfg(kani)"
             ]
             .map(OsString::from),
         );

The warning will still be emitted when running cargo build though (if the crate uses the yet-to-be-released rust 1.80 or a nightly beyond 2024-05-05).

zhassan-aws added a commit that referenced this issue May 16, 2024
…about an unknown `cfg`. (#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 #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 #3186 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
1 participant