diff --git a/src/lib.rs b/src/lib.rs index e1c30328bb8063da484ef85a279897eb3bf440d9..ddf1d7bce9e56a9e53d806620c0779d1f649e1ce 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -29,3 +29,6 @@ pub use lib_klee_analysis::*; // functions and macros mod lib_klee_replay; #[cfg(feature = "klee-replay")] pub use lib_klee_replay::*; // functions and macros + +#[cfg(all(not(feature = "klee-analysis"), not(feature = "klee-replay")))] +compile_error!("feature required, either `klee-analysis` or `klee-replay`"); diff --git a/src/lib_klee_analysis.rs b/src/lib_klee_analysis.rs index d8a30c2c25ccbe2c5c5b80d8d55cf5e6f2678982..08deefce70af09f909e277f08cf9635ade6c872f 100644 --- a/src/lib_klee_analysis.rs +++ b/src/lib_klee_analysis.rs @@ -4,11 +4,6 @@ use cstr_core::c_char; #[doc(hidden)] pub use cstr_core::CStr; -#[inline(always)] -fn klee_abort() -> ! { - unsafe { crate::ll::abort() }; -} - /// introduces assumption #[inline(always)] pub fn klee_assume(cond: bool) { @@ -17,7 +12,7 @@ pub fn klee_assume(cond: bool) { } } -/// makes refence symbolic +/// makes reference symbolic #[inline(always)] pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) { unsafe {