diff --git a/.gdbinit_old b/.gdbinit_old
new file mode 100644
index 0000000000000000000000000000000000000000..7c72d4fb1f4064ffbe5275f665caa65846bf90da
--- /dev/null
+++ b/.gdbinit_old
@@ -0,0 +1,6 @@
+target remote :3333
+
+monitor arm semihosting enable
+
+load
+step
diff --git a/.vscode/.cortex-debug.peripherals.state.json b/.vscode/.cortex-debug.peripherals.state.json
new file mode 100644
index 0000000000000000000000000000000000000000..0637a088a01e8ddab3bf3fa98dbe804cbde1a0dc
--- /dev/null
+++ b/.vscode/.cortex-debug.peripherals.state.json
@@ -0,0 +1 @@
+[]
\ No newline at end of file
diff --git a/.vscode/.cortex-debug.registers.state.json b/.vscode/.cortex-debug.registers.state.json
new file mode 100644
index 0000000000000000000000000000000000000000..0637a088a01e8ddab3bf3fa98dbe804cbde1a0dc
--- /dev/null
+++ b/.vscode/.cortex-debug.registers.state.json
@@ -0,0 +1 @@
+[]
\ No newline at end of file
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000000000000000000000000000000000000..be44a236499bf1c984950dd42468192d6756a701
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,4 @@
+{
+    "python.linting.enabled": false,
+    "python.formatting.provider": "autopep8"
+}
\ No newline at end of file
diff --git a/Cargo.toml b/Cargo.toml
index 40d43efe7a0252695c7cd1423977954fe1d70868..ca27c3473fa8b376ae83844942c9bf62eaf0a48a 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -36,7 +36,7 @@ path = "./klee"
 
 [features]
 wcet_bkpt = ["cortex-m-rtfm-macros/wcet_bkpt"] 
-wcet_nop = []
+wcet_nop = ["cortex-m-rtfm-macros/wcet_nop"]
 klee_mode = ["cortex-m-rtfm-macros/klee_mode", "klee/klee_mode"] 
 
 cm7-r0p1 = ["cortex-m/cm7-r0p1"]
diff --git a/examples/resource.rs b/examples/resource.rs
index 586939308a788065c6caddf2a7c679b7ee2ae93e..fda75f6fe8fe183f6c47060e1da7424b6c78f08d 100644
--- a/examples/resource.rs
+++ b/examples/resource.rs
@@ -3,14 +3,15 @@
 #![feature(proc_macro)]
 #![feature(used)]
 #![no_std]
-
+#![feature(asm)]
 extern crate cortex_m_rtfm as rtfm;
 // IMPORTANT always do this rename
 extern crate stm32f413;
 
 #[macro_use]
 extern crate klee;
-//use klee::k_abort;
+use klee::*;
+use rtfm::{bkpt_1, bkpt_2, bkpt_3};
 
 // import the procedural macro
 use rtfm::{app, Resource, Threshold};
@@ -73,7 +74,9 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
 fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
     r.X.claim_mut(t, |x, _| {
         *x += 1;
-    })
+    });
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt()
 }
 
 #[inline(never)]
@@ -82,8 +85,11 @@ fn init(_p: init::Peripherals, _r: init::Resources) {}
 
 #[inline(never)]
 #[allow(dead_code)]
