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?