lib fix + examples

klee-examples/examples/cc_loop.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    let mut j = 0;
+    for _i in 0..u {
+        j += 1;
+    }
+    j
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}

klee-examples/examples/cc_native_add.rs

+#![no_std]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u + 1
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}

klee-examples/examples/cc_saturating.rs

+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ops::Add;
+
+use core::ptr;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 saturating
+fn f1(u: u8) -> u8 {
+    //if u < 255 { u + 1 } else { u } 
+    u.checked_add(1).unwrap_or(u)
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}

klee-examples/examples/cc_wrapping.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+ use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div( 100, u) }
+}

klee-examples/examples/foo.rs

@@ -13,7 +13,7 @@ fn main() {
     }
 }
 
-// add 1 and saturate
+// add 1 wrapping
 fn f1(u: u8) -> u8 {
     u.wrapping_add(1)
 }

klee/src/lib.rs

@@ -9,11 +9,17 @@ mod ll;
 
 use core::mem;
 
-use cty::c_void;
+use cty::{c_int, 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() }
 }