diff --git a/README.md b/README.md index 78be56fed8ec350075affbac071dc5e9788bfd0d..5c5dcab24ac2d82b9162769b25c8a1c5ff763217 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,67 @@ # 1 minute introduction +## requirements +- docker +- nightly toolchain + +## usage + ``` console +$ systemctl start docker.service # if not already started/enabled + $ cargo install --path cargo-klee # add -f, if already installed $ cd klee-examples $ cargo klee --example foo --release + +KLEE: output directory is "/mnt/target/release/examples/klee-out-0" +KLEE: Using STP solver backend +KLEE: ERROR: /home/pln/klee/klee-rust/klee/src/lib.rs:24: abort failure +KLEE: NOTE: now ignoring this error at this location + +KLEE: done: total instructions = 20 +KLEE: done: completed paths = 2 +KLEE: done: generated tests = 2 + +$ more target/release/examples/klee-out-0/test000001.abort.err +Error: abort failure +File: /home/pln/klee/klee-rust/klee/src/lib.rs +Line: 24 +assembly.ll line: 76 +Stack: + #000000076 in _ZN4core9panicking9panic_fmt17hc7d7358b749037fdE () at /home/pln/klee/klee-rust/klee/src/lib.rs:24 + #100000070 in _ZN4core9panicking5panic17h4680eb5ae9b0e3d0E () at HOME/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/pani +cking.rs:51 + #200000044 in main (=1, =94362321163792) at PWD/klee-examples/examples/foo.rs:22 + ``` + +The error found is at line 22. + +``` rust + +#![no_std] + +#[macro_use] +extern crate klee; + +use core::ptr; + +fn main() { + let u = ksymbol!("u"); + + unsafe { + ptr::read_volatile(&f2(f1(u))); + } +} + +// add 1 wrapping +fn f1(u: u8) -> u8 { + u.wrapping_add(1) +} + +fn f2(u: u8) -> u8 { + 100 / u // <- error found here is a Rust div 0 panic! . +} +``` \ No newline at end of file diff --git a/rls1509755957780.log b/rls1509755957780.log deleted file mode 100644 index a29dede1f0aa9fb441095f9c518bbd6a570dae8a..0000000000000000000000000000000000000000 --- a/rls1509755957780.log +++ /dev/null @@ -1,6 +0,0 @@ -error: expected expression, found `+` - --> stdin:22:11 - | -22 | j++; - | ^ -