lib_klee_replay.rs

use core::ffi::c_void;
use cstr_core::c_char;

#[doc(hidden)]
pub use cstr_core::CStr;

#[inline(always)]
fn klee_abort() -> ! {
    panic!();
}

/// 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 {
        asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile")
    }
}

/// 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 })
    };
}