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

lib.rs

Blame
  • Forked from Per Lindgren / klee-sys
    Source project has a limited visibility.
    lib.rs 940 B
    #![no_std]
    
    use core::ffi::c_void;
    #[doc(hidden)]
    pub use cstr_core::CStr;
    
    pub mod ll;
    
    pub mod panic;
    
    //#[inline(always)]
    #[inline(never)]
    pub fn klee_abort() -> ! {
        unsafe { ll::abort() };
    }
    
    #[inline(always)]
    pub fn klee_assume(cond: bool) {
        unsafe {
            ll::klee_assume(cond);
        }
    }
    
    // #[inline(always)]
    // pub fn klee_assert(cond: bool) {
    //     if !cond {
    //         klee_abort();
    //     }
    // }
    
    #[inline(always)]
    fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
        unsafe {
            ll::klee_make_symbolic(
                t as *mut T as *mut c_void,
                core::mem::size_of::<T>(),
                name.as_ptr() as *const u8,
            )
        }
    }
    
    #[macro_export]
    macro_rules! klee_make_symbolic {
        (&mut $id:expr, $name:expr) => {
            $crate::klee_make_symbolic(unsafe { &mut $id }, unsafe {
                $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
            })
        };
    }