wip (its a mess)

82e9a08f · Per · df8eaa8c · 82e9a08f · 82e9a08f · 82e9a08f
Commit 82e9a08f authored 5 years ago by Per
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,11 +2,8 @@
 # It is not intended for manual editing.
 [[package]]
 name = "aligned"
-version = "0.3.2"
+version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-dependencies = [
- "as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
-]

 [[package]]
 name = "as-slice"
@@ -39,38 +36,38 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 [[package]]
 name = "cortex-m"
 version = "0.6.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
 "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
 "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
 name = "cortex-m-rt"
 version = "0.6.11"
-source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.1",
+ "cortex-m-rt-macros 0.1.7",
+ "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
 "r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
 name = "cortex-m-rt-macros"
 version = "0.1.7"
-source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
 "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
- "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
 name = "cortex-m-rtfm"
 version = "0.5.1"
 dependencies = [
- "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
- "cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.1",
+ "cortex-m-rt 0.6.11",
 "cortex-m-rtfm-macros 0.5.0",
 "heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
 "rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -80,10 +77,10 @@ dependencies = [
 name = "cortex-m-rtfm-macros"
 version = "0.5.0"
 dependencies = [
- "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
 "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
 "rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
- "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
@@ -91,7 +88,7 @@ name = "cortex-m-semihosting"
 version = "0.3.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.1",
 ]

 [[package]]
@@ -154,21 +151,22 @@ dependencies = [
 name = "klee-examples"
 version = "0.1.0"
 dependencies = [
- "cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.1",
+ "cortex-m-rt 0.6.11",
 "cortex-m-rtfm 0.5.1",
 "cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
 "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
 "lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
 "panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
 "panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
- "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+ "vcell 0.1.2",
 "volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
 name = "klee-sys"
 version = "0.1.0"
-source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#e3a296be9ce3376aa501dd60eefb3d0699506aef"
+source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#c8275a34cffb895984d6bdea80e9c6ff9079f769"
 dependencies = [
 "cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
 ]
@@ -179,7 +177,7 @@ version = "0.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
 "bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
- "cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m-rt 0.6.11",
 ]

 [[package]]
@@ -199,7 +197,7 @@ source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff

 [[package]]
 name = "proc-macro2"
-version = "1.0.6"
+version = "1.0.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
 "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -210,7 +208,7 @@ name = "quote"
 version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
@@ -229,8 +227,8 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
 "indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
- "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
- "syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
 ]

 [[package]]
@@ -261,10 +259,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index"

 [[package]]
 name = "syn"
-version = "1.0.11"
+version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
 "quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
 "unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
 ]
@@ -282,7 +280,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 [[package]]
 name = "vcell"
 version = "0.1.2"
-source = "git+https://github.com/perlindgren/vcell.git?branch=trustit#29304497be5cf16aec53447473ff5a3f41783ba3"
 dependencies = [
 "klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
 ]
@@ -292,18 +289,15 @@ name = "volatile-register"
 version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
- "vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
+ "vcell 0.1.2",
 ]

 [metadata]
-"checksum aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
+"checksum aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "d39da9b88ae1a81c03c9c082b8db83f1d0e93914126041962af61034ab44c4a5"
 "checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
 "checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
 "checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
 "checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5"
-"checksum cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)" = "145da2fc379bbd378ed425e75e1748214add9bbd800d4d5b77abb54ca423dbca"
-"checksum cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)" = "33a716cd7d8627fae3892c2eede9249e50d2d79aedfb43ca28dad9a2b23876d9"
-"checksum cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "72b1073338d1e691b3b7aaf6bd61993e589ececce9242a02dfa5453e1b98918d"
 "checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
 "checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
 "checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
@@ -317,7 +311,7 @@ dependencies = [
 "checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
 "checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
 "checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
-"checksum proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)" = "9c9e470a8dc4aeae2dee2f335e8f533e2d4b347e1434e5671afc49b054592f27"
+"checksum proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)" = "0319972dcae462681daf4da1adeeaa066e3ebd29c69be96c6abb1259d2ee2bcc"
 "checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
 "checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
 "checksum rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "9ec893edb2aa5b70320b94896ffea22a7ebb1cf3f942bb67cd5b60a865a63493"
@@ -326,8 +320,7 @@ dependencies = [
 "checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
 "checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
 "checksum stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
-"checksum syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)" = "dff0acdb207ae2fe6d5976617f887eb1e35a2ba52c13c7234c790960cdad9238"
+"checksum syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)" = "ddc157159e2a7df58cd67b1cace10b8ed256a404fb0070593f137d8ba6bef4de"
 "checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
 "checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
-"checksum vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)" = "<none>"
 "checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -37,22 +37,37 @@ optional = true
 # #features = ["inline-asm", "klee-analysis"]

 [patch.crates-io]
-vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
-cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
+#vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
+vcell = { path = "../vcell" }
+
+#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" }
+#volatile-register = { path = "../volatile-register" }
+
+#cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
+cortex-m = { path = "../cortex-m" }
+
 #cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
 cortex-m-rt = { path = "../cortex-m-rt" }

 [features] 
-klee-analysis = [ "vcell/klee-analysis", "cortex-m/klee-analysis", "cortex-m-rt/klee-analysis" ]
+klee-analysis = [ 
+    "vcell/klee-analysis",
+#    "volatile-register/klee-analysis", 
+    "cortex-m/klee-analysis", 
+    "cortex-m-rt/klee-analysis" 
+    ]
+inline-asm = ["cortex-m/inline-asm"]
 rtpro = [ "cortex-m-rtfm/klee-analysis", "lm3s6965" ]

 [profile.dev]
 panic = "abort"
-incremental = false
+# incremental = false
 lto = true
+# codegen-units = 1

 [profile.release]
 debug = true
 panic = "abort"
 incremental = false
 lto = true
+codegen-units = 1
--- a/compile.txt
+++ b/compile.txt
--- a/examples/cortex_m_test2.rs
+++ b/examples/cortex_m_test2.rs
+#![no_std]
+#![no_main]
+
+use klee_sys::klee_abort;
+extern crate cortex_m;
+extern crate panic_klee;
+
+use cortex_m::peripheral::Peripherals;
+
+static mut S: u32 = 100;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    let a = dwt.cyccnt.read();
+    if a == unsafe { S } {
+        panic!();
+    }
+
+    klee_abort!();
+}
+
+// #[no_mangle]
+// pub fn some_interrupt() {
+//     unsafe { S = 0 };
+// }
--- a/examples/klee_cortex_m_test.rs
+++ b/examples/klee_cortex_m_test.rs
-// > cargo klee --example klee_cortex_m_test -r -k -g -v --release
-// ...
-// KLEE: done: total instructions = 33
-// KLEE: done: completed paths = 1
-// KLEE: done: generated tests = 1
-//
-// The example, has just one path, leading up to an abort.
-// The reason is that the progam unconditionally will panic, as
-// taking the peripheral is only only allowed once (for soundness).
-// (Internally this in tracked by a state variable.)
-//
-// This is very good news, that KLEE will detect the error at compile time.
-//
-// Let's remove the error to see if the example code is correct.
-// (comment out the second `take`)
-//
 // > cargo klee --example klee_cortex_m_test -r -k -g -v
 // ...
 // KLEE: ERROR: examples/klee_cortex_m_test.rs:120: divide by zero
@@ -108,11 +92,11 @@
 // Notice here, that this error is spotted EVEN while we are telling
 // Rust to use the primitive (intrinsic) division for "unchecked_div" performance.
 //
-#![feature(core_intrinsics)] // we use intrinsic division
+#![feature(core_intrinsics)] // intrinsic division requires nightly
 #![no_std]
 #![no_main]

-// extern crate klee_sys;
+use klee_sys::klee_abort;
 extern crate cortex_m;
 extern crate panic_klee;

@@ -133,4 +117,5 @@ fn main() {
        let some_time_quota = unchecked_div(a, c - (b - 100));
        read_volatile(&some_time_quota); // prevent optimization
    }
+    klee_abort!();
 }
