simple files

examples/simple.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+//#[macro_use]
+extern crate klee;
+//use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+    },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+    if *r.X > 10 {
+        *r.Y = 5;
+    } else {
+        *r.Y = 8;
+    }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple2.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+    },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+    if *r.X > 10 {
+        *r.Y = 5;
+    } else {
+        if *r.X < 5 {
+            *r.Y = 8;
+        }
+    }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple3.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+    },
+}
+
+#[inline(never)]
+fn exti1(_t: &mut Threshold, mut r: EXTI1::Resources) {
+    if *r.X < 5 {
+        let old = *r.Y;
+        for _ in 0..*r.X {
+            *r.Y += 1;
+        }
+        k_assert!(*r.Y == *r.X + old);
+    }
+}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple4.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 2,
+            resources: [X, Y],
+        },
+    },
+}
+
+#[inline(never)]
+#[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, _| {
+            let old = *y;
+            if *x < 5 {
+                for _ in 0..*x {
+                    *y += 1;
+                }
+                //assert!(*y == *x + old);
+            }
+        });
+    });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple5.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 2,
+            resources: [Y],
+        },
+    },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    Y.claim_mut(t, |y, _| {
+        if *X < 5 {
+            for _ in 0..*X {
+                *y += 1;
+            }
+        }
+    });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple6.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume, k_read};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 2,
+            resources: [X],
+        },
+    },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    X.claim(t, |x, _| {
+        if *x > 10 {
+            *Y = 5;
+        } else {
+            if *x < 5 {
+                *Y = 8;
+            }
+        }
+    });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?

examples/simple7.rs

+//! Minimal example with zero tasks
+//#![deny(unsafe_code)]
+// IMPORTANT always include this feature gate
+#![feature(proc_macro)]
+#![feature(used)]
+#![no_std]
+
+extern crate cortex_m_rtfm as rtfm;
+// IMPORTANT always do this rename
+extern crate stm32f413;
+
+#[macro_use]
+extern crate klee;
+use klee::{k_abort, k_assert, k_assume, k_read};
+
+// import the procedural macro
+use rtfm::{app, Resource, Threshold};
+
+app! {
+    // this is the path to the device crate
+    device: stm32f413,
+
+    resources: {
+        static X:u32 = 1;
+        static Y:u32 = 1;
+    },
+
+    tasks: {
+        EXTI1: {
+            path: exti1,
+            priority: 1,
+            resources: [X, Y],
+        },
+        EXTI2: {
+            path: exti2,
+            priority: 2,
+            resources: [X, Y],
+        },
+    },
+}
+
+#[inline(never)]
+#[allow(non_snake_case)]
+fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) {
+    X.claim(t, |x, t| {
+        Y.claim_mut(t, |y, _| {
+            if *x > 10 {
+                *y = 5;
+            } else {
+                if *x < 5 {
+                    *y = 8;
+                }
+            }
+        });
+    });
+}
+
+fn exti2(_: &mut Threshold, _: EXTI2::Resources) {}
+
+// The `init` function
+//
+// This function runs as an atomic section before any tasks
+// are allowed to start
+#[inline(never)]
+#[allow(dead_code)]
+fn init(_: init::Peripherals, _: init::Resources) {}
+
+// The idle loop.
+//
+// This runs after `init` and has a priority of 0. All tasks can preempt this
+// function. This function can never return so it must contain some sort of
+// endless loop.
+#[inline(never)]
+fn idle() -> ! {
+    loop {}
+}
+
+// Assignments
+//
+// Rust strives at being a safe language.
+// - Memory safety,
+//   - static checking where possible
+//   - run-time checking causing `panic!` on violation
+//
+// - No undefined behavior in "safe" Rust
+//   - panic! in case undef behavior (e.g., div 0)
+//
+// Compiling and analysing the code using KLEE
+//
+// What problem(s) did KLEE identify
+// ** your answer here **
+//
+// Now try to solve this by contracts
+// You should not change the code, just enable the contacts
+// The `_` should be filled with concrete values
+//
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
+// at the same time.
+//
+// If not, why is that not possible?