Handle pointer overflow in the back-end

[tautschnig]

At present, pointer overflow gets peculiar treatment in the front-end, and overflow expressions do not have well-defined semantics when their arguments are pointer typed. This should be remedied by moving the logic from the front-end to the back-end.

[TGWDB]

@thomasspriggs Bringing this to your attention since you were looking at some of this related to the new SMT backend and may have some insight.

[kroening]

We need to be careful to distinguish three things:

1. Pointers getting out-of-objects bounds, which is undefined.
2. Pointer overflow considering the full width of the pointer. Always implies 1 since objects cannot be bigger than size_t.
3. Overflow of the offset part in the current split representation that CBMC uses. Need not imply 1 if the object is big enough.

[tautschnig]

We need to be careful to distinguish three things:

1. Pointers getting out-of-objects bounds, which is undefined.

2. Pointer overflow considering the full width of the pointer. Always implies 1 since objects cannot be bigger than size_t.

3. Overflow of the offset part in the current split representation that CBMC uses. Need not imply 1 if the object is big enough.

The approach taken in #6881 seeks to do 3, and does not bother with 1 for that can be tested for using __CPROVER_r_ok.