Pointer arithmetic overflow is overflow on integer representation

[tautschnig]

At a bare minimum, we should report an overflow when performing pointer
arithmetic that would result in an overflow on the underlying integer
representation.

As future work, we may want to expand on those checks by reporting
overflows when exceeding object bounds, as discussed in #5426.

Fixes: #5284

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #5814 (a20fb34) into develop (f6ce727) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #5814   +/-   ##
========================================
  Coverage    69.75%   69.76%           
========================================
  Files         1242     1242           
  Lines       100892   100893    +1     
========================================
+ Hits         70382    70383    +1     
  Misses       30510    30510           

Flag	Coverage Δ
cproversmt2	43.39% <100.00%> (+<0.01%)	⬆️
regression	66.72% <100.00%> (+<0.01%)	⬆️
unit	32.30% <0.00%> (-0.01%)	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	88.37% <100.00%> (+0.01%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f6ce727...a20fb34. Read the comment docs.