From cd7a46e76b7046b8187fa24dc21db3c9870bc1ff Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Fri, 28 Dec 2018 23:00:34 +0100
Subject: [PATCH] updated examples
---
klee-examples/Cargo.toml | 32 ++++++++++++++++-------------
klee-examples/examples/gpioa.rs | 23 +++++++++++++++++++++
klee-examples/examples/modify.rs | 5 +++--
klee-examples/examples/registers.rs | 2 +-
klee-examples/examples/systick.rs | 20 ++++++++++++++++++
klee-examples/src/foo.rs | 1 +
klee-examples/src/peripheral.rs | 5 -----
klee-examples/src/register.rs | 4 ++--
8 files changed, 68 insertions(+), 24 deletions(-)
create mode 100644 klee-examples/examples/gpioa.rs
create mode 100644 klee-examples/examples/systick.rs
diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index e973928..81189e5 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -1,33 +1,38 @@
[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"]
diff --git a/klee-examples/examples/gpioa.rs b/klee-examples/examples/gpioa.rs
new file mode 100644
index 0000000..cf21409
--- /dev/null
+++ b/klee-examples/examples/gpioa.rs
@@ -0,0 +1,23 @@
+#![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();
+ }
+}
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
index 2d59b5d..6febd18 100644
--- a/klee-examples/examples/modify.rs
+++ b/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
}
}
diff --git a/klee-examples/examples/registers.rs b/klee-examples/examples/registers.rs
index 6c93e98..037ee4f 100644
--- a/klee-examples/examples/registers.rs
+++ b/klee-examples/examples/registers.rs
@@ -1,8 +1,8 @@
#![no_std]
#![no_main]
-#[macro_use]
extern crate klee;
+extern crate panic_abort;
extern crate volatile_register;
use volatile_register::{RO, RW, WO};
diff --git a/klee-examples/examples/systick.rs b/klee-examples/examples/systick.rs
new file mode 100644
index 0000000..266651a
--- /dev/null
+++ b/klee-examples/examples/systick.rs
@@ -0,0 +1,20 @@
+#![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!();
+ }
+ }
+}
diff --git a/klee-examples/src/foo.rs b/klee-examples/src/foo.rs
index 76ba440..a86342d 100644
--- a/klee-examples/src/foo.rs
+++ b/klee-examples/src/foo.rs
@@ -3,6 +3,7 @@
#[macro_use]
extern crate klee;
+extern crate panic_abort;
use core::ptr;
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index 53d7706..e281cd8 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -1,15 +1,11 @@
#![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();
};
};
-
}
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index f5a6fae..3df905d 100644
--- a/klee-examples/src/register.rs
+++ b/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();
}
}
}
--
GitLab