diff --git a/klee-examples/Xargo.toml b/klee-examples/Xargo.toml new file mode 100644 index 0000000000000000000000000000000000000000..89ad4cdcaeb6cce198c64fb0e03f570429243b42 --- /dev/null +++ b/klee-examples/Xargo.toml @@ -0,0 +1,6 @@ +[dependencies.core] +stage = 0 + +[dependencies.compiler_builtins] +features = ["mem"] +stage = 1 \ No newline at end of file diff --git a/klee/src/lib.rs b/klee/src/lib.rs index af4cc48ec414ed1ca955c70a2e8046cf2f38e60d..3f21d50c1cf92f64daa5f057747a2e4db0666fb8 100644 --- a/klee/src/lib.rs +++ b/klee/src/lib.rs @@ -1,6 +1,8 @@ #![no_std] +#![feature(compiler_builtins_lib)] #![feature(lang_items)] +extern crate compiler_builtins; extern crate cstr_core; extern crate cty; @@ -9,17 +11,11 @@ mod ll; use core::mem; -use cty::{c_int, c_void}; +use cty::c_void; #[doc(hidden)] pub use cstr_core::CStr; -//extern "C" fn memcmp(cx: *const c_void, ct: *const c_void, n: size_t) -> c_int { -#[no_mangle] -pub fn memcmp(_cx: *const c_void, _ct: *const c_void, _n: usize) -> c_int { - ::abort(); -} - pub fn abort() -> ! { unsafe { ll::abort() } }