Skip to content
Snippets Groups Projects
Commit 16491601 authored by Nils Fitinghoff's avatar Nils Fitinghoff
Browse files

rustfmt

parent 799276ea
Branches
No related tags found
No related merge requests found
...@@ -142,7 +142,6 @@ fn main() { ...@@ -142,7 +142,6 @@ fn main() {
// } // }
// } // }
let mut is_visited = false; let mut is_visited = false;
match STATE { match STATE {
S8004 | S8005 | S8014 => { S8004 | S8005 | S8014 => {
......
...@@ -2,9 +2,8 @@ ...@@ -2,9 +2,8 @@
#![no_main] #![no_main]
#![no_std] #![no_std]
extern crate panic_abort;
extern crate klee; extern crate klee;
extern crate panic_abort;
use klee::{kassert, kassume, ksymbol}; use klee::{kassert, kassume, ksymbol};
#[derive(Debug, Copy, Clone)] #[derive(Debug, Copy, Clone)]
...@@ -40,6 +39,7 @@ fn main() { ...@@ -40,6 +39,7 @@ fn main() {
let mut STATE = S8001; let mut STATE = S8001;
let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; // STATE_HISTORY let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; // STATE_HISTORY
let mut CNTR: u32 = unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR let mut CNTR: u32 = unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
// TIMEOUT_CNTR_HISTORY // TIMEOUT_CNTR_HISTORY
let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() }; let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
...@@ -63,18 +63,11 @@ fn main() { ...@@ -63,18 +63,11 @@ fn main() {
match STATE_H[i - 1] { match STATE_H[i - 1] {
// (3) // (3)
C001 | C002 | C003 => { C001 | C002 | C003 => {
kassert!( kassert!((STATE == S8001) | (STATE == STATE_H[i - 1]));
(STATE == S8001)
| (STATE == STATE_H[i - 1])
);
} }
// (4) // (4)
S8005 => { S8005 => {
kassert!( kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
(STATE == S8001)
| (STATE == C003)
| (STATE == STATE_H[i - 1])
);
} }
_ => (), _ => (),
} }
...@@ -97,7 +90,11 @@ fn main() { ...@@ -97,7 +90,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 { *STATE = match STATE {
S8000 => match (data.a, data.b) { S8000 => match (data.a, data.b) {
(F, F) => S8001, (F, F) => S8001,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment