From b907b418ef6985acacfcd707ff859d1318c772f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20Tj=C3=A4der?= <henrik@tjaders.com> Date: Mon, 5 Mar 2018 00:09:09 +0100 Subject: [PATCH] Updated the README to reflect the updates to the script --- README.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/README.md b/README.md index 88dae5a..b7df320 100644 --- a/README.md +++ b/README.md @@ -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 -- GitLab