diff --git a/klee-examples/.vscode/settings.json b/klee-examples/.vscode/settings.json index 1635b458a41518480db8b89beb7d6641e07638f9..a8a3dd8da3ed1224ff89619eae1a71274e2b61d9 100644 --- a/klee-examples/.vscode/settings.json +++ b/klee-examples/.vscode/settings.json @@ -1,6 +1,9 @@ { "cSpell.ignoreWords": [ + "eabihf", "istats", - "ktest" + "klee_make_symbolic", + "ktest", + "thumbv" ] } \ No newline at end of file diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml index 801094d815517351606e5737b719853d8e9d5a52..619b90b7d6a10f98b903ec1d9a8646b1b55746ec 100644 --- a/klee-examples/Cargo.toml +++ b/klee-examples/Cargo.toml @@ -2,7 +2,7 @@ name = "cargo_klee_examples" version = "0.3.0" authors = ["pln <Per Lindgren>"] -edition = "2018" +edition = "2021" [dependencies.klee-sys] git = "https://gitlab.henriktjader.com/pln/klee-sys.git" @@ -27,4 +27,3 @@ debug = true # better debugging incremental = false # better optimization lto = true # better optimization codegen-units = 1 # better optimization - diff --git a/klee-examples/examples/get_sign.rs b/klee-examples/examples/get_sign.rs index 418f7b404c9cff289ecfeaaea28c23f518972634..717a16ebea49edaf367c3d4b8c5e6043af7c4b2f 100644 --- a/klee-examples/examples/get_sign.rs +++ b/klee-examples/examples/get_sign.rs @@ -32,13 +32,14 @@ fn main() { // Compile a Rust program for KLEE test case generation. // -// > cargo klee --examples get_sign +// > cargo klee --example get_sign // ... // // KLEE: Using Z3 solver backend // // KLEE: done: total instructions = 89 // KLEE: done: completed paths = 3 +// KLEE: done: partially completed paths = 0 // KLEE: done: generated tests = 3 // // To view the generated tests: diff --git a/klee-examples/src/main.rs b/klee-examples/src/main.rs new file mode 100644 index 0000000000000000000000000000000000000000..1a6b0753f08442ead59eee62f6f3a7b5589c58f7 --- /dev/null +++ b/klee-examples/src/main.rs @@ -0,0 +1,31 @@ +// Testing a small Rust function. +// Inspired by `get_sign` https://klee.github.io/tutorials/testing-function/ + +// Here, we do not want to analyse the Rust run-time, thus `no_std`. +#![no_std] +#![no_main] + +// Low level binding(s) to the KLEE API. +use klee_sys::klee_make_symbolic; + +// Binding of Rust `panic` to KLEE `abort`. +use panic_klee as _; + +fn get_sign(x: i32) -> i32 { + if x == 0 { + return 0; + } + if x < 0 { + return -1; + } else { + return 1; + } +} + +// KLEE needs the non mangled `main` symbol. +#[no_mangle] +fn main() { + let mut a: i32 = 0; + klee_make_symbolic!(&mut a, "a"); + get_sign(a); +}