+#[allow(private_no_mangle_fns)]
 #[no_mangle]
 fn idle() -> ! {
+    let r = stub_EXTI1;
+    k_read(&r());
     loop {
         rtfm::nop();
     }
diff --git a/expan.rs b/expan.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0510aab29c68e43d22d7b6a634aa6072e36a26d6
--- /dev/null
+++ b/expan.rs
@@ -0,0 +1,199 @@
+tasks
+EXTI1
+#![feature(prelude_import)]
+#![no_std]
+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![no_std]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core as core;
+
+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_assert};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+// this is the path to the device crate
+
+#[allow(non_camel_case_types)]
+#[allow(non_snake_case)]
+pub struct _initResources<'a> {
+    pub X: &'a mut u32,
+}
+#[allow(unsafe_code)]
+mod init {
+    pub struct Peripherals {
+        pub core: ::stm32f103xx::CorePeripherals,
+        pub device: ::stm32f103xx::Peripherals,
+    }
+    pub use _initResources as Resources;
+    #[allow(unsafe_code)]
+    impl<'a> Resources<'a> {
+        pub unsafe fn new() -> Self {
+            Resources { X: &mut ::_X }
+        }
+    }
+}
+static mut _X: u32 = 0;
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        // 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();
+        // }
+        if !(t.value() >= 1u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 1u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 1u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 1u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 1u8, stm32f103xx::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 1u8, stm32f103xx::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI1::X {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_X }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI1::X {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _X }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI1"]
+pub unsafe extern "C" fn _EXTI1() {
+    let f: fn(&mut rtfm::Threshold, EXTI1::Resources) = exti1;
+    f(
+        &mut if 1u8 == 1 << stm32f103xx::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(1u8)
+        },
+        EXTI1::Resources::new(),
+    )
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI1 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (1u8 - 1, (1 << ::stm32f103xx::NVIC_PRIO_BITS) - 1u8);
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+fn main() {
+    let init: fn(init::Peripherals, init::Resources) = init;
+    rtfm::atomic(unsafe { &mut rtfm::Threshold::new(0) }, |_t| unsafe {
+        let _late_resources = init(
+            init::Peripherals {
+                core: ::stm32f103xx::CorePeripherals::steal(),
+                device: ::stm32f103xx::Peripherals::steal(),
+            },
+            init::Resources::new(),
+        );
+        let mut nvic: stm32f103xx::NVIC = core::mem::transmute(());
+        let prio_bits = stm32f103xx::NVIC_PRIO_BITS;
+        let hw = ((1 << prio_bits) - 1u8) << (8 - prio_bits);
+        nvic.set_priority(stm32f103xx::Interrupt::EXTI1, hw);
+        nvic.enable(stm32f103xx::Interrupt::EXTI1);
+    });
+}
+fn exti1(_t: &mut Threshold, _r: EXTI1::Resources) {}
+fn t(x: &mut u32) {
+    let mut y = 0;
+    if *x < 10 {
+        for _ in 0..*x {
+            y += 1;
+            {
+                #[allow(unsafe_code)]
+                unsafe {
+                    core::ptr::read_volatile(&0);
+                }
+            };
+        }
+    }
+}
+#[inline(never)]
+fn init(_p: init::Peripherals, r: init::Resources) {
+    let mut x: &mut u32 = r.X;
+    {
+        #[allow(unsafe_code)]
+        #[allow(warnings)]
+        ::k_mk_symbol(unsafe { x }, unsafe {
+            ::CStr::from_bytes_with_nul_unchecked("X\u{0}".as_bytes())
+        })
+    };
+    t(x);
+}
diff --git a/expand_klee.rs b/expand_klee.rs
new file mode 100644
index 0000000000000000000000000000000000000000..73dd942dcfa874eb11435697cb17197dee4d3a79
--- /dev/null
+++ b/expand_klee.rs
@@ -0,0 +1,4 @@
+tasks
+EXTI1
+EXTI2
+EXTI3
diff --git a/expand_nop b/expand_nop
new file mode 100644
index 0000000000000000000000000000000000000000..cc6b7cce4f2f50c20b44e0d80cc678e07e44cb27
--- /dev/null
+++ b/expand_nop
@@ -0,0 +1,925 @@
+#![feature(prelude_import)]
+#![no_std]
+//! Example using shared resources
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core as core;
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+//use klee::k_abort;
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+// this is the path to the device crate
+
+#[allow(non_camel_case_types)]
+#[allow(non_snake_case)]
+pub struct _initResources<'a> {
+    pub X: &'a mut u32,
+    pub Y: &'a mut u32,
+}
+#[allow(unsafe_code)]
+mod init {
+    pub struct Peripherals {
+        pub core: ::stm32f413::CorePeripherals,
+        pub device: ::stm32f413::Peripherals,
+    }
+    pub use _initResources as Resources;
+    #[allow(unsafe_code)]
+    impl<'a> Resources<'a> {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: &mut ::_X,
+                Y: &mut ::_Y,
+            }
+        }
+    }
+}
+static mut _X: u32 = 0;
+static mut _Y: u32 = 0;
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        // extern crate cortex_m;
+
+        // Static code analysis
+        // In this lab we will study how a Rust RTFM application can be
+        // statically analysed.
+        //
+        // The application has three tasks EXTI1, EXTI2 and EXTI3,
+        // with associated priorites 1 (lowest), 3 (highest), and 2 (mid).
+        //
+        // Assignment 1.
+        // Build the application for KLEE analysis.
+        // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // Start the KLEE docker
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
+        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        //
+        // Now run KLEE in the docker.
+        // > klee resource-*.bc
+        // KLEE: WARNING: executable has module level assembly (ignoring)
+        // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
+        // KLEE: NOTE: now ignoring this error at this location
+
+        // KLEE: done: total instructions = 11575
+        // KLEE: done: completed paths = 25
+        // KLEE: done: generated tests = 16
+        //
+        // When compiled with the --features klee_mode, resources are treated as symbolic.
+        // Investigate the output files (in `klee-last`). Use `ktest-tool` to examine the tests.
+        // The file `klee/tasks.txt` gives the order of tasks, it may vary for each run.
+        // ```
+        // // autogenerated file
+        // ["EXTI1", "EXTI2", "EXTI3"]
+        // ```
+        //
+        // How many tests were generated for task EXIT1?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT2?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT3?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // (There will be one additional "dymmy" test for testing "no task".)
+        //
+        // Now identify the cause of generated error.
+        // > more klee-last/*.abort.err
+        //
+        // Find the error on the source code and fix it.
+        // Hint, use *wrapping arithmetics*.
+        //
+        // Repeat the code generation, run KLEE agian and fix errors until
+        // no more errors are found.
+        //
+        // How many errors were identified?
+        // ** your answer here **
+        //
+        // For one of the arithmetic operations, no error was found.
+        // Explain why this is no error.
+        // ** your answer here **
+        //
+        // Why didn't KLEE report all the errors initially?
+        // Scroll back and compare the stack traces of the generated errors.
+        // Hint, for each line in the code KLEE will spot ONE error.
+        // ** your answer here **
+        //
+        // Assignment 2.
+        // KLEE has now generated tests covering EACH feasible path for EACH task.
+        // Now we will analyse the exection time for each such test.
+        //
+        // In order to do that comiple your application.
+        // > xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf
+        //
+        // We build in --release for optimizing the performance.
+        // The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
+        // of each resource. This allows you to monitor the number of clock cyckles using gdb.
+        //
+        // Connect your Nucleo64 board with the `stm32f401re` (or `stm32f411re`) MCU.
+        // Start openocd in a separate terminal (and let it run there).
+        //
+        // > openocd -f interface/stlink.cfg -f target/stm32f4x.cfg
+        // (You may use `-f inteface/stlink-v2-1.cfg`, if `stlink.cfg` is missing.)
+        //
+        // Start gdb.
+        // > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
+        //
+        // The `gdbinit_manual` has the following content.
+        // ```
+        // target remote :3333
+        // mon reset halt
+        // load
+        // tb main
+        // continue
+        //
+        // Line by line, it:
+        // - connects to the target (the MCU)
+        // - resets the MCU
+        // - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
+        // - sets a temporary breakpoint to `main`, and
+        // - continues executing until `main` is reached.
+        //
+        // At the point the MCU hits `main` it stops.
+        // (You may be promted to continue working <return> or quit, in such case press <return>.)
+        //
+        // Now you can inspect where the processor halted.
+        // >  (gdb) list
+        // 560                 // be executed *before* enabling the FPU and that would generate an
+        // 561                 // exception
+        // 562                 #[inline(never)]
+        // 563                 fn main() {
+        // 564                     unsafe {
+        // 565                         ::main(0, ::core::ptr::null());
+        // 566                     }
+        // 567                 }
+        // 568
+        // 569                 main()
+        //
+        // As you see this is not part of your program, rather it originates from the library startup code.
+        //
+        // This is perfect, now the MCU is initiated and under your control.
+        //
+        // At this point the memory (resources), holds their initial values from the
+        // your application (this was set by the library code prior to hitting main).
+        // You can inspect the global reasources (they are prepended by `_`).
+        //
+        // (gdb) p resource::_X
+        // $1 = 0
+        // (gdb) p resource::_Y
+        // $2 = 0
+        //
+        // Before calling our tasks we need to enable the debug timer (cycle counter in the DWT unit of the MCU).
+        //
+        // (gdb) mon mww 0xe0001000 1
+        //
+        // and set the counter value to 0
+        //
+        // (gdb) mon mww 0xe0001004 0
+        //
+        // Now we can call the task(s). Lets start easy with EXTI3.
+        // (gdb) call stub_EXTI3()
+        // (gdb) mon mrw 0xe0001004
+        // 9
+        //
+        // Wow, it took only 9 clock cycles to run the complete task!!!!
+        // (Compare to a threaded OS that would require several 100 clock cycles to start a thread/task)
+        //
+        // But hey, where did my claim go? Wasn't I supposed to hit a breakpoint when claiming the resource?
+        // (In this case the resource X)
+        // Well Rust RTFM is smart enough to know that you are already at sufficient threshold (priority)
+        // in order to grant you the resource dircectly. Let us look at the code.
+        //
+        // (gdb) disassemble stub_EXTI3
+        // Dump of assembler code for function stub_EXTI3:
+        //    0x08000268 <+0>:     movw    r0, #0
+        //    0x0800026c <+4>:     movt    r0, #8192       ; 0x2000
+        //    0x08000270 <+8>:     ldr     r1, [r0, #0]
+        //    0x08000272 <+10>:    adds    r1, #1
+        //    0x08000274 <+12>:    str     r1, [r0, #0]
+        //    0x08000276 <+14>:    bx      lr
+        // End of assembler dump.
+        //
+        // Here you go, cannot be simpler that this, it:
+        // - sets up the address to X in r0
+        // - reads the old value
+        // - adds 1 (wrapping arithmetics)
+        // - stores the new value in X, and
+        // - it returns
+        // (On Cortex M functions and inerrupt handlers are essentially treated the same way)
+        //
+        // So now you can check the value of X. See above...
+        // ** your answer here **
+        //
+        // Now let us turn to EXTI2.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI2()
+        // (gdb) mon mrw 0xe0001004
+        // 13
+        //
+        // Also in this case we see that the resource (`Y`) was granted without overhead
+        // The code took a few additional clock cycles (its contians a condition, right).
+        // Figure out which path was triggered by this test.
+        // ** your answer here **
+        //
+        // Now figure out how to test the other branch
+        // you can use
+        // (gdb) set resource::_Y=...
+        // to set a value in memory
+        //
+        // Make a call to the `stub_EXTI2()` with the set value of `_Y`.
+        // How many clock cycles did you get (rember to set the counter to 0 before calling)
+        // ** your answer here **
+        //
+        // Check the nwe value of `_Y`.
+        // ** your answer here **
+        //
+        // Hint, if done correctly, you should have the same number of cycles for both paths.
+        // Ok, so the cycle count was the same ;)
+        // How so, lets have a look at the generated assembly.
+        //
+        //  (gdb) disassemble stub_EXTI2
+        // Dump of assembler code for function stub_EXTI2:
+        //    0x080002aa <+0>:     movw    r0, #0
+        //    0x080002ae <+4>:     mov.w   r2, #4294967295 ; 0xffffffff
+        //    0x080002b2 <+8>:     movt    r0, #8192       ; 0x2000
+        //    0x080002b6 <+12>:    ldr     r1, [r0, #4]
+        //    0x080002b8 <+14>:    cmp     r1, #10
+        //    0x080002ba <+16>:    it      cc
+        //    0x080002bc <+18>:    movcc   r2, #1
+        //    0x080002be <+20>:    add     r1, r2
+        //    0x080002c0 <+22>:    str     r1, [r0, #4]
+        //    0x080002c2 <+24>:    bx      lr
+        // End of assembler dump.
+        //
+        // This one is a bit harder to understand.
+        // What it does essentially is:
+        // - read `Y` into r1,
+        // - store -1 in r2
+        // - conditionally overwrite the r2 by a 1 if `Y < 10`
+        // - add r2 to r1 (the value of `Y`),
+        // - update `Y`.
+        //
+        // So this is beautiful, the COSTLY branch is replaced by a CHEAP
+        // condtitonal assigmnet `movcc`.
+        // You can read more on this on
+        // http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0553a/BABEHFEF.html
+        //
+        // Ok, back to the program...
+        // Now recall the KLEE generated test cases.
+        // Spot the ones regarding EXTI2.
+        // What assignments would KLEE suggest to `Y` to test both paths.
+        // ** your answers here **
+        //
+        // So, your test assignments or the ones from KLEE, which ones is better?
+        // ** your answer here **
+
+        // (We will return to optimising test cases later... so put this on your mental stack :)
+        //
+        // Now lets have a look at the tricky one EXTI1.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI1()
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // The program being debugged was signaled while in a function called from GDB.
+        // GDB remains in the frame where the signal was received.
+        // To change this behavior use "set unwindonsignal on".
+        // Evaluation of the expression containing the function
+        // (stub_EXTI1) will be abandoned.
+        // When the function is done executing, GDB will silently stop.
+        //
+        // So what is happening here is that it runs into the (first) brkp intstruction (LOCK `X`).
+        // You may ignore the verbose output at this point....
+        //
+        // Run
+        // (gdb) mon mrw 0xe0001004
+        // 15
+        //
+        // So all in all it took 15 cycles to get there, `claim X`.
+        // We can look at the code causing the `bkpt`
+        // (gdb) list
+        // 162                         }
+        // 163
+        // 164                         // wcet_bkpt mode
+        // 165                         // put breakpoint at raise ceiling, for tracing execution time
+        // 166                         if cfg!(feature = "wcet_bkpt") {
+        // 167                             bkpt();
+        // 168                         }
+        //
+        // That makes sense, we are in the RTFM library handling the `claim X`
+        // (gdb) c
+        // Continuing.
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // (gdb) mon mrw 0xe0001004
+        // 19
+        //
+        // So after 19 clock cycles we claim `Y`
+        //
+        // Now lets have a look at the generated assembly.
+        // (gdb) disassemble
+        // ...
+        //    0x080002f6 <+4>:     bcs.n   0x8000334 <resource::<impl rtfm_core::Resource for resource::EXTI1::X>::claim+66>
+        //    0x080002f8 <+6>:     movs    r1, #224        ; 0xe0
+        //    0x080002fa <+8>:     movs    r2, #208        ; 0xd0
+        //    0x080002fc <+10>:    mrs     r12, BASEPRI
+        //    0x08000300 <+14>:    msr     BASEPRI, r1
+        //    0x08000304 <+18>:    bkpt    0x0000
+        //    0x08000306 <+20>:    mrs     r1, BASEPRI
+        //    0x0800030a <+24>:    msr     BASEPRI, r2
+        //    0x0800030e <+28>:    movw    r2, #0
+        // => 0x08000312 <+32>:    bkpt    0x0000
+        //    0x08000314 <+34>:    movt    r2, #8192       ; 0x2000
+        //    0x08000318 <+38>:    ldr     r3, [r2, #0]
+        //    0x0800031a <+40>:    subs    r0, r3, #1
+        //    0x0800031c <+42>:    cmp     r0, #8
+        //    0x0800031e <+44>:    ittt    ls
+        //    0x08000320 <+46>:    ldrls   r0, [r2, #4]
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // We are now inside the critital sections of both X and Y and have access to both resources for the loop.
+        // (gdb) c
+        // Continuing.
+        //
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        //
+        // We are now releasing `Y`.
+        // (gdb) mon mrw 0xe0001004
+        // 29
+        //
+        // How long (in cycles) was the critical section on `Y`?
+        // ** your answer here **
+
+        // (gdb) disassemble
+        // ...
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        // => 0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // Let us continue
+        // (gdb) c
+        // Continuing.
+
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        // 181                             bkpt();
+        //
+        // (gdb) mon mrw 0xe0001004
+        // 30
+        //
+        // How long (in cycles) was the critical section on `X`?
+        // ** your answer here **
+        //
+        // (gdb) disassemble
+        // ...
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // => 0x0800032c <+58>:    bkpt    0x0000
+        //    0x0800032e <+60>:    msr     BASEPRI, r12
+        //    0x08000332 <+64>:    bx      lr
+        //
+        // At this point we can contiue
+        // (gdb) c
+        // Continuing.
+        // EXTI1 has now run to completion.
+        //
+        // What was the total excecution time for EXTI1?
+        // ** your answer here **
+        //
+        // What is the value of the resouce X?
+        // ** your answer here **
+        //
+        // Just by looking at the code, what would the worst case assignment of X be?
+        // I.e., the assingnment of `X' that gives the worst case execution time.
+        // ** your answer here **
+        //
+        // Measure that execution time. What did you get.
+        // ** your answer here **
+        //
+        // Your answer might blow your mind!!! How the heck is that even possible?
+        //
+        // At this point you should find that the worst case time stays the same ...
+        //
+        // Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
+        // What it does is that it figures out that we actually increase `Y`, by the value of `X`.
+        // So the loop is all gone, optimized out, and replaced by a simple addition.
+        //
+        // Now lets look at best case execution time.
+        // Figure out an assignment of `X`, that might actually reduce the execution time.
+        // ** your answer here **
+        //
+        // Redo the experiment with this value. How many clock cycles did you get?
+        // ** your answer here **
+        //
+        // Assignment 3.
+        // In assignment 2 we analysed EXTI1
+        // We found that for the examples, Rust RTFM was able to generate extremely efficient
+        // implementations, replacing branching with contdiditonal assignments and
+        // even remove comlete loops.
+        //
+        // Now lets have a look at using optimized LLVM and how it affects the number of tests.
+        // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // and now start a docker for the optimized build
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // and in the docker run
+        // > klee resource*.bc
+        //
+        // Look at the generated tests.
+        // Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
+        // ** your answers (5) here **
+        //
+        // Were the optimized tests sufficient to cover the execution time behavior.
+        // ** your answer here **
+        //
+        // Can you come up with a case where --release mode based analysis would miss cricital cases.
+        // ** your answer here, --- actually a research question, we will discuss in class --- **
+        //
+        // On a side note.
+        // Rust in --release mode makes the job for KLEE much easier. Look the number of instuctions carried out.
+        // In dev/debug you had som 10 000 instuctions executed for generating the test cases.
+        // In --relesase you had 34!!!!!
+        //
+        // This vastly improves on the performance of analysis, allowing larger applications to be scrutenized.
+        // The code we looked at here was by intention simple (to facilitate inspection).
+        // However, the code is NOT trivial, under the hood it utilizes advanced language features, such as
+        // closures and intence use of abstractions, such as Traits/genecics etc. It indeed covers a large
+        // degree of the Rust, for which it demonstrates that our approach to based program analysis
+        // actually works.
+        //
+        // For the future we intend the framework to cover the reading and writing to peripherals, and the
+        // sequenced access to resources. In class we will further discuss current limitations, and
+        // oportunities to improvements.
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI1"]
+pub unsafe extern "C" fn _EXTI1() {
+    let f: fn(&mut rtfm::Threshold, EXTI1::Resources) = exti1;
+    f(
+        &mut if 1u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(1u8)
+        },
+        EXTI1::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI1() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI1();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI1 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (1u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 1u8);
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub Y: Y,
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                Y: Y { _0: PhantomData },
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI3::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI3::X {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_X }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI3::X {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _X }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI3"]
+pub unsafe extern "C" fn _EXTI3() {
+    let f: fn(&mut rtfm::Threshold, EXTI3::Resources) = exti3;
+    f(
+        &mut if 2u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(2u8)
+        },
+        EXTI3::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI3() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI3();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI3 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (2u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 2u8);
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI2::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI2::Y {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_Y }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI2::Y {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _Y }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI2"]
+pub unsafe extern "C" fn _EXTI2() {
+    let f: fn(&mut rtfm::Threshold, EXTI2::Resources) = exti2;
+    f(
+        &mut if 3u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(3u8)
+        },
+        EXTI2::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI2() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI2();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI2 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (3u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 3u8);
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub Y: Y,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                Y: Y { _0: PhantomData },
+            }
+        }
+    }
+}
+extern crate cortex_m;
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+pub fn wcet_start() {
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt();
+    stub_EXTI1();
+    stub_EXTI3();
+    stub_EXTI2();
+}
+#[allow(private_no_mangle_fns)]
+#[allow(unsafe_code)]
+fn main() {
+    let init: fn(init::Peripherals, init::Resources) = init;
+    rtfm::atomic(unsafe { &mut rtfm::Threshold::new(0) }, |_t| unsafe {
+        let _late_resources = init(
+            init::Peripherals {
+                core: ::stm32f413::CorePeripherals::steal(),
+                device: ::stm32f413::Peripherals::steal(),
+            },
+            init::Resources::new(),
+        );
+        let mut nvic: stm32f413::NVIC = core::mem::transmute(());
+        let prio_bits = stm32f413::NVIC_PRIO_BITS;
+        let hw = ((1 << prio_bits) - 1u8) << (8 - prio_bits);
+        nvic.set_priority(stm32f413::Interrupt::EXTI1, hw);
+        nvic.enable(stm32f413::Interrupt::EXTI1);
+        let prio_bits = stm32f413::NVIC_PRIO_BITS;
+        let hw = ((1 << prio_bits) - 2u8) << (8 - prio_bits);
+        nvic.set_priority(stm32f413::Interrupt::EXTI3, hw);
+        nvic.enable(stm32f413::Interrupt::EXTI3);
+        let prio_bits = stm32f413::NVIC_PRIO_BITS;
+        let hw = ((1 << prio_bits) - 3u8) << (8 - prio_bits);
+        nvic.set_priority(stm32f413::Interrupt::EXTI2, hw);
+        nvic.enable(stm32f413::Interrupt::EXTI2);
+    });
+    let idle: fn() -> ! = idle;
+    idle();
+}
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    X.claim(t, |x, t1| {
+        Y.claim_mut(t1, |y, _| {
+            if *x < 10 {
+                for _ in 0..*x {
+                    *y += 1;
+                }
+            }
+        });
+    });
+}
+#[allow(non_snake_case)]
+fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
+    r.Y.claim_mut(t, |y, _| {
+        if *y < 10 {
+            *y += 1;
+        } else {
+            *y -= 1;
+        }
+    });
+}
+#[allow(non_snake_case)]
+fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
+    r.X.claim_mut(t, |x, _| {
+        *x += 1;
+    });
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt()
+}
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals, _r: init::Resources) {}
+#[inline(never)]
+#[allow(dead_code)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+fn idle() -> ! {
+    loop {
+        rtfm::nop();
+    }
+}
diff --git a/expand_nop.rs b/expand_nop.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d92afdd2e03578072157a5bc60c748454c762777
--- /dev/null
+++ b/expand_nop.rs
@@ -0,0 +1,903 @@
+#![feature(prelude_import)]
+#![no_std]
+//! Example using shared resources
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core as core;
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+//use klee::k_abort;
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+// this is the path to the device crate
+
+#[allow(non_camel_case_types)]
+#[allow(non_snake_case)]
+pub struct _initResources<'a> {
+    pub X: &'a mut u32,
+    pub Y: &'a mut u32,
+}
+#[allow(unsafe_code)]
+mod init {
+    pub struct Peripherals {
+        pub core: ::stm32f413::CorePeripherals,
+        pub device: ::stm32f413::Peripherals,
+    }
+    pub use _initResources as Resources;
+    #[allow(unsafe_code)]
+    impl<'a> Resources<'a> {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: &mut ::_X,
+                Y: &mut ::_Y,
+            }
+        }
+    }
+}
+static mut _X: u32 = 0;
+static mut _Y: u32 = 0;
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        // extern crate cortex_m;
+
+        // Static code analysis
+        // In this lab we will study how a Rust RTFM application can be
+        // statically analysed.
+        //
+        // The application has three tasks EXTI1, EXTI2 and EXTI3,
+        // with associated priorites 1 (lowest), 3 (highest), and 2 (mid).
+        //
+        // Assignment 1.
+        // Build the application for KLEE analysis.
+        // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // Start the KLEE docker
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
+        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        //
+        // Now run KLEE in the docker.
+        // > klee resource-*.bc
+        // KLEE: WARNING: executable has module level assembly (ignoring)
+        // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
+        // KLEE: NOTE: now ignoring this error at this location
+
+        // KLEE: done: total instructions = 11575
+        // KLEE: done: completed paths = 25
+        // KLEE: done: generated tests = 16
+        //
+        // When compiled with the --features klee_mode, resources are treated as symbolic.
+        // Investigate the output files (in `klee-last`). Use `ktest-tool` to examine the tests.
+        // The file `klee/tasks.txt` gives the order of tasks, it may vary for each run.
+        // ```
+        // // autogenerated file
+        // ["EXTI1", "EXTI2", "EXTI3"]
+        // ```
+        //
+        // How many tests were generated for task EXIT1?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT2?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT3?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // (There will be one additional "dymmy" test for testing "no task".)
+        //
+        // Now identify the cause of generated error.
+        // > more klee-last/*.abort.err
+        //
+        // Find the error on the source code and fix it.
+        // Hint, use *wrapping arithmetics*.
+        //
+        // Repeat the code generation, run KLEE agian and fix errors until
+        // no more errors are found.
+        //
+        // How many errors were identified?
+        // ** your answer here **
+        //
+        // For one of the arithmetic operations, no error was found.
+        // Explain why this is no error.
+        // ** your answer here **
+        //
+        // Why didn't KLEE report all the errors initially?
+        // Scroll back and compare the stack traces of the generated errors.
+        // Hint, for each line in the code KLEE will spot ONE error.
+        // ** your answer here **
+        //
+        // Assignment 2.
+        // KLEE has now generated tests covering EACH feasible path for EACH task.
+        // Now we will analyse the exection time for each such test.
+        //
+        // In order to do that comiple your application.
+        // > xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf
+        //
+        // We build in --release for optimizing the performance.
+        // The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
+        // of each resource. This allows you to monitor the number of clock cyckles using gdb.
+        //
+        // Connect your Nucleo64 board with the `stm32f401re` (or `stm32f411re`) MCU.
+        // Start openocd in a separate terminal (and let it run there).
+        //
+        // > openocd -f interface/stlink.cfg -f target/stm32f4x.cfg
+        // (You may use `-f inteface/stlink-v2-1.cfg`, if `stlink.cfg` is missing.)
+        //
+        // Start gdb.
+        // > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
+        //
+        // The `gdbinit_manual` has the following content.
+        // ```
+        // target remote :3333
+        // mon reset halt
+        // load
+        // tb main
+        // continue
+        //
+        // Line by line, it:
+        // - connects to the target (the MCU)
+        // - resets the MCU
+        // - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
+        // - sets a temporary breakpoint to `main`, and
+        // - continues executing until `main` is reached.
+        //
+        // At the point the MCU hits `main` it stops.
+        // (You may be promted to continue working <return> or quit, in such case press <return>.)
+        //
+        // Now you can inspect where the processor halted.
+        // >  (gdb) list
+        // 560                 // be executed *before* enabling the FPU and that would generate an
+        // 561                 // exception
+        // 562                 #[inline(never)]
+        // 563                 fn main() {
+        // 564                     unsafe {
+        // 565                         ::main(0, ::core::ptr::null());
+        // 566                     }
+        // 567                 }
+        // 568
+        // 569                 main()
+        //
+        // As you see this is not part of your program, rather it originates from the library startup code.
+        //
+        // This is perfect, now the MCU is initiated and under your control.
+        //
+        // At this point the memory (resources), holds their initial values from the
+        // your application (this was set by the library code prior to hitting main).
+        // You can inspect the global reasources (they are prepended by `_`).
+        //
+        // (gdb) p resource::_X
+        // $1 = 0
+        // (gdb) p resource::_Y
+        // $2 = 0
+        //
+        // Before calling our tasks we need to enable the debug timer (cycle counter in the DWT unit of the MCU).
+        //
+        // (gdb) mon mww 0xe0001000 1
+        //
+        // and set the counter value to 0
+        //
+        // (gdb) mon mww 0xe0001004 0
+        //
+        // Now we can call the task(s). Lets start easy with EXTI3.
+        // (gdb) call stub_EXTI3()
+        // (gdb) mon mrw 0xe0001004
+        // 9
+        //
+        // Wow, it took only 9 clock cycles to run the complete task!!!!
+        // (Compare to a threaded OS that would require several 100 clock cycles to start a thread/task)
+        //
+        // But hey, where did my claim go? Wasn't I supposed to hit a breakpoint when claiming the resource?
+        // (In this case the resource X)
+        // Well Rust RTFM is smart enough to know that you are already at sufficient threshold (priority)
+        // in order to grant you the resource dircectly. Let us look at the code.
+        //
+        // (gdb) disassemble stub_EXTI3
+        // Dump of assembler code for function stub_EXTI3:
+        //    0x08000268 <+0>:     movw    r0, #0
+        //    0x0800026c <+4>:     movt    r0, #8192       ; 0x2000
+        //    0x08000270 <+8>:     ldr     r1, [r0, #0]
+        //    0x08000272 <+10>:    adds    r1, #1
+        //    0x08000274 <+12>:    str     r1, [r0, #0]
+        //    0x08000276 <+14>:    bx      lr
+        // End of assembler dump.
+        //
+        // Here you go, cannot be simpler that this, it:
+        // - sets up the address to X in r0
+        // - reads the old value
+        // - adds 1 (wrapping arithmetics)
+        // - stores the new value in X, and
+        // - it returns
+        // (On Cortex M functions and inerrupt handlers are essentially treated the same way)
+        //
+        // So now you can check the value of X. See above...
+        // ** your answer here **
+        //
+        // Now let us turn to EXTI2.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI2()
+        // (gdb) mon mrw 0xe0001004
+        // 13
+        //
+        // Also in this case we see that the resource (`Y`) was granted without overhead
+        // The code took a few additional clock cycles (its contians a condition, right).
+        // Figure out which path was triggered by this test.
+        // ** your answer here **
+        //
+        // Now figure out how to test the other branch
+        // you can use
+        // (gdb) set resource::_Y=...
+        // to set a value in memory
+        //
+        // Make a call to the `stub_EXTI2()` with the set value of `_Y`.
+        // How many clock cycles did you get (rember to set the counter to 0 before calling)
+        // ** your answer here **
+        //
+        // Check the nwe value of `_Y`.
+        // ** your answer here **
+        //
+        // Hint, if done correctly, you should have the same number of cycles for both paths.
+        // Ok, so the cycle count was the same ;)
+        // How so, lets have a look at the generated assembly.
+        //
+        //  (gdb) disassemble stub_EXTI2
+        // Dump of assembler code for function stub_EXTI2:
+        //    0x080002aa <+0>:     movw    r0, #0
+        //    0x080002ae <+4>:     mov.w   r2, #4294967295 ; 0xffffffff
+        //    0x080002b2 <+8>:     movt    r0, #8192       ; 0x2000
+        //    0x080002b6 <+12>:    ldr     r1, [r0, #4]
+        //    0x080002b8 <+14>:    cmp     r1, #10
+        //    0x080002ba <+16>:    it      cc
+        //    0x080002bc <+18>:    movcc   r2, #1
+        //    0x080002be <+20>:    add     r1, r2
+        //    0x080002c0 <+22>:    str     r1, [r0, #4]
+        //    0x080002c2 <+24>:    bx      lr
+        // End of assembler dump.
+        //
+        // This one is a bit harder to understand.
+        // What it does essentially is:
+        // - read `Y` into r1,
+        // - store -1 in r2
+        // - conditionally overwrite the r2 by a 1 if `Y < 10`
+        // - add r2 to r1 (the value of `Y`),
+        // - update `Y`.
+        //
+        // So this is beautiful, the COSTLY branch is replaced by a CHEAP
+        // condtitonal assigmnet `movcc`.
+        // You can read more on this on
+        // http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0553a/BABEHFEF.html
+        //
+        // Ok, back to the program...
+        // Now recall the KLEE generated test cases.
+        // Spot the ones regarding EXTI2.
+        // What assignments would KLEE suggest to `Y` to test both paths.
+        // ** your answers here **
+        //
+        // So, your test assignments or the ones from KLEE, which ones is better?
+        // ** your answer here **
+
+        // (We will return to optimising test cases later... so put this on your mental stack :)
+        //
+        // Now lets have a look at the tricky one EXTI1.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI1()
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // The program being debugged was signaled while in a function called from GDB.
+        // GDB remains in the frame where the signal was received.
+        // To change this behavior use "set unwindonsignal on".
+        // Evaluation of the expression containing the function
+        // (stub_EXTI1) will be abandoned.
+        // When the function is done executing, GDB will silently stop.
+        //
+        // So what is happening here is that it runs into the (first) brkp intstruction (LOCK `X`).
+        // You may ignore the verbose output at this point....
+        //
+        // Run
+        // (gdb) mon mrw 0xe0001004
+        // 15
+        //
+        // So all in all it took 15 cycles to get there, `claim X`.
+        // We can look at the code causing the `bkpt`
+        // (gdb) list
+        // 162                         }
+        // 163
+        // 164                         // wcet_bkpt mode
+        // 165                         // put breakpoint at raise ceiling, for tracing execution time
+        // 166                         if cfg!(feature = "wcet_bkpt") {
+        // 167                             bkpt();
+        // 168                         }
+        //
+        // That makes sense, we are in the RTFM library handling the `claim X`
+        // (gdb) c
+        // Continuing.
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // (gdb) mon mrw 0xe0001004
+        // 19
+        //
+        // So after 19 clock cycles we claim `Y`
+        //
+        // Now lets have a look at the generated assembly.
+        // (gdb) disassemble
+        // ...
+        //    0x080002f6 <+4>:     bcs.n   0x8000334 <resource::<impl rtfm_core::Resource for resource::EXTI1::X>::claim+66>
+        //    0x080002f8 <+6>:     movs    r1, #224        ; 0xe0
+        //    0x080002fa <+8>:     movs    r2, #208        ; 0xd0
+        //    0x080002fc <+10>:    mrs     r12, BASEPRI
+        //    0x08000300 <+14>:    msr     BASEPRI, r1
+        //    0x08000304 <+18>:    bkpt    0x0000
+        //    0x08000306 <+20>:    mrs     r1, BASEPRI
+        //    0x0800030a <+24>:    msr     BASEPRI, r2
+        //    0x0800030e <+28>:    movw    r2, #0
+        // => 0x08000312 <+32>:    bkpt    0x0000
+        //    0x08000314 <+34>:    movt    r2, #8192       ; 0x2000
+        //    0x08000318 <+38>:    ldr     r3, [r2, #0]
+        //    0x0800031a <+40>:    subs    r0, r3, #1
+        //    0x0800031c <+42>:    cmp     r0, #8
+        //    0x0800031e <+44>:    ittt    ls
+        //    0x08000320 <+46>:    ldrls   r0, [r2, #4]
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // We are now inside the critital sections of both X and Y and have access to both resources for the loop.
+        // (gdb) c
+        // Continuing.
+        //
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        //
+        // We are now releasing `Y`.
+        // (gdb) mon mrw 0xe0001004
+        // 29
+        //
+        // How long (in cycles) was the critical section on `Y`?
+        // ** your answer here **
+
+        // (gdb) disassemble
+        // ...
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        // => 0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // Let us continue
+        // (gdb) c
+        // Continuing.
+
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        // 181                             bkpt();
+        //
+        // (gdb) mon mrw 0xe0001004
+        // 30
+        //
+        // How long (in cycles) was the critical section on `X`?
+        // ** your answer here **
+        //
+        // (gdb) disassemble
+        // ...
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // => 0x0800032c <+58>:    bkpt    0x0000
+        //    0x0800032e <+60>:    msr     BASEPRI, r12
+        //    0x08000332 <+64>:    bx      lr
+        //
+        // At this point we can contiue
+        // (gdb) c
+        // Continuing.
+        // EXTI1 has now run to completion.
+        //
+        // What was the total excecution time for EXTI1?
+        // ** your answer here **
+        //
+        // What is the value of the resouce X?
+        // ** your answer here **
+        //
+        // Just by looking at the code, what would the worst case assignment of X be?
+        // I.e., the assingnment of `X' that gives the worst case execution time.
+        // ** your answer here **
+        //
+        // Measure that execution time. What did you get.
+        // ** your answer here **
+        //
+        // Your answer might blow your mind!!! How the heck is that even possible?
+        //
+        // At this point you should find that the worst case time stays the same ...
+        //
+        // Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
+        // What it does is that it figures out that we actually increase `Y`, by the value of `X`.
+        // So the loop is all gone, optimized out, and replaced by a simple addition.
+        //
+        // Now lets look at best case execution time.
+        // Figure out an assignment of `X`, that might actually reduce the execution time.
+        // ** your answer here **
+        //
+        // Redo the experiment with this value. How many clock cycles did you get?
+        // ** your answer here **
+        //
+        // Assignment 3.
+        // In assignment 2 we analysed EXTI1
+        // We found that for the examples, Rust RTFM was able to generate extremely efficient
+        // implementations, replacing branching with contdiditonal assignments and
+        // even remove comlete loops.
+        //
+        // Now lets have a look at using optimized LLVM and how it affects the number of tests.
+        // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // and now start a docker for the optimized build
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // and in the docker run
+        // > klee resource*.bc
+        //
+        // Look at the generated tests.
+        // Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
+        // ** your answers (5) here **
+        //
+        // Were the optimized tests sufficient to cover the execution time behavior.
+        // ** your answer here **
+        //
+        // Can you come up with a case where --release mode based analysis would miss cricital cases.
+        // ** your answer here, --- actually a research question, we will discuss in class --- **
+        //
+        // On a side note.
+        // Rust in --release mode makes the job for KLEE much easier. Look the number of instuctions carried out.
+        // In dev/debug you had som 10 000 instuctions executed for generating the test cases.
+        // In --relesase you had 34!!!!!
+        //
+        // This vastly improves on the performance of analysis, allowing larger applications to be scrutenized.
+        // The code we looked at here was by intention simple (to facilitate inspection).
+        // However, the code is NOT trivial, under the hood it utilizes advanced language features, such as
+        // closures and intence use of abstractions, such as Traits/genecics etc. It indeed covers a large
+        // degree of the Rust, for which it demonstrates that our approach to based program analysis
+        // actually works.
+        //
+        // For the future we intend the framework to cover the reading and writing to peripherals, and the
+        // sequenced access to resources. In class we will further discuss current limitations, and
+        // oportunities to improvements.
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI1"]
+pub unsafe extern "C" fn _EXTI1() {
+    let f: fn(&mut rtfm::Threshold, EXTI1::Resources) = exti1;
+    f(
+        &mut if 1u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(1u8)
+        },
+        EXTI1::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI1() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI1();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI1 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (1u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 1u8);
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub Y: Y,
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                Y: Y { _0: PhantomData },
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI3::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI3::X {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_X }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI3::X {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _X }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI3"]
+pub unsafe extern "C" fn _EXTI3() {
+    let f: fn(&mut rtfm::Threshold, EXTI3::Resources) = exti3;
+    f(
+        &mut if 2u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(2u8)
+        },
+        EXTI3::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI3() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI3();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI3 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (2u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 2u8);
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI2::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI2::Y {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_Y }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI2::Y {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _Y }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI2"]
+pub unsafe extern "C" fn _EXTI2() {
+    let f: fn(&mut rtfm::Threshold, EXTI2::Resources) = exti2;
+    f(
+        &mut if 3u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(3u8)
+        },
+        EXTI2::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI2() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI2();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI2 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (3u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 3u8);
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub Y: Y,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                Y: Y { _0: PhantomData },
+            }
+        }
+    }
+}
+extern crate cortex_m;
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+pub fn wcet_start() {
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt();
+    stub_EXTI1();
+    stub_EXTI3();
+    stub_EXTI2();
+}
+#[allow(private_no_mangle_fns)]
+#[allow(unsafe_code)]
+fn main() {
+    wcet_start();
+    let idle: fn() -> ! = idle;
+    idle();
+}
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    X.claim(t, |x, t1| {
+        Y.claim_mut(t1, |y, _| {
+            if *x < 10 {
+                for _ in 0..*x {
+                    *y += 1;
+                }
+            }
+        });
+    });
+}
+#[allow(non_snake_case)]
+fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
+    r.Y.claim_mut(t, |y, _| {
+        if *y < 10 {
+            *y += 1;
+        } else {
+            *y -= 1;
+        }
+    });
+}
+#[allow(non_snake_case)]
+fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
+    r.X.claim_mut(t, |x, _| {
+        *x += 1;
+    });
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt()
+}
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals, _r: init::Resources) {}
+#[inline(never)]
+#[allow(dead_code)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+fn idle() -> ! {
+    loop {
+        rtfm::nop();
+    }
+}
diff --git a/expand_wcet.rs b/expand_wcet.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4744ee8ad29b1446bcf79beea505d175380ba46a
--- /dev/null
+++ b/expand_wcet.rs
@@ -0,0 +1,914 @@
+#![feature(prelude_import)]
+#![no_std]
+//! Example using shared resources
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+#![feature(asm)]
+#[prelude_import]
+use core::prelude::v1::*;
+#[macro_use]
+extern crate core as core;
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+//use klee::k_abort;
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+// this is the path to the device crate
+
+#[allow(non_camel_case_types)]
+#[allow(non_snake_case)]
+pub struct _initResources<'a> {
+    pub X: &'a mut u32,
+    pub Y: &'a mut u32,
+}
+#[allow(unsafe_code)]
+mod init {
+    pub struct Peripherals {
+        pub core: ::stm32f413::CorePeripherals,
+        pub device: ::stm32f413::Peripherals,
+    }
+    pub use _initResources as Resources;
+    #[allow(unsafe_code)]
+    impl<'a> Resources<'a> {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: &mut ::_X,
+                Y: &mut ::_Y,
+            }
+        }
+    }
+}
+static mut _Y: u32 = 0;
+static mut _X: u32 = 0;
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI2::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        // extern crate cortex_m;
+
+        // Static code analysis
+        // In this lab we will study how a Rust RTFM application can be
+        // statically analysed.
+        //
+        // The application has three tasks EXTI1, EXTI2 and EXTI3,
+        // with associated priorites 1 (lowest), 3 (highest), and 2 (mid).
+        //
+        // Assignment 1.
+        // Build the application for KLEE analysis.
+        // > xargo build --example resource  --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // Start the KLEE docker
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/debug/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // Notice, in this case we have compiled in dev/debug mode, such to avoid optimzation
+        // of the generated LLVM IR code. Thus the docker should run in the `.../debug/..` folder.
+        //
+        // Now run KLEE in the docker.
+        // > klee resource-*.bc
+        // KLEE: WARNING: executable has module level assembly (ignoring)
+        // KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/cortex-m-rt-0.3.13/src/lang_items.rs:1: abort failure
+        // KLEE: NOTE: now ignoring this error at this location
+
+        // KLEE: done: total instructions = 11575
+        // KLEE: done: completed paths = 25
+        // KLEE: done: generated tests = 16
+        //
+        // When compiled with the --features klee_mode, resources are treated as symbolic.
+        // Investigate the output files (in `klee-last`). Use `ktest-tool` to examine the tests.
+        // The file `klee/tasks.txt` gives the order of tasks, it may vary for each run.
+        // ```
+        // // autogenerated file
+        // ["EXTI1", "EXTI2", "EXTI3"]
+        // ```
+        //
+        // How many tests were generated for task EXIT1?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT2?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // How many tests were generated for task EXIT3?
+        // ** your answer here **
+        // Why that many, (look at the code and the generted tests).
+        // ** your answer here **
+        //
+        // (There will be one additional "dymmy" test for testing "no task".)
+        //
+        // Now identify the cause of generated error.
+        // > more klee-last/*.abort.err
+        //
+        // Find the error on the source code and fix it.
+        // Hint, use *wrapping arithmetics*.
+        //
+        // Repeat the code generation, run KLEE agian and fix errors until
+        // no more errors are found.
+        //
+        // How many errors were identified?
+        // ** your answer here **
+        //
+        // For one of the arithmetic operations, no error was found.
+        // Explain why this is no error.
+        // ** your answer here **
+        //
+        // Why didn't KLEE report all the errors initially?
+        // Scroll back and compare the stack traces of the generated errors.
+        // Hint, for each line in the code KLEE will spot ONE error.
+        // ** your answer here **
+        //
+        // Assignment 2.
+        // KLEE has now generated tests covering EACH feasible path for EACH task.
+        // Now we will analyse the exection time for each such test.
+        //
+        // In order to do that comiple your application.
+        // > xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf
+        //
+        // We build in --release for optimizing the performance.
+        // The --features wcet_bkpt will insert a `bkpt` instruction on LOCK ond UNLOCK of
+        // of each resource. This allows you to monitor the number of clock cyckles using gdb.
+        //
+        // Connect your Nucleo64 board with the `stm32f401re` (or `stm32f411re`) MCU.
+        // Start openocd in a separate terminal (and let it run there).
+        //
+        // > openocd -f interface/stlink.cfg -f target/stm32f4x.cfg
+        // (You may use `-f inteface/stlink-v2-1.cfg`, if `stlink.cfg` is missing.)
+        //
+        // Start gdb.
+        // > arm-none-eabi-gdb -x gdbinit_manual target/thumbv7em-none-eabihf/release/examples/resource
+        //
+        // The `gdbinit_manual` has the following content.
+        // ```
+        // target remote :3333
+        // mon reset halt
+        // load
+        // tb main
+        // continue
+        //
+        // Line by line, it:
+        // - connects to the target (the MCU)
+        // - resets the MCU
+        // - loads the binary, in this case set to target/thumbv7em-none-eabihf/release/examples/resource
+        // - sets a temporary breakpoint to `main`, and
+        // - continues executing until `main` is reached.
+        //
+        // At the point the MCU hits `main` it stops.
+        // (You may be promted to continue working <return> or quit, in such case press <return>.)
+        //
+        // Now you can inspect where the processor halted.
+        // >  (gdb) list
+        // 560                 // be executed *before* enabling the FPU and that would generate an
+        // 561                 // exception
+        // 562                 #[inline(never)]
+        // 563                 fn main() {
+        // 564                     unsafe {
+        // 565                         ::main(0, ::core::ptr::null());
+        // 566                     }
+        // 567                 }
+        // 568
+        // 569                 main()
+        //
+        // As you see this is not part of your program, rather it originates from the library startup code.
+        //
+        // This is perfect, now the MCU is initiated and under your control.
+        //
+        // At this point the memory (resources), holds their initial values from the
+        // your application (this was set by the library code prior to hitting main).
+        // You can inspect the global reasources (they are prepended by `_`).
+        //
+        // (gdb) p resource::_X
+        // $1 = 0
+        // (gdb) p resource::_Y
+        // $2 = 0
+        //
+        // Before calling our tasks we need to enable the debug timer (cycle counter in the DWT unit of the MCU).
+        //
+        // (gdb) mon mww 0xe0001000 1
+        //
+        // and set the counter value to 0
+        //
+        // (gdb) mon mww 0xe0001004 0
+        //
+        // Now we can call the task(s). Lets start easy with EXTI3.
+        // (gdb) call stub_EXTI3()
+        // (gdb) mon mrw 0xe0001004
+        // 9
+        //
+        // Wow, it took only 9 clock cycles to run the complete task!!!!
+        // (Compare to a threaded OS that would require several 100 clock cycles to start a thread/task)
+        //
+        // But hey, where did my claim go? Wasn't I supposed to hit a breakpoint when claiming the resource?
+        // (In this case the resource X)
+        // Well Rust RTFM is smart enough to know that you are already at sufficient threshold (priority)
+        // in order to grant you the resource dircectly. Let us look at the code.
+        //
+        // (gdb) disassemble stub_EXTI3
+        // Dump of assembler code for function stub_EXTI3:
+        //    0x08000268 <+0>:     movw    r0, #0
+        //    0x0800026c <+4>:     movt    r0, #8192       ; 0x2000
+        //    0x08000270 <+8>:     ldr     r1, [r0, #0]
+        //    0x08000272 <+10>:    adds    r1, #1
+        //    0x08000274 <+12>:    str     r1, [r0, #0]
+        //    0x08000276 <+14>:    bx      lr
+        // End of assembler dump.
+        //
+        // Here you go, cannot be simpler that this, it:
+        // - sets up the address to X in r0
+        // - reads the old value
+        // - adds 1 (wrapping arithmetics)
+        // - stores the new value in X, and
+        // - it returns
+        // (On Cortex M functions and inerrupt handlers are essentially treated the same way)
+        //
+        // So now you can check the value of X. See above...
+        // ** your answer here **
+        //
+        // Now let us turn to EXTI2.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI2()
+        // (gdb) mon mrw 0xe0001004
+        // 13
+        //
+        // Also in this case we see that the resource (`Y`) was granted without overhead
+        // The code took a few additional clock cycles (its contians a condition, right).
+        // Figure out which path was triggered by this test.
+        // ** your answer here **
+        //
+        // Now figure out how to test the other branch
+        // you can use
+        // (gdb) set resource::_Y=...
+        // to set a value in memory
+        //
+        // Make a call to the `stub_EXTI2()` with the set value of `_Y`.
+        // How many clock cycles did you get (rember to set the counter to 0 before calling)
+        // ** your answer here **
+        //
+        // Check the nwe value of `_Y`.
+        // ** your answer here **
+        //
+        // Hint, if done correctly, you should have the same number of cycles for both paths.
+        // Ok, so the cycle count was the same ;)
+        // How so, lets have a look at the generated assembly.
+        //
+        //  (gdb) disassemble stub_EXTI2
+        // Dump of assembler code for function stub_EXTI2:
+        //    0x080002aa <+0>:     movw    r0, #0
+        //    0x080002ae <+4>:     mov.w   r2, #4294967295 ; 0xffffffff
+        //    0x080002b2 <+8>:     movt    r0, #8192       ; 0x2000
+        //    0x080002b6 <+12>:    ldr     r1, [r0, #4]
+        //    0x080002b8 <+14>:    cmp     r1, #10
+        //    0x080002ba <+16>:    it      cc
+        //    0x080002bc <+18>:    movcc   r2, #1
+        //    0x080002be <+20>:    add     r1, r2
+        //    0x080002c0 <+22>:    str     r1, [r0, #4]
+        //    0x080002c2 <+24>:    bx      lr
+        // End of assembler dump.
+        //
+        // This one is a bit harder to understand.
+        // What it does essentially is:
+        // - read `Y` into r1,
+        // - store -1 in r2
+        // - conditionally overwrite the r2 by a 1 if `Y < 10`
+        // - add r2 to r1 (the value of `Y`),
+        // - update `Y`.
+        //
+        // So this is beautiful, the COSTLY branch is replaced by a CHEAP
+        // condtitonal assigmnet `movcc`.
+        // You can read more on this on
+        // http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0553a/BABEHFEF.html
+        //
+        // Ok, back to the program...
+        // Now recall the KLEE generated test cases.
+        // Spot the ones regarding EXTI2.
+        // What assignments would KLEE suggest to `Y` to test both paths.
+        // ** your answers here **
+        //
+        // So, your test assignments or the ones from KLEE, which ones is better?
+        // ** your answer here **
+
+        // (We will return to optimising test cases later... so put this on your mental stack :)
+        //
+        // Now lets have a look at the tricky one EXTI1.
+        // (gdb) mon mww 0xe0001004 0
+        // (gdb) call stub_EXTI1()
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // The program being debugged was signaled while in a function called from GDB.
+        // GDB remains in the frame where the signal was received.
+        // To change this behavior use "set unwindonsignal on".
+        // Evaluation of the expression containing the function
+        // (stub_EXTI1) will be abandoned.
+        // When the function is done executing, GDB will silently stop.
+        //
+        // So what is happening here is that it runs into the (first) brkp intstruction (LOCK `X`).
+        // You may ignore the verbose output at this point....
+        //
+        // Run
+        // (gdb) mon mrw 0xe0001004
+        // 15
+        //
+        // So all in all it took 15 cycles to get there, `claim X`.
+        // We can look at the code causing the `bkpt`
+        // (gdb) list
+        // 162                         }
+        // 163
+        // 164                         // wcet_bkpt mode
+        // 165                         // put breakpoint at raise ceiling, for tracing execution time
+        // 166                         if cfg!(feature = "wcet_bkpt") {
+        // 167                             bkpt();
+        // 168                         }
+        //
+        // That makes sense, we are in the RTFM library handling the `claim X`
+        // (gdb) c
+        // Continuing.
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:167
+        // 167                             bkpt();
+        // (gdb) mon mrw 0xe0001004
+        // 19
+        //
+        // So after 19 clock cycles we claim `Y`
+        //
+        // Now lets have a look at the generated assembly.
+        // (gdb) disassemble
+        // ...
+        //    0x080002f6 <+4>:     bcs.n   0x8000334 <resource::<impl rtfm_core::Resource for resource::EXTI1::X>::claim+66>
+        //    0x080002f8 <+6>:     movs    r1, #224        ; 0xe0
+        //    0x080002fa <+8>:     movs    r2, #208        ; 0xd0
+        //    0x080002fc <+10>:    mrs     r12, BASEPRI
+        //    0x08000300 <+14>:    msr     BASEPRI, r1
+        //    0x08000304 <+18>:    bkpt    0x0000
+        //    0x08000306 <+20>:    mrs     r1, BASEPRI
+        //    0x0800030a <+24>:    msr     BASEPRI, r2
+        //    0x0800030e <+28>:    movw    r2, #0
+        // => 0x08000312 <+32>:    bkpt    0x0000
+        //    0x08000314 <+34>:    movt    r2, #8192       ; 0x2000
+        //    0x08000318 <+38>:    ldr     r3, [r2, #0]
+        //    0x0800031a <+40>:    subs    r0, r3, #1
+        //    0x0800031c <+42>:    cmp     r0, #8
+        //    0x0800031e <+44>:    ittt    ls
+        //    0x08000320 <+46>:    ldrls   r0, [r2, #4]
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // We are now inside the critital sections of both X and Y and have access to both resources for the loop.
+        // (gdb) c
+        // Continuing.
+        //
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=3, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        //
+        // We are now releasing `Y`.
+        // (gdb) mon mrw 0xe0001004
+        // 29
+        //
+        // How long (in cycles) was the critical section on `Y`?
+        // ** your answer here **
+
+        // (gdb) disassemble
+        // ...
+        //    0x08000322 <+48>:    addls   r0, r3
+        //    0x08000324 <+50>:    strls   r0, [r2, #4]
+        // => 0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // ...
+        //
+        // Let us continue
+        // (gdb) c
+        // Continuing.
+
+        // Program received signal SIGTRAP, Trace/breakpoint trap.
+        // cortex_m_rtfm::claim (ceiling=2, _nvic_prio_bits=4, data=<optimized out>, t=<optimized out>, f=...)
+        //     at /home/pln/klee/cortex-m-rtfm/src/lib.rs:181
+        // 181                             bkpt();
+        //
+        // (gdb) mon mrw 0xe0001004
+        // 30
+        //
+        // How long (in cycles) was the critical section on `X`?
+        // ** your answer here **
+        //
+        // (gdb) disassemble
+        // ...
+        //    0x08000326 <+52>:    bkpt    0x0000
+        //    0x08000328 <+54>:    msr     BASEPRI, r1
+        // => 0x0800032c <+58>:    bkpt    0x0000
+        //    0x0800032e <+60>:    msr     BASEPRI, r12
+        //    0x08000332 <+64>:    bx      lr
+        //
+        // At this point we can contiue
+        // (gdb) c
+        // Continuing.
+        // EXTI1 has now run to completion.
+        //
+        // What was the total excecution time for EXTI1?
+        // ** your answer here **
+        //
+        // What is the value of the resouce X?
+        // ** your answer here **
+        //
+        // Just by looking at the code, what would the worst case assignment of X be?
+        // I.e., the assingnment of `X' that gives the worst case execution time.
+        // ** your answer here **
+        //
+        // Measure that execution time. What did you get.
+        // ** your answer here **
+        //
+        // Your answer might blow your mind!!! How the heck is that even possible?
+        //
+        // At this point you should find that the worst case time stays the same ...
+        //
+        // Well, this one is not due to RTFM, its due to Rust and the cleverness of LLVM.
+        // What it does is that it figures out that we actually increase `Y`, by the value of `X`.
+        // So the loop is all gone, optimized out, and replaced by a simple addition.
+        //
+        // Now lets look at best case execution time.
+        // Figure out an assignment of `X`, that might actually reduce the execution time.
+        // ** your answer here **
+        //
+        // Redo the experiment with this value. How many clock cycles did you get?
+        // ** your answer here **
+        //
+        // Assignment 3.
+        // In assignment 2 we analysed EXTI1
+        // We found that for the examples, Rust RTFM was able to generate extremely efficient
+        // implementations, replacing branching with contdiditonal assignments and
+        // even remove comlete loops.
+        //
+        // Now lets have a look at using optimized LLVM and how it affects the number of tests.
+        // > xargo build --example resource --release --features klee_mode --target x86_64-unknown-linux-gnu
+        //
+        // and now start a docker for the optimized build
+        // > docker run --rm --user $(id -u):$(id -g) -v $PWD/target/x86_64-unknown-linux-gnu/release/examples:/mnt -w /mnt -it afoht/llvm-klee-4 /bin/bash
+        //
+        // and in the docker run
+        // > klee resource*.bc
+        //
+        // Look at the generated tests.
+        // Motivate for each of the 5 test cases, which one it matches of the hand generated tests from Assignment 2.
+        // ** your answers (5) here **
+        //
+        // Were the optimized tests sufficient to cover the execution time behavior.
+        // ** your answer here **
+        //
+        // Can you come up with a case where --release mode based analysis would miss cricital cases.
+        // ** your answer here, --- actually a research question, we will discuss in class --- **
+        //
+        // On a side note.
+        // Rust in --release mode makes the job for KLEE much easier. Look the number of instuctions carried out.
+        // In dev/debug you had som 10 000 instuctions executed for generating the test cases.
+        // In --relesase you had 34!!!!!
+        //
+        // This vastly improves on the performance of analysis, allowing larger applications to be scrutenized.
+        // The code we looked at here was by intention simple (to facilitate inspection).
+        // However, the code is NOT trivial, under the hood it utilizes advanced language features, such as
+        // closures and intence use of abstractions, such as Traits/genecics etc. It indeed covers a large
+        // degree of the Rust, for which it demonstrates that our approach to based program analysis
+        // actually works.
+        //
+        // For the future we intend the framework to cover the reading and writing to peripherals, and the
+        // sequenced access to resources. In class we will further discuss current limitations, and
+        // oportunities to improvements.
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI2::Y {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_Y }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI2::Y {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _Y }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI2"]
+pub unsafe extern "C" fn _EXTI2() {
+    let f: fn(&mut rtfm::Threshold, EXTI2::Resources) = exti2;
+    f(
+        &mut if 3u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(3u8)
+        },
+        EXTI2::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI2() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI2();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI2 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (3u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 3u8);
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub Y: Y,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                Y: Y { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI1::Y {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_Y }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 3u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 3u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _Y }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _Y, 3u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI1"]
+pub unsafe extern "C" fn _EXTI1() {
+    let f: fn(&mut rtfm::Threshold, EXTI1::Resources) = exti1;
+    f(
+        &mut if 1u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(1u8)
+        },
+        EXTI1::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI1() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI1();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI1 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (1u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 1u8);
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_camel_case_types)]
+    pub struct Y {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub X: X,
+        pub Y: Y,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: X { _0: PhantomData },
+                Y: Y { _0: PhantomData },
+            }
+        }
+    }
+}
+#[allow(unsafe_code)]
+unsafe impl rtfm::Resource for EXTI3::X {
+    type Data = u32;
+    fn borrow<'cs>(&'cs self, t: &'cs Threshold) -> &'cs Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &_X }
+    }
+    fn borrow_mut<'cs>(
+        &'cs mut self,
+        t: &'cs Threshold,
+    ) -> &'cs mut Self::Data {
+        if !(t.value() >= 2u8) {
+            {
+                ::panicking::panic(&(
+                    "assertion failed: t.value() >= 2u8",
+                    "examples/resource.rs",
+                    18u32,
+                    1u32,
+                ))
+            }
+        };
+        unsafe { &mut _X }
+    }
+    fn claim<R, F>(&self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&_X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+    fn claim_mut<R, F>(&mut self, t: &mut Threshold, f: F) -> R
+    where
+        F: FnOnce(&mut Self::Data, &mut Threshold) -> R,
+    {
+        unsafe { rtfm::claim(&mut _X, 2u8, stm32f413::NVIC_PRIO_BITS, t, f) }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::Deref for EXTI3::X {
+    type Target = u32;
+    fn deref(&self) -> &Self::Target {
+        unsafe { &_X }
+    }
+}
+#[allow(unsafe_code)]
+impl core::ops::DerefMut for EXTI3::X {
+    fn deref_mut(&mut self) -> &mut Self::Target {
+        unsafe { &mut _X }
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+#[export_name = "EXTI3"]
+pub unsafe extern "C" fn _EXTI3() {
+    let f: fn(&mut rtfm::Threshold, EXTI3::Resources) = exti3;
+    f(
+        &mut if 2u8 == 1 << stm32f413::NVIC_PRIO_BITS {
+            rtfm::Threshold::new(::core::u8::MAX)
+        } else {
+            rtfm::Threshold::new(2u8)
+        },
+        EXTI3::Resources::new(),
+    )
+}
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+#[allow(non_snake_case)]
+fn stub_EXTI3() {
+    #[allow(unsafe_code)]
+    unsafe {
+        _EXTI3();
+    }
+}
+#[allow(non_snake_case)]
+#[allow(unsafe_code)]
+mod EXTI3 {
+    use core::marker::PhantomData;
+    #[allow(dead_code)]
+    #[deny(const_err)]
+    const CHECK_PRIORITY: (u8, u8) =
+        (2u8 - 1, (1 << ::stm32f413::NVIC_PRIO_BITS) - 2u8);
+    #[allow(non_camel_case_types)]
+    pub struct X {
+        _0: PhantomData<*const ()>,
+    }
+    #[allow(non_snake_case)]
+    pub struct Resources {
+        pub X: X,
+    }
+    #[allow(unsafe_code)]
+    impl Resources {
+        pub unsafe fn new() -> Self {
+            Resources {
+                X: X { _0: PhantomData },
+            }
+        }
+    }
+}
+extern crate cortex_m;
+#[inline(never)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+pub fn wcet_start() {
+    bkpt_imm(1);
+    bkpt_imm(2);
+    stub_EXTI2();
+    stub_EXTI1();
+    stub_EXTI3();
+}
+#[allow(unused_variables)]
+#[inline]
+pub fn bkpt_imm(v: u8) {
+    match () {
+        #[cfg(target_arch = "arm")]
+        #[allow(unused_variables)]
+        () => unsafe {
+            asm!("bkpt $0":  : "r"(v) : "memory" : "volatile");
+        },
+    }
+}
+#[allow(private_no_mangle_fns)]
+#[allow(unsafe_code)]
+fn main() {
+    wcet_start();
+    let idle: fn() -> ! = idle;
+    idle();
+}
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    X.claim(t, |x, t1| {
+        Y.claim_mut(t1, |y, _| {
+            if *x < 10 {
+                for _ in 0..*x {
+                    *y += 1;
+                }
+            }
+        });
+    });
+}
+#[allow(non_snake_case)]
+fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) {
+    r.Y.claim_mut(t, |y, _| {
+        if *y < 10 {
+            *y += 1;
+        } else {
+            *y -= 1;
+        }
+    });
+}
+#[allow(non_snake_case)]
+fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) {
+    r.X.claim_mut(t, |x, _| {
+        *x += 1;
+    });
+    cortex_m::asm::bkpt();
+    cortex_m::asm::bkpt()
+}
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_p: init::Peripherals, _r: init::Resources) {}
+#[inline(never)]
+#[allow(dead_code)]
+#[allow(private_no_mangle_fns)]
+#[no_mangle]
+fn idle() -> ! {
+    loop {
+        rtfm::nop();
+    }
+}
diff --git a/expand_wcet_nop.rs b/expand_wcet_nop.rs
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/gdbinit_manual b/gdbinit_manual
index 339c2877f0fd15de7971b70fec8a969a9955f546..f8979165ac3f6e82580605cbda1ff5b6bf0697d9 100644
--- a/gdbinit_manual
+++ b/gdbinit_manual
@@ -1,5 +1,5 @@
 target remote :3333
 mon reset halt
 load
