diff --git a/.vscode/launch.json b/.vscode/launch.json new file mode 100644 index 0000000000000000000000000000000000000000..3b89df7d90d24b28d84ea9e49436cf0f3d065d33 --- /dev/null +++ b/.vscode/launch.json @@ -0,0 +1,33 @@ +{ + // Use IntelliSense to learn about possible attributes. + // Hover to view descriptions of existing attributes. + // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 + "version": "0.2.0", + "configurations": [ + { + "type": "cortex-debug", + "request": "launch", + "servertype": "openocd", + "name": "resource 16Mhz", + "executable": "./target/thumbv7em-none-eabihf/release/examples/resource", + "configFiles": [ + "interface/stlink.cfg", + "target/stm32f4x.cfg" + ], + "swoConfig": { + "enabled": true, + "cpuFrequency": 16000000, + "swoFrequency": 2000000, // you may try 1000000 if not working + "source": "probe", + "decoders": [ + { + "type": "console", + "label": "Name", + "port": 0 + } + ] + }, + "cwd": "${workspaceRoot}" + }, + ] +} \ No newline at end of file diff --git a/.vscode/tasks.json b/.vscode/tasks.json index 615a4dfe06dc41d2b0760402acd315c984bad1f1..f0085b9e135804c08235bf8b55dd8e29a0a90736 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -3,6 +3,18 @@ // for the documentation about the tasks.json format "version": "2.0.0", "tasks": [ + { + "label": "xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf", + "type": "shell", + "command": "xargo build --example resource --release --features wcet_bkpt --target thumbv7em-none-eabihf", + "group": { + "kind": "build", + "isDefault": true + }, + "problemMatcher": [ + "$rustc" + ] + }, { "label": "xargo build --example resource --features klee_mode --target x86_64-unknown-linux-gnu", "type": "shell", diff --git a/Cargo.toml b/Cargo.toml index 3a4cc3b1e737ca9ee083593e79845c1a154af97c..d54df3789127edbb80a94f24523b8741c3cae847 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,9 +25,11 @@ untagged-option = "0.1.1" features = ["abort-on-panic"] version = "0.3.9" -[dev-dependencies.stm32f103xx] +[dev-dependencies.stm32f413] +git = "https://gitlab.henriktjader.com/pln/stm32f413.git" features = ["rt"] -version = "0.8.0" +version = "0.2.0" + [dev-dependencies.klee] path = "./klee" diff --git a/examples/resource.rs b/examples/resource.rs index 39c40f87807cbd57e57c89b89f7c6dc9fd2b69f6..3fced4cffa2d676b2460d00f17ad2fd3a52282e0 100644 --- a/examples/resource.rs +++ b/examples/resource.rs @@ -6,7 +6,7 @@ extern crate cortex_m_rtfm as rtfm; // IMPORTANT always do this rename -extern crate stm32f103xx; +extern crate stm32f413; #[macro_use] extern crate klee; @@ -17,7 +17,7 @@ use rtfm::{app, Resource, Threshold}; app! { // this is the path to the device crate - device: stm32f103xx, + device: stm32f413, resources: { static X:u32 = 0; @@ -27,13 +27,21 @@ app! { tasks: { EXTI1: { path: exti1, + priority: 1, resources: [X, Y], }, EXTI2: { path: exti2, + priority: 3, resources: [Y], }, + + EXTI3: { + path: exti3, + priority: 2, + resources: [X], + }, }, } @@ -60,6 +68,8 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) { }); } +fn exti3(_t: &mut Threshold, _r: EXTI3::Resources) {} + #[inline(never)] #[allow(dead_code)] fn init(_p: init::Peripherals, _r: init::Resources) {} diff --git a/klee/src/lib.rs b/klee/src/lib.rs index 0ae4873045128215bf8540911939c3750a972487..c770cbdc01543a43d2a35835c2b823f27533aa38 100644 --- a/klee/src/lib.rs +++ b/klee/src/lib.rs @@ -93,9 +93,9 @@ macro_rules! k_visit { } #[cfg(feature = "klee_mode")] -pub fn k_read<T>(p: &T) { +pub fn k_read<T>(_p: &T) { unsafe { core::ptr::read_volatile(p) }; } #[cfg(not(feature = "klee_mode"))] -pub fn k_read<T>(p: &T) {} +pub fn k_read<T>(_p: &T) {}