Fix loop contracts transformation when loops in branching

model-checking · Oct 24, 2024 · bd12d9d · bd12d9d
1 parent 325c9e4
commit bd12d9d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 deletions.
diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs
@@ -114,7 +114,7 @@ impl TransformPass for LoopContractPass {
                     let mut loop_queue: VecDeque<BasicBlockIdx> = VecDeque::new();
                     queue.push_back(0);
 
-                    while let Some(bb_idx) = queue.pop_front().or(loop_queue.pop_front()) {
+                    while let Some(bb_idx) = queue.pop_front().or_else(|| loop_queue.pop_front()) {
                         visited.insert(bb_idx);
 
                         let terminator = new_body.blocks()[bb_idx].terminator.clone();
@@ -126,9 +126,11 @@ impl TransformPass for LoopContractPass {
                         // the visiting queue.
                         for to_visit in terminator.successors() {
                             if !visited.contains(&to_visit) {
-                                let target_queue =
-                                    if is_loop_head { &mut loop_queue } else { &mut queue };
-                                target_queue.push_back(to_visit);
+                                if is_loop_head {
+                                    loop_queue.push_back(to_visit);
+                                } else {
+                                    queue.push_back(to_visit)
+                                };
                             }
                         }
                     }

diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs
@@ -11,12 +11,14 @@
 fn multiple_loops() {
     let mut x: u8 = kani::any_where(|i| *i >= 10);
 
-    #[kani::loop_invariant(x >= 5)]
-    while x > 5 {
-        x = x - 1;
+    if x != 20 {
+        #[kani::loop_invariant(x >= 5)]
+        while x > 5 {
+            x = x - 1;
+        }
     }
 
-    assert!(x == 5);
+    assert!(x == 5 || x == 20);
 
     #[kani::loop_invariant(x >= 2)]
     while x > 2 {