-tb idle
+
 continue
diff --git a/klee.py b/klee.py
index 4dbcc80f71250e6a2b6176f1c7cdaa8733104463..2e8d1db320927889793da3828e2c22556c05eb71 100644
--- a/klee.py
+++ b/klee.py
@@ -42,8 +42,16 @@ def gdb_cyccnt_write(num):
 def gdb_call(task):
     # call task
     print("#### call task %s" % task)
-    gdb.execute('call %s' % "stub_" + task + "()")
-    print("<<<<<<<<<<<<<<<<< after call >>>>>>>>>>>>>>>>>")
+    try:
+        gdb.execute('call %s' % "stub_" + task + "()")
+        print("<<<<<<<<<<<<<<<<< after call >>>>>>>>>>>>>>>>>")
+    except gdb.error:
+        print("!!!!!!!!!!!!!!!!! after call !!!!!!!!!!!!!!!!!")
+
+
+def gdb_bkpt_read():
+    # Read imm field of the current bkpt
+    return int(gdb.execute("x/i $pc", False, True).split("bkpt")[1].strip("\t").strip("\n"), 0)
 
 
 def gdb_setup():
@@ -64,32 +72,53 @@ def gdb_setup():
 def stop_event(evt):
     print("#### stop event %r" % evt)
 
-    try:
-        ceiling = int(gdb.parse_and_eval("ceiling").
-                      cast(gdb.lookup_type('u8')))
-        print("ceiling %r" % ceiling)
+    imm = gdb_bkpt_read()
+
+    print(" imm = {}".format(imm))
+
+    if imm == 1:
+        print("Enter")
         gdb_continue()
 
-    except gdb.error:
-        print("#### return")
-        gdb.post_event(next)
+    if imm == 2:
+        print("Exit")
+        gdb_continue()
+
+    if imm == 3:
+        print("Finished")
 
-        next()
+    # try:
+    #     ceiling = int(gdb.parse_and_eval("ceiling").
+    #                   cast(gdb.lookup_type('u8')))
+    #     print("ceiling %r" % ceiling)
+    #     gdb_continue()
 
+    # except:
+    #     print("#### return")
+    #     return
 
-def next():
-    global task_nr
-    global tasks
+    #     # gdb_continue()
+    #     # gdb.post_event(next)
+    #     # next()
 
-    task_nr = task_nr + 1
 
-    if task_nr == len(tasks):
-        print("------------ all done ---------")
-        return
-    print("-------------- start {}-------------".format(task_nr))
-    gdb_call(tasks[task_nr - 1])
-    print("-------------- finshed {}-------------".format(task_nr))
-    next()
+# def next():
+#     global task_nr
+#     global tasks
+
+#     if task_nr == len(tasks):
+#         print("------------ all done ---------")
+#         return
+
+#     task_nr = task_nr + 1
+#     print("-------------- start {}-------------".format(task_nr))
+
+#     try:
+#         gdb.execute('call %s' % "stub_" + task + "()")
+#         print("-------------- finshed {}-------------".format(task_nr))
+#     except:
+
+#     next()
 
 # def next_event(next):
 #     global task_nr
