From 1f3199bdeb703c314273596088b13096ca75cd6a Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 16:31:00 +0100
Subject: [PATCH] rustfmt: limit line width to fit the paper
---
examples/concurrent.rs | 9 ++++++---
examples/eq.rs | 29 ++++++++++++++++++++++-------
examples/eq_dfs.rs | 27 ++++++++++++++++++++-------
examples/eq_paper.rs | 23 +++++++++++++++++------
examples/model2.rs | 6 ++++--
examples/model3.rs | 6 ++++--
examples/model4.rs | 6 ++++--
rustfmt.toml | 1 +
src/main.rs | 15 +++++++++++----
9 files changed, 89 insertions(+), 33 deletions(-)
diff --git a/examples/concurrent.rs b/examples/concurrent.rs
index 000bcab..81229d7 100644
--- a/examples/concurrent.rs
+++ b/examples/concurrent.rs
@@ -11,9 +11,12 @@ use volatile_register::{RO, RW, WO};
#[no_mangle]
fn main() {
- let rw: RW<u32> = unsafe { core::mem::uninitialized() };
- let ro: RO<u32> = unsafe { core::mem::uninitialized() };
- let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+ let rw: RW<u32> =
+ unsafe { core::mem::uninitialized() };
+ let ro: RO<u32> =
+ unsafe { core::mem::uninitialized() };
+ let wo: WO<u32> =
+ unsafe { core::mem::uninitialized() };
unsafe { wo.write(2) };
diff --git a/examples/eq.rs b/examples/eq.rs
index 59600a5..50f7e7c 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -31,18 +31,26 @@ 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 {
- periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+ periodic(
+ &mut STATE,
+ &mut TIMEOUT_CNTR,
+ &mut DATA[i],
+ );
STATE_H[i] = STATE;
CNTR_H[i] = TIMEOUT_CNTR;
@@ -76,10 +84,17 @@ fn main() {
match STATE_H[i - 1] {
C001 | C002 | C003 => {
// transitions from error
- kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE_H[i] == S8001)
+ | (STATE == STATE_H[i - 1])
+ );
}
S8005 => {
- kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE_H[i] == S8001)
+ | (STATE == C003)
+ | (STATE == STATE_H[i - 1])
+ );
}
_ => (),
}
diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
index 5c0c70c..5a372b8 100644
--- a/examples/eq_dfs.rs
+++ b/examples/eq_dfs.rs
@@ -35,14 +35,18 @@ const F: bool = false;
#[no_mangle]
fn main() {
- let mut DATA: [Data; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+ let mut DATA: [Data; HORIZON + 1] =
+ unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
- let mut STATE_H: [State; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+ let mut STATE_H: [State; HORIZON + 1] =
+ unsafe { core::mem::uninitialized() };
- let mut CNTR_H: [u32; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+ let mut CNTR_H: [u32; HORIZON + 1] =
+ unsafe { core::mem::uninitialized() };
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ let mut TIMEOUT_CNTR: u32 =
+ unsafe { core::mem::uninitialized() };
// initial state, Init
let mut i = 0;
let mut TIMEOUT_CNTR: u32 = DISCREPANCY;
@@ -86,10 +90,17 @@ fn main() {
match STATE_H[i - 1] {
C001 | C002 | C003 => {
// transitions from error
- kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE_H[i] == S8001)
+ | (STATE == STATE_H[i - 1])
+ );
}
S8005 => {
- kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE_H[i] == S8001)
+ | (STATE == C003)
+ | (STATE == STATE_H[i - 1])
+ );
}
_ => (),
}
@@ -146,7 +157,9 @@ fn main() {
match STATE {
S8004 | S8005 | S8014 => {
for j in 0..i {
- if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
+ 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 ad1ffd0..8449c50 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -33,15 +33,19 @@ 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 = S8001;
- let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; // STATE_HISTORY
- let mut CNTR: u32 = unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
+ 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() };
+ let mut CNTR_H: [u32; HORIZON] =
+ unsafe { core::mem::uninitialized() };
for i in 0..HORIZON {
eq(&mut STATE, &mut CNTR, &mut DATA[i]);
@@ -63,11 +67,18 @@ fn main() {
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])
+ );
}
_ => (),
}
diff --git a/examples/model2.rs b/examples/model2.rs
index b3842f0..1155ac3 100644
--- a/examples/model2.rs
+++ b/examples/model2.rs
@@ -50,8 +50,10 @@ impl RegB {
#[no_mangle]
fn main() {
- let reg_a: RegA = unsafe { core::mem::uninitialized() };
- let reg_b: RegB = unsafe { core::mem::uninitialized() };
+ let reg_a: RegA =
+ unsafe { core::mem::uninitialized() };
+ let reg_b: RegB =
+ unsafe { core::mem::uninitialized() };
unsafe {
reg_b.write(0);
diff --git a/examples/model3.rs b/examples/model3.rs
index ddea1f0..8ca3db0 100644
--- a/examples/model3.rs
+++ b/examples/model3.rs
@@ -38,8 +38,10 @@ impl RegC {
#[no_mangle]
fn main() {
- let reg_c: RegC = unsafe { core::mem::uninitialized() };
- let mut init: u32 = unsafe { core::mem::uninitialized() };
+ let reg_c: RegC =
+ unsafe { core::mem::uninitialized() };
+ let mut init: u32 =
+ unsafe { core::mem::uninitialized() };
klee::ksymbol!(&mut init, "init");
//klee::kassume(init < 0xFFFF_FFFC);
//init = 0xFFFF_FFFD;
diff --git a/examples/model4.rs b/examples/model4.rs
index e1de248..3053828 100644
--- a/examples/model4.rs
+++ b/examples/model4.rs
@@ -37,8 +37,10 @@ impl RegC {
#[no_mangle]
fn main() {
- let reg_c: RegC = unsafe { core::mem::uninitialized() };
- let mut init: u32 = unsafe { core::mem::uninitialized() };
+ let reg_c: RegC =
+ unsafe { core::mem::uninitialized() };
+ let mut init: u32 =
+ unsafe { core::mem::uninitialized() };
klee::ksymbol!(&mut init, "init");
unsafe {
reg_c.write(init); // to ensure that the initial value is symbolic
diff --git a/rustfmt.toml b/rustfmt.toml
index 1ddeb65..7d71938 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -1,2 +1,3 @@
tab_spaces = 2
fn_args_density = "Vertical"
+max_width = 56
diff --git a/src/main.rs b/src/main.rs
index 6f3432e..f86a220 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -5,13 +5,16 @@ use klee::{kassert, ksymbol};
#[no_mangle]
fn main() {
- let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
+ let mut DATA: [Data; (DISCREPENCY + 1) as usize] =
+ unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ let mut TIMEOUT_CNTR: u32 =
+ unsafe { core::mem::uninitialized() };
ksymbol!(&mut TIMEOUT_CNTR, "TIMEOUT_CNTR");
- let mut STATE_HISTORY: [State; (DISCREPENCY + 1) as usize] =
+ let mut STATE_HISTORY: [State;
+ (DISCREPENCY + 1) as usize] =
unsafe { core::mem::uninitialized() };
DATA[0] = Data { a: false, b: false };
@@ -19,7 +22,11 @@ fn main() {
let mut STATE = S8001;
for i in 0..(DISCREPENCY + 1) as usize {
- periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+ periodic(
+ &mut STATE,
+ &mut TIMEOUT_CNTR,
+ &mut DATA[i as usize],
+ );
// invariants
// S8000 -> a & b
--
GitLab