diff --git a/klee/src/lib.rs b/klee/src/lib.rs index 52044219ae206d843aec228f9537609a08c9a2a5..31b22b5a9e06768687b0431e00d2926a42a1e730 100644 --- a/klee/src/lib.rs +++ b/klee/src/lib.rs @@ -7,7 +7,7 @@ extern crate cstr_core; extern crate cty; // mod lang_items; -pub mod ll; +mod ll; use core::mem; @@ -42,7 +42,7 @@ pub fn k_mk_symbol<T>(t: &mut T, name: &CStr) { } } -#[inline(always)] +#[inline(never)] pub fn k_abort() -> ! { unsafe { ll::abort(); @@ -50,7 +50,7 @@ pub fn k_abort() -> ! { } /// assume a condition involving symbolic variables -#[inline(always)] +#[inline(never)] pub fn k_assume(cond: bool) { unsafe { ll::klee_assume(cond); @@ -58,12 +58,10 @@ pub fn k_assume(cond: bool) { } /// assert a condition involving symbolic variables -#[inline(always)] +#[inline(never)] pub fn k_assert(e: bool) { if !e { - unsafe { - ll::abort(); - } + k_abort(); } } @@ -72,27 +70,12 @@ pub fn k_assert(e: bool) { macro_rules! k_symbol { ($id:expr, $name:expr) => { { - #[allow(unsafe_code)] - #[allow(warnings)] - $crate::k_mk_symbol( - unsafe { $id }, - unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) } - ) - } - } -} - -/// assertion -#[macro_export] -macro_rules! k_assert { - ($e: expr) => { - { - use klee::ll; - if !$e { - unsafe { - ll::abort(); - } - } + #[allow(unsafe_code)] + #[allow(warnings)] + $crate::k_mk_symbol( + unsafe { $id }, + unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) } + ) } } }