From b716f56a02f03e339b5841f94e364fd4d703cf16 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Mon, 24 Dec 2018 23:56:12 +0100
Subject: [PATCH] tmp
---
klee-examples/Cargo.toml | 18 +++++++++++-------
klee-examples/src/peripheral.rs | 32 ++++++++++++++++++++++++++++++++
klee-examples/src/register.rs | 4 ++--
3 files changed, 45 insertions(+), 9 deletions(-)
create mode 100644 klee-examples/src/peripheral.rs
diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 52cc15c..2668b3c 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -5,20 +5,20 @@ 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"
+panic-abort = "0.3.1"
[dependencies.volatile-register]
version = "0.3.0"
-# [replace]
-[patch.crates-io]
-"volatile-register" = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
-
-# [dependencies.cortex-m]
-# version = "0.6.0"
+[dependencies.cortex-m]
+version = "0.6.0"
# #features = ["inline-asm", "klee-analysis"]
+[patch.crates-io]
+volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
# [dependencies.stm32f413]
# version = "0.3.0"
# path = "../stm32f413"
@@ -35,6 +35,10 @@ path = "src/foo.rs"
name = "register"
path = "src/register.rs"
+[[bin]]
+name = "peripheral"
+path = "src/peripheral.rs"
+
[profile.dev]
incremental = false
# lto = true
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
new file mode 100644
index 0000000..1912ea7
--- /dev/null
+++ b/klee-examples/src/peripheral.rs
@@ -0,0 +1,32 @@
+#![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]
+fn main() {
+ let peripherals = Peripherals::take().unwrap();
+ let mut dwt = peripherals.DWT;
+ dwt.enable_cycle_counter();
+ unsafe {
+ dwt.ctrl.write(0);
+ }
+ if dwt.ctrl.read() == 0 {
+ if dwt.ctrl.read() == 0 {
+ klee::abort();
+ };
+ };
+
+ unsafe {
+ ptr::read_volatile(&dwt);
+ }
+}
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index df1d7d2..5a771fa 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -1,8 +1,8 @@
//! showcase volatile register
//!
-//! $ cargo klee --bin main2 -r -g
+//! $ cargo klee --bin register -r -g
//! ...
-//! Reading symbols from main2.replay...done.
+//! Reading symbols from register.replay...done.
//!
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
//! (gdb) run
--
GitLab