Skip to content

Commit 404fc41

Browse files
authored
Change how we enforce deny warnings (rust-lang#2672)
Enforce that no warning is being added as part of our regression script instead at a crate level. This will also enforce no warnings for all our crates, instead of just kani-compiler as is today. This makes development a bit easier, since warnings of unused code shows up fairly often when a feature is half implemented. So this allow us to compile and test the code before it's production ready. That said, it is nice to avoid warnings from piling up, so change the check to the regression instead, which should be executed before we create PR / merge changes. This also aligns with the recommendation from https://rust-unofficial.github.io/patterns/anti_patterns/deny-warnings.html
1 parent 596bc50 commit 404fc41

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

kani-compiler/src/main.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@
66
//!
77
//! Like miri, clippy, and other tools developed on the top of rustc, we rely on the
88
//! rustc_private feature and a specific version of rustc.
9-
#![deny(warnings)]
109
#![feature(extern_types)]
1110
#![recursion_limit = "256"]
1211
#![feature(box_patterns)]

scripts/kani-regression.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,8 @@ check_kissat_version.sh
2626
# Formatting check
2727
${SCRIPT_DIR}/kani-fmt.sh --check
2828

29-
# Build all packages in the workspace
30-
cargo build-dev
29+
# Build all packages in the workspace and ensure no warning is emitted.
30+
RUSTFLAGS="-D warnings" cargo build-dev
3131

3232
# Unit tests
3333
cargo test -p cprover_bindings

0 commit comments

Comments
 (0)