Select Git revision
lib.rs 1.49 KiB
#![no_std]
#![feature(compiler_builtins_lib)]
#![feature(lang_items)]
#![feature(core_intrinsics)]
extern crate cstr_core;
mod lang_items;
pub mod ll;
pub mod mutex;
use core::mem;
use core::ffi::c_void;
#[doc(hidden)]
pub use cstr_core::CStr;
#[inline(always)]
pub fn abort() -> ! {
unsafe { ll::abort() }
}
#[inline(always)]
pub fn kassume(cond: bool) {
unsafe {
ll::klee_assume(cond);
}
}
#[doc(hidden)]
#[inline]
pub fn ksymbol<T>(name: &CStr) -> T {
let mut t: T = unsafe { mem::uninitialized() };
unsafe {
ll::klee_make_symbolic(
&mut t as *mut T as *mut c_void,
mem::size_of::<T>(),
name.as_ptr(),
)
}
t
}
pub fn kmksymbol<T>(t: &mut T, name: &CStr) {
unsafe {
ll::klee_make_symbolic(
t as *mut T as *mut c_void,
mem::size_of::<T>(),
name.as_ptr(),
)
}
}
#[macro_export]
macro_rules! ksymbol {
($name:expr) => {
$crate::ksymbol(unsafe {
$crate::CStr::from_bytes_with_nul_unchecked(
concat!($name, "\0").as_bytes(),
)
})
};
(&mut $id:expr, $name:expr) => {
$crate::kmksymbol(unsafe { &mut $id }, unsafe {
$crate::CStr::from_bytes_with_nul_unchecked(
concat!($name, "\0").as_bytes(),
)
})
};
}
#[macro_export]
macro_rules! kassert {
($e:expr) => {
if !$e {
unsafe { $crate::ll::abort() }
}
};
}