diff --git a/Cargo.lock b/Cargo.lock
index 06c5d27b410e83dd860233a3c6a038daf75390c2..911b013c9211ca762aaef15496dd9c80380059b4 100644
--- 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"
diff --git a/Cargo.toml b/Cargo.toml
index 9cb2a14337da4d8939e9815bcb218479e5f7e70b..43d66639b4b9280555845a160d4f8c579547106b 100644
--- 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
diff --git a/compile.txt b/compile.txt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/examples/cortex_m_test2.rs b/examples/cortex_m_test2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..34bbd97687c6ad7fc32eeaab69811e7bcd5fa9db
--- /dev/null
+++ b/examples/cortex_m_test2.rs
@@ -0,0 +1,27 @@
+#![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 };
+// }
diff --git a/examples/klee_cortex_m_test.rs b/examples/cortex_m_test_nightly.rs
similarity index 85%
rename from examples/klee_cortex_m_test.rs
rename to examples/cortex_m_test_nightly.rs
index 940e46e4b8f6f51eb20dc6d07b940d03dd92a7a9..c38f294e3cfff7b1062c7a721ece0e1aeba029e3 100644
--- a/examples/klee_cortex_m_test.rs
+++ b/examples/cortex_m_test_nightly.rs
@@ -1,19 +1,3 @@
-// > 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!();
}
diff --git a/examples/expand.rs b/examples/expand.rs
new file mode 100644
index 0000000000000000000000000000000000000000..c7a40efd6e9122f916fed8ced240c1051b512380
--- /dev/null
+++ b/examples/expand.rs
@@ -0,0 +1,51 @@
+#![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() };
+}
diff --git a/examples/klee_cortex_m_rt_test.rs b/examples/klee_cortex_m_rt_test.rs
index d18f52a764358868c905782eb153bec088a8c4ec..266bec4b8e6d22cfd10b661a60edde03ef5926d7 100644
--- a/examples/klee_cortex_m_rt_test.rs
+++ b/examples/klee_cortex_m_rt_test.rs
@@ -1,24 +1,32 @@
#![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 mut dwt = peripherals.DWT;
- // dwt.enable_cycle_counter();
- // let a = dwt.cyccnt.read();
- // if a == 100 {
- // klee_abort!();
- // }
+ 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!();
}
diff --git a/examples/klee_cortex_m_rt_test2.rs b/examples/klee_cortex_m_rt_test2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d8309ef8cf1541b879d04de02fa804560a0ac1a5
--- /dev/null
+++ b/examples/klee_cortex_m_rt_test2.rs
@@ -0,0 +1,28 @@
+#![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() {}
diff --git a/examples/klee_cortex_m_rt_test3.rs b/examples/klee_cortex_m_rt_test3.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4743c4fe7e25f3a9637537939b96069079bb21a1
--- /dev/null
+++ b/examples/klee_cortex_m_rt_test3.rs
@@ -0,0 +1,44 @@
+#![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!();
+ }
+}
diff --git a/examples/klee_cortex_m_test_stable copy.rs b/examples/klee_cortex_m_test_stable copy.rs
new file mode 100644
index 0000000000000000000000000000000000000000..af498fe1fecee513adafa716a33214104a6d0344
--- /dev/null
+++ b/examples/klee_cortex_m_test_stable copy.rs
@@ -0,0 +1,202 @@
+// > 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!();
+}
diff --git a/examples/klee_cortex_m_test_stable.rs b/examples/klee_cortex_m_test_stable.rs
index f72afdcea62619963eaadfd484bc51835567ad06..af498fe1fecee513adafa716a33214104a6d0344 100644
--- a/examples/klee_cortex_m_test_stable.rs
+++ b/examples/klee_cortex_m_test_stable.rs
@@ -1,54 +1,46 @@
-// > 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
+// ...
+//
+// 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.
//
-// 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
+// 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.)
//
-// So we see that test000001.ktest was causing a division error,
-// the other test case passed
+// This access is along the "happy path" towards the error, so any value would
+// suffice (in this case 0x00000000 was selected by KLEE).
//
-// (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));
+// 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).
//
-// 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']
+// > 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();
+ 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 {
- let some_time_quota = a / (c - (b - 100));
read_volatile(&some_time_quota); // prevent optimization
}
+ klee_abort!();
}
diff --git a/examples/klee_init.rs b/examples/klee_init.rs
new file mode 100644
index 0000000000000000000000000000000000000000..f9838a50bd3c7271cfa614a226f9bebfd323da19
--- /dev/null
+++ b/examples/klee_init.rs
@@ -0,0 +1,52 @@
+//! 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() {}
diff --git a/examples/klee_init_expand.rs b/examples/klee_init_expand.rs
new file mode 100644
index 0000000000000000000000000000000000000000..15f596f3805d3f625a199ccd372fd56dd2038575
--- /dev/null
+++ b/examples/klee_init_expand.rs
@@ -0,0 +1,54 @@
+#![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());
+}
diff --git a/examples/klee_rtfm_expand.rs b/examples/klee_rtfm_expand.rs
new file mode 100644
index 0000000000000000000000000000000000000000..97951b28842f095c291e90254050f5c3f45f9c35
--- /dev/null
+++ b/examples/klee_rtfm_expand.rs
@@ -0,0 +1,29 @@
+// 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();
diff --git a/examples/klee_rtfm_init_test.rs b/examples/klee_rtfm_init_test.rs
new file mode 100644
index 0000000000000000000000000000000000000000..488f793857124a123db1479fd98d71341b9fefbe
--- /dev/null
+++ b/examples/klee_rtfm_init_test.rs
@@ -0,0 +1,26 @@
+//! 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();
+ }
+};
diff --git a/examples/klee_test copy 2.rs b/examples/klee_test copy 2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..2dc2836ca0c6f519ba1bf369f67cf5ea0f91b57b
--- /dev/null
+++ b/examples/klee_test copy 2.rs
@@ -0,0 +1,33 @@
+#![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
+}