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

Readme

parent c0796c44
No related branches found
No related tags found
No related merge requests found
# 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
error: expected expression, found `+`
--> stdin:22:11
|
22 | j++;
| ^
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment