painc

.gitignore

+/target
+**/*.rs.bk

Cargo.lock

+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "cstr_core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "cty"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "klee-examples"
+version = "0.1.0"
+dependencies = [
+ "klee-sys 0.1.0",
+ "panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "klee-sys"
+version = "0.1.0"
+dependencies = [
+ "cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "memchr"
+version = "2.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "panic-halt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[metadata]
+"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
+"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
+"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
+"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"

Cargo.toml

+[package]
+name = "klee-examples"
+version = "0.1.0"
+authors = ["pln <Per Lindgren>"]
+edition = "2018"
+
+[dependencies]
+panic-halt = "0.2.0"
+
+[dependencies.klee-sys]
+path = "../klee-sys"
+
+[features] 
+klee-analysis = ["klee-sys/klee-analysis"]
+
+[profile.dev]
+panic = "abort"
+
+[profile.release]
+debug = true
+panic = "abort"
+incremental = false
+lto = true

examples/kabort.rs

+#![no_std]
+#![no_main]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_make_symbolic};
+
+#[cfg(not(feature = "klee-analysis"))]
+use panic_halt as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    // ksymbol!(&mut a, "a");
+    panic!();
+}
+
+#[cfg(feature = "klee-analysis")]
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    klee_make_symbolic(&mut a, "a");
+    // match a {
+    //     0 => klee_abort(),
+    //     2 => klee_abort(),
+    //     _ => (),
+    // };
+    panic();
+}

examples/struct.rs

+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee_sys;
+
+#[cfg(not(feature = "klee-analysis"))]
+extern crate panic_halt;
+
+struct A {
+    a: u8,
+    b: u32,
+}
+
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    // ksymbol!(&mut a, "a");
+    let mut u = A { a: a, b: 0 };
+    u.b = 7;
+    let _ = f2(f1(u.a));
+}
+
+// add 1 wrapping instead of panic
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}