build:
docker build -t rkd .
run:
docker run --rm -it rkd
you can test klee with klee-example
:
Go to klee-example
:
cd cargo-klee/klee-examples
Compile to llvm-ir
(you can also compile to llvm-bc
)
cargo rustc -v --features klee-analysis --example get_sign --color=always -- -C linker=true -C lto --emit=llvm-ir
Run klee on the .ll
file (or .bc
file if you used llvm-bc
)
klee target/debug/examples/get_sign*.ll
output:
KLEE: output directory is "/home/arch/klee-example/target/debug/examples/klee-out-0"
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
cargo klee --example get_sign
rustup: 1.51.0
klee: 2.2
LLVM: 10.0.0
Thanks henriktjader
for:
cargo klee
: https://gitlab.henriktjader.com/pln/cargo-kleeklee_tutorial
: https://gitlab.henriktjader.com/pln/klee_tutorial