Select Git revision
lib_klee_replay.rs
Forked from
KLEE / klee-sys
Source project has a limited visibility.
-
Per Lindgren authoredPer Lindgren authored
lib_klee_replay.rs 993 B
#[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 {
llvm_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 })
};
}