tmp

klee-examples/Cargo.toml

@@ -5,20 +5,20 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io
 
 [dependencies]
 klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
-#panic-abort = "0.3.1"
+panic-abort = "0.3.1"
 
 
 [dependencies.volatile-register]
 version = "0.3.0"
 
-# [replace]
-[patch.crates-io]
-"volatile-register" = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
-
-# [dependencies.cortex-m]
-# version = "0.6.0"
+[dependencies.cortex-m]
+version = "0.6.0"
 # #features = ["inline-asm", "klee-analysis"]
 
+[patch.crates-io]
+volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
 # [dependencies.stm32f413]
 # version = "0.3.0"
 # path = "../stm32f413"
@@ -35,6 +35,10 @@ path = "src/foo.rs"
 name = "register"
 path = "src/register.rs"
 
+[[bin]]
+name = "peripheral"
+path = "src/peripheral.rs"
+
 [profile.dev]
 incremental = false
 # lto = true

klee-examples/src/peripheral.rs

+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+#[cfg(not(feature = "klee-analysis"))]
+extern crate panic_abort;
+
+extern crate cortex_m;
+
+use core::ptr;
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let mut dwt = peripherals.DWT;
+    dwt.enable_cycle_counter();
+    unsafe {
+        dwt.ctrl.write(0);
+    }
+    if dwt.ctrl.read() == 0 {
+        if dwt.ctrl.read() == 0 {
+            klee::abort();
+        };
+    };
+
+    unsafe {
+        ptr::read_volatile(&dwt);
+    }
+}

klee-examples/src/register.rs

 //! showcase volatile register
 //! 
-//! $ cargo klee --bin main2 -r -g
+//! $ cargo klee --bin register -r -g
 //! ...
-//! Reading symbols from main2.replay...done.
+//! Reading symbols from register.replay...done.
 //! 
 //! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
 //! (gdb) run