Initial commit

.gitignore

+/target
+**/*.rs.bk
+Cargo.lock

Cargo.toml

+[package]
+name = "klee-sys"
+version = "0.1.0"
+authors = ["pln <Per Lindgren>"]
+edition = "2018"
+
+[dependencies]
+cstr_core = "0.1.2"
+
+[features]
+klee-analysis = []

README.md

+# klee-sys
+
+Low-level bindings to LLVM-KLEE.

src/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);
+}