diff --git a/Cargo.toml b/Cargo.toml
index e88210d978c57c996317011a7d7029a9eee0f41e..b5e2518c817cd7d309c85a519bd0c1178425254b 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,18 +1,33 @@
[package]
-name = "plcopen"
-version = "0.1.0"
-authors = ["Per Lindgren <per.lindgren@ltu.se>"]
-edition = "2018"
+name = "klee-examples"
+version = "0.2.0"
+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"
-[[bin]]
-name = "main"
-path = "src/main.rs"
+[dependencies.cortex-m]
+version = "0.6.0"
-[features]
-klee-analysis = ["klee/klee-analysis"]
+[patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
+[dependencies.volatile-register]
+version = "0.3.0"
+
+[dependencies.stm32f413]
+version = "0.3.0"
+git = "https://gitlab.henriktjader.com/pln/stm32f413.git"
+branch = "klee-analysis"
+optional = true
+
+[[examples]]
+name = "gpioa"
+path = "examples/gpioa.rs"
+#required-features = ["klee-device"] # seem to work only in [[bin]]
[profile.dev]
incremental = false
@@ -21,4 +36,8 @@ incremental = false
[profile.release]
debug = true
panic = "abort"
-lto = true
\ No newline at end of file
+lto = true
+
+[features]
+klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
+klee-device = ["stm32f413/klee-analysis"]
diff --git a/examples/assume.rs b/examples/assume.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6195bdd35a033404d54c03d57e72ba720b89e75c
--- /dev/null
+++ b/examples/assume.rs
@@ -0,0 +1,26 @@
+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+#[no_mangle]
+fn main() {
+ let mut a: u32 = unsafe { core::mem::uninitialized() };
+ let mut b: u32 = unsafe { core::mem::uninitialized() };
+
+ klee::ksymbol!(&mut a, "a");
+ klee::ksymbol!(&mut b, "b");
+
+ // klee::kassume(a > b && a - b > 0);
+ klee::kassume( ((a - b > 0) as u32 & (a - b > 0) as u32 ) == 1 );
+
+ unsafe {
+ core::ptr::read_volatile(&a);
+ core::ptr::read_volatile(&b);
+ }
+ // klee::kassume(a - b > 0);
+ // klee::kassert!(a> b);
+}
diff --git a/examples/concurrent.rs b/examples/concurrent.rs
new file mode 100644
index 0000000000000000000000000000000000000000..1552def793c75002b0d5783206926a504140d1b9
--- /dev/null
+++ b/examples/concurrent.rs
@@ -0,0 +1,34 @@
+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+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/examples/model.rs b/examples/model.rs
new file mode 100644
index 0000000000000000000000000000000000000000..66fcab18fb956dc7d21d9273a0edf900280581b9
--- /dev/null
+++ b/examples/model.rs
@@ -0,0 +1,44 @@
+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+struct Device<'a> {
+ ptr: &'a RW<u32>,
+}
+
+// HW model.
+// The register holds values 0..31
+impl<'a> Device<'a> {
+ pub fn read(&self) -> u32 {
+ let v = self.ptr.read();
+ klee::kassume(v < 32);
+ v
+ }
+ pub unsafe fn write(&self, v: u32) {
+ klee::kassert!(v < 32);
+ let v = self.ptr.write(v);
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let reg = unsafe { core::mem::uninitialized() };
+ let device = Device { ptr: ® };
+
+ let v = device.read();
+ if v > 5 {
+ unsafe {
+ device.write(v - 1);
+ }
+ if device.read() == v - 1 {
+ panic!();
+ }
+ }
+}
diff --git a/examples/model2.rs b/examples/model2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..9cc479c4e999e399273a1e75ff1205234c5ab746
--- /dev/null
+++ b/examples/model2.rs
@@ -0,0 +1,70 @@
+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+// model RegA
+// values always in the range 0..31
+struct RegA(RW<u32>);
+
+impl RegA {
+ pub fn read(&self) -> u32 {
+ let v = self.0.read();
+ klee::kassume(v < 32);
+ v
+ }
+ pub unsafe fn write(&self, v: u32) {
+ klee::kassert!(v < 32);
+ let v = self.0.write(v);
+ }
+}
+
+// model RegB
+// values always increases
+struct RegB(RW<u32>);
+
+static mut STATE: u32 = 0; // reset value
+impl RegB {
+ pub fn read(&self) -> u32 {
+ unsafe {
+ STATE += 1;
+ STATE
+ }
+ }
+ pub unsafe fn write(&self, v: u32) {
+ STATE = v;
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let reg_a: RegA = unsafe { core::mem::uninitialized() };
+ let reg_b: RegB = unsafe { core::mem::uninitialized() };
+
+ unsafe {
+ reg_b.write(0);
+ }
+
+ let t1 = reg_b.read();
+ let t2 = reg_b.read();
+
+ let diff = 100 / (t2 - t1);
+
+ klee::kassert!(t2 > t1);
+
+ let v = reg_a.read();
+ if v > 5 {
+ unsafe {
+ reg_a.write(v - 1);
+ }
+ if reg_a.read() == v - 1 {
+ panic!();
+ }
+ }
+}
diff --git a/examples/model3.rs b/examples/model3.rs
new file mode 100644
index 0000000000000000000000000000000000000000..39182dd369062109eee63603cfa929db7621178c
--- /dev/null
+++ b/examples/model3.rs
@@ -0,0 +1,56 @@
+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+// model RegC
+// values always increases
+// but are non-deterministic
+struct RegC(RW<u32>);
+
+static mut OLD_STATE: u32 = 0; // reset value
+impl RegC {
+ pub fn read(&self) -> u32 {
+ let v = self.0.read();
+ unsafe {
+ // klee::kassume(v - 0xFFFF_FFFC > 0);
+ // klee::kassume(v - OLD_STATE > 0);
+ // klee::kassert!(v > OLD_STATE);
+ klee::kassume(v > OLD_STATE);
+
+ OLD_STATE = v;
+ }
+ v
+ }
+ pub unsafe fn write(&self, v: u32) {
+ OLD_STATE = v;
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let reg_c: RegC = unsafe { core::mem::uninitialized() };
+ let mut init: u32 = unsafe { core::mem::uninitialized() };
+ klee::ksymbol!(&mut init, "init");
+ //klee::kassume(init < 0xFFFF_FFFC);
+ //init = 0xFFFF_FFFD;
+ unsafe {
+ reg_c.write(init);
+ }
+
+ let t1 = reg_c.read();
+ let t2 = reg_c.read();
+ // let t3 = reg_c.read();
+
+ // let diff = 100 / (t2 - t1);
+
+ klee::kassert!(t2 > t1);
+ //klee::kassert!(t3 > t2);
+ //klee::kassert!(t3 > t1);
+}