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

rust wip (inccomlpete)

parent d80c56a9
No related branches found
No related tags found
No related merge requests found
[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
// 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment