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

Readme updated

parent 40facbca
No related branches found
No related tags found
No related merge requests found
...@@ -11,6 +11,9 @@ ...@@ -11,6 +11,9 @@
# Klee based analysis. # Klee based analysis.
## Exam
Details are found in `klee.py`
## Complilation ## Complilation
Use a Rust toolchain with a llvm4 backend, e.g., nightly-2018-01-10-x86_64-unknown-linux-gnu. Use a Rust toolchain with a llvm4 backend, e.g., nightly-2018-01-10-x86_64-unknown-linux-gnu.
...@@ -64,7 +67,7 @@ A docker daemon should be started/enabled. ...@@ -64,7 +67,7 @@ A docker daemon should be started/enabled.
In the current folder: In the current folder:
``` ```
arm-none-eabi-gdb -x klee_stm_gdb.py arm-none-eabi-gdb -x klee.py
``` ```
The script will build for both KLEE and the MCU, run the KLEE tests and then proceed with testing the KLEE-generated values on the MCU. The script will build for both KLEE and the MCU, run the KLEE tests and then proceed with testing the KLEE-generated values on the MCU.
...@@ -78,6 +81,11 @@ The steps described separately: ...@@ -78,6 +81,11 @@ The steps described separately:
``` ```
xargo build --example example_name --features klee_mode --target x86_64-unknown-linux-gnu xargo build --example example_name --features klee_mode --target x86_64-unknown-linux-gnu
``` ```
or for analysis on optimized code (you may need to do manually)
```
xargo build --release --example example_name --features klee_mode --target x86_64-unknown-linux-gnu
```
### Compilation for benchmarking on MCU ### Compilation for benchmarking on MCU
...@@ -90,6 +98,9 @@ xargo build --release --example example_name --features wcet_bkpt --target thum ...@@ -90,6 +98,9 @@ xargo build --release --example example_name --features wcet_bkpt --target thum
> docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
or
> docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
This starts a shell in the docker `llvm-klee-4`, with a shared mount to the examples directory, where your `panic1-xxxx.bc` is located. This starts a shell in the docker `llvm-klee-4`, with a shared mount to the examples directory, where your `panic1-xxxx.bc` is located.
From there you can run various commands like: From there you can run various commands like:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment