compile.txt

//#[cfg(not(feature = "inline-asm"))]
//compile_error!("klee-replay requires feature `inline-asm`");

/// suppress assumption
#[inline(always)]
pub fn klee_assume(_cond: bool) {}

#[inline(always)]
pub fn klee_make_symbolic<T>(t: &mut T) {
    // force LLVM to consider data to be mutated
    unsafe {
        core::arch::asm!("bkpt #3")
    }
}

/// terminates path
#[macro_export]
macro_rules! klee_abort {
    () => {
        panic!()
    };
}

/// conditionally terminates path
#[macro_export]
macro_rules! klee_assert {
    ($e:expr) => {
        assert!($e)
    };
}

/// conditionally terminates path
#[macro_export]
macro_rules! klee_assert_eq {
    ($e1:expr, $e2:expr ) => {
        assert_eq!($e1, $e2)
    };
}

/// makes mutable reference symbolic associated to static string
#[macro_export]
macro_rules! klee_make_symbolic {
    (&mut $id:expr, $name:expr) => {
        $crate::klee_make_symbolic(unsafe { &mut $id })
    };
}