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

rustfmt: limit line width to fit the paper

parent 16491601
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
examples/concurrent.rs
+ 6
− 3
View file @ 1f3199bd
......@@ -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) };
......
examples/eq.rs
+ 22
− 7
View file @ 1f3199bd
......@@ -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])
);
}
_ => (),
}
......
examples/eq_dfs.rs
+ 20
− 7
View file @ 1f3199bd
......@@ -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;
}
}
......
examples/eq_paper.rs
+ 17
− 6
View file @ 1f3199bd
......@@ -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])
);
}
_ => (),
}
......
examples/model2.rs
+ 4
− 2
View file @ 1f3199bd
......@@ -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);
......
examples/model3.rs
+ 4
− 2
View file @ 1f3199bd
......@@ -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;
......
examples/model4.rs
+ 4
− 2
View file @ 1f3199bd
......@@ -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
......
rustfmt.toml
+ 1
− 0
View file @ 1f3199bd
tab_spaces = 2
fn_args_density = "Vertical"
max_width = 56
src/main.rs
+ 11
− 4
View file @ 1f3199bd
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment