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

rustfmt

parent 296a8323
Branches
No related tags found
No related merge requests found
...@@ -2,8 +2,8 @@ ...@@ -2,8 +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)]
...@@ -33,14 +33,18 @@ const F: bool = false; ...@@ -33,14 +33,18 @@ const F: bool = false;
#[no_mangle] #[no_mangle]
fn main() { fn main() {
let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() }; let mut DATA: [Data; HORIZON] =
unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA"); 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; let mut STATE = S8001;
for i in 0..HORIZON { for i in 0..HORIZON {
...@@ -79,11 +83,18 @@ fn main() { ...@@ -79,11 +83,18 @@ fn main() {
C001 | C002 | C003 => { C001 | C002 | C003 => {
// (3) // (3)
// transitions from error // transitions from error
kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1])); kassert!(
(STATE_H[i] == S8001)
| (STATE == STATE_H[i - 1])
);
} }
S8005 => { S8005 => {
// (4) // (4)
kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1])); kassert!(
(STATE_H[i] == S8001)
| (STATE == C003)
| (STATE == STATE_H[i - 1])
);
} }
_ => (), _ => (),
} }
...@@ -111,7 +122,11 @@ fn main() { ...@@ -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 { *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