diff --git a/Cargo.toml b/Cargo.toml
index 48c9d8105f15a806e56e6269e8edcb7897495308..ef7258bd3da2cd7287ee77f8cccf5227827db558 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -36,6 +36,7 @@ incremental = false
[profile.release]
debug = true
panic = "abort"
+incremental = false
lto = true
[features]
diff --git a/examples/eq.rs b/examples/eq.rs
index fccca3bcbae62906eb89fecd930592f68d788ea9..b4e36a8689287e78da514e07b7d08858f99907a6 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -4,10 +4,33 @@
extern crate klee;
use klee::{kassert, kassume, ksymbol};
+#[derive(Debug, Copy, Clone)]
+pub struct Data {
+ a: bool,
+ b: bool,
+}
+
+#[derive(Debug, Copy, Clone, PartialEq)]
+pub enum State {
+ S8000,
+ S8001,
+ S8004,
+ S8014,
+ S8005,
+ C001,
+ C002,
+ C003,
+}
+
+use State::*;
+
+const DISCREPENCY: u32 = 3;
+const T: bool = true;
+const F: bool = false;
+
#[no_mangle]
fn main() {
- let mut DATA: [Data; (DISCREPENCY + 2) as usize] =
- unsafe { core::mem::uninitialized() };
+ let mut DATA: [Data; (DISCREPENCY + 2) as usize] = unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
@@ -41,7 +64,8 @@ fn main() {
// S8001 -> !a & !b
// we can only stay or enter the Init state if both inputs are false
if STATE == S8001 {
- kassert!(TIMEOUT_CNTR == DISCREPENCY && !DATA[i].a | !DATA[i].b);
+ kassert!(TIMEOUT_CNTR == DISCREPENCY);
+ kassert!(!DATA[i].a | !DATA[i].b);
}
// !a & !b & !timeout-> S8001
@@ -51,7 +75,7 @@ fn main() {
kassert!(STATE == S8001);
}
- // DISCREPANCY relatod invariants
+ // DISCREPANCY related invariants
match STATE {
// Error -> timeout
// error states implies TIMEOUT_CNTR to have expired
@@ -59,9 +83,7 @@ fn main() {
// Waiting states -> !timeout
// wait states implies that TIMEOUT_CNTR not yet expired
// and that the time remaining is not longer than the discrepency
- S8004 | S8005 | S8014 => {
- kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
- }
+ S8004 | S8005 | S8014 => kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY),
_ => {}
}
@@ -85,56 +107,21 @@ fn main() {
}
}
-#[derive(Debug, Copy, Clone)]
-pub struct Data {
- a: bool,
- b: bool,
-}
-
-#[derive(Debug, Copy, Clone, PartialEq)]
-pub enum State {
- S8000,
- S8001,
- S8004,
- S8014,
- S8005,
- C001,
- C002,
- C003,
-}
-
-use State::*;
-
-const DISCREPENCY: u32 = 3;
-const T: bool = true;
-const F: bool = false;
-
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
- // we start directly in the init state S80001
- // static mut STATE: State = State::S8001;
- // static mut TIMEOUT_CNTR: u32 = 0;
-
- let data = DATA;
+fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
*STATE = match STATE {
S8000 => match (data.a, data.b) {
- (F, F) => S8001,
- (F, T) | (T, F) => {
+ (F, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
- S8005
+ S8001
}
+ (F, T) | (T, F) => S8005,
(T, T) => S8000,
},
S8001 => match (data.a, data.b) {
(F, F) => S8001,
- (F, T) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8014
- }
- (T, F) => {
- *TIMEOUT_CNTR = DISCREPENCY;
- S8004
- }
+ (F, T) => S8014,
+ (T, F) => S8004,
(T, T) => S8000,
},
S8004 => {
@@ -142,7 +129,10 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
match *TIMEOUT_CNTR {
0 => C001,
_ => match (data.a, data.b) {
- (F, _) => S8001,
+ (F, _) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8001
+ }
(_, T) => S8000,
_ => S8004,
},
@@ -153,7 +143,10 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
match *TIMEOUT_CNTR {
0 => C002,
_ => match (data.a, data.b) {
- (_, F) => S8001,
+ (_, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8001
+ }
(T, _) => S8000,
_ => S8014,
},
@@ -164,17 +157,26 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
match *TIMEOUT_CNTR {
0 => C003,
_ => match (data.a, data.b) {
- (F, F) => S8001,
+ (F, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8001
+ }
_ => S8005,
},
}
}
C001 | C002 => match (data.a, data.b) {
- (F, F) => S8001,
+ (F, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8001
+ }
_ => *STATE,
},
C003 => match (data.a, data.b) {
- (F, F) => S8001,
+ (F, F) => {
+ *TIMEOUT_CNTR = DISCREPENCY;
+ S8001
+ }
_ => C003,
},
};