From 9ad7eebf20257aed630bc53fb509bee63476199d Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 3 Mar 2023 16:07:14 -0800 Subject: [PATCH] Minor cleanup for kani-compiler (#2263) --- Cargo.lock | 1 - kani-compiler/Cargo.toml | 3 +-- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- kani-compiler/src/kani_compiler.rs | 1 + 4 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ae60ec6456473..5c2bb76e44954 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -497,7 +497,6 @@ version = "0.22.0" dependencies = [ "ar", "atty", - "bitflags", "clap", "cprover_bindings", "home", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index f8770975702cf..8259acdb73ab3 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -11,7 +11,6 @@ publish = false [dependencies] ar = { version = "0.9.0", optional = true } atty = "0.2.14" -bitflags = { version = "1.0", optional = true } cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } clap = { version = "4.1.3", features = ["cargo"] } home = "0.5" @@ -36,7 +35,7 @@ tracing-tree = "0.2.2" # Future proofing: enable backend dependencies using feature. [features] default = ['cprover'] -cprover = ['ar', 'bitflags', 'cbmc', 'libc', 'num', 'object', 'rustc-demangle', 'serde', +cprover = ['ar', 'cbmc', 'libc', 'num', 'object', 'rustc-demangle', 'serde', 'serde_json', "strum", "strum_macros"] unsound_experiments = ["kani_queries/unsound_experiments"] diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 56f5142a1b19d..11ba4916025db 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -12,7 +12,6 @@ use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items, }; -use bitflags::_core::any::Any; use cbmc::goto_program::Location; use cbmc::{InternedString, MachineModel}; use kani_metadata::CompilerArtifactStub; @@ -39,6 +38,7 @@ use rustc_session::Session; use rustc_span::def_id::DefId; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; +use std::any::Any; use std::collections::BTreeMap; use std::ffi::OsString; use std::fmt::Write; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index f958cbe294924..51b12a00f9adb 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,6 +15,7 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. +#[cfg(feature = "cprover")] use crate::codegen_cprover_gotoc::GotocCodegenBackend; use crate::kani_middle::stubbing; use crate::parser::{self, KaniCompilerParser};