--- a/examples/expand.rs
+++ b/examples/expand.rs
+#![feature(prelude_import)]
+#![no_std]
+#![no_main]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core;
+#[macro_use]
+extern crate compiler_builtins;
+
+use cortex_m_rt::{entry, exception, pre_init};
+use panic_klee as _;
+
+use klee_sys::{klee_abort, klee_make_symbolic};
+
+use cortex_m::peripheral::Peripherals;
+
+static mut S: u32 = 100;
+
+#[doc(hidden)]
+#[export_name = "main_klee"]
+pub unsafe extern "C" fn __cortex_m_rt_main_trampoline() {
+    __cortex_m_rt_main()
+}
+unsafe fn __cortex_m_rt_main() -> ! {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    let a = dwt.cyccnt.read();
+    if a == unsafe { S } {
+        ::core::panicking::panic("explicit panic", ::core::intrinsics::caller_location());
+    }
+    unsafe { ::klee_sys::ll::abort() };
+}
+#[export_name = "__pre_init"]
+pub unsafe fn pre_init() {
+    let mut a = 0;
+    ::klee_sys::klee_make_symbolic(unsafe { &mut a }, unsafe {
+        ::klee_sys::CStr::from_bytes_with_nul_unchecked("a\u{0}".as_bytes())
+    });
+    if a == 100 {
+        unsafe { ::klee_sys::ll::abort() };
+    }
+}
+#[doc(hidden)]
+#[export_name = "DefaultHandler"]
+fn __cortex_m_rt_DefaultHandler(_irqn: i16) -> ! {
+    if _irqn > 255 {
+        unsafe { ::klee_sys::ll::abort() };
+    }
+    unsafe { ::klee_sys::ll::abort() };
+}
--- a/examples/klee_cortex_m_rt_test.rs
+++ b/examples/klee_cortex_m_rt_test.rs
 #![no_std]
 #![no_main]

-// extern crate cortex_m;
+extern crate cortex_m;
+extern crate cortex_m_rt;
+
 use cortex_m_rt::{entry, pre_init};
 use panic_klee as _;

-use klee_sys::klee_abort;
+use klee_sys::{klee_abort, klee_make_symbolic};

-// use cortex_m::peripheral::Peripherals;
+use cortex_m::peripheral::Peripherals;
+extern crate vcell;
+use volatile_register::RW;

+use core::ptr::read_volatile;
 #[entry]
 unsafe fn main() -> ! {
+    let peripherals = Peripherals::take().unwrap();
    // let peripherals = Peripherals::take().unwrap();
-    //     // let peripherals = Peripherals::take().unwrap();
-    //     let mut dwt = peripherals.DWT;
-    //     dwt.enable_cycle_counter();
-    //     let a = dwt.cyccnt.read();
-    //     if a == 100 {
-    //         klee_abort!();
-    //     }
+    let mut dwt = peripherals.DWT;
+    dwt.enable_cycle_counter();
+    let a: u32 = dwt.cyccnt.read();
+    let b: u32 = dwt.cyccnt.read();
+    let c: u32 = dwt.cyccnt.read();
+    let some_time_quota = a / (c - (b - 100));
+    unsafe {
+        read_volatile(&some_time_quota); // prevent optimization
+    }
    klee_abort!();
 }


