example updated

Cargo.lock

+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+[[package]]
+name = "aligned"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "bare-metal"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
 [[package]]
 name = "cfg-if"
 version = "0.1.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 
+[[package]]
+name = "cortex-m"
+version = "0.6.0"
+source = "git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis#144cac26c7a12cf5be65f81f37dbf1ceb8369319"
+dependencies = [
+ "aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "bare-metal 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)",
+ "volatile-register 0.3.0 (git+https://github.com/perlindgren/volatile-register.git)",
+]
+
 [[package]]
 name = "cstr_core"
 version = "0.1.2"
@@ -25,6 +51,16 @@ dependencies = [
  "cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
 ]
 
+[[package]]
+name = "klee-examples"
+version = "0.2.0"
+dependencies = [
+ "cortex-m 0.6.0 (git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis)",
+ "klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)",
+ "stm32f413 0.3.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git?branch=klee-analysis)",
+ "volatile-register 0.3.0 (git+https://github.com/perlindgren/volatile-register.git)",
+]
+
 [[package]]
 name = "memchr"
 version = "2.1.2"
@@ -35,8 +71,40 @@ dependencies = [
 ]
 
 [[package]]
-name = "plcopen"
-version = "0.1.0"
+name = "rustc_version"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "semver-parser"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "stm32f413"
+version = "0.3.0"
+source = "git+https://gitlab.henriktjader.com/pln/stm32f413.git?branch=klee-analysis#f2cc8f4f6c38378216d27554653ffbfce3dee29d"
+dependencies = [
+ "bare-metal 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)",
+ "cortex-m 0.6.0 (git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis)",
+ "vcell 0.2.0 (git+https://github.com/perlindgren/vcell.git)",
+]
+
+[[package]]
+name = "vcell"
+version = "0.2.0"
+source = "git+https://github.com/perlindgren/vcell.git#5d2a4683e2a5a864f1d88f02aa6d3ca054834d15"
 dependencies = [
  "klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)",
 ]
@@ -46,10 +114,27 @@ name = "version_check"
 version = "0.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 
+[[package]]
+name = "volatile-register"
+version = "0.3.0"
+source = "git+https://github.com/perlindgren/volatile-register.git#0320d1bf1507de2a45d924e02b83a52d61746cea"
+dependencies = [
+ "vcell 0.2.0 (git+https://github.com/perlindgren/vcell.git)",
+]
+
 [metadata]
+"checksum aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "d39da9b88ae1a81c03c9c082b8db83f1d0e93914126041962af61034ab44c4a5"
+"checksum bare-metal 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)" = "a3caf393d93b2d453e80638d0674597020cef3382ada454faacd43d1a55a735a"
 "checksum cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)" = "082bb9b28e00d3c9d39cc03e64ce4cea0f1bb9b3fde493f0cbc008472d22bdf4"
+"checksum cortex-m 0.6.0 (git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis)" = "<none>"
 "checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
 "checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
 "checksum klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)" = "<none>"
 "checksum memchr 2.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "db4c41318937f6e76648f42826b1d9ade5c09cafb5aef7e351240a70f39206e9"
+"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
+"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
+"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
+"checksum stm32f413 0.3.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git?branch=klee-analysis)" = "<none>"
+"checksum vcell 0.2.0 (git+https://github.com/perlindgren/vcell.git)" = "<none>"
 "checksum version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"
+"checksum volatile-register 0.3.0 (git+https://github.com/perlindgren/volatile-register.git)" = "<none>"

Cargo.toml

@@ -5,7 +5,7 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.
 
 [dependencies]
 klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
-panic-abort = "0.3.1"
+# panic-abort = "0.3.1"
 
 [dependencies.cortex-m]
 version = "0.6.0"

examples/model4.rs

@@ -20,7 +20,9 @@ impl RegC {
         let v = self.0.read(); // to get a symbolic value
         klee::kassume(v > 0); // to ensure that the value is positive
         unsafe {
-            OLD_STATE += v;
+            if (OLD_STATE as u64 + v as u64) < 0x1_0000_0000 {
+                OLD_STATE += v
+            }
             OLD_STATE
         }
     }
@@ -40,6 +42,7 @@ fn main() {
     }
 
     let t1 = reg_c.read();
-    let t2 = reg_c.read();
-    klee::kassert!(t2 > t1);
+    // let t2 = reg_c.read();
+    let c = 100 / (t1 - init);
+    //     klee::kassert!(t2 > t1);
 }

src/main.rs

@@ -5,7 +5,8 @@ use klee::{kassert, ksymbol};
 
 #[no_mangle]
 fn main() {
-    let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
+    let mut DATA: [Data; (DISCREPENCY + 1) as usize] =
+        unsafe { core::mem::uninitialized() };
     ksymbol!(&mut DATA, "DATA");
 
     let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };