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(
1106
1106
// - `GOTO` jumps out of the loops, which model C `break` statements.
1107
1107
// These instructions are allowed to be missing from `loop_content`,
1108
1108
// 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)
1110
1110
{
1111
1111
if (loop_content.contains (i))
1112
1112
continue ;
@@ -1124,7 +1124,7 @@ void code_contractst::apply_loop_contract(
1124
1124
{
1125
1125
do
1126
1126
i++;
1127
- while (i->is_dead ());
1127
+ while (i != loop_end && i ->is_dead ());
1128
1128
1129
1129
// because we increment `i` in the outer `for` loop
1130
1130
i--;
You can’t perform that action at this time.
0 commit comments