--- a/examples/klee_cortex_m_rt_test2.rs
+++ b/examples/klee_cortex_m_rt_test2.rs
+#![no_std]
+#![no_main]
+
+use cortex_m_rt::{entry, pre_init};
+use panic_klee as _;
+
+use klee_sys::klee_abort;
+
+use cortex_m::peripheral::Peripherals;
+
+const X: u32 = 100;
+
+#[entry]
+unsafe fn main() -> ! {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    dwt.enable_cycle_counter();
+    let a = dwt.cyccnt.read();
+    match a {
+        0 => klee_abort!(),
+        X => klee_abort!(),
+        _ => (),
+    }
+    klee_abort!();
+}
+
+#[pre_init]
+unsafe fn pre_init() {}
--- a/examples/klee_cortex_m_rt_test3.rs
+++ b/examples/klee_cortex_m_rt_test3.rs
+#![no_std]
+#![no_main]
+
+use cortex_m_rt::{entry, exception, pre_init};
+use panic_klee as _;
+
+use klee_sys::{klee_abort, klee_make_symbolic};
+
+use cortex_m::peripheral::Peripherals;
+
+static mut S: u32 = 100;
+
+#[entry]
+unsafe fn main() -> ! {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    let a = dwt.cyccnt.read();
+    if a == unsafe { S } {
+        panic!();
+    }
+
+    klee_abort!();
+}
+
+#[pre_init]
+unsafe fn pre_init() {
+    let mut a = 0;
+    klee_make_symbolic!(&mut a, "a");
+    if a == 100 {
+        klee_abort!();
+    }
+}
+
+#[exception]
+fn DefaultHandler(irqn: i16) -> ! {
+    static mut X: i16 = 0;
+    if irqn > 255 {
+        unsafe { core::ptr::write_volatile(&mut X, irqn) };
+        klee_abort!();
+    } else {
+        unsafe { core::ptr::write_volatile(&mut X, 0) };
+        klee_abort!();
+    }
+}
--- a/examples/klee_cortex_m_test_stable copy.rs
+++ b/examples/klee_cortex_m_test_stable copy.rs
+// > cargo klee --example klee_cortex_m_test_stable --release
+// ...
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+
+// KLEE: done: total instructions = 92
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+// ...
+//
+// In order to analyze hardware dependent code, hardware access are treated
+// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
+// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
+// might in the future change to giving the address to the register instead.
+//
+// A breakdown of the example:
+// Behind the scenes the PRIMASK register is accessed, and given concrete value.
+// (Under the hood, `Peripherals.take` executes in a global critical section.)
+//
+// This access is along the "happy path" towards the error, so any value would
+// suffice (in this case 0x00000000 was selected by KLEE).
+//
+// The first `vcell` access: was done when enabling the cycle counter.
+// The rest of accesses stem from reading `a`, `b`, and `c`.
+// Critical here is that `a/(c - (b - 100)) can lead up to a number of errors.
+// Notice that arithmics are "checked" by default in Rust.
+// - (b - 100)            may overflow (u32 can never be negative)
+// - (c - (b - 100))      may overflow (u32 can never be negative)
+// - a / (c - (b - 100))  may render a division by zero
+//
+// Rust injects run-time verification code, that yields a panic!() on error.
+// KLEE reports just one such error site (on the panic handler).
+//
+// > ktest-tool target/release/examples/klee-last/test000001.ktest
+// ktest file : 'target/release/examples/klee-last/test000001.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/release/examples/klee_cortex_m_test_stable-be284cfed3691349.ll']
+// num objects: 5
+// object 0: name: 'PRIMASK'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// object 2: name: 'vcell'
+// object 2: size: 4
+// object 2: data: b'\x00\x00\x00\x00'
+// object 2: hex : 0x00000000
+// object 2: int : 0
+// object 2: uint: 0
+// object 2: text: ....
+// object 3: name: 'vcell'
+// object 3: size: 4
+// object 3: data: b'd\x00\x00\x00'
+// object 3: hex : 0x64000000
+// object 3: int : 100
+// object 3: uint: 100
+// object 3: text: d...
+// object 4: name: 'vcell'
+// object 4: size: 4
+// object 4: data: b'\x00\x00\x00\x00'
+// object 4: hex : 0x00000000
+// object 4: int : 0
+// object 4: uint: 0
+// object 4: text: ....
+//
+// For this test, a = 0, b = 100, c = 0, which hits the division by zero.
+//
+// >  ktest-tool target/release/examples/klee-last/test000002.ktest
+// ktest file : 'target/release/examples/klee-last/test000002.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/release/examples/klee_cortex_m_test_stable-be284cfed3691349.ll']
+// num objects: 5
+// object 0: name: 'PRIMASK'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// object 2: name: 'vcell'
+// object 2: size: 4
+// object 2: data: b'\x00\x00\x00\x00'
+// object 2: hex : 0x00000000
+// object 2: int : 0
+// object 2: uint: 0
+// object 2: text: ....
+// object 3: name: 'vcell'
+// object 3: size: 4
+// object 3: data: b'\x00\x00\x00\x00'
+// object 3: hex : 0x00000000
+// object 3: int : 0
+// object 3: uint: 0
+// object 3: text: ....
+// object 4: name: 'vcell'
+// object 4: size: 4
+// object 4: data: b'\x00\x00\x00\x00'
+// object 4: hex : 0x00000000
+// object 4: int : 0
+// object 4: uint: 0
+// object 4: text: ....
+//
+// If we want to have a closer look on what's going on we can compile the project in
+// without optimization (AKA dev mode or debug mode), and replay the tests in gdb.
+// > cargo klee --example klee_cortex_m_test_stable -r -k -g
+// ...
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/klee_cortex_m_test_stable.rs:100: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 1719
+// KLEE: done: completed paths = 8
+// KLEE: done: generated tests = 2
+// ...
+// For help, type "help".
+// Type "apropos word" to search for commands related to "word"...
+// Reading symbols from klee_cortex_m_test_stable.replay...
+//
+// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
+// (gdb) run
+// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/klee_cortex_m_test_stable.replay
+
+// Program received signal SIGABRT, Aborted.
+// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// (gdb) backtrace
+// #0  0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// #1  0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
+// #2  0x000055555555512b in rust_begin_unwind (_info=0x7fffffffd1b8) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
+// #3  0x00005555555557ed in core::panicking::panic_fmt () at src/libcore/panicking.rs:139
+// #4  0x0000555555555859 in core::panicking::panic () at src/libcore/panicking.rs:70
+// #5  0x0000555555555389 in main () at examples/klee_cortex_m_test_stable.rs:96
+//
+// (gdb) frame 5
+// #5  0x0000555555555389 in main () at examples/klee_cortex_m_test_stable.rs:96
+// 96          let some_time_quota = a / (c - (b - 100));
+// (gdb) p a
+// $1 = 0
+// (gdb) p b
+// $2 = 0
+// (gdb) p c
+// $3 = 0
+//
+// In this case (b - 100) overflows. (In debug mode we have checked not wrapping arithmetics.)
+//
+// (gdb) shell ktest-tool klee-last/test000002.ktest
+// Program received signal SIGABRT, Aborted.
+// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// (gdb) backtrace
+// #0  0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// #1  0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
+// #2  0x00005555555553dd in main () at examples/klee_cortex_m_test_stable.rs:100
+// (gdb) frame 2
+// #2  0x00005555555553dd in main () at examples/klee_cortex_m_test_stable.rs:100
+// 100         klee_abort!();
+// (gdb) p a
+// $4 = 0
+// (gdb) p b
+// $5 = 276938064
+// (gdb) p c
+// $6 = 1350613988
+//
+// In this case there was no arithmetic error and we hit the `klee_abort!()` at the last line.
+
+#![no_std]
+#![no_main]
+
+extern crate cortex_m;
+extern crate panic_klee;
+
+use cortex_m::peripheral::Peripherals;
+use klee_sys::klee_abort;
+
+use core::ptr::read_volatile;
+#[no_mangle]
+fn main() -> ! {
+    let peripherals = Peripherals::take().unwrap();
+    // let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    dwt.enable_cycle_counter();
+    let a: u32 = dwt.cyccnt.read();
+    let b: u32 = dwt.cyccnt.read();
+    let c: u32 = dwt.cyccnt.read();
+    let some_time_quota = a / (c - (b - 100));
+    unsafe {
+        read_volatile(&some_time_quota); // prevent optimization
+    }
+    klee_abort!();
+}
--- a/examples/klee_cortex_m_test_stable.rs
+++ b/examples/klee_cortex_m_test_stable.rs
-// > cargo klee --example klee_cortex_m_test -r -k -g -v --release
+// > cargo klee --example klee_cortex_m_test_stable --release
 // ...
