Assume var is 0 if there was no assign before loop

goblint · Oct 2, 2024 · 25a1aca · 25a1aca
1 parent bb6f9aa
commit 25a1aca
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -277,7 +277,8 @@ let fixedLoopSize loopStatement func =
   if getsPointedAt var func then
     None
   else
-    let* start = constBefore var loopStatement func in
+    (* Assume var value to be 0 if there was no constant assignment to the var before loop *)
+    let start = Option.value (constBefore var loopStatement func) ~default:Z.zero in
     let* diff = assignmentDifference (loopBody loopStatement) var in
     let* goal = adjustGoal diff goal op in
     let iterations = loopIterations start diff goal (op=Ne) in