@@ -112,20 +141,13 @@ task_nr = 0
 print("simple python script started")
 gdb_setup()
 gdb.events.stop.connect(stop_event)
-next()
+
 # gdb.events.next.connect(next_event)
 # gdb.post_event(next)
 
 
-# for t_nr, t_index in enumerate(tasks):
-#     busy = True
-#     sad = False
-
-#     try:
-#         gdb_call(tasks[t_nr])
-#     except:
-#         print("############ call failed #############")
-#         while busy:
-#             gdb_continue()
-#             while sad:
-#                 pass
+for t_nr, t_index in enumerate(tasks):
+    try:
+        gdb_call(tasks[t_nr])
+    except:
+        print("--------------------fail")
diff --git a/klee1.py b/klee1.py
new file mode 100644
index 0000000000000000000000000000000000000000..b84fb9012e2e414dc5acb60547984050515da059
--- /dev/null
+++ b/klee1.py
@@ -0,0 +1,43 @@
+#!/usr/bin/env python
+import gdb
+import os
+import sys
+import struct
+from subprocess import call
+import subprocess
+import glob
+
+
+def posted_event_init():
+    print("--------------- Entering posted_event_init")
+
+
+# class MainBP(gdb.Breakpoint):
+
+#     def stop(self):
+#         print("zzzzzzzzzzzzzzz")
+#         print("Breakpoint location: %s" % self.location)
+#         gdb.execute('c')
+
+
+def stop_event(evt):
+        print("zzzzzzzzzzzzzzz")
+        print("Stop event: %s" % evt)
+        #gdb.execute('c')
+
+
+print("Python script started")
+gdb.execute("set confirm off")
+gdb.execute("set pagination off")
+gdb.execute("set verbose off")
+gdb.execute("set height 0")
+
+gdb.events.stop.connect(stop_event)
+gdb.execute('call stub_EXTI1()')
+
+
+# Hooking the prompt:
+def prompt(current):
+    # print("current %r" % current)
+    # print("#### prompt")
+    gdb.prompt_hook = current
\ No newline at end of file
diff --git a/klee_stm_gdb.1.py b/klee_stm_gdb.1.py
new file mode 100644
index 0000000000000000000000000000000000000000..8805c1d39830ced6601ae850eb672497126df1b2
--- /dev/null
+++ b/klee_stm_gdb.1.py
@@ -0,0 +1,609 @@
+#!/usr/bin/env python
+import gdb
+import os
+import sys
+import struct
+from subprocess import call
+import subprocess
+import glob
+
+""" ktest file version """
+version_no = 3
+
+debug = False
+autobuild = True
+
+debug_file = "resource"
+
+klee_out_folder = 'target/x86_64-unknown-linux-gnu/debug/examples/'
+stm_out_folder = 'target/thumbv7em-none-eabihf/release/examples/'
+
+file_list = []
+file_index_current = 0
+object_index_current = 0
+
+
+tasks = []
+task_to_test = 0
+
+task_name = ""
+
+# Name, Cyccnt, ceiling
+outputdata = []
+
+init_done = 0
+enable_output = 0
+
+""" Max number of events guard """
+object_index_max = 100
+
+""" Define the original working directory """
+original_pwd = os.getcwd()
+
+
+class KTestError(Exception):
+    pass
+
+
+class KTest:
+
+    @staticmethod
+    def fromfile(path):
+        if not os.path.exists(path):
+            print("ERROR: file %s not found" % (path))
+            sys.exit(1)
+
+        f = open(path, 'rb')
+        hdr = f.read(5)
+        if len(hdr) != 5 or (hdr != b'KTEST' and hdr != b"BOUT\n"):
+            raise KTestError('unrecognized file')
+        version, = struct.unpack('>i', f.read(4))
+        if version > version_no:
+            raise KTestError('unrecognized version')
+        numArgs, = struct.unpack('>i', f.read(4))
+        args = []
+        for i in range(numArgs):
+            size, = struct.unpack('>i', f.read(4))
+            args.append(str(f.read(size).decode(encoding='ascii')))
+
+        if version >= 2:
+            symArgvs, = struct.unpack('>i', f.read(4))
+            symArgvLen, = struct.unpack('>i', f.read(4))
+        else:
+            symArgvs = 0
+            symArgvLen = 0
+
+        numObjects, = struct.unpack('>i', f.read(4))
+        objects = []
+        for i in range(numObjects):
+            size, = struct.unpack('>i', f.read(4))
+            name = f.read(size)
+            size, = struct.unpack('>i', f.read(4))
+            bytes = f.read(size)
+            objects.append((name, bytes))
+
+        # Create an instance
+        b = KTest(version, args, symArgvs, symArgvLen, objects)
+        # Augment with extra filename field
+        b.filename = path
+        return b
+
+    def __init__(self, version, args, symArgvs, symArgvLen, objects):
+        self.version = version
+        self.symArgvs = symArgvs
+        self.symArgvLen = symArgvLen
+        self.args = args
+        self.objects = objects
+
+        # add a field that represents the name of the program used to
+        # generate this .ktest file:
+        program_full_path = self.args[0]
+        program_name = os.path.basename(program_full_path)
+        # sometimes program names end in .bc, so strip them
+        if program_name.endswith('.bc'):
+            program_name = program_name[:-3]
+        self.programName = program_name
+
+
+def do_continue():
+    gdb.execute("continue")
+
+
+class MainBP(gdb.Breakpoint):
+
+    def stop(self):
+        global init_done
+        global enable_output
+
+        print("Breakpoint location: %s" % self.location)
+        if self.location == "main":
+
+            if not init_done:
+                # gdb.prompt_hook = prompt
+                init_done = 1
+                gdb.post_event(posted_event_init)
+            else:
+                gdb.post_event(gather_data)
+
+        elif self.location == "idle":
+            print("Reached IDLE")
+            enable_output = 1
+            gdb_cyccnt_reset()
+            gdb.prompt_hook = prompt
+            return True
+
+        """ Needed to actually stop after the breakpoint
+            True: Return prompt
+            False: Continue?
+        """
+        return True
+        # return False
+
+
+# Subscribing to the stop events
+def stop_event(evt):
+    # print("#### stop event")
+    # print("evt %r" % evt)
+
+    global outputdata
+    global task_name
+    global file_index_current
+    global file_list
+    global enable_output
+
+    file_name = file_list[file_index_current].split('/')[-1]
+    """
+    Get the current ceiling level, cast it to an integer
+    """
+    try:
+        ceiling = int(gdb.parse_and_eval("ceiling").
+                      cast(gdb.lookup_type('u8')))
+    except gdb.error:
+
+        """
+        If there is no ceiling, it means we have returned to main
+        since every claim have ceiling
+        """
+        cyccnt = gdb_cyccnt_read()
+        if enable_output:
+            outputdata.append([file_name, task_name, cyccnt, 0, "Finish"])
+        gdb_cyccnt_reset()
+
+        if file_index_current < len(file_list) - 1:
+            gather_data()
+        else:
+            offset = 1
+            print("\nFinished all ktest files!\n")
+            print("Claims:")
+            for index, obj in enumerate(outputdata):
+                if obj[4] == "Exit":
+                    claim_time = (obj[2] -
+                                  outputdata[index - (offset)][2])
+                    print("%s Claim time: %s" % (obj, claim_time))
+                    offset += 2
+                elif obj[4] == "Finish" and not obj[2] == 0:
+                    offset = 1
+                    tot_time = obj[2]
+                    print("%s Total time: %s" % (obj, tot_time))
+                else:
+                    print("%s" % (obj))
+
+            gdb.execute("quit")
+
+        return
+
+    """
+    If outputdata is empty, we start
+    If the same ceiling as previously: exit
+    """
+    # print("outputdata: %s" % outputdata)
+    if enable_output:
+        if len(outputdata):
+            if outputdata[-1][3] >= ceiling:
+                action = "Exit"
+            else:
+                action = "Enter"
+        else:
+            action = "Enter"
+
+        cyccnt = gdb_cyccnt_read()
+        outputdata.append([file_name, task_name, cyccnt, ceiling, action])
+
+        print("CYCCNT:  %s\nCeiling: %s" % (cyccnt, outputdata[-1][3]))
+    do_continue()
+
+
+# Hooking the prompt:
+def prompt(current):
+    # print("current %r" % current)
+    # print("#### prompt")
+    gdb.prompt_hook = current
+
+
+# Posting events (which seem to work well when height=0)
+# def posted_event():
+    # print("#### posted event")
+    # gdb.execute("
+
+
+def posted_event_init():
+    """
+    Called at the very beginning of execution
+    when the breakpoint at main() is hit
+
+    Loads each defined task
+
+    """
+
+    """
+    Subscribe stop_event to Breakpoint notifications
+    """
+    gdb.events.stop.connect(stop_event)
+
+    # print("Entering posted_event_init")
+
+    global init_done
+    global tasks
+    global task_to_test
+    global task_name
+    global file_index_current
+    global file_list
+    global outputdata
+    global enable_output
+
+    """ Load the variable data """
+    ktest_setdata(file_index_current)
+
+    """
+    If the number of the task is greater than the available tasks just finish
+    """
+    if task_to_test > len(tasks):
+        print("Nothing to call...")
+        init_done = 0
+        file_index_current += 1
+        gdb.post_event(posted_event_init)
+        # gdb.post_event(gather_data)
+        return
+
+    """
+    Prepare the cycle counter
+    """
+    gdb_cyccnt_enable()
+    gdb_cyccnt_reset()
+
+    # print("Tasks: ", tasks)
+    # print("Name of task to test:", tasks[task_to_test])
+    if not task_to_test == -1:
+        file_name = file_list[file_index_current].split('/')[-1]
+        task_name = tasks[task_to_test]
+        if enable_output:
+            outputdata.append([file_name, task_name, 0, 0, "Start"])
+
+        gdb.write('Task to call: %s \n' % (
+                  tasks[task_to_test] + "()"))
+        # gdb.prompt_hook = prompt
+        gdb.execute('call %s' % "stub_" +
+                    tasks[task_to_test] + "()")
+        # print("Called stub")
+
+        task_to_test = -1
+        do_continue()
+    else:
+        print("Done else")
+
+
+def gather_data():
+
+    global outputdata
+    global file_index_current
+    global file_list
+    global init_done
+
+    if file_index_current < len(file_list):
+        init_done = 0
+        file_index_current += 1
+        # print("Current file: %s" % file_list[file_index_current])
+        gdb.post_event(posted_event_init)
+
+    else:
+        print("Finished everything")
+
+        print(outputdata)
+        gdb.execute("quit")
+
+
+def trimZeros(str):
+    for i in range(len(str))[::-1]:
+        if str[i] != '\x00':
+            return str[:i + 1]
+
+    return ''
+
+
+def ktest_setdata(file_index):
+    """
+    Substitute every variable found in ktest-file
+    """
+    global file_list
+    global task_to_test
+    global debug
+
+    b = KTest.fromfile(file_list[file_index])
+    if debug:
+        # print('ktest filename : %r' % filename)
+        gdb.write('ktest file: %r \n' % file_list[file_index])
+        # print('args       : %r' % b.args)
+        # print('num objects: %r' % len(b.objects))
+    for i, (name, data) in enumerate(b.objects):
+        str = trimZeros(data)
+
+        """ If Name is "task", skip it """
+        if name.decode('UTF-8') == "task":
+            if debug:
+                print('object %4d: name: %r' % (i, name))
+                print('object %4d: size: %r' % (i, len(data)))
+            # print(struct.unpack('i', str).repr())
+            # task_to_test = struct.unpack('i', str)[0]
+            # print("str: ", str)
+            # print("str: ", str[0])
+            task_to_test = struct.unpack('i', str)[0]
+            # task_to_test = int(str[0])
+            if debug:
+                print("Task to test:", task_to_test)
+        else:
+            if debug:
+                print('object %4d: name: %r' % (i, name))
+                print('object %4d: size: %r' % (i, len(data)))
+                print(str)
+            # if opts.writeInts and len(data) == 4:
+            obj_data = struct.unpack('i', str)[0]
+            if debug:
+                print('object %4d: data: %r' %
+                      (i, obj_data))
+            # gdb.execute('whatis %r' % name.decode('UTF-8'))
+            # gdb.execute('whatis %r' % obj_data)
+            gdb.execute('set variable %s = %r' %
+                        (example_name + "::" + name.decode('UTF-8'), obj_data))
+            # gdb.write('Variable %s is:' % name.decode('UTF-8'))
+            # gdb.execute('print %s' % name.decode('UTF-8'))
+            # else:
+            # print('object %4d: data: %r' % (i, str))
+    if debug:
+        print("Done with setdata")
+
+
+def ktest_iterate():
+    """ Get the list of folders in current directory, sort and then grab the
+        last one.
+    """
+    global debug
+    global autobuild
+
+    curdir = os.getcwd()
+    if debug:
+        print(curdir)
+
+    rustoutputfolder = curdir + "/" + klee_out_folder
+    try:
+        os.chdir(rustoutputfolder)
+    except IOError:
+        print(rustoutputfolder + "not found. Need to run\n")
+        print("xargo build --example " + example_name + " --features" +
+              "klee_mode --target x86_64-unknown-linux-gnu ")
+        print("\nand docker run --rm --user (id -u):(id -g)" +
+              "-v $PWD" + "/" + klee_out_folder + ":/mnt" +
+              "-w /mnt -it afoht/llvm-klee-4 /bin/bash ")
+        if autobuild:
+            xargo_run("klee")
+            klee_run()
+        else:
+            print("Run the above commands before proceeding")
+            sys.exit(1)
+
+    if os.listdir(rustoutputfolder) == []:
+        """
+        The folder is empty, generate some files
+        """
+        xargo_run("klee")
+        klee_run()
+
+    dirlist = next(os.walk("."))[1]
+    dirlist.sort()
+    if debug:
+        print(dirlist)
+
+    if not dirlist:
+        print("No KLEE output, need to run KLEE")
+        print("Running klee...")
+        klee_run()
+
+    """ Ran KLEE, need to update the dirlist """
+    dirlist = next(os.walk("."))[1]
+    dirlist.sort()
+    try:
+        directory = dirlist[-1]
+    except IOError:
+        print("No KLEE output, need to run KLEE")
+        print("Running klee...")
+        klee_run()
+
+    print("Using ktest-files from directory:\n" + rustoutputfolder + directory)
+
+    """ Iterate over all files ending with ktest in the "klee-last" folder """
+    for filename in os.listdir(directory):
+        if filename.endswith(".ktest"):
+            file_list.append(os.path.join(rustoutputfolder + directory,
+                                          filename))
+        else:
+            continue
+
+    file_list.sort()
+    """ Return to the old path """
+    os.chdir(curdir)
+    return file_list
+
+
+def tasklist_get():
+    """ Parse the automatically generated tasklist
+    """
+
+    if debug:
+        print(os.getcwd())
+    with open('klee/tasks.txt') as fin:
+            for line in fin:
+                # print(line)
+                if not line == "// autogenerated file\n":
+                    return [x.strip().strip("[]\"") for x in line.split(',')]
+
+
+def xargo_run(mode):
+    """
+    Run xargo for building
+    """
+
+    if "klee" in mode:
+        xargo_cmd = ("xargo build --example " + example_name + " --features " +
+                     "klee_mode --target x86_64-unknown-linux-gnu ")
+    elif "stm" in mode:
+        xargo_cmd = ("xargo build --release --example " + example_name +
+                     " --features " +
+                     "wcet_bkpt --target thumbv7em-none-eabihf")
+    else:
+        print("Provide either 'klee' or 'stm' as mode")
+        sys.exit(1)
+
+    call(xargo_cmd, shell=True)
+
+
+def klee_run():
+    """
+    Stub for running KLEE on the LLVM IR
+    """
+    global debug
+    global original_pwd
+
+    PWD = original_pwd
+
+    user_id = subprocess.check_output(['id', '-u']).decode()
+    group_id = subprocess.check_output(['id', '-g']).decode()
+
+    bc_file = (glob.glob(PWD + "/" +
+               klee_out_folder +
+               '*.bc', recursive=False))[-1].split('/')[-1].strip('\'')
+    if debug:
+        print(PWD + "/" + klee_out_folder)
+        print(bc_file)
+
+    klee_cmd = ("docker run --rm --user " +
+                user_id[:-1] + ":" + group_id[:-1] +
+                " -v '"
+                + PWD + "/"
+                + klee_out_folder + "':'/mnt'" +
+                " -w /mnt -it afoht/llvm-klee-4 " +
+                "/bin/bash -c 'klee %s'" % bc_file)
+    if debug:
+        print(klee_cmd)
+    call(klee_cmd, shell=True)
+
+
+def gdb_cyccnt_enable():
+    # Enable cyccnt
+    gdb.execute("mon mww 0xe0001000 1")
+
+
+def gdb_cyccnt_disable():
+    # Disble cyccnt
+    gdb.execute("mon mww 0xe0001000 0")
+
+
+def gdb_cyccnt_reset():
+    # Reset cycle counter to 0
+    gdb.execute("mon mww 0xe0001004 0")
+
+
+def gdb_cyccnt_read():
+    # Read cycle counter
+    return int(gdb.execute("mon mdw 0xe0001004", False, True).strip(
+        '\n').strip('0xe000012004:').strip(',').strip(), 16)
+
+
+def gdb_cyccnt_write(num):
+    # Write to cycle counter
+    gdb.execute('mon mww 0xe0001004 %r' % num)
+
+
+"""Used for making GDB scriptable"""
+gdb.execute("set confirm off")
+gdb.execute("set pagination off")
+gdb.execute("set verbose off")
+gdb.execute("set height 0")
+
+"""
+Setup GDB for remote debugging
+"""
+gdb.execute("target remote :3333")
+gdb.execute("monitor arm semihosting enable")
+
+"""
+Check if the user passed a file to use as the source.
+
+If a file is given, use this as the example_name
+"""
+if gdb.progspaces()[0].filename:
+    """ A filename was given on the gdb command line """
+    example_name = gdb.progspaces()[0].filename.split('/')[-1]
+    print("The resource used for debugging: %s" % example_name)
+    try:
+        os.path.exists(gdb.progspaces()[0].filename)
+    except IOError:
+        """ Compiles the given example """
+        xargo_run("stm")
+        xargo_run("klee")
+else:
+    example_name = debug_file
+    print("Defaulting to example '%s' for debugging." % example_name)
+    try:
+        if example_name not in os.listdir(stm_out_folder):
+            """ Compiles the default example """
+            xargo_run("stm")
+            xargo_run("klee")
+    except IOError:
+        """ Compiles the default example """
+        xargo_run("stm")
+        xargo_run("klee")
+
+""" Tell GDB to load the file """
+gdb.execute("file %s" % (stm_out_folder + example_name))
+gdb.execute("load %s" % (stm_out_folder + example_name))
+
+# gdb.execute("step")
+
+""" Run KLEE on the generated files """
+# print(klee_run())
+
+""" Break at main to set variable values """
+# AddBreakpoint("main")
+MainBP("main")
+MainBP("init")
+
+
+""" Tell gdb-dashboard to hide """
+# gdb.execute("dashboard -enabled off")
+# gdb.execute("dashboard -output /dev/null")
+
+""" Also break at the idle-loop """
+MainBP("idle")
+# MainBP("terminate_execution")
+
+""" Save all ktest files into an array """
+file_list = ktest_iterate()
+# print(file_list)
+
+""" Get all the tasks to jump to """
+tasks = tasklist_get()
+print("Available tasks:")
+for t in tasks:
+    print(t)
+
+""" Run until the next breakpoint """
+gdb.execute("c")
diff --git a/macros/Cargo.toml b/macros/Cargo.toml
index d59431d13a9036844c314166494e576baffcded9..617f77ce036a771bb14018cca436873692616005 100644
--- a/macros/Cargo.toml
+++ b/macros/Cargo.toml
@@ -23,4 +23,5 @@ proc-macro = true
 
 [features]
 klee_mode = [] 
