File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
src/goto-instrument/contracts Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -1106,7 +1106,7 @@ void code_contractst::apply_loop_contract(
11061106 // - `GOTO` jumps out of the loops, which model C `break` statements.
11071107 // These instructions are allowed to be missing from `loop_content`,
11081108 // and may be safely ignored for the purpose of our instrumentation.
1109- for (auto i = loop_head; i < loop_end; ++i)
1109+ for (auto i = loop_head; i != loop_end; ++i)
11101110 {
11111111 if (loop_content.contains (i))
11121112 continue ;
@@ -1124,7 +1124,7 @@ void code_contractst::apply_loop_contract(
11241124 {
11251125 do
11261126 i++;
1127- while (i->is_dead ());
1127+ while (i != loop_end && i ->is_dead ());
11281128
11291129 // because we increment `i` in the outer `for` loop
11301130 i--;
You can’t perform that action at this time.
0 commit comments