diff --git a/Cargo.lock b/Cargo.lock
index 6f7b3edcde8634e2f084e64b26c3166e49fd1611..1ee0de8c724789aa9815740624ea80443af71c80 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,3 +1,5 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
[[package]]
name = "aligned"
version = "0.1.1"
@@ -82,7 +84,7 @@ dependencies = [
[[package]]
name = "cortex-m-rtfm"
-version = "0.3.1"
+version = "0.3.2"
dependencies = [
"cortex-m 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rt 0.3.13 (registry+https://github.com/rust-lang/crates.io-index)",
diff --git a/Cargo.toml b/Cargo.toml
index dff7f7dddc41ad134d65385cbff776f7bf3247b0..2df0ea10bf9a79ffe41c8e63419f560b57d1fa5c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -10,7 +10,7 @@ keywords = ["arm", "cortex-m"]
license = "MIT OR Apache-2.0"
name = "cortex-m-rtfm"
repository = "https://github.com/japaric/cortex-m-rtfm"
-version = "0.3.1"
+version = "0.3.2"
[dependencies]
cortex-m = "0.4.0"
diff --git a/README.md b/README.md
index badaa9cec16b4d66c14f936ad9fa373824321319..4baeeacb08c957d899616a2e0a0a9cfdf68f3117 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,11 @@
## Exam
Details are found in `klee.py`
-## Complilation
+## Compilation
+
+Install this version of xargo:
+
+> cargo install xargo --version 0.3.10 --force
Use a Rust toolchain with a llvm4 backend, e.g., nightly-2018-01-10-x86_64-unknown-linux-gnu.
@@ -60,10 +64,6 @@ panic = "abort"
## KLEE Analysis
-A docker daemon should be started/enabled.
-
-> systemctl start docker.service # if not already started/enabled
-
In the current folder:
```
@@ -95,15 +95,7 @@ xargo build --release --example example_name --features wcet_bkpt --target thum
### 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
-
-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:
+A native installation of KLEE required
> klee panic1-xxxxx.bc
diff --git a/examples/panic1.rs b/examples/panic1.rs
index 90ef243c3b30bbb6a819c8d13c002ad3e5039cbf..ef2fe676478888b76f018a05d5dd7d174d8f0d70 100644
--- a/examples/panic1.rs
+++ b/examples/panic1.rs
@@ -69,14 +69,8 @@ fn idle() -> ! {
//
// 2) As LLVM runs on our host we generate the `.bc` with x86 as target
//
-// Start a docker with pre-installed KLEE tools
//
-// 3> 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
-//
-// 3) This will start the docker with the right privileges and mount the directory
-// where the example `.bc` file(s) are stored (shared/overlaid with the host file system).
-//
-// You can now let KLEE run on the `.bc` file.
+// 3) You can now let KLEE run on the `.bc` file.
//
// 4> klee panic1*.bc
// ...
diff --git a/examples/resource.rs b/examples/resource.rs
index 84551aba280212bba08373f5d33980ba54c37307..87661792713bf7cbf6a39591c261fd06e577889f 100644
--- a/examples/resource.rs
+++ b/examples/resource.rs
@@ -103,13 +103,11 @@ fn idle() -> ! {
// Build the application for KLEE analysis.
// > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
//
-// Start the KLEE docker
-// > 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
//
// Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
-// of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+// of the generated LLVM IR code.
//
-// Now run KLEE in the docker.
+// Now run KLEE
// > klee resource-*.bc
// KLEE: WARNING: executable has module level assembly (ignoring)
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -493,10 +491,7 @@ fn idle() -> ! {
// Now lets have a look at using optimized LLVM and how it affects the number of tests.
// > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
//
-// and now start a docker for the optimized build
-// > 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
-//
-// and in the docker run
+// and run
// > klee resource*.bc
//
// Look at the generated tests.
diff --git a/expand_nop b/expand_nop
index cc6b7cce4f2f50c20b44e0d80cc678e07e44cb27..ea028ba8cc676ecc12b92b8349bdfe41f976bcbe 100644
--- a/expand_nop
+++ b/expand_nop
@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI1::Y {
// Build the application for KLEE analysis.
// > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
//
- // Start the KLEE docker
- // > 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
- //
// Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
- // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+ // of the generated LLVM IR code.
//
- // Now run KLEE in the docker.
+ // Now run KLEE.
// > klee resource-*.bc
// KLEE: WARNING: executable has module level assembly (ignoring)
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI1::Y {
// Now lets have a look at using optimized LLVM and how it affects the number of tests.
// > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
//
- // and now start a docker for the optimized build
- // > 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
- //
- // and in the docker run
+ // and run
// > klee resource*.bc
//
// Look at the generated tests.
diff --git a/expand_nop.rs b/expand_nop.rs
index d92afdd2e03578072157a5bc60c748454c762777..eda7023f2cab02ac07432655d6eba591f7288b3d 100644
--- a/expand_nop.rs
+++ b/expand_nop.rs
@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI1::Y {
// Build the application for KLEE analysis.
// > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
//
- // Start the KLEE docker
- // > 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
- //
// Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
- // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+ // of the generated LLVM IR code.
//
- // Now run KLEE in the docker.
+ // Now run KLEE.
// > klee resource-*.bc
// KLEE: WARNING: executable has module level assembly (ignoring)
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI1::Y {
// Now lets have a look at using optimized LLVM and how it affects the number of tests.
// > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
//
- // and now start a docker for the optimized build
- // > 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
- //
- // and in the docker run
+ // and run
// > klee resource*.bc
//
// Look at the generated tests.
diff --git a/expand_wcet.rs b/expand_wcet.rs
index 4744ee8ad29b1446bcf79beea505d175380ba46a..3cf7c3f3097f91bf37c0c2b03b7d860b7e16b742 100644
--- a/expand_wcet.rs
+++ b/expand_wcet.rs
@@ -65,13 +65,10 @@ unsafe impl rtfm::Resource for EXTI2::Y {
// Build the application for KLEE analysis.
// > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
//
- // Start the KLEE docker
- // > 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
- //
// Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
- // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+ // of the generated LLVM IR code.
//
- // Now run KLEE in the docker.
+ // Now run KLEE.
// > klee resource-*.bc
// KLEE: WARNING: executable has module level assembly (ignoring)
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -455,10 +452,7 @@ unsafe impl rtfm::Resource for EXTI2::Y {
// Now lets have a look at using optimized LLVM and how it affects the number of tests.
// > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
//
- // and now start a docker for the optimized build
- // > 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
- //
- // and in the docker run
+ // and run
// > klee resource*.bc
//
// Look at the generated tests.
diff --git a/expand_wcet_bkpt.rs b/expand_wcet_bkpt.rs
index 3e23cde2a55d34acb35594e96a0d834df4beb641..88afb8a84a9a267abcb8dd3a75f0203fbb8d8edd 100644
--- a/expand_wcet_bkpt.rs
+++ b/expand_wcet_bkpt.rs
@@ -75,13 +75,10 @@ unsafe impl rtfm::Resource for EXTI2::Y {
// Build the application for KLEE analysis.
// > xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu
//
- // Start the KLEE docker
- // > 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
- //
// Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
- // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+ // of the generated LLVM IR code.
//
- // Now run KLEE in the docker.
+ // Now run KLEE
// > klee resource-*.bc
// KLEE: WARNING: executable has module level assembly (ignoring)
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
@@ -465,10 +462,7 @@ unsafe impl rtfm::Resource for EXTI2::Y {
// Now lets have a look at using optimized LLVM and how it affects the number of tests.
// > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
//
- // and now start a docker for the optimized build
- // > 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
- //
- // and in the docker run
+ // and run
// > klee resource*.bc
//
// Look at the generated tests.
diff --git a/klee_stm_gdb.1.py b/klee_stm_gdb.1.py
index 8805c1d39830ced6601ae850eb672497126df1b2..8dc7f5f1499ca831daaac6d1fff6501b0a785beb 100644
--- a/klee_stm_gdb.1.py
+++ b/klee_stm_gdb.1.py
@@ -390,9 +390,6 @@ def ktest_iterate():
print(rustoutputfolder + "not found. Need to run\n")
print("xargo build --example " + example_name + " --features" +
"klee_mode --target x86_64-unknown-linux-gnu ")
- print("\nand docker run --rm --user (id -u):(id -g)" +
- "-v $PWD" + "/" + klee_out_folder + ":/mnt" +
- "-w /mnt -it afoht/llvm-klee-4 /bin/bash ")
if autobuild:
xargo_run("klee")
klee_run()
@@ -494,13 +491,8 @@ def klee_run():
print(PWD + "/" + klee_out_folder)
print(bc_file)
- klee_cmd = ("docker run --rm --user " +
- user_id[:-1] + ":" + group_id[:-1] +
- " -v '"
- + PWD + "/"
- + klee_out_folder + "':'/mnt'" +
- " -w /mnt -it afoht/llvm-klee-4 " +
- "/bin/bash -c 'klee %s'" % bc_file)
+ klee_cmd = ("klee %s" % bc_file)
+
if debug:
print(klee_cmd)
call(klee_cmd, shell=True)