From 54e2dd555f0826fc3c38902f7479c003cea2ba4e Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Sat, 4 Nov 2017 02:00:27 +0100
Subject: [PATCH] lib fix + examples

---
 klee-examples/examples/cc_loop.rs       | 29 +++++++++++++++++++++++++
 klee-examples/examples/cc_native_add.rs | 23 ++++++++++++++++++++
 klee-examples/examples/cc_saturating.rs | 25 +++++++++++++++++++++
 klee-examples/examples/cc_wrapping.rs   | 25 +++++++++++++++++++++
 klee-examples/examples/foo.rs           |  2 +-
 klee/src/lib.rs                         |  8 ++++++-
 6 files changed, 110 insertions(+), 2 deletions(-)
 create mode 100644 klee-examples/examples/cc_loop.rs
 create mode 100644 klee-examples/examples/cc_native_add.rs
 create mode 100644 klee-examples/examples/cc_saturating.rs
 create mode 100644 klee-examples/examples/cc_wrapping.rs

diff --git a/klee-examples/examples/cc_loop.rs b/klee-examples/examples/cc_loop.rs
new file mode 100644
index 0000000..b3dcaaa
--- /dev/null
+++ b/klee-examples/examples/cc_loop.rs
@@ -0,0 +1,29 @@
+#![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) }
+}
diff --git a/klee-examples/examples/cc_native_add.rs b/klee-examples/examples/cc_native_add.rs
new file mode 100644
index 0000000..6f272c7
--- /dev/null
+++ b/klee-examples/examples/cc_native_add.rs
@@ -0,0 +1,23 @@
+#![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
+}
diff --git a/klee-examples/examples/cc_saturating.rs b/klee-examples/examples/cc_saturating.rs
new file mode 100644
index 0000000..2ee2f41
--- /dev/null
+++ b/klee-examples/examples/cc_saturating.rs
@@ -0,0 +1,25 @@
+#![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
+}
diff --git a/klee-examples/examples/cc_wrapping.rs b/klee-examples/examples/cc_wrapping.rs
new file mode 100644
index 0000000..2689548
--- /dev/null
+++ b/klee-examples/examples/cc_wrapping.rs
@@ -0,0 +1,25 @@
+#![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) }
+}
diff --git a/klee-examples/examples/foo.rs b/klee-examples/examples/foo.rs
index 4de0a25..83851e4 100644
--- a/klee-examples/examples/foo.rs
+++ b/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)
 }
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index 75ad8d9..f2b035b 100644
--- a/klee/src/lib.rs
+++ b/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() }
 }
-- 
GitLab