lib.rs

#![no_std]

// use core::intrinsics;
// use core::panic::PanicInfo;

// #[panic_handler]
// fn panic(_info: &PanicInfo) -> ! {
//     unsafe { intrinsics::abort() }
// }

// #[lang = "eh_personality"]
// extern "C" fn eh_personality() {}
// extern crate cstr_core;

// // #[cfg(feature = "klee-analysis")]
// // mod lang_items;
// #[cfg(feature = "klee-analysis")]
// pub mod ll;

// #[cfg(feature = "klee-analysis")]
// use core::ffi::c_void;

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

// /// Aborts the path in KLEE mode, does nothing otherwise
// #[macro_export]
// macro_rules! kabort {
//     () => {
//         #[cfg(feature = "klee-analysis")]
//         unsafe { $crate::ll::abort() };
//     };
// }

// #[cfg(feature = "klee-analysis")]
// pub fn kassume(cond: bool) {
//     unsafe {
//         ll::klee_assume(cond);
//     }
// }

// #[cfg(not(feature = "klee-analysis"))]
// pub fn kassume(_cond: bool) {}

// #[cfg(feature = "klee-analysis")]
// pub fn kmksymbol<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(),
//         )
//     }
// }

// #[cfg(not(feature = "klee-analysis"))]
// pub fn kmksymbol<T>(_t: &mut T, _name: &'static CStr) {}

// #[macro_export]
// macro_rules! ksymbol {
//     (&mut $id:expr, $name:expr) => {
//         $crate::kmksymbol(unsafe { &mut $id }, unsafe {
//             $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
//         })
//     };
// }

// /// If in KLEE mode, the assertion is made.
// /// Otherwise, this is does nothing.
// #[macro_export]
// macro_rules! kassert {
//     ($e:expr) => {
//         #[cfg(feature = "klee-analysis")]
//         {
//             if !$e {
//                 $crate::kabort!();
//             }
//         }
//     };
// }

use core::ffi::c_void;

extern "C" {
    pub fn abort() -> !;
    pub fn klee_assume(cond: bool);
    pub fn klee_make_symbolic(ptr: *mut c_void, size: usize, name: *const i8);
}