Skip to content

Commit

Permalink
Change how we enforce deny warnings (#2672)
Browse files Browse the repository at this point in the history
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
  • Loading branch information
celinval committed Aug 11, 2023
1 parent 596bc50 commit 404fc41
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 3 deletions.
1 change: 0 additions & 1 deletion kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@
//!
//! Like miri, clippy, and other tools developed on the top of rustc, we rely on the
//! rustc_private feature and a specific version of rustc.
#![deny(warnings)]
#![feature(extern_types)]
#![recursion_limit = "256"]
#![feature(box_patterns)]
Expand Down
4 changes: 2 additions & 2 deletions scripts/kani-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ check_kissat_version.sh
# Formatting check
${SCRIPT_DIR}/kani-fmt.sh --check

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

# Unit tests
cargo test -p cprover_bindings
Expand Down

0 comments on commit 404fc41

Please sign in to comment.