Include pointer offset in counterexample output #3135
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
kroening
changed the title
There was a problem hiding this comment.
Well this seems like an unpleasant omission. Are you sure that pointer_expr() is only used in output? If it is used elsewhere we might want to see if this fixes other things.
I guess if we really wanted to show off we could check if the base object was an array and turn it into &(a[i]). Would this be more human friendly than a + i ?
| int A[2]; | ||
| int *ip = &A[1]; | ||
| uuu.structbb.intb = 1; | ||
| // assert(*ptr == 1); |
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 8652d9c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87494837
| return typecast_exprt::conditional_cast( | ||
| plus_exprt( | ||
| base, from_integer(pointer.offset % *object_size, pointer_diff_type())), | ||
| type); |
There was a problem hiding this comment.
You probably meant pointer.offset / *object_size
There was a problem hiding this comment.
Ooops - that clearly shows that my test case is not good enough. Thanks for catching that! I'll extend my test.
|
@martin-cs said:
I need to review #2161 as that has modifications in the same area of code. |
|
Marking do-not-merge as this needs to be built on top of the fixes in #2161. |
While the bit-level pointer output would convey the information, the human-readable expression previously did not consider non-zero offsets except for null pointers.
tautschnig
force-pushed
the
union-arithmetic
branch
from
8652d9c to
e140d16
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: e140d16).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89854653
While the bit-level pointer output would convey the information, the
human-readable expression previously did not consider non-zero offsets except
for null pointers.