lib_klee_analysis.rs

use core::ffi::c_void;
use cstr_core::c_char;

#[doc(hidden)]
pub use cstr_core::CStr;

/// introduces assumption
#[inline(always)]
pub fn klee_assume(cond: bool) {
    unsafe {
        crate::ll::klee_assume(cond);
    }
}

/// makes reference symbolic
#[inline(always)]
pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
    unsafe {
        crate::ll::klee_make_symbolic(
            t as *mut T as *mut c_void,
            core::mem::size_of::<T>(),
            name.as_ptr() as *const c_char,
        )
    }
}

/// terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_abort {
    () => {
        unsafe { $crate::ll::abort() };
    };
}

/// conditionally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert {
    ($e:expr) => {{
        if !$e {
            unsafe { $crate::ll::abort() };
        }
    }};
}

/// conditionally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert_eq {
    ($e1:expr, $e2:expr ) => {{
        if !($e1 == $e2) {
            unsafe { $crate::ll::abort() };
        }
    }};
}

/// 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 }, unsafe {
            $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
        })
    };
}