-// KLEE: done: total instructions = 33
-// KLEE: done: completed paths = 1
-// KLEE: done: generated tests = 1
-//
-// The example, has just one path, leading up to an abort.
-// The reason is that the progam unconditionally will panic, as
-// taking the peripheral is only only allowed once (for soundness).
-// (Internally this in tracked by a state variable.)
-//
-// This is very good news, that KLEE will detect the error at compile time.
-//
-// Let's remove the error to see if the example code is correct.
-// (comment out the second `take`)
-//
-// > cargo klee --example klee_cortex_m_test -r -k -g -v
-// ...
-// KLEE: ERROR: examples/klee_cortex_m_test.rs:120: divide by zero
-// KLEE: NOTE: now ignoring this error at this location
 // KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
 // KLEE: NOTE: now ignoring this error at this location
+
+// KLEE: done: total instructions = 92
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+// ...
 //
-// KLEE: done: total instructions = 1454
-// KLEE: done: completed paths = 6
-// KLEE: done: generated tests = 4
-// ..
-//(gdb) shell ls klee-last
-// assembly.ll  info  messages.txt  run.istats  run.stats  test000001.div.err  test000001.kquery  test000001.ktest  test000002.ktest  warnings.txt
+// In order to analyze hardware dependent code, hardware access are treated
+// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
+// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
+// might in the future change to giving the address to the register instead.
 //
