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