Make stable mir reachability default

model-checking · Nov 25, 2023 · de0c793 · de0c793
1 parent 66866b3
commit de0c793
Show file tree

Hide file tree

Showing 4 changed files with 279 additions and 1,068 deletions.
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -30,7 +30,6 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
 default = ['cprover']
 cprover = ['cbmc', 'num', 'serde']
 write_json_symtab = []
-stable_mir = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
@@ -33,16 +33,10 @@ pub mod coercion;
 mod intrinsics;
 pub mod metadata;
 pub mod provide;
-#[cfg(not(feature = "stable_mir"))]
 pub mod reachability;
-#[cfg(feature = "stable_mir")]
-pub mod reachability_smir;
 pub mod resolve;
 pub mod stubbing;
 
-#[cfg(feature = "stable_mir")]
-pub use reachability_smir as reachability;
-
 /// Check that all crate items are supported and there's no misconfiguration.
 /// This method will exhaustively print any error / warning and it will abort at the end if any
 /// error was found.