Skip to content

Commit b268c6d

Browse files
committed
Fix undefined behavior on iterator comparison
Inequality comparison on iterators was leading to undefined behavior and flakiness: incorrect instrumentation loop contracts.
1 parent b76cce8 commit b268c6d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/goto-instrument/contracts/contracts.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff 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--;

0 commit comments

Comments
 (0)