diff --git a/examples/resource.rs b/examples/resource.rs index 2b090ebbb9be365241348cb9d1756e2ec8bce215..f6c4e36be25785ab05d94eca614b110f2a13689d 100644 --- a/examples/resource.rs +++ b/examples/resource.rs @@ -10,7 +10,7 @@ extern crate stm32f103xx; #[macro_use] extern crate klee; -use klee::{k_abort, k_read}; +use klee::k_abort; // import the procedural macro use rtfm::{app, Resource, Threshold}; @@ -27,7 +27,7 @@ app! { tasks: { EXTI1: { path: exti1, - resources: [X], + resources: [X, Y], }, EXTI2: { @@ -37,22 +37,31 @@ app! { }, } -fn exti1(t: &mut Threshold, r: EXTI1::Resources) { - let mut y = 0; - r.X.claim(t, |x, _| { - if *x < 10 { - for _ in 0..*x { - y += 1; - k_visit!(); +#[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; + } } - } + }); }); - k_read(&y); } -fn exti2(_t: &mut Threshold, _r: EXTI2::Resources) {} +fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) { + r.Y.claim_mut(t, |y, _| { + if *y < 10 { + *y += 1; + } else { + *y -= 1; + } + }); +} #[inline(never)] +#[allow(dead_code)] fn init(_p: init::Peripherals, _r: init::Resources) {} // The idle loop. @@ -62,6 +71,7 @@ fn init(_p: init::Peripherals, _r: init::Resources) {} // endless loop. #[inline(never)] +#[allow(dead_code)] fn idle() -> ! { k_abort() } diff --git a/macros/src/trans.rs b/macros/src/trans.rs index 03ec0fe475bd2a0b6471e69db4e81dd9f48f4884..ffdafae5d90b3629075b7b52268324d53f0f4f29 100644 --- a/macros/src/trans.rs +++ b/macros/src/trans.rs @@ -435,8 +435,8 @@ fn init(app: &App, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) { // } // make each resource symbolic - // later we can theink of "type invariants" - k_symbol!(&mut _X, "X"); + // later we can think of "type invariants" + make_resources_symbolic(); // task set as symbolic // will generate a set of tests for each task