diff --git a/cargo-klee/src/main.rs b/cargo-klee/src/main.rs index 09beb69011c9ea96b6d93156d8c59c2c32af252e..92a81c7bd7189062c5b9fc06b718c61b68d7f966 100644 --- a/cargo-klee/src/main.rs +++ b/cargo-klee/src/main.rs @@ -104,7 +104,7 @@ fn run() -> Result<i32, failure::Error> { let verbose = matches.is_present("verbose"); let is_release = matches.is_present("release"); let is_replay = matches.is_present("replay"); - let is_ktest = matches.is_present("ktest"); + let is_ktest = matches.is_present("klee"); let is_gdb = matches.is_present("gdb"); // let target_flag = matches.value_of("target"); // not currently supported diff --git a/klee-examples/examples/gpioa.rs b/klee-examples/examples/gpioa.rs index cf21409e755ec357983e5836402d9480c5433219..39a92766aab68a7c81b7c3101401ef9d1377c7b2 100644 --- a/klee-examples/examples/gpioa.rs +++ b/klee-examples/examples/gpioa.rs @@ -1,3 +1,5 @@ +//! $ cargo klee --example gpioa --features klee-device +//! #![no_std] #![no_main] @@ -6,18 +8,19 @@ extern crate klee; extern crate panic_abort; extern crate stm32f413; -use core::ptr; use cortex_m::peripheral::Peripherals; #[no_mangle] fn main() { + // accesss to core peripherals let peripherals = Peripherals::take().unwrap(); let syst = peripherals.SYST; + // access to device peripherals let p = stm32f413::Peripherals::take().unwrap(); let gpioa = p.GPIOA; - if gpioa.moder.read().bits() == 0 { - let p = Peripherals::take().unwrap(); + if gpioa.moder.read().bits() == 0 && syst.rvr.read() == 0 { + let _p = Peripherals::take().unwrap(); } } diff --git a/klee-examples/examples/systick.rs b/klee-examples/examples/systick.rs index 266651a44a1a7479b9407b9366733e52ae3d83e3..2c77034c3b2d5980765cef3623999b7f22ed3f5b 100644 --- a/klee-examples/examples/systick.rs +++ b/klee-examples/examples/systick.rs @@ -9,6 +9,7 @@ use cortex_m::peripheral::Peripherals; #[no_mangle] fn main() { + // access to core peripherals let peripherals = Peripherals::take().unwrap(); let syst = peripherals.SYST;