-// So we see that test000001.ktest was causing a division error,
-// the other test case passed
+// A breakdown of the example:
+// Behind the scenes the PRIMASK register is accessed, and given concrete value.
+// (Under the hood, `Peripherals.take` executes in a global critical section.)
 //
-// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
-// (gdb) run
-// Starting program: /home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test.replay
-// Program received signal SIGFPE, Arithmetic exception.
-// 0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
-// 133             let some_time_quota = unchecked_div(a, c - (b - 100));
+// This access is along the "happy path" towards the error, so any value would
+// suffice (in this case 0x00000000 was selected by KLEE).
 //
-// Let's look at the actual test
-// (gdb) shell ktest-tool klee-last/test000001.ktest
-// ktest file : 'klee-last/test000001.ktest'
-// args       : ['/home/pln/rust/grepit/klee-examples/target/debug/examples/klee_cortex_m_test-d9038188a1e4d0b0.ll']
+// The first `vcell` access: was done when enabling the cycle counter.
+// The rest of accesses stem from reading `a`, `b`, and `c`.
+// Critical here is that `a/(c - (b - 100)) can lead up to a number of errors.
+// Notice that arithmics are "checked" by default in Rust.
+// - (b - 100)            may overflow (u32 can never be negative)
+// - (c - (b - 100))      may overflow (u32 can never be negative)
+// - a / (c - (b - 100))  may render a division by zero
+//
+// Rust injects run-time verification code, that yields a panic!() on error.
+// KLEE reports just one such error site (on the panic handler).
+//
+// > ktest-tool target/release/examples/klee-last/test000001.ktest
+// ktest file : 'target/release/examples/klee-last/test000001.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/release/examples/klee_cortex_m_test_stable-be284cfed3691349.ll']
 // num objects: 5
 // object 0: name: 'PRIMASK'
 // object 0: size: 4
-// object 0: data: b'\x01\x01\x01\x01'
-// object 0: hex : 0x01010101
-// object 0: int : 16843009
-// object 0: uint: 16843009
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
 // object 0: text: ....
 // object 1: name: 'vcell'
 // object 1: size: 4
@@ -79,57 +71,132 @@
 // object 4: uint: 0
 // object 4: text: ....
 //
-// (gdb) backtrace
-// #0  0x0000555555555528 in main () at examples/klee_cortex_m_test.rs:133
-// (gdb) print a
-// $1 = 0
-// (gdb) print b
-// $2 = 100
-// (gdb) print c
-// $3 = 0
+// For this test, a = 0, b = 100, c = 0, which hits the division by zero.
 //
-// In order to analyze hardware dependent code, hardware access are treated
-// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
-// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
-// might in the future change to giving the address to the register instead.
+// >  ktest-tool target/release/examples/klee-last/test000002.ktest
+// ktest file : 'target/release/examples/klee-last/test000002.ktest'
+// args       : ['/home/pln/rust/trustit/klee-examples/target/release/examples/klee_cortex_m_test_stable-be284cfed3691349.ll']
+// num objects: 5
+// object 0: name: 'PRIMASK'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// object 2: name: 'vcell'
+// object 2: size: 4
+// object 2: data: b'\x00\x00\x00\x00'
+// object 2: hex : 0x00000000
+// object 2: int : 0
+// object 2: uint: 0
+// object 2: text: ....
+// object 3: name: 'vcell'
+// object 3: size: 4
+// object 3: data: b'\x00\x00\x00\x00'
+// object 3: hex : 0x00000000
+// object 3: int : 0
+// object 3: uint: 0
+// object 3: text: ....
+// object 4: name: 'vcell'
+// object 4: size: 4
+// object 4: data: b'\x00\x00\x00\x00'
+// object 4: hex : 0x00000000
+// object 4: int : 0
+// object 4: uint: 0
+// object 4: text: ....
 //
-// A breakdown of the example:
-// Behind the scenes the PRIMASK register is accessed, and given concrete value.
-// (Under the hood, `Peripherals.take` executes in a global critical section.)
+// If we want to have a closer look on what's going on we can compile the project in
+// without optimization (AKA dev mode or debug mode), and replay the tests in gdb.
+// > cargo klee --example klee_cortex_m_test_stable -r -k -g
+// ...
+// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+// KLEE: ERROR: examples/klee_cortex_m_test_stable.rs:100: abort failure
+// KLEE: NOTE: now ignoring this error at this location
 //
