updated examples

klee-examples/Cargo.toml

 [package]
 name = "klee-examples"
 version = "0.2.0"
-authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
+authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
 
 [dependencies]
-klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+#klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+klee = {path =".."}
 panic-abort = "0.3.1"
 
 
-[dependencies.volatile-register]
-version = "0.3.0"
-
 [dependencies.cortex-m]
 version = "0.6.0"
 # #features = ["inline-asm", "klee-analysis"]
 
 [patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+#vcell = { path = "../../vcell" }
+#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
 volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.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"
-# path = "../stm32f413"
+[dependencies.volatile-register]
+version = "0.3.0"
+
+[dependencies.stm32f413]
+version = "0.3.0"
+path = "../../klee/stm32f413/"
+optional = true
 
-#[patch.crates-io]
-#cortex-m = { path = "../cortex-m" }
-#volatile-register = { version = "0.3.0", path = "../volatile-register" }
+[[examples]]
+name = "gpioa"
+path = "examples/gpioa.rs"
+#required-features = ["klee-device"] # seem to work only in [[bin]]
 
 [[bin]]
 name = "foo"
@@ -51,6 +56,5 @@ panic = "abort"
 lto = true
 
 [features]
-#klee-analysis = ["stm32f413/klee-analysis", "cortex-m/klee-analysis", "klee/klee-analysis"]
 klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
-#klee-replay = ["klee/klee-replay"]
+klee-device = ["stm32f413/klee-analysis"]

klee-examples/examples/gpioa.rs

+#![no_std]
+#![no_main]
+
+extern crate cortex_m;
+extern crate klee;
+extern crate panic_abort;
+extern crate stm32f413;
+
+use core::ptr;
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let syst = peripherals.SYST;
+
+    let p = stm32f413::Peripherals::take().unwrap();
+    let gpioa = p.GPIOA;
+
+    if gpioa.moder.read().bits() == 0 {
+        let p =  Peripherals::take().unwrap();
+    }
+}

klee-examples/examples/modify.rs

@@ -3,6 +3,7 @@
 
 #[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::RW;
@@ -14,13 +15,13 @@ fn main() {
     unsafe {
         rw.modify(|r| {
             if r == 0 {
-                klee::abort();
+                panic!(); // rust compiler calls panic abort
             }
             0
         });
     }
 
     if rw.read() == 0 {
-        klee::abort();
+        klee::abort(); // we directly call the intrinsic abort
     }
 }

klee-examples/examples/registers.rs

 #![no_std]
 #![no_main]
 
-#[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::{RO, RW, WO};

klee-examples/examples/systick.rs

+#![no_std]
+#![no_main]
+
+extern crate cortex_m;
+extern crate klee;
+extern crate panic_abort;
+
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let syst = peripherals.SYST;
+
+    if syst.rvr.read() == 0 {
+        if syst.cvr.read() == 0x21 {
+            panic!();
+        }
+    }
+}

klee-examples/src/foo.rs

@@ -3,6 +3,7 @@
 
 #[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 use core::ptr;
 

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]
@@ -25,5 +21,4 @@ fn main() {
             klee::abort();
         };
     };
-
 }

klee-examples/src/register.rs

@@ -39,8 +39,8 @@
 #![no_std]
 #![no_main]
 
-#[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::RO;
@@ -51,7 +51,7 @@ fn main() {
 
     if rw.read() == 0 {
         if rw.read() == 0 {
-            panic!();
+            klee::abort();
         }
     }
 }