From f30fd92bac9de11155e0ff6b492b09fcf0bd2e03 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Fri, 17 Jan 2020 23:09:43 +0100
Subject: [PATCH] compiler error on missing feauture
---
src/lib.rs | 3 +++
src/lib_klee_analysis.rs | 7 +------
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/lib.rs b/src/lib.rs
index e1c3032..ddf1d7b 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 d8a30c2..08deefc 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 {
--
GitLab