diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs index c3813692434f91fc73aebc4917b318d2502b315f..7797817d9f97869d47dec7c33295e73348ee5255 100644 --- a/examples/eq_paper.rs +++ b/examples/eq_paper.rs @@ -2,8 +2,8 @@ #![no_main] #![no_std] -extern crate panic_abort; extern crate klee; +extern crate panic_abort; use klee::{kassert, kassume, ksymbol}; #[derive(Debug, Copy, Clone)] @@ -33,14 +33,18 @@ const F: bool = false; #[no_mangle] fn main() { - let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() }; + let mut DATA: [Data; HORIZON] = + unsafe { core::mem::uninitialized() }; ksymbol!(&mut DATA, "DATA"); - let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; + let mut STATE_H: [State; HORIZON] = + unsafe { core::mem::uninitialized() }; - let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() }; + let mut CNTR_H: [u32; HORIZON] = + unsafe { core::mem::uninitialized() }; - let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() }; + let mut TIMEOUT_CNTR: u32 = + unsafe { core::mem::uninitialized() }; let mut STATE = S8001; for i in 0..HORIZON { @@ -79,11 +83,18 @@ fn main() { C001 | C002 | C003 => { // (3) // transitions from error - kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1])); + kassert!( + (STATE_H[i] == S8001) + | (STATE == STATE_H[i - 1]) + ); } S8005 => { - // (4) - kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1])); + // (4) + kassert!( + (STATE_H[i] == S8001) + | (STATE == C003) + | (STATE == STATE_H[i - 1]) + ); } _ => (), } @@ -111,7 +122,11 @@ fn main() { } } -fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) { +fn eq( + STATE: &mut State, + TIMEOUT_CNTR: &mut u32, + data: &Data, +) { *STATE = match STATE { S8000 => match (data.a, data.b) { (F, F) => S8001,