From 537b53f278fc802bf382e5424b774dc9113d9ae2 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 25 Dec 2018 15:17:15 +0100
Subject: [PATCH] examples

---
 klee-examples/Cargo.toml            |  6 ++++--
 klee-examples/examples/modify.rs    | 26 +++++++++++++++++++++++
 klee-examples/examples/registers.rs | 32 +++++++++++++++++++++++++++++
 klee-examples/src/peripheral.rs     | 22 ++++++++++----------
 klee-examples/src/register.rs       |  6 +++---
 5 files changed, 76 insertions(+), 16 deletions(-)
 create mode 100644 klee-examples/examples/modify.rs
 create mode 100644 klee-examples/examples/registers.rs

diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 2668b3c..2418d2b 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -17,7 +17,9 @@ version = "0.6.0"
 
 [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" }
+#volatile-register = { path = "../../klee/volatile-register/" }
+#cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+cortex-m = { path = "../../cortex-m" }
 
 # [dependencies.stm32f413]
 # version = "0.3.0"
@@ -50,5 +52,5 @@ lto = true
 
 [features]
 #klee-analysis = ["stm32f413/klee-analysis", "cortex-m/klee-analysis", "klee/klee-analysis"]
-klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis"]
+klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
 #klee-replay = ["klee/klee-replay"]
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
new file mode 100644
index 0000000..2d59b5d
--- /dev/null
+++ b/klee-examples/examples/modify.rs
@@ -0,0 +1,26 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+#[no_mangle]
+fn main() {
+    let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+
+    unsafe {
+        rw.modify(|r| {
+            if r == 0 {
+                klee::abort();
+            }
+            0
+        });
+    }
+
+    if rw.read() == 0 {
+        klee::abort();
+    }
+}
diff --git a/klee-examples/examples/registers.rs b/klee-examples/examples/registers.rs
new file mode 100644
index 0000000..6c93e98
--- /dev/null
+++ b/klee-examples/examples/registers.rs
@@ -0,0 +1,32 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate volatile_register;
+use volatile_register::{RO, RW, WO};
+
+#[no_mangle]
+fn main() {
+    let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+    let ro: RO<u32> = unsafe { core::mem::uninitialized() };
+    let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+
+    unsafe { wo.write(2) };
+
+    if rw.read() == 0 {
+        unsafe {
+            rw.write(0);
+        }
+        if rw.read() == 0 {
+            panic!();
+        }
+    }
+
+    if ro.read() == 0 {
+        if ro.read() == 0 {
+            panic!();
+        }
+    }
+}
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index 1912ea7..346cdfe 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -17,16 +17,16 @@ 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 {
+    //     dwt.ctrl.write(0);
+    // }
+    // if dwt.ctrl.read() == 0 {
+    //     if dwt.ctrl.read() == 0 {
+    //         klee::abort();
+    //     };
+    // };
 
-    unsafe {
-        ptr::read_volatile(&dwt);
-    }
+    // unsafe {
+    //     ptr::read_volatile(&dwt);
+    // }
 }
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index 5a771fa..f5a6fae 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -1,14 +1,14 @@
 //! showcase volatile register
-//! 
+//!
 //! $ cargo klee --bin register -r -g
 //! ...
 //! Reading symbols from register.replay...done.
-//! 
+//!
 //! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
 //! (gdb) run
 //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
 //! [Inferior 1 (process 25074) exited with code 01]
-//! 
+//!
 //! (gdb) set env KTEST_FILE=klee-last/test000003.ktest
 //! (gdb) run
 //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
-- 
GitLab