From c3b8fe4fd03ab6d271f112a0f6bfb7a861bfba71 Mon Sep 17 00:00:00 2001 From: Per Lindgren <per.lindgren@ltu.se> Date: Sun, 11 Mar 2018 14:10:39 +0100 Subject: [PATCH] Readme updated --- README.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index b7df320..8118940 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,9 @@ # Klee based analysis. +## Exam +Details are found in `klee.py` + ## Complilation 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. 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. @@ -78,6 +81,11 @@ The steps described separately: ``` 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 @@ -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 +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. From there you can run various commands like: -- GitLab