path enumeration now works

.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",

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]

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();
         }
     }
-
-    unsafe {
-        k_assert(core::ptr::read_volatile(&y) == 0);
+    y
 }
+
+#[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.