Skip to content
Snippets Groups Projects
Select Git revision
  • 02835397656fb497b5f607ceabdf0831dc710b7e
  • master default protected
2 results

lib_klee_replay.rs

Blame
  • Forked from KLEE / klee-sys
    Source project has a limited visibility.
    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 })
        };
    }