klee_assert! as macro

allows multiple assert fails to be reported by klee

klee/src/lib.rs

@@ -7,7 +7,7 @@ extern crate cstr_core;
 extern crate cty;
 
 // mod lang_items;
-mod ll;
+pub mod ll;
 
 use core::mem;
 
@@ -42,7 +42,7 @@ pub fn k_mk_symbol<T>(t: &mut T, name: &CStr) {
     }
 }
 
-#[inline(never)]
+#[inline(always)]
 pub fn k_abort() -> ! {
     unsafe {
         ll::abort();
@@ -50,7 +50,7 @@ pub fn k_abort() -> ! {
 }
 
 /// assume a condition involving symbolic variables
-#[inline(never)]
+#[inline(always)]
 pub fn k_assume(cond: bool) {
     unsafe {
         ll::klee_assume(cond);
@@ -58,10 +58,12 @@ pub fn k_assume(cond: bool) {
 }
 
 /// assert a condition involving symbolic variables
-#[inline(never)]
+#[inline(always)]
 pub fn k_assert(e: bool) {
     if !e {
-        k_abort();
+        unsafe {
+            ll::abort();
+        }
     }
 }
 
@@ -80,6 +82,21 @@ macro_rules! k_symbol {
     }
 }
 
+/// assertion
+#[macro_export]
+macro_rules! k_assert {
+    ($e: expr) => {
+        {
+            use klee::ll;
+            if !$e {
+                unsafe {
+                    ll::abort();
+                }
+            }
+        }
+    }
+}
+
 #[macro_export]
 macro_rules! k_visit {
     ()=> {