Skip to content
Snippets Groups Projects
Select Git revision
  • 82e9a08fb47db931574c0afc7025ae5073739f9b
  • master default protected
2 results

compile.txt

Blame
  • Forked from Per Lindgren / klee-examples
    Source project has a limited visibility.
    lib_klee_replay.rs 941 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 {
            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 })
        };
    }