Merge branch 'klee' of gitlab.henriktjader.com:KLEE/cortex-m-rtfm-klee into klee

macros/src/trans.rs

@@ -18,7 +18,9 @@ pub fn app(app: &App, ownerships: &Ownerships) -> Tokens {
     ::trans::tasks(app, ownerships, &mut root);
 
     root.push(quote! {
+        #[allow(private_no_mangle_fns)]
         #[allow(unsafe_code)]
+        //#[no_mangle]
         fn main() {
             #(#main)*
         }
@@ -427,15 +429,11 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
                 });
             });
         } else {
-            // wcet_mode
-            // panic!();
-            for (name, _task) in &app.tasks {
-                let _name = Ident::new(format!("stub_{}", name.as_ref()));
+            // wcet_mode, call to wcet_start
             main.push(quote! {
-                    #_name();
+                wcet_start();
             });
         }
-        }
     } else {
         // code generation for klee_mode
         let mut tasks = vec![];
@@ -713,4 +711,24 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             }
         });
     }
+    if cfg!(feature = "wcet_bkpt") {
+        let mut stubs = vec![];
+        for (name, _task) in &app.tasks {
+            let _name = Ident::new(format!("stub_{}", name.as_ref()));
+            stubs.push(quote!{
+                #_name();
+            });
+        }
+
+        root.push(quote! {
+            extern crate cortex_m;
+            #[inline(never)]
+            #[allow(private_no_mangle_fns)]
+            #[no_mangle]
+            pub fn wcet_start() {
+                #(#stubs)*
+                cortex_m::asm::bkpt();
+            }
+        });
+    }
 }