step towards automation

examples/resource.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f103xx;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_read};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f103xx,
+
+    resources: {
+        static X:u32 = 0;
+        static Y:u32 = 0;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            resources: [X],
+        },
+
+        EXTI2: {
+            path: exti2,
+            resources: [X, Y],
+        },
+    },
+}
+
+fn exti1(t: &mut Threshold, r: EXTI1::Resources) {
+    let mut y = 0;
+    r.X.claim(t, |x, _| {
+        if *x < 10 {
+            for _ in 0..*x {
+                y += 1;
+                k_visit!();
+            }
+        }
+    });
+    k_read(&y);
+}
+
+fn exti2(_t: &mut Threshold, _r: EXTI2::Resources) {}
+
+#[inline(never)]
+fn init(_p: init::Peripherals, _r: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+
+#[inline(never)]
+fn idle() -> ! {
+    k_abort()
+}

macros/src/trans.rs

@@ -220,6 +220,8 @@ fn idle(
     }
 
     if !cfg!(feature = "klee_mode") {
+        // in non klee mode we will call idle from init
+
         let idle = &app.idle.path;
         main.push(quote! {
             // type check
@@ -227,6 +229,8 @@ fn idle(
 
             idle(#(#exprs),*);
         });
+    } else {
+        // in klee mode we do NOT call idle its treated as a task
     }
 }
 
@@ -473,6 +477,25 @@ fn resources(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             },
         });
     }
+
+    if cfg!(feature = "klee_mode") {
+        // collect the identifiers for our resources
+
+        let mut names = Vec::new();
+        for name in ownerships.keys() {
+            let _name = Ident::new(format!("_{}", name.as_ref()));
+            names.push(quote!{
+                k_symbol!(&mut #_name, "#_name");
+            });
+        }
+
+        // generate a function setting all resources to symbolic
+        root.push(quote!{
+            pub unsafe fn make_resources_symbolic() {
+                #(#names)*
+            }
+        });
+    }
 }
 
 fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {