Skip to content
Snippets Groups Projects
Commit a7968bec authored by Per Lindgren's avatar Per Lindgren
Browse files

lib.rs

parent 111b305c
No related branches found
No related tags found
No related merge requests found
Pipeline #100 canceled
......@@ -10,8 +10,6 @@ mod lang_items;
#[cfg(feature = "klee-analysis")]
pub mod ll;
use core::mem;
#[cfg(feature = "klee-analysis")]
use core::ffi::c_void;
......@@ -39,32 +37,12 @@ pub fn kassume(cond: bool) {
#[cfg(not(feature = "klee-analysis"))]
pub fn kassume(_cond: bool) {}
#[doc(hidden)]
#[inline]
#[cfg(feature = "klee-analysis")]
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
}
#[cfg(not(feature = "klee-analysis"))]
pub fn ksymbol<T>(_name: &CStr) -> T {
unsafe { mem::uninitialized() }
}
#[cfg(feature = "klee-analysis")]
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>(),
core::mem::size_of::<T>(),
name.as_ptr(),
)
}
......@@ -75,11 +53,6 @@ pub fn kmksymbol<T>(_t: &mut T, _name: &CStr) {}
#[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())
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment