From 018672467926800fe1c88c44df5523cbd5c11f7f Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Sun, 18 Feb 2018 19:52:33 +0100
Subject: [PATCH] path enumeration now works
---
.vscode/tasks.json | 12 ++++++++++++
Cargo.toml | 1 +
examples/empty2.rs | 27 ++++++++++++++++++++++-----
3 files changed, 35 insertions(+), 5 deletions(-)
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index 74b97ef..15335af 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -27,6 +27,18 @@
"$rustc"
]
},
+ {
+ "label": "xargo build --example empty2 --features klee_mode --target x86_64-unknown-linux-gnu",
+ "type": "shell",
+ "command": "xargo build --example empty2 --features klee_mode --target x86_64-unknown-linux-gnu",
+ "group": {
+ "kind": "build",
+ "isDefault": true
+ },
+ "problemMatcher": [
+ "$rustc"
+ ]
+ },
{
"label": "xargo build --example empty --release --target thumbv7m-none-eabi",
"type": "shell",
diff --git a/Cargo.toml b/Cargo.toml
index 2b516b7..3a4cc3b 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -42,6 +42,7 @@ cm7-r0p1 = ["cortex-m/cm7-r0p1"]
[profile.dev]
codegen-units = 1
incremental = false
+lto = true
panic = "abort"
[profile.release]
diff --git a/examples/empty2.rs b/examples/empty2.rs
index 42fa9f4..97e6be0 100644
--- a/examples/empty2.rs
+++ b/examples/empty2.rs
@@ -21,20 +21,37 @@ app! {
}
#[inline(never)]
-fn init(_p: init::Peripherals) {
+fn t() -> i32 {
let mut x = unsafe { core::mem::uninitialized() };
let mut y = 0;
k_symbol!(x, "x");
if x < 10 {
for _ in 0..x {
y += 1;
- unsafe { core::ptr::read_volatile(&y) };
+ // unsafe { core::ptr::read_volatile(&y) };
+ // k_abort();
}
}
+ y
+}
- unsafe {
- k_assert(core::ptr::read_volatile(&y) == 0);
- }
+#[inline(never)]
+fn init(_p: init::Peripherals) {
+ // let mut x = unsafe { core::mem::uninitialized() };
+ // let mut y = 0;
+ // k_symbol!(x, "x");
+ // if x < 10 {
+ // for _ in 0..x {
+ // y += 1;
+ // unsafe { core::ptr::read_volatile(&y) };
+ // // k_abort();
+ // }
+ // }
+
+ // unsafe {
+ // k_assert(core::ptr::read_volatile(&y) == 0);
+ // }
+ t();
}
// The idle loop.
--
GitLab