all proofs now works

examples/eq.rs

@@ -24,23 +24,22 @@ pub enum State {
 
 use State::*;
 
-const DISCREPENCY: u32 = 3;
+const DISCREPENCY: u32 = 2;
 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 + 3) as usize] = unsafe { core::mem::uninitialized() };
     ksymbol!(&mut DATA, "DATA");
 
-    let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
+    let mut STATE_HISTORY: [State; (DISCREPENCY + 3) as usize] =
         unsafe { core::mem::uninitialized() };
 
     let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
     let mut STATE = S8001;
 
-    for i in 0..(DISCREPENCY + 2) as usize {
+    for i in 0..(DISCREPENCY + 3) as usize {
         periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
 
         // invariants
@@ -54,59 +53,53 @@ fn main() {
         // !a | !b -> !S8000
         // ensures that if any input is false we cannot enter the Enable state
         // this can also be seen as a safty condition
-        // (can it be derived from the first condition, not really sure?
-        // perhaps from the set of passible STATEs as finite, bla, think about it...
-        // not entirely straightforward...
-        // if we come up with a proof of redundancy it can be removed
+        // (can it be derived from the first condition, but we keep is as
+        // an indication that the verification works as expected)
+        // Indeed the number of spanned paths remains the same 
+        // (with or without the below assertion, so its proven redundant by KLEE)
         if !DATA[i].a | !DATA[i].b {
             kassert!(!(STATE == S8000));
         }
 
         // S8001 -> !a & !b
-        // we can only stay or enter the Init state if either input are false
+        // we can only stay or enter the Init state unless either (or both) inputs are false
         if STATE == S8001 {
-            // kassert!(TIMEOUT_CNTR == DISCREPENCY);
             kassert!(!DATA[i].a | !DATA[i].b);
         }
 
-        // // !a & !b & !timeout-> S8001
-        // // ensures that we enter the Init state if both inputs are false
-        // // under the condition that a timout has not occured
-        // if !DATA[i].a & !DATA[i].b {
-        //     kassert!(STATE == S8001);
-        // }
-
-        // // DISCREPANCY related invariants
-        // match STATE {
-        //     // Error -> timeout
-        //     // error states implies TIMEOUT_CNTR to have expired
-        //     C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
-        //     // 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)
-        //     }
-        //     _ => {}
-        // }
-
-        // // transition invariants
-        // if i > 0 {
-        //     match STATE_HISTORY[i - 1] {
-        //         C001 | C002 | C003 | S8005 => {
-        //             //
-        //             // no (immediate) transition from error / recover to Enable state
-        //             kassert!(!(STATE == S8000));
-        //         }
-        //         _ => {
-        //             // liveness from Init and Wait states, Enable is ensured
-        //             if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
-        //                 kassert!(STATE == S8000);
-        //             }
-        //         }
-        //     }
-        // }
+        
+
+        // DISCREPANCY related invariants
+        match STATE {
+            // Error -> timeout
+            C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+        
+            // Waiting states -> !timeout
+            // Waiting states implies that TIMEOUT_CNTR has not yet expired
+            // and that the time remaining is not longer than the discrepency
+            S8004 | S8005 | S8014 => {
+                kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
+            }
+            _ => {}
+        }
+
+        // transition invariants
+        if i > 0 {
+            match STATE_HISTORY[i - 1] {
+                C001 | C002 | C003 | S8005 => {
+                    // no (immediate) transition from error / recover to Enable state
+                    kassert!(!(STATE == S8000));
+                }
+                _ => {
+                    // liveness from Init and Wait states, Enable is ensured
+                    if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
+                        kassert!(STATE == S8000);
+                    }
+                }
+            }
+        }
         STATE_HISTORY[i] = STATE;
+        unsafe { core::ptr::read_volatile(&STATE_HISTORY[i]) };
     }
 }