From 51dedf4e282b4e215c8d6ea45713dfcb9a20a4d6 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Tue, 7 Jan 2020 17:08:45 +0100
Subject: [PATCH] rtfm rtpro compiles
---
Cargo.toml | 6 +-----
examples/rtfm_init.rs | 46 +++++++++++++++++++++++++++++++++++++++++++
2 files changed, 47 insertions(+), 5 deletions(-)
create mode 100644 examples/rtfm_init.rs
diff --git a/Cargo.toml b/Cargo.toml
index ec8aee6..b39720d 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -40,9 +40,6 @@ optional = true
vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
#vcell = { path = "../vcell" }
-#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" }
-#volatile-register = { path = "../volatile-register" }
-
cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
#cortex-m = { path = "../cortex-m" }
@@ -52,12 +49,11 @@ cortex-m-rt = { path = "../cortex-m-rt" }
[features]
klee-analysis = [
"vcell/klee-analysis",
-# "volatile-register/klee-analysis",
"cortex-m/klee-analysis",
"cortex-m-rt/klee-analysis"
]
inline-asm = ["cortex-m/inline-asm"]
-rtpro = [ "cortex-m-rtfm/klee-analysis", "lm3s6965" ]
+rtpro = [ "cortex-m-rtfm/klee-analysis", "cortex-m-rt/rtpro", "lm3s6965" ]
[profile.dev]
panic = "abort"
diff --git a/examples/rtfm_init.rs b/examples/rtfm_init.rs
new file mode 100644
index 0000000..e07956e
--- /dev/null
+++ b/examples/rtfm_init.rs
@@ -0,0 +1,46 @@
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
+
+#[rtfm::app(device = lm3s6965)]
+const APP: () = {
+ #[init]
+ fn init(cx: init::Context) {
+ static mut X: u32 = 0;
+
+ // // Safe access to local `static mut` variable
+ // let _x: &'static mut u32 = X;
+ // if cfg!(feature = "klee-analysis") {
+ // fn_to_test();
+ // } else {
+ // hprintln!("init").unwrap();
+ // debug::exit(debug::EXIT_SUCCESS);
+ // }
+ }
+};
+
+// #[cfg(feature = "klee-analysis")]
+// fn fn_to_test() {
+// let mut a = 0;
+// klee_make_symbolic!(&mut a, "a");
+// match a {
+// 0 => klee_abort!(),
+// 1 => klee_abort!(),
+// 2 => panic!(),
+// 3 => panic!("3"), // just one instance of panic! will be spotted
+// 4 => klee_assert!(false),
+// 5 => klee_assert_eq!(false, true),
+// 6 => klee_assert_eq!(false, true),
+// _ => (),
+// };
+// panic!("at end"); // just one instane of panic! will be spotted
+// }
+
+// #[cfg(not(feature = "klee-analysis"))]
+// fn fn_to_test() {}
--
GitLab