Skip to content
Snippets Groups Projects
Commit b907b418 authored by Henrik Tjäder's avatar Henrik Tjäder
Browse files

Updated the README to reflect the updates to the script

parent 7872d539
No related branches found
No related tags found
No related merge requests found
......@@ -63,6 +63,31 @@ A docker daemon should be started/enabled.
In the current folder:
```
arm-none-eabi-gdb -x klee_stm_gdb.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 steps described separately:
### Compilation of KLEE input
```
xargo build --example example_name --features klee_mode --target x86_64-unknown-linux-gnu
```
### Compilation for benchmarking on MCU
```
xargo build --release --example example_name --features wcet_bkpt --target thumbv7em-none-eabihf
```
### Running KLEE
> 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
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.
......@@ -79,6 +104,7 @@ this will generate a test-file for each and every path encountered.
See KLEE for detailed information.
Licensed under either of
- Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE) or
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment