From 16491601722c959d6026649d581bab8ad360413f Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 16:22:03 +0100
Subject: [PATCH] rustfmt
---
examples/eq_dfs.rs | 3 +--
examples/eq_paper.rs | 25 +++++++++++--------------
2 files changed, 12 insertions(+), 16 deletions(-)
diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
index fcccef2..5c0c70c 100644
--- a/examples/eq_dfs.rs
+++ b/examples/eq_dfs.rs
@@ -142,11 +142,10 @@ fn main() {
// }
// }
-
let mut is_visited = false;
match STATE {
S8004 | S8005 | S8014 => {
- for j in 0..i {
+ for j in 0..i {
if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
is_visited = true;
}
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 9eeeb2a..ad1ffd0 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -2,9 +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)]
@@ -40,6 +39,7 @@ fn main() {
let mut STATE = S8001;
let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; // STATE_HISTORY
let mut CNTR: u32 = unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
+
// TIMEOUT_CNTR_HISTORY
let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
@@ -53,28 +53,21 @@ fn main() {
if !DATA[i].a | !DATA[i].b {
kassert!(!(STATE == S8000));
}
-
+
// (2) S8000 -> a & b
if STATE == S8000 {
kassert!(DATA[i].a & DATA[i].b);
}
-
+
if i > 0 {
match STATE_H[i - 1] {
// (3)
C001 | C002 | C003 => {
- kassert!(
- (STATE == S8001)
- | (STATE == STATE_H[i - 1])
- );
+ kassert!((STATE == S8001) | (STATE == STATE_H[i - 1]));
}
// (4)
S8005 => {
- kassert!(
- (STATE == S8001)
- | (STATE == C003)
- | (STATE == STATE_H[i - 1])
- );
+ kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
}
_ => (),
}
@@ -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 {
S8000 => match (data.a, data.b) {
(F, F) => S8001,
--
GitLab