-wcet_bkpt = [] 
\ No newline at end of file
+wcet_bkpt = [] 
+wcet_nop = [] 
\ No newline at end of file
diff --git a/macros/src/trans.rs b/macros/src/trans.rs
index 47d58045d678f551cadbac049d9e78a8bf7e2d3e..585fbcf55e76476edeb48f4a493cf72dc1f2506e 100644
--- a/macros/src/trans.rs
+++ b/macros/src/trans.rs
@@ -414,7 +414,12 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
 
     if !cfg!(feature = "klee_mode") {
         // code generation for normal/wcet mode
-        if !cfg!(feature = "wcet_bkpt") {
+        if cfg!(feature = "wcet_bkpt") || cfg!(feature = "wcet_nop") {
+            // wcet_mode, call to wcet_start
+            main.push(quote! {
+                wcet_start();
+            });
+        } else {
             // normal mode
             main.push(quote! {
                 // type check
@@ -428,11 +433,6 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) {
                     #(#interrupts)*
                 });
             });
-        } else {
-            // wcet_mode, call to wcet_start
-            main.push(quote! {
-                wcet_start();
-            });
         }
     } else {
         // code generation for klee_mode
@@ -483,10 +483,14 @@ fn resources(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
 
         root.push(match *expr {
             Some(ref expr) => quote! {
+                #[allow(private_no_mangle_statics)]
+                #[no_mangle]
                 static mut #_name: #ty = #expr;
             },
             None => quote! {
                 // Resource initialized in `init`
+                #[allow(private_no_mangle_statics)]
+                #[no_mangle]
                 static mut #_name: #krate::UntaggedOption<#ty> =
                     #krate::UntaggedOption { none: () };
             },
@@ -511,6 +515,25 @@ fn resources(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
                 #(#names)*
             }
         });
+    } else {
+        if cfg!(feature = "wcet_nop") || cfg!(feature = "wcet_bkpt") {
+            // collect the identifiers for our resources
+
+            let mut names = vec![];
+            for name in ownerships.keys() {
+                let _name = Ident::new(format!("_{}", name.as_ref()));
+                names.push(quote!{
+                    let _ = k_read(&#_name);
+                });
+            }
+
+            // generate a function reading all resources
+            root.push(quote!{
+                pub unsafe fn read_resources() {
+                    #(#names)*
+                }
+            });
+        }
     }
 }
 
@@ -680,7 +703,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             }
         });
 
-        if cfg!(feature = "wcet_bkpt") {
+        if cfg!(feature = "wcet_bkpt") || cfg!(feature = "wcet_nop") {
             let _stub_tname = Ident::new(format!("stub_{}", tname));
             root.push(quote! {
                 #[inline(never)]
@@ -690,6 +713,7 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
                 fn #_stub_tname() {
                     #[allow(unsafe_code)]
                     unsafe { #_tname(); }
+                    unsafe { bkpt_3(); }
                 }
             });
         }
@@ -711,12 +735,13 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             }
         });
     }
-    if cfg!(feature = "wcet_bkpt") {
+    if cfg!(feature = "wcet_bkpt") || cfg!(feature = "wcet_nop") {
         let mut stubs = vec![];
         for (name, _task) in &app.tasks {
             let _name = Ident::new(format!("stub_{}", name.as_ref()));
             stubs.push(quote!{
-                #_name();
+                //#_name();
+                let _ = k_read(&#_name);
             });
         }
 
@@ -726,9 +751,10 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) {
             #[allow(private_no_mangle_fns)]
             #[no_mangle]
             pub fn wcet_start() {
+
                 #(#stubs)*
-                cortex_m::asm::bkpt();
             }
+
         });
     }
 }
diff --git a/objdump.txt b/objdump.txt
new file mode 100644
index 0000000000000000000000000000000000000000..a1a71624cc9f81aacbf37fd7a799889ca3c42a79
--- /dev/null
+++ b/objdump.txt
@@ -0,0 +1,484 @@
+
+target/thumbv7em-none-eabihf/release/examples/resource:     file format elf32-littlearm
+
+
+Disassembly of section .text:
+
+080001d8 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E>:
+ 80001d8:	f240 0010 	movw	r0, #16
+ 80001dc:	f240 0100 	movw	r1, #0
+ 80001e0:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80001e4:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001e8:	4281      	cmp	r1, r0
+ 80001ea:	d208      	bcs.n	80001fe <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x26>
+ 80001ec:	f240 0100 	movw	r1, #0
+ 80001f0:	2200      	movs	r2, #0
+ 80001f2:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001f6:	f841 2b04 	str.w	r2, [r1], #4
+ 80001fa:	4281      	cmp	r1, r0
+ 80001fc:	d3fb      	bcc.n	80001f6 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x1e>
+ 80001fe:	f240 0010 	movw	r0, #16
+ 8000202:	f240 0110 	movw	r1, #16
+ 8000206:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800020a:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800020e:	4281      	cmp	r1, r0
+ 8000210:	d20d      	bcs.n	800022e <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x56>
+ 8000212:	f240 6188 	movw	r1, #1672	; 0x688
+ 8000216:	f240 0210 	movw	r2, #16
+ 800021a:	f6c0 0100 	movt	r1, #2048	; 0x800
+ 800021e:	f2c2 0200 	movt	r2, #8192	; 0x2000
+ 8000222:	f851 3b04 	ldr.w	r3, [r1], #4
+ 8000226:	f842 3b04 	str.w	r3, [r2], #4
+ 800022a:	4282      	cmp	r2, r0
+ 800022c:	d3f9      	bcc.n	8000222 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x4a>
+ 800022e:	b580      	push	{r7, lr}
+ 8000230:	466f      	mov	r7, sp
+ 8000232:	f64e 5088 	movw	r0, #60808	; 0xed88
+ 8000236:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 800023a:	6801      	ldr	r1, [r0, #0]
+ 800023c:	f441 0170 	orr.w	r1, r1, #15728640	; 0xf00000
+ 8000240:	6001      	str	r1, [r0, #0]
+ 8000242:	f000 f804 	bl	800024e <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>
+ 8000246:	e8bd 4080 	ldmia.w	sp!, {r7, lr}
+ 800024a:	bf30      	wfi
+ 800024c:	e7fd      	b.n	800024a <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x72>
+
+0800024e <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>:
+ 800024e:	b580      	push	{r7, lr}
+ 8000250:	466f      	mov	r7, sp
+ 8000252:	f240 10d8 	movw	r0, #472	; 0x1d8
+ 8000256:	f6c0 0000 	movt	r0, #2048	; 0x800
+ 800025a:	7800      	ldrb	r0, [r0, #0]
+ 800025c:	f000 f835 	bl	80002ca <_ZN8resource4main17hc01c798b126b22ebE.llvm.477FACE7>
+ 8000260:	defe      	udf	#254	; 0xfe
+
+08000262 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>:
+ 8000262:	be00      	bkpt	0x0000
+ 8000264:	e7fe      	b.n	8000264 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E+0x2>
+
+08000266 <BUS_FAULT>:
+ 8000266:	f3ef 8008 	mrs	r0, MSP
+ 800026a:	f7ff bffa 	b.w	8000262 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>
+ 800026e:	defe      	udf	#254	; 0xfe
+
+08000270 <_ZN8resource4init17hc0d2161d64f65159E>:
+ 8000270:	4770      	bx	lr
+
+08000272 <EXTI3>:
+ 8000272:	4770      	bx	lr
+
+08000274 <EXTI1>:
+ 8000274:	21e0      	movs	r1, #224	; 0xe0
+ 8000276:	22d0      	movs	r2, #208	; 0xd0
+ 8000278:	f3ef 8c11 	mrs	ip, BASEPRI
+ 800027c:	f381 8811 	msr	BASEPRI, r1
+ 8000280:	be00      	bkpt	0x0000
+ 8000282:	f3ef 8111 	mrs	r1, BASEPRI
+ 8000286:	f382 8811 	msr	BASEPRI, r2
+ 800028a:	f240 0204 	movw	r2, #4
+ 800028e:	be00      	bkpt	0x0000
+ 8000290:	f2c2 0200 	movt	r2, #8192	; 0x2000
+ 8000294:	6813      	ldr	r3, [r2, #0]
+ 8000296:	1e58      	subs	r0, r3, #1
+ 8000298:	2808      	cmp	r0, #8
+ 800029a:	bf9e      	ittt	ls
+ 800029c:	6850      	ldrls	r0, [r2, #4]
+ 800029e:	4418      	addls	r0, r3
+ 80002a0:	6050      	strls	r0, [r2, #4]
+ 80002a2:	be00      	bkpt	0x0000
+ 80002a4:	f381 8811 	msr	BASEPRI, r1
+ 80002a8:	be00      	bkpt	0x0000
+ 80002aa:	f38c 8811 	msr	BASEPRI, ip
+ 80002ae:	4770      	bx	lr
+
+080002b0 <EXTI2>:
+ 80002b0:	f240 0004 	movw	r0, #4
+ 80002b4:	f04f 32ff 	mov.w	r2, #4294967295	; 0xffffffff
+ 80002b8:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80002bc:	6841      	ldr	r1, [r0, #4]
+ 80002be:	290a      	cmp	r1, #10
+ 80002c0:	bf38      	it	cc
+ 80002c2:	2201      	movcc	r2, #1
+ 80002c4:	4411      	add	r1, r2
+ 80002c6:	6041      	str	r1, [r0, #4]
+ 80002c8:	4770      	bx	lr
+
+080002ca <_ZN8resource4main17hc01c798b126b22ebE.llvm.477FACE7>:
+ 80002ca:	b580      	push	{r7, lr}
+ 80002cc:	466f      	mov	r7, sp
+ 80002ce:	b082      	sub	sp, #8
+ 80002d0:	f240 2071 	movw	r0, #625	; 0x271
+ 80002d4:	4669      	mov	r1, sp
+ 80002d6:	f6c0 0000 	movt	r0, #2048	; 0x800
+ 80002da:	9000      	str	r0, [sp, #0]
+ 80002dc:	2000      	movs	r0, #0
+ 80002de:	f807 0c01 	strb.w	r0, [r7, #-1]
+ 80002e2:	1e78      	subs	r0, r7, #1
+ 80002e4:	f000 f801 	bl	80002ea <_ZN13cortex_m_rtfm6atomic17h640c0e6d1b68ca24E>
+ 80002e8:	defe      	udf	#254	; 0xfe
+
+080002ea <_ZN13cortex_m_rtfm6atomic17h640c0e6d1b68ca24E>:
+ 80002ea:	b5f0      	push	{r4, r5, r6, r7, lr}
+ 80002ec:	af03      	add	r7, sp, #12
+ 80002ee:	f84d bd04 	str.w	fp, [sp, #-4]!
+ 80002f2:	7800      	ldrb	r0, [r0, #0]
+ 80002f4:	f24e 1400 	movw	r4, #57600	; 0xe100
+ 80002f8:	f2ce 0400 	movt	r4, #57344	; 0xe000
+ 80002fc:	28ff      	cmp	r0, #255	; 0xff
+ 80002fe:	d04e      	beq.n	800039e <_ZN13cortex_m_rtfm6atomic17h640c0e6d1b68ca24E+0xb4>
+ 8000300:	f240 0000 	movw	r0, #0
+ 8000304:	b672      	cpsid	i
+ 8000306:	2501      	movs	r5, #1
+ 8000308:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800030c:	680a      	ldr	r2, [r1, #0]
+ 800030e:	f240 0104 	movw	r1, #4
+ 8000312:	7005      	strb	r5, [r0, #0]
+ 8000314:	f240 000c 	movw	r0, #12
+ 8000318:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800031c:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 8000320:	7005      	strb	r5, [r0, #0]
+ 8000322:	f240 0008 	movw	r0, #8
+ 8000326:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800032a:	4790      	blx	r2
+ 800032c:	2009      	movs	r0, #9
+ 800032e:	f000 f883 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000332:	f504 7640 	add.w	r6, r4, #768	; 0x300
+ 8000336:	b2c0      	uxtb	r0, r0
+ 8000338:	21e0      	movs	r1, #224	; 0xe0
+ 800033a:	5431      	strb	r1, [r6, r0]
+ 800033c:	2009      	movs	r0, #9
+ 800033e:	f000 f87b 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000342:	f000 011f 	and.w	r1, r0, #31
+ 8000346:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 800034a:	fa05 f101 	lsl.w	r1, r5, r1
+ 800034e:	08c0      	lsrs	r0, r0, #3
+ 8000350:	5021      	str	r1, [r4, r0]
+ 8000352:	2007      	movs	r0, #7
+ 8000354:	f000 f870 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000358:	b2c0      	uxtb	r0, r0
+ 800035a:	21f0      	movs	r1, #240	; 0xf0
+ 800035c:	5431      	strb	r1, [r6, r0]
+ 800035e:	2007      	movs	r0, #7
+ 8000360:	f000 f86a 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000364:	f000 011f 	and.w	r1, r0, #31
+ 8000368:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 800036c:	fa05 f101 	lsl.w	r1, r5, r1
+ 8000370:	08c0      	lsrs	r0, r0, #3
+ 8000372:	5021      	str	r1, [r4, r0]
+ 8000374:	2008      	movs	r0, #8
+ 8000376:	f000 f85f 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 800037a:	b2c0      	uxtb	r0, r0
+ 800037c:	21d0      	movs	r1, #208	; 0xd0
+ 800037e:	5431      	strb	r1, [r6, r0]
+ 8000380:	2008      	movs	r0, #8
+ 8000382:	f000 f859 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000386:	f000 011f 	and.w	r1, r0, #31
+ 800038a:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 800038e:	fa05 f101 	lsl.w	r1, r5, r1
+ 8000392:	08c0      	lsrs	r0, r0, #3
+ 8000394:	5021      	str	r1, [r4, r0]
+ 8000396:	b662      	cpsie	i
+ 8000398:	f85d bb04 	ldr.w	fp, [sp], #4
+ 800039c:	bdf0      	pop	{r4, r5, r6, r7, pc}
+ 800039e:	f240 0000 	movw	r0, #0
+ 80003a2:	2501      	movs	r5, #1
+ 80003a4:	680a      	ldr	r2, [r1, #0]
+ 80003a6:	f240 0104 	movw	r1, #4
+ 80003aa:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80003ae:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80003b2:	7005      	strb	r5, [r0, #0]
+ 80003b4:	f240 000c 	movw	r0, #12
+ 80003b8:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80003bc:	7005      	strb	r5, [r0, #0]
+ 80003be:	f240 0008 	movw	r0, #8
+ 80003c2:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80003c6:	4790      	blx	r2
+ 80003c8:	2009      	movs	r0, #9
+ 80003ca:	f000 f835 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 80003ce:	f504 7640 	add.w	r6, r4, #768	; 0x300
+ 80003d2:	b2c0      	uxtb	r0, r0
+ 80003d4:	21e0      	movs	r1, #224	; 0xe0
+ 80003d6:	5431      	strb	r1, [r6, r0]
+ 80003d8:	2009      	movs	r0, #9
+ 80003da:	f000 f82d 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 80003de:	f000 011f 	and.w	r1, r0, #31
+ 80003e2:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 80003e6:	fa05 f101 	lsl.w	r1, r5, r1
+ 80003ea:	08c0      	lsrs	r0, r0, #3
+ 80003ec:	5021      	str	r1, [r4, r0]
+ 80003ee:	2007      	movs	r0, #7
+ 80003f0:	f000 f822 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 80003f4:	b2c0      	uxtb	r0, r0
+ 80003f6:	21f0      	movs	r1, #240	; 0xf0
+ 80003f8:	5431      	strb	r1, [r6, r0]
+ 80003fa:	2007      	movs	r0, #7
+ 80003fc:	f000 f81c 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000400:	f000 011f 	and.w	r1, r0, #31
+ 8000404:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 8000408:	fa05 f101 	lsl.w	r1, r5, r1
+ 800040c:	08c0      	lsrs	r0, r0, #3
+ 800040e:	5021      	str	r1, [r4, r0]
+ 8000410:	2008      	movs	r0, #8
+ 8000412:	f000 f811 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000416:	b2c0      	uxtb	r0, r0
+ 8000418:	21d0      	movs	r1, #208	; 0xd0
+ 800041a:	5431      	strb	r1, [r6, r0]
+ 800041c:	2008      	movs	r0, #8
+ 800041e:	f000 f80b 	bl	8000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>
+ 8000422:	f000 011f 	and.w	r1, r0, #31
+ 8000426:	f000 00e0 	and.w	r0, r0, #224	; 0xe0
+ 800042a:	fa05 f101 	lsl.w	r1, r5, r1
+ 800042e:	08c0      	lsrs	r0, r0, #3
+ 8000430:	5021      	str	r1, [r4, r0]
+ 8000432:	f85d bb04 	ldr.w	fp, [sp], #4
+ 8000436:	bdf0      	pop	{r4, r5, r6, r7, pc}
+
+08000438 <_ZN66_$LT$stm32f413..interrupt..Interrupt$u20$as$u20$bare_metal..Nr$GT$2nr17hb1f95fa82962cc37E.llvm.509AB16>:
+ 8000438:	f000 007f 	and.w	r0, r0, #127	; 0x7f
+ 800043c:	3801      	subs	r0, #1
+ 800043e:	285e      	cmp	r0, #94	; 0x5e
+ 8000440:	bf84      	itt	hi
+ 8000442:	2000      	movhi	r0, #0
+ 8000444:	4770      	bxhi	lr
+ 8000446:	e8df f010 	tbh	[pc, r0, lsl #1]
+ 800044a:	005f      	.short	0x005f
+ 800044c:	00630061 	.word	0x00630061
+ 8000450:	00670065 	.word	0x00670065
+ 8000454:	006b0069 	.word	0x006b0069
+ 8000458:	006f006d 	.word	0x006f006d
+ 800045c:	00730071 	.word	0x00730071
+ 8000460:	00770075 	.word	0x00770075
+ 8000464:	007b0079 	.word	0x007b0079
+ 8000468:	007f007d 	.word	0x007f007d
+ 800046c:	00830081 	.word	0x00830081
+ 8000470:	00870085 	.word	0x00870085
+ 8000474:	008b0089 	.word	0x008b0089
+ 8000478:	008f008d 	.word	0x008f008d
+ 800047c:	00930091 	.word	0x00930091
+ 8000480:	00970095 	.word	0x00970095
+ 8000484:	009b0099 	.word	0x009b0099
+ 8000488:	009f009d 	.word	0x009f009d
+ 800048c:	00a300a1 	.word	0x00a300a1
+ 8000490:	00a700a5 	.word	0x00a700a5
+ 8000494:	00ab00a9 	.word	0x00ab00a9
+ 8000498:	00af00ad 	.word	0x00af00ad
+ 800049c:	00b300b1 	.word	0x00b300b1
+ 80004a0:	00b700b5 	.word	0x00b700b5
+ 80004a4:	00bb00b9 	.word	0x00bb00b9
+ 80004a8:	00bf00bd 	.word	0x00bf00bd
+ 80004ac:	00c300c1 	.word	0x00c300c1
+ 80004b0:	00c700c5 	.word	0x00c700c5
+ 80004b4:	00cb00c9 	.word	0x00cb00c9
+ 80004b8:	00cf00cd 	.word	0x00cf00cd
+ 80004bc:	00d300d1 	.word	0x00d300d1
+ 80004c0:	00d700d5 	.word	0x00d700d5
+ 80004c4:	00db00d9 	.word	0x00db00d9
+ 80004c8:	00df00dd 	.word	0x00df00dd
+ 80004cc:	00e300e1 	.word	0x00e300e1
+ 80004d0:	00e700e5 	.word	0x00e700e5
+ 80004d4:	00eb00e9 	.word	0x00eb00e9
+ 80004d8:	00ef00ed 	.word	0x00ef00ed
+ 80004dc:	00f300f1 	.word	0x00f300f1
+ 80004e0:	00f700f5 	.word	0x00f700f5
+ 80004e4:	00fb00f9 	.word	0x00fb00f9
+ 80004e8:	00ff00fd 	.word	0x00ff00fd
+ 80004ec:	01030101 	.word	0x01030101
+ 80004f0:	01070105 	.word	0x01070105
+ 80004f4:	010b0109 	.word	0x010b0109
+ 80004f8:	010f010d 	.word	0x010f010d
+ 80004fc:	01130111 	.word	0x01130111
+ 8000500:	01170115 	.word	0x01170115
+ 8000504:	011b0119 	.word	0x011b0119
+ 8000508:	2001      	movs	r0, #1
+ 800050a:	4770      	bx	lr
+ 800050c:	2002      	movs	r0, #2
+ 800050e:	4770      	bx	lr
+ 8000510:	2003      	movs	r0, #3
+ 8000512:	4770      	bx	lr
+ 8000514:	2004      	movs	r0, #4
+ 8000516:	4770      	bx	lr
+ 8000518:	2005      	movs	r0, #5
+ 800051a:	4770      	bx	lr
+ 800051c:	2006      	movs	r0, #6
+ 800051e:	4770      	bx	lr
+ 8000520:	2007      	movs	r0, #7
+ 8000522:	4770      	bx	lr
+ 8000524:	2008      	movs	r0, #8
+ 8000526:	4770      	bx	lr
+ 8000528:	2009      	movs	r0, #9
+ 800052a:	4770      	bx	lr
+ 800052c:	200a      	movs	r0, #10
+ 800052e:	4770      	bx	lr
+ 8000530:	200b      	movs	r0, #11
+ 8000532:	4770      	bx	lr
+ 8000534:	200c      	movs	r0, #12
+ 8000536:	4770      	bx	lr
+ 8000538:	200d      	movs	r0, #13
+ 800053a:	4770      	bx	lr
+ 800053c:	200e      	movs	r0, #14
+ 800053e:	4770      	bx	lr
+ 8000540:	200f      	movs	r0, #15
+ 8000542:	4770      	bx	lr
+ 8000544:	2010      	movs	r0, #16
+ 8000546:	4770      	bx	lr
+ 8000548:	2011      	movs	r0, #17
+ 800054a:	4770      	bx	lr
+ 800054c:	2012      	movs	r0, #18
+ 800054e:	4770      	bx	lr
+ 8000550:	2013      	movs	r0, #19
+ 8000552:	4770      	bx	lr
+ 8000554:	2014      	movs	r0, #20
+ 8000556:	4770      	bx	lr
+ 8000558:	2015      	movs	r0, #21
+ 800055a:	4770      	bx	lr
+ 800055c:	2016      	movs	r0, #22
+ 800055e:	4770      	bx	lr
+ 8000560:	2017      	movs	r0, #23
+ 8000562:	4770      	bx	lr
+ 8000564:	2018      	movs	r0, #24
+ 8000566:	4770      	bx	lr
+ 8000568:	2019      	movs	r0, #25
+ 800056a:	4770      	bx	lr
+ 800056c:	201a      	movs	r0, #26
+ 800056e:	4770      	bx	lr
+ 8000570:	201b      	movs	r0, #27
+ 8000572:	4770      	bx	lr
+ 8000574:	201c      	movs	r0, #28
+ 8000576:	4770      	bx	lr
+ 8000578:	201d      	movs	r0, #29
+ 800057a:	4770      	bx	lr
+ 800057c:	201e      	movs	r0, #30
+ 800057e:	4770      	bx	lr
+ 8000580:	201f      	movs	r0, #31
+ 8000582:	4770      	bx	lr
+ 8000584:	2020      	movs	r0, #32
+ 8000586:	4770      	bx	lr
+ 8000588:	2021      	movs	r0, #33	; 0x21
+ 800058a:	4770      	bx	lr
+ 800058c:	2022      	movs	r0, #34	; 0x22
+ 800058e:	4770      	bx	lr
+ 8000590:	2023      	movs	r0, #35	; 0x23
+ 8000592:	4770      	bx	lr
+ 8000594:	2024      	movs	r0, #36	; 0x24
+ 8000596:	4770      	bx	lr
+ 8000598:	2025      	movs	r0, #37	; 0x25
+ 800059a:	4770      	bx	lr
+ 800059c:	2026      	movs	r0, #38	; 0x26
+ 800059e:	4770      	bx	lr
+ 80005a0:	2027      	movs	r0, #39	; 0x27
+ 80005a2:	4770      	bx	lr
+ 80005a4:	2028      	movs	r0, #40	; 0x28
+ 80005a6:	4770      	bx	lr
+ 80005a8:	2029      	movs	r0, #41	; 0x29
+ 80005aa:	4770      	bx	lr
+ 80005ac:	202a      	movs	r0, #42	; 0x2a
+ 80005ae:	4770      	bx	lr
+ 80005b0:	202b      	movs	r0, #43	; 0x2b
+ 80005b2:	4770      	bx	lr
+ 80005b4:	202c      	movs	r0, #44	; 0x2c
+ 80005b6:	4770      	bx	lr
+ 80005b8:	202d      	movs	r0, #45	; 0x2d
+ 80005ba:	4770      	bx	lr
+ 80005bc:	202e      	movs	r0, #46	; 0x2e
+ 80005be:	4770      	bx	lr
+ 80005c0:	202f      	movs	r0, #47	; 0x2f
+ 80005c2:	4770      	bx	lr
+ 80005c4:	2030      	movs	r0, #48	; 0x30
+ 80005c6:	4770      	bx	lr
+ 80005c8:	2031      	movs	r0, #49	; 0x31
+ 80005ca:	4770      	bx	lr
+ 80005cc:	2032      	movs	r0, #50	; 0x32
+ 80005ce:	4770      	bx	lr
+ 80005d0:	2033      	movs	r0, #51	; 0x33
+ 80005d2:	4770      	bx	lr
+ 80005d4:	2034      	movs	r0, #52	; 0x34
+ 80005d6:	4770      	bx	lr
+ 80005d8:	2035      	movs	r0, #53	; 0x35
+ 80005da:	4770      	bx	lr
+ 80005dc:	2036      	movs	r0, #54	; 0x36
+ 80005de:	4770      	bx	lr
+ 80005e0:	2037      	movs	r0, #55	; 0x37
+ 80005e2:	4770      	bx	lr
+ 80005e4:	2038      	movs	r0, #56	; 0x38
+ 80005e6:	4770      	bx	lr
+ 80005e8:	2039      	movs	r0, #57	; 0x39
+ 80005ea:	4770      	bx	lr
+ 80005ec:	203a      	movs	r0, #58	; 0x3a
+ 80005ee:	4770      	bx	lr
+ 80005f0:	203b      	movs	r0, #59	; 0x3b
+ 80005f2:	4770      	bx	lr
+ 80005f4:	203c      	movs	r0, #60	; 0x3c
+ 80005f6:	4770      	bx	lr
+ 80005f8:	203d      	movs	r0, #61	; 0x3d
+ 80005fa:	4770      	bx	lr
+ 80005fc:	203e      	movs	r0, #62	; 0x3e
+ 80005fe:	4770      	bx	lr
+ 8000600:	203f      	movs	r0, #63	; 0x3f
+ 8000602:	4770      	bx	lr
+ 8000604:	2040      	movs	r0, #64	; 0x40
+ 8000606:	4770      	bx	lr
+ 8000608:	2041      	movs	r0, #65	; 0x41
+ 800060a:	4770      	bx	lr
+ 800060c:	2042      	movs	r0, #66	; 0x42
+ 800060e:	4770      	bx	lr
+ 8000610:	2043      	movs	r0, #67	; 0x43
+ 8000612:	4770      	bx	lr
+ 8000614:	2044      	movs	r0, #68	; 0x44
+ 8000616:	4770      	bx	lr
+ 8000618:	2045      	movs	r0, #69	; 0x45
+ 800061a:	4770      	bx	lr
+ 800061c:	2046      	movs	r0, #70	; 0x46
+ 800061e:	4770      	bx	lr
+ 8000620:	2047      	movs	r0, #71	; 0x47
+ 8000622:	4770      	bx	lr
+ 8000624:	2048      	movs	r0, #72	; 0x48
+ 8000626:	4770      	bx	lr
+ 8000628:	2049      	movs	r0, #73	; 0x49
+ 800062a:	4770      	bx	lr
+ 800062c:	204a      	movs	r0, #74	; 0x4a
+ 800062e:	4770      	bx	lr
+ 8000630:	204b      	movs	r0, #75	; 0x4b
+ 8000632:	4770      	bx	lr
+ 8000634:	204c      	movs	r0, #76	; 0x4c
+ 8000636:	4770      	bx	lr
+ 8000638:	204d      	movs	r0, #77	; 0x4d
+ 800063a:	4770      	bx	lr
+ 800063c:	204f      	movs	r0, #79	; 0x4f
+ 800063e:	4770      	bx	lr
+ 8000640:	2050      	movs	r0, #80	; 0x50
+ 8000642:	4770      	bx	lr
+ 8000644:	2051      	movs	r0, #81	; 0x51
+ 8000646:	4770      	bx	lr
+ 8000648:	2052      	movs	r0, #82	; 0x52
+ 800064a:	4770      	bx	lr
+ 800064c:	2053      	movs	r0, #83	; 0x53
+ 800064e:	4770      	bx	lr
+ 8000650:	2054      	movs	r0, #84	; 0x54
+ 8000652:	4770      	bx	lr
+ 8000654:	2055      	movs	r0, #85	; 0x55
+ 8000656:	4770      	bx	lr
+ 8000658:	2057      	movs	r0, #87	; 0x57
+ 800065a:	4770      	bx	lr
+ 800065c:	2058      	movs	r0, #88	; 0x58
+ 800065e:	4770      	bx	lr
+ 8000660:	2059      	movs	r0, #89	; 0x59
+ 8000662:	4770      	bx	lr
+ 8000664:	205c      	movs	r0, #92	; 0x5c
+ 8000666:	4770      	bx	lr
+ 8000668:	205f      	movs	r0, #95	; 0x5f
+ 800066a:	4770      	bx	lr
+ 800066c:	2060      	movs	r0, #96	; 0x60
+ 800066e:	4770      	bx	lr
+ 8000670:	2061      	movs	r0, #97	; 0x61
+ 8000672:	4770      	bx	lr
+ 8000674:	2062      	movs	r0, #98	; 0x62
+ 8000676:	4770      	bx	lr
+ 8000678:	2063      	movs	r0, #99	; 0x63
+ 800067a:	4770      	bx	lr
+ 800067c:	2064      	movs	r0, #100	; 0x64
+ 800067e:	4770      	bx	lr
+ 8000680:	2065      	movs	r0, #101	; 0x65
+ 8000682:	4770      	bx	lr
+
+08000684 <ADC>:
+ 8000684:	f7ff bdef 	b.w	8000266 <BUS_FAULT>
diff --git a/simple.obj b/simple.obj
new file mode 100644
index 0000000000000000000000000000000000000000..3fab8f521579c94bc610bdb14777d9785777ef42
--- /dev/null
+++ b/simple.obj
@@ -0,0 +1,92 @@
+
+target/thumbv7em-none-eabihf/release/examples/simple:     file format elf32-littlearm
+
+
+Disassembly of section .text:
+
+080001d8 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E>:
+ 80001d8:	f240 0000 	movw	r0, #0
+ 80001dc:	f240 0100 	movw	r1, #0
+ 80001e0:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80001e4:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001e8:	4281      	cmp	r1, r0
+ 80001ea:	d208      	bcs.n	80001fe <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x26>
+ 80001ec:	f240 0100 	movw	r1, #0
+ 80001f0:	2200      	movs	r2, #0
+ 80001f2:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001f6:	f841 2b04 	str.w	r2, [r1], #4
+ 80001fa:	4281      	cmp	r1, r0
+ 80001fc:	d3fb      	bcc.n	80001f6 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x1e>
+ 80001fe:	f240 000c 	movw	r0, #12
+ 8000202:	f240 0100 	movw	r1, #0
+ 8000206:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800020a:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800020e:	4281      	cmp	r1, r0
+ 8000210:	d20d      	bcs.n	800022e <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x56>
+ 8000212:	f240 21b4 	movw	r1, #692	; 0x2b4
+ 8000216:	f240 0200 	movw	r2, #0
+ 800021a:	f6c0 0100 	movt	r1, #2048	; 0x800
+ 800021e:	f2c2 0200 	movt	r2, #8192	; 0x2000
+ 8000222:	f851 3b04 	ldr.w	r3, [r1], #4
+ 8000226:	f842 3b04 	str.w	r3, [r2], #4
+ 800022a:	4282      	cmp	r2, r0
+ 800022c:	d3f9      	bcc.n	8000222 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x4a>
+ 800022e:	b580      	push	{r7, lr}
+ 8000230:	466f      	mov	r7, sp
+ 8000232:	f64e 5088 	movw	r0, #60808	; 0xed88
+ 8000236:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 800023a:	6801      	ldr	r1, [r0, #0]
+ 800023c:	f441 0170 	orr.w	r1, r1, #15728640	; 0xf00000
+ 8000240:	6001      	str	r1, [r0, #0]
+ 8000242:	f000 f81b 	bl	800027c <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>
+ 8000246:	e8bd 4080 	ldmia.w	sp!, {r7, lr}
+ 800024a:	bf30      	wfi
+ 800024c:	e7fd      	b.n	800024a <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x72>
+	...
+
+08000250 <ADC>:
+ 8000250:	f000 b80f 	b.w	8000272 <BUS_FAULT>
+
+08000254 <_ZN6simple5exti117h4e0103028550e03eE>:
+ 8000254:	f240 0000 	movw	r0, #0
+ 8000258:	2208      	movs	r2, #8
+ 800025a:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800025e:	6841      	ldr	r1, [r0, #4]
+ 8000260:	290a      	cmp	r1, #10
+ 8000262:	bf88      	it	hi
+ 8000264:	2205      	movhi	r2, #5
+ 8000266:	6082      	str	r2, [r0, #8]
+ 8000268:	4770      	bx	lr
+
+0800026a <EXTI1>:
+ 800026a:	f7ff bff3 	b.w	8000254 <_ZN6simple5exti117h4e0103028550e03eE>
+
+0800026e <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>:
+ 800026e:	be00      	bkpt	0x0000
+ 8000270:	e7fe      	b.n	8000270 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E+0x2>
+
+08000272 <BUS_FAULT>:
+ 8000272:	f3ef 8008 	mrs	r0, MSP
+ 8000276:	f7ff bffa 	b.w	800026e <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>
+ 800027a:	defe      	udf	#254	; 0xfe
+
+0800027c <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>:
+ 800027c:	f240 10d8 	movw	r0, #472	; 0x1d8
+ 8000280:	2101      	movs	r1, #1
+ 8000282:	f6c0 0000 	movt	r0, #2048	; 0x800
+ 8000286:	7800      	ldrb	r0, [r0, #0]
+ 8000288:	b672      	cpsid	i
+ 800028a:	f240 0000 	movw	r0, #0
+ 800028e:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 8000292:	7041      	strb	r1, [r0, #1]
+ 8000294:	7001      	strb	r1, [r0, #0]
+ 8000296:	f24e 4007 	movw	r0, #58375	; 0xe407
+ 800029a:	21f0      	movs	r1, #240	; 0xf0
+ 800029c:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 80002a0:	7001      	strb	r1, [r0, #0]
+ 80002a2:	f24e 1000 	movw	r0, #57600	; 0xe100
+ 80002a6:	2180      	movs	r1, #128	; 0x80
+ 80002a8:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 80002ac:	6001      	str	r1, [r0, #0]
+ 80002ae:	b662      	cpsie	i
+ 80002b0:	defe      	udf	#254	; 0xfe
diff --git a/simple2.obj b/simple2.obj
new file mode 100644
index 0000000000000000000000000000000000000000..44dcce827f55e96906fe52bc8d36870b8a22c3d2
--- /dev/null
+++ b/simple2.obj
@@ -0,0 +1,97 @@
+
+target/thumbv7em-none-eabihf/release/examples/simple2:     file format elf32-littlearm
+
+
+Disassembly of section .text:
+
+080001d8 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E>:
+ 80001d8:	f240 0000 	movw	r0, #0
+ 80001dc:	f240 0100 	movw	r1, #0
+ 80001e0:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80001e4:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001e8:	4281      	cmp	r1, r0
+ 80001ea:	d208      	bcs.n	80001fe <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x26>
+ 80001ec:	f240 0100 	movw	r1, #0
+ 80001f0:	2200      	movs	r2, #0
+ 80001f2:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001f6:	f841 2b04 	str.w	r2, [r1], #4
+ 80001fa:	4281      	cmp	r1, r0
+ 80001fc:	d3fb      	bcc.n	80001f6 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x1e>
+ 80001fe:	f240 000c 	movw	r0, #12
+ 8000202:	f240 0100 	movw	r1, #0
+ 8000206:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800020a:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800020e:	4281      	cmp	r1, r0
+ 8000210:	d20d      	bcs.n	800022e <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x56>
+ 8000212:	f240 21bc 	movw	r1, #700	; 0x2bc
+ 8000216:	f240 0200 	movw	r2, #0
+ 800021a:	f6c0 0100 	movt	r1, #2048	; 0x800
+ 800021e:	f2c2 0200 	movt	r2, #8192	; 0x2000
+ 8000222:	f851 3b04 	ldr.w	r3, [r1], #4
+ 8000226:	f842 3b04 	str.w	r3, [r2], #4
+ 800022a:	4282      	cmp	r2, r0
+ 800022c:	d3f9      	bcc.n	8000222 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x4a>
+ 800022e:	b580      	push	{r7, lr}
+ 8000230:	466f      	mov	r7, sp
+ 8000232:	f64e 5088 	movw	r0, #60808	; 0xed88
+ 8000236:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 800023a:	6801      	ldr	r1, [r0, #0]
+ 800023c:	f441 0170 	orr.w	r1, r1, #15728640	; 0xf00000
+ 8000240:	6001      	str	r1, [r0, #0]
+ 8000242:	f000 f820 	bl	8000286 <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>
+ 8000246:	e8bd 4080 	ldmia.w	sp!, {r7, lr}
+ 800024a:	bf30      	wfi
+ 800024c:	e7fd      	b.n	800024a <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x72>
+	...
+
+08000250 <ADC>:
+ 8000250:	f000 b814 	b.w	800027c <BUS_FAULT>
+
+08000254 <_ZN7simple25exti117h18211c8605f73318E>:
+ 8000254:	f240 0000 	movw	r0, #0
+ 8000258:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800025c:	6841      	ldr	r1, [r0, #4]
+ 800025e:	290a      	cmp	r1, #10
+ 8000260:	d902      	bls.n	8000268 <_ZN7simple25exti117h18211c8605f73318E+0x14>
+ 8000262:	2105      	movs	r1, #5
+ 8000264:	6081      	str	r1, [r0, #8]
+ 8000266:	4770      	bx	lr
+ 8000268:	2904      	cmp	r1, #4
+ 800026a:	bf88      	it	hi
+ 800026c:	4770      	bxhi	lr
+ 800026e:	2108      	movs	r1, #8
+ 8000270:	6081      	str	r1, [r0, #8]
+ 8000272:	4770      	bx	lr
+
+08000274 <EXTI1>:
+ 8000274:	f7ff bfee 	b.w	8000254 <_ZN7simple25exti117h18211c8605f73318E>
+
+08000278 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>:
+ 8000278:	be00      	bkpt	0x0000
+ 800027a:	e7fe      	b.n	800027a <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E+0x2>
+
+0800027c <BUS_FAULT>:
+ 800027c:	f3ef 8008 	mrs	r0, MSP
+ 8000280:	f7ff bffa 	b.w	8000278 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>
+ 8000284:	defe      	udf	#254	; 0xfe
+
+08000286 <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>:
+ 8000286:	f240 10d8 	movw	r0, #472	; 0x1d8
+ 800028a:	2101      	movs	r1, #1
+ 800028c:	f6c0 0000 	movt	r0, #2048	; 0x800
+ 8000290:	7800      	ldrb	r0, [r0, #0]
+ 8000292:	b672      	cpsid	i
+ 8000294:	f240 0000 	movw	r0, #0
+ 8000298:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800029c:	7041      	strb	r1, [r0, #1]
+ 800029e:	7001      	strb	r1, [r0, #0]
+ 80002a0:	f24e 4007 	movw	r0, #58375	; 0xe407
+ 80002a4:	21f0      	movs	r1, #240	; 0xf0
+ 80002a6:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 80002aa:	7001      	strb	r1, [r0, #0]
+ 80002ac:	f24e 1000 	movw	r0, #57600	; 0xe100
+ 80002b0:	2180      	movs	r1, #128	; 0x80
+ 80002b2:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 80002b6:	6001      	str	r1, [r0, #0]
+ 80002b8:	b662      	cpsie	i
+ 80002ba:	defe      	udf	#254	; 0xfe
diff --git a/simple4.obj b/simple4.obj
new file mode 100644
index 0000000000000000000000000000000000000000..3b5a0d633e8d29eb07d67ca909a8c19dcd19a101
--- /dev/null
+++ b/simple4.obj
@@ -0,0 +1,122 @@
+
+target/thumbv7em-none-eabihf/release/examples/simple4:     file format elf32-littlearm
+
+
+Disassembly of section .text:
+
+080001d8 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E>:
+ 80001d8:	f240 0000 	movw	r0, #0
+ 80001dc:	f240 0100 	movw	r1, #0
+ 80001e0:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80001e4:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001e8:	4281      	cmp	r1, r0
+ 80001ea:	d208      	bcs.n	80001fe <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x26>
+ 80001ec:	f240 0100 	movw	r1, #0
+ 80001f0:	2200      	movs	r2, #0
+ 80001f2:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 80001f6:	f841 2b04 	str.w	r2, [r1], #4
+ 80001fa:	4281      	cmp	r1, r0
+ 80001fc:	d3fb      	bcc.n	80001f6 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x1e>
+ 80001fe:	f240 000c 	movw	r0, #12
+ 8000202:	f240 0100 	movw	r1, #0
+ 8000206:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 800020a:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800020e:	4281      	cmp	r1, r0
+ 8000210:	d20d      	bcs.n	800022e <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x56>
+ 8000212:	f240 21f8 	movw	r1, #760	; 0x2f8
+ 8000216:	f240 0200 	movw	r2, #0
+ 800021a:	f6c0 0100 	movt	r1, #2048	; 0x800
+ 800021e:	f2c2 0200 	movt	r2, #8192	; 0x2000
+ 8000222:	f851 3b04 	ldr.w	r3, [r1], #4
+ 8000226:	f842 3b04 	str.w	r3, [r2], #4
+ 800022a:	4282      	cmp	r2, r0
+ 800022c:	d3f9      	bcc.n	8000222 <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x4a>
+ 800022e:	b580      	push	{r7, lr}
+ 8000230:	466f      	mov	r7, sp
+ 8000232:	f64e 5088 	movw	r0, #60808	; 0xed88
+ 8000236:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 800023a:	6801      	ldr	r1, [r0, #0]
+ 800023c:	f441 0170 	orr.w	r1, r1, #15728640	; 0xf00000
+ 8000240:	6001      	str	r1, [r0, #0]
+ 8000242:	f000 f838 	bl	80002b6 <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>
+ 8000246:	e8bd 4080 	ldmia.w	sp!, {r7, lr}
+ 800024a:	bf30      	wfi
+ 800024c:	e7fd      	b.n	800024a <_ZN11cortex_m_rt13reset_handler17hcc1e0cbd9ca427e4E+0x72>
+	...
+
+08000250 <ADC>:
+ 8000250:	f000 b82c 	b.w	80002ac <BUS_FAULT>
+
+08000254 <_ZN7simple45exti117hb874f931b42f1cbaE>:
+ 8000254:	b2c0      	uxtb	r0, r0
+ 8000256:	2802      	cmp	r0, #2
+ 8000258:	d212      	bcs.n	8000280 <_ZN7simple45exti117hb874f931b42f1cbaE+0x2c>
+ 800025a:	21e0      	movs	r1, #224	; 0xe0
+ 800025c:	f3ef 8011 	mrs	r0, BASEPRI
+ 8000260:	f381 8811 	msr	BASEPRI, r1
+ 8000264:	f240 0100 	movw	r1, #0
+ 8000268:	f2c2 0100 	movt	r1, #8192	; 0x2000
+ 800026c:	688a      	ldr	r2, [r1, #8]
+ 800026e:	1e53      	subs	r3, r2, #1
+ 8000270:	2b03      	cmp	r3, #3
+ 8000272:	bf9e      	ittt	ls
+ 8000274:	684b      	ldrls	r3, [r1, #4]
+ 8000276:	441a      	addls	r2, r3
+ 8000278:	604a      	strls	r2, [r1, #4]
+ 800027a:	f380 8811 	msr	BASEPRI, r0
+ 800027e:	4770      	bx	lr
+ 8000280:	f240 0000 	movw	r0, #0
+ 8000284:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 8000288:	6881      	ldr	r1, [r0, #8]
+ 800028a:	1e4a      	subs	r2, r1, #1
+ 800028c:	2a03      	cmp	r2, #3
+ 800028e:	bf9f      	itttt	ls
+ 8000290:	6842      	ldrls	r2, [r0, #4]
+ 8000292:	4411      	addls	r1, r2
+ 8000294:	6041      	strls	r1, [r0, #4]
+ 8000296:	4770      	bxls	lr
+ 8000298:	4770      	bx	lr
+
+0800029a <EXTI2>:
+ 800029a:	4770      	bx	lr
+
+0800029c <EXTI1>:
+ 800029c:	b580      	push	{r7, lr}
+ 800029e:	466f      	mov	r7, sp
+ 80002a0:	2001      	movs	r0, #1
+ 80002a2:	f7ff ffd7 	bl	8000254 <_ZN7simple45exti117hb874f931b42f1cbaE>
+ 80002a6:	bd80      	pop	{r7, pc}
+
+080002a8 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>:
+ 80002a8:	be00      	bkpt	0x0000
+ 80002aa:	e7fe      	b.n	80002aa <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E+0x2>
+
+080002ac <BUS_FAULT>:
+ 80002ac:	f3ef 8008 	mrs	r0, MSP
+ 80002b0:	f7ff bffa 	b.w	80002a8 <_ZN11cortex_m_rt15default_handler17he14cdabe3be9cb17E>
+ 80002b4:	defe      	udf	#254	; 0xfe
+
+080002b6 <_ZN11cortex_m_rt13reset_handler4main17h16e582aa055c56b3E>:
+ 80002b6:	f240 10d8 	movw	r0, #472	; 0x1d8
+ 80002ba:	2101      	movs	r1, #1
+ 80002bc:	f44f 7280 	mov.w	r2, #256	; 0x100
+ 80002c0:	f6c0 0000 	movt	r0, #2048	; 0x800
+ 80002c4:	7800      	ldrb	r0, [r0, #0]
+ 80002c6:	b672      	cpsid	i
+ 80002c8:	f240 0000 	movw	r0, #0
+ 80002cc:	f2c2 0000 	movt	r0, #8192	; 0x2000
+ 80002d0:	7041      	strb	r1, [r0, #1]
+ 80002d2:	7001      	strb	r1, [r0, #0]
+ 80002d4:	f24e 4007 	movw	r0, #58375	; 0xe407
+ 80002d8:	21e0      	movs	r1, #224	; 0xe0
+ 80002da:	f2ce 0000 	movt	r0, #57344	; 0xe000
+ 80002de:	7041      	strb	r1, [r0, #1]
+ 80002e0:	f24e 1100 	movw	r1, #57600	; 0xe100
+ 80002e4:	f2ce 0100 	movt	r1, #57344	; 0xe000
+ 80002e8:	600a      	str	r2, [r1, #0]
+ 80002ea:	22f0      	movs	r2, #240	; 0xf0
+ 80002ec:	7002      	strb	r2, [r0, #0]
+ 80002ee:	2080      	movs	r0, #128	; 0x80
+ 80002f0:	6008      	str	r0, [r1, #0]
+ 80002f2:	b662      	cpsie	i
+ 80002f4:	defe      	udf	#254	; 0xfe
diff --git a/src/lib.rs b/src/lib.rs
index a6bcdf94fc0fd99e7e2f93df84a19c4bcd589767..666df9ab42398f6f3f9759f4a9fc03bd2bd99303 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -80,6 +80,7 @@
 #![deny(missing_docs)]
 #![deny(warnings)]
 #![feature(proc_macro)]
+#![feature(asm)]
 #![no_std]
 
 extern crate cortex_m;
@@ -164,7 +165,7 @@ where
                     // wcet_bkpt mode
                     // put breakpoint at raise ceiling, for tracing execution time
                     if cfg!(feature = "wcet_bkpt") {
-                        bkpt();
+                        bkpt_1();
                     }
 
                     // wcet_nop mode
@@ -178,7 +179,7 @@ where
                     // wcet_bkpt mode
                     // put breakpoint at lower ceiling, for tracing execution time
                     if cfg!(feature = "wcet_bkpt") {
-                        bkpt();
+                        bkpt_2();
                     }
 
                     // wcet_nop mode
@@ -213,3 +214,36 @@ where
     let mut nvic: NVIC = unsafe { mem::transmute(()) };
     nvic.set_pending(interrupt);
 }
+
+/// breakpoints with immediate field set, used for wcet analysis
+#[inline]
+pub unsafe fn bkpt_1() {
+    match () {
+        #[cfg(target_arch = "arm")]
+        () => asm!("bkpt #0x01" ::: "memory" : "volatile"),
+        #[cfg(not(target_arch = "arm"))]
+        () => unimplemented!(),
+    }
+}
+
+/// breakpoints with immediate field set, used for wcet analysis
+#[inline]
+pub unsafe fn bkpt_2() {
+    match () {
+        #[cfg(target_arch = "arm")]
+        () => asm!("bkpt #0x02" ::: "memory" : "volatile"),
+        #[cfg(not(target_arch = "arm"))]
+        () => unimplemented!(),
+    }
+}
+
+/// breakpoints with immediate field set, used for wcet analysis
+#[inline]
+pub unsafe fn bkpt_3() {
+    match () {
+        #[cfg(target_arch = "arm")]
+        () => asm!("bkpt #0x03" ::: "memory" : "volatile"),
+        #[cfg(not(target_arch = "arm"))]
+        () => unimplemented!(),
+    }
+}