Select Git revision
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())
})
};
}