File tree Expand file tree Collapse file tree 1 file changed +0
-15
lines changed Expand file tree Collapse file tree 1 file changed +0
-15
lines changed Original file line number Diff line number Diff 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
You can’t perform that action at this time.
0 commit comments