diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml index 52cc15cba7ced8c8cf956e217df2103a8fc11960..2668b3ccd9fd35ef5b23f7810abad914a82bcdfe 100644 --- a/klee-examples/Cargo.toml +++ b/klee-examples/Cargo.toml @@ -5,20 +5,20 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io [dependencies] klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"} -#panic-abort = "0.3.1" +panic-abort = "0.3.1" [dependencies.volatile-register] version = "0.3.0" -# [replace] -[patch.crates-io] -"volatile-register" = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" } - -# [dependencies.cortex-m] -# version = "0.6.0" +[dependencies.cortex-m] +version = "0.6.0" # #features = ["inline-asm", "klee-analysis"] +[patch.crates-io] +volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" } +cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" } + # [dependencies.stm32f413] # version = "0.3.0" # path = "../stm32f413" @@ -35,6 +35,10 @@ path = "src/foo.rs" name = "register" path = "src/register.rs" +[[bin]] +name = "peripheral" +path = "src/peripheral.rs" + [profile.dev] incremental = false # lto = true diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs new file mode 100644 index 0000000000000000000000000000000000000000..1912ea79fc85280835893f9db1721429f061f9da --- /dev/null +++ b/klee-examples/src/peripheral.rs @@ -0,0 +1,32 @@ +#![no_std] +#![no_main] + +#[macro_use] +extern crate klee; + +#[cfg(not(feature = "klee-analysis"))] +extern crate panic_abort; + +extern crate cortex_m; + +use core::ptr; +use cortex_m::peripheral::Peripherals; + +#[no_mangle] +fn main() { + let peripherals = Peripherals::take().unwrap(); + let mut dwt = peripherals.DWT; + dwt.enable_cycle_counter(); + unsafe { + dwt.ctrl.write(0); + } + if dwt.ctrl.read() == 0 { + if dwt.ctrl.read() == 0 { + klee::abort(); + }; + }; + + unsafe { + ptr::read_volatile(&dwt); + } +} diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs index df1d7d27cac50ab5aa565b9db901ec3242a874a5..5a771fa0a98425041ac1319e7c035ed68dfdbd0f 100644 --- a/klee-examples/src/register.rs +++ b/klee-examples/src/register.rs @@ -1,8 +1,8 @@ //! showcase volatile register //! -//! $ cargo klee --bin main2 -r -g +//! $ cargo klee --bin register -r -g //! ... -//! Reading symbols from main2.replay...done. +//! Reading symbols from register.replay...done. //! //! (gdb) set env KTEST_FILE=klee-last/test000001.ktest //! (gdb) run