From 12e3a48fb11a8bb80b10f201fb54ba2532baf72a Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Tue, 5 Feb 2019 13:19:20 +0100
Subject: [PATCH] example updated
---
Cargo.lock | 89 ++++++++++++++++++++++++++++++++++++++++++++--
Cargo.toml | 2 +-
examples/assume.rs | 2 +-
examples/model4.rs | 9 +++--
src/main.rs | 3 +-
5 files changed, 97 insertions(+), 8 deletions(-)
diff --git a/Cargo.lock b/Cargo.lock
index 7d2fb3b..111a7ac 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,8 +1,34 @@
+# 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>"
diff --git a/Cargo.toml b/Cargo.toml
index b5e2518..48c9d81 100644
--- a/Cargo.toml
+++ b/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"
diff --git a/examples/assume.rs b/examples/assume.rs
index c8853a7..429372d 100644
--- a/examples/assume.rs
+++ b/examples/assume.rs
@@ -16,7 +16,7 @@ fn main() {
let mut c = 0;
if a > 10 {
- c+= 1;
+ c += 1;
}
// klee::kassume(b > 0);
let v = a + b;
diff --git a/examples/model4.rs b/examples/model4.rs
index b06ac7f..8e0b6cc 100644
--- a/examples/model4.rs
+++ b/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);
}
diff --git a/src/main.rs b/src/main.rs
index 1ee0085..75165be 100644
--- a/src/main.rs
+++ b/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() };
--
GitLab