Skip to content

Commit 3360696

Browse files
committed
fixup! Value set: lift offset from numeric constants to expressions
Kani's test `tests/kani/Iterator/flat_map.rs` does reach this branch.
1 parent eeb8689 commit 3360696

File tree

1 file changed

+0
-15
lines changed

1 file changed

+0
-15
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -356,21 +356,6 @@ bool value_sett::eval_pointer_offset(
356356
return false;
357357
else
358358
{
359-
// This branch should not be reached as any constant offset will have
360-
// been used before already. The following code will trigger
361-
// `eval_pointer_offset`, yet we wouldn't end up in this branch:
362-
// struct S { int a; char b; };
363-
//
364-
// int main()
365-
// {
366-
// struct S s;
367-
// int offset;
368-
// __CPROVER_assume(offset >= 0 && offset <= 1 && offset % 2 == 0);
369-
// int *p = (char*)&s + offset;
370-
// int x = *p;
371-
// __CPROVER_assert(s.a == x, "");
372-
// }
373-
UNREACHABLE;
374359
const exprt &object=object_numbering[it->first];
375360
auto ptr_offset = compute_pointer_offset(object, ns);
376361

0 commit comments

Comments
 (0)