-// This access is along the "happy path" towards the error, so any value would
-// suffice (in this case 0x00000000 was selected by KLEE).
+// KLEE: done: total instructions = 1719
+// KLEE: done: completed paths = 8
+// KLEE: done: generated tests = 2
+// ...
+// For help, type "help".
+// Type "apropos word" to search for commands related to "word"...
+// Reading symbols from klee_cortex_m_test_stable.replay...
 //
-// The first `vcell` access: was done when enabling the cycle counter.
-// The rest of accesses stem from reading `a`, `b`, and `c`.
-// Critical here is that KLEE spots that `(c - (b - 100)) = 0`, leading up to a division
-// by zero error (satisfied by `c == 0` and `b == 100`)
+// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
+// (gdb) run
+// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/klee_cortex_m_test_stable.replay
+
+// Program received signal SIGABRT, Aborted.
+// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// (gdb) backtrace
+// #0  0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// #1  0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
+// #2  0x000055555555512b in rust_begin_unwind (_info=0x7fffffffd1b8) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
+// #3  0x00005555555557ed in core::panicking::panic_fmt () at src/libcore/panicking.rs:139
+// #4  0x0000555555555859 in core::panicking::panic () at src/libcore/panicking.rs:70
+// #5  0x0000555555555389 in main () at examples/klee_cortex_m_test_stable.rs:96
+//
+// (gdb) frame 5
+// #5  0x0000555555555389 in main () at examples/klee_cortex_m_test_stable.rs:96
+// 96          let some_time_quota = a / (c - (b - 100));
+// (gdb) p a
+// $1 = 0
+// (gdb) p b
+// $2 = 0
+// (gdb) p c
+// $3 = 0
+//
+// In this case (b - 100) overflows. (In debug mode we have checked not wrapping arithmetics.)
 //
-// Notice here, that this error is spotted EVEN while we are telling
-// Rust to use the primitive (intrinsic) division for "unchecked_div" performance.
+// (gdb) shell ktest-tool klee-last/test000002.ktest
+// Program received signal SIGABRT, Aborted.
+// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// (gdb) backtrace
+// #0  0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
+// #1  0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
+// #2  0x00005555555553dd in main () at examples/klee_cortex_m_test_stable.rs:100
+// (gdb) frame 2
+// #2  0x00005555555553dd in main () at examples/klee_cortex_m_test_stable.rs:100
+// 100         klee_abort!();
+// (gdb) p a
+// $4 = 0
+// (gdb) p b
+// $5 = 276938064
+// (gdb) p c
+// $6 = 1350613988
 //
+// In this case there was no arithmetic error and we hit the `klee_abort!()` at the last line.
+
 #![no_std]
 #![no_main]

-// extern crate klee_sys;
 extern crate cortex_m;
 extern crate panic_klee;

 use cortex_m::peripheral::Peripherals;
+use klee_sys::klee_abort;

 use core::ptr::read_volatile;
-
 #[no_mangle]
