Skip to content
Snippets Groups Projects
Commit 436f05fe authored by Per Lindgren's avatar Per Lindgren
Browse files

examples

parent eeb224f3
No related branches found
No related tags found
No related merge requests found
{
"cSpell.ignoreWords": [
"eabihf",
"istats",
"ktest"
"klee_make_symbolic",
"ktest",
"thumbv"
]
}
\ No newline at end of file
......@@ -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
......@@ -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:
......
// 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);
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment