Plumbing for Boogie backend (#2506)

model-checking · Dec 13, 2023 · d8dc0ad · d8dc0ad
1 parent a7c239e
commit d8dc0ad
Show file tree

Hide file tree

Showing 19 changed files with 840 additions and 18 deletions.
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -27,7 +27,8 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
-default = ['cprover']
+default = ['boogie', 'cprover']
+boogie = ['serde']
 cprover = ['cbmc', 'num', 'serde']
 write_json_symtab = []
 

diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
@@ -4,6 +4,20 @@
 use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 use tracing_subscriber::filter::Directive;
 
+#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
+#[strum(serialize_all = "snake_case")]
+pub enum BackendOption {
+    /// Boogie backend
+    Boogie,
+
+    /// CProver (Goto) backend
+    CProver,
+
+    /// Backend option was not explicitly set
+    #[default]
+    None,
+}
+
 #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityType {
@@ -68,7 +82,6 @@ pub struct Arguments {
     #[clap(long)]
     /// Pass the kani version to the compiler to ensure cache coherence.
     check_version: Option<String>,
-    #[clap(long)]
-    /// A legacy flag that is now ignored.
-    goto_c: bool,
+    #[clap(long = "backend", default_value = "none")]
+    pub backend: BackendOption,
 }