The overflow intrinsics have surprising behaviour on pointer arithmatic

[danielsn]

x+1 on a pointer is x+sizeof(*x)*1. The overflow check is treating it as (int)x+1

Ideally, we'd love to have a __pointer_<op>_overflow() intrinsic which would do the right thing for pointers.

[tautschnig]

I'm not sure there ever was a claim that __CPROVER_overflow_plus supported pointers (in a meaningful way). So if we were to have something like __CPROVER_overflow_pointer_plus: what would be the "the right thing" for pointers? We have --pointer-overflow-check to do what might be "the right thing," but then it generates non-trivial expressions.

Given that --pointer-overflow-check already does generate checks, what would be the rationale to have some intrinsic do do this?

[tautschnig]

Can we resolve this one once #6631 has been addressed/closed?

[tautschnig]

Resolving as #6631 has been resolved.