examples

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"]

klee-examples/examples/modify.rs

+#![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();
+    }
+}

klee-examples/examples/registers.rs

+#![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!();
+        }
+    }
+}

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);
+    // }
 }