klee-examples

klee-examples/Cargo.toml

+[package]
+name = "klee-examples"
+version = "0.1.0"
+authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
+
+[dependencies]
+klee = {path=".."}
+
+[profile.release]
+debug = true
+panic = "abort"
+lto = true
\ No newline at end of file

klee-examples/examples/foo.rs

+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+#[no_mangle]
+fn main() {
+    let u = ksymbol!("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 {
+    100 / u
+}