diff --git a/CHANGELOG.md b/CHANGELOG.md index b84b8bff335a825e8c81d921df8766a2cb29af9f..1a2f9a0828bd8d72c1adeda6ebf883da0faa9eba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,4 +4,4 @@ Most recent changes: - 2020-12-08 Update `README.md` for Ubuntu (like) system with `z3` dependency. -- 2020-12-08 Update `README.md` and `examples/get_sign` to reflect the recent `klee 2.2` and `aur` package. \ No newline at end of file +- 2020-12-08 Update `README.md` and `examples/get_sign` to reflect the recent `klee 2.2` and `aur` package. diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000000000000000000000000000000000000..c288b3d4ffef11d0950e10be999ee51cf885ffcc --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,33 @@ +[package] +name = "klee_tutorial" +version = "0.1.0" +authors = ["pln <Per Lindgren>"] +edition = "2018" + +[dependencies.panic-klee] +git = "https://gitlab.henriktjader.com/pln/panic-klee.git" +version = "0.1.0" + + +[dependencies.klee-sys] +git = "https://gitlab.henriktjader.com/pln/klee-sys.git" +# path = "../klee-sys" +version = "0.1.0" +#features = ["inline-asm"] + +[features] +klee-analysis = [ "klee-sys/klee-analysis" ] +klee-replay = [ "klee-sys/klee-replay"] + +[profile.dev] +panic = "abort" +incremental = false # better optimization +lto = true # better optimization +codegen-units = 1 # better optimization + +[profile.release] +panic = "abort" +debug = true # better debugging +incremental = false # better optimization +lto = true # better optimization +codegen-units = 1 # better optimization \ No newline at end of file diff --git a/examples/get_sign.rs b/examples/get_sign.rs new file mode 100644 index 0000000000000000000000000000000000000000..1ad6f7fb624738e3a68fdc4713d4a1ab41b3f5ae --- /dev/null +++ b/examples/get_sign.rs @@ -0,0 +1,27 @@ +// example that shows different types of path termination +// and their effect to KLEE test case generation +#![no_std] +#![no_main] + +use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic}; +use panic_klee as _; + +fn get_sign(x: i32) -> i32 { + if x == 0 { + return 0; + } + if x < 0 { + return -1; + } else { + return 1; + } +} + +#[no_mangle] +fn main() { + let mut a: i32 = 0; + klee_make_symbolic!(&mut a, "a"); + // std::process::exit(get_sign(a)); +} + +// > cargo rustc --example get_sign -- --emit=llvm-ir