-fn main() {
+fn main() -> ! {
    let peripherals = Peripherals::take().unwrap();
    // let peripherals = Peripherals::take().unwrap();
    let mut dwt = peripherals.DWT;
    dwt.enable_cycle_counter();
-    let a = dwt.cyccnt.read();
-    let b = dwt.cyccnt.read();
-    let c = dwt.cyccnt.read();
-    unsafe {
+    let a: u32 = dwt.cyccnt.read();
+    let b: u32 = dwt.cyccnt.read();
+    let c: u32 = dwt.cyccnt.read();
    let some_time_quota = a / (c - (b - 100));
+    unsafe {
        read_volatile(&some_time_quota); // prevent optimization
    }
+    klee_abort!();
 }
--- a/examples/klee_init.rs
+++ b/examples/klee_init.rs
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+
+#[cfg(not(feature = "klee-analysis"))]
+use panic_halt as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+use cortex_m_semihosting::{debug, hprintln};
+
+#[rtfm::app(device = lm3s6965)]
+const APP: () = {
+    #[init]
+    fn init(cx: init::Context) {
+        static mut X: u32 = 0;
+
+        // Safe access to local `static mut` variable
+        let _x: &'static mut u32 = X;
+        if cfg!(feature = "klee-analysis") {
+            fn_to_test();
+        } else {
+            hprintln!("init").unwrap();
+            debug::exit(debug::EXIT_SUCCESS);
+        }
+    }
+};
+
+#[cfg(feature = "klee-analysis")]
+fn fn_to_test() {
+    let mut a = 0;
+    klee_make_symbolic!(&mut a, "a");
+    match a {
+        0 => klee_abort!(),
+        1 => klee_abort!(),
+        2 => panic!(),
+        3 => panic!("3"), // just one instance of panic! will be spotted
+        4 => klee_assert!(false),
+        5 => klee_assert_eq!(false, true),
+        6 => klee_assert_eq!(false, true),
+        _ => (),
+    };
+    panic!("at end"); // just one instane of panic! will be spotted
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+fn fn_to_test() {}
--- a/examples/klee_init_expand.rs
+++ b/examples/klee_init_expand.rs
+#![feature(core_intrinsics)]
+#![feature(rustc_private)]
+#![feature(core_panic)]
+#![feature(prelude_import)]
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+
+#[no_mangle]
+fn main() -> ! {
+    fn_to_test();
+    loop {}
+}
+
+// Safe access to local `static mut` variable
+
+#[cfg(feature = "klee-analysis")]
+fn fn_to_test() {
+    let mut a = 0; // just one instance of panic! will be spotted
+                   // just one instane of panic! will be spotted
+
+    ::klee_sys::klee_make_symbolic(unsafe { &mut a }, unsafe {
+        ::klee_sys::CStr::from_bytes_with_nul_unchecked("a\u{0}".as_bytes())
+    });
+    match a {
+        0 => unsafe { ::klee_sys::ll::abort() },
+        1 => unsafe { ::klee_sys::ll::abort() },
+        2 => ::core::panicking::panic("explicit panic", ::core::intrinsics::caller_location()),
+        3 => ::core::panicking::panic("3", ::core::intrinsics::caller_location()),
+        4 => {
+            if !false {
+                unsafe { ::klee_sys::ll::abort() };
+            }
+        }
+        5 => {
+            if !(false == true) {
+                unsafe { ::klee_sys::ll::abort() };
+            }
+        }
+        6 => {
+            if !(false == true) {
+                unsafe { ::klee_sys::ll::abort() };
+            }
+        }
+        _ => (),
+    };
+    ::core::panicking::panic("at end", ::core::intrinsics::caller_location());
+}
--- a/examples/klee_rtfm_expand.rs
+++ b/examples/klee_rtfm_expand.rs
+// klee-analysis
+#![feature(prelude_import)]
+#![feature(rustc_private)]
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core;
+#[macro_use]
+extern crate compiler_builtins;
+
+// use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
+// use rtfm;
+
+#[no_mangle]
+fn main() -> ! {
+    loop {}
+}
+//static mut X: u32 = 0;
+
+// Safe access to local `static mut` variable
+// let _x: &'static mut u32 = X;
+//    fn_to_test();
--- a/examples/klee_rtfm_init_test.rs
+++ b/examples/klee_rtfm_init_test.rs
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+
+// use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
+// use rtfm;
+// use cortex_m_rt as _;
+// use lm3s6965 as _;
+// extern crate cortex_m_rt;
+// extern crate lm3s6965;
+
+#[rtfm::app(device = lm3s6965)]
+const APP: () = {
+    #[init]
+    fn init(_cx: init::Context) {
+        //static mut X: u32 = 0;
+
+        // Safe access to local `static mut` variable
+        // let _x: &'static mut u32 = X;
+        //    fn_to_test();
+    }
+};
--- a/examples/klee_test copy 2.rs
+++ b/examples/klee_test copy 2.rs
+#![no_std]
+#![no_main]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+
+#[cfg(not(feature = "klee-analysis"))]
+use panic_halt as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    panic!();
+}
+
+#[cfg(feature = "klee-analysis")]
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    klee_make_symbolic!(&mut a, "a");
+    match a {
+        0 => klee_abort!(),
+        1 => klee_abort!(),
+        2 => panic!(),
+        3 => panic!("3"), // just one instance of panic! will be spotted
+        4 => klee_assert!(false),
+        5 => klee_assert_eq!(false, true),
+        6 => klee_assert_eq!(false, true),
+        _ => (),
+    };
+    panic!("at end"); // just one instane of panic! will be spotted
+}