diff --git a/src/lib.rs b/src/lib.rs index 401d045000ba78eb40a88a9675d64945e0548411..9be2219b5ff0bcc3a3b375787030358a840680dc 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -9,7 +9,7 @@ pub use cstr_core::CStr; pub mod ll; #[inline(always)] -pub fn klee_abort() -> ! { +fn klee_abort() -> ! { unsafe { ll::abort() }; } @@ -31,6 +31,7 @@ pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) { } } +/// terminates path (and generates unique test) #[macro_export] macro_rules! klee_abort { () => { @@ -38,6 +39,7 @@ macro_rules! klee_abort { }; } +/// conditionally terminates path (and generates unique test) #[macro_export] macro_rules! klee_assert { ($e:expr) => {{ @@ -47,6 +49,7 @@ macro_rules! klee_assert { }}; } +/// condititonally terminates path (and generates unique test) #[macro_export] macro_rules! klee_assert_eq { ($e1:expr, $e2:expr ) => {{ @@ -56,6 +59,7 @@ macro_rules! klee_assert_eq { }}; } +/// makes mutable reference symbolic associated to static string #[macro_export] macro_rules! klee_make_symbolic { (&mut $id:expr, $name:expr) => {