Pointer subtraction in back-end: no need for bounds checking

[tautschnig]

5b8028a added pointer validity checks in the back-end when performing pointer minus pointer operations. Given our pointer encoding it seems important to do a same-object test as, for distinct objects, the object identifier part would start to play into the subtraction. When operating on the same object, however, even out-of-bounds pointers' subtraction should be indistinguishable from how this works on actual hardware.

Therefore, this commit removes the bounds-checking part. (C semantics have a pointer-validity requirement, but we need to catch this via checks inserted in the front-end, not in the back-end.)

• 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

All modified and coverable lines are covered by tests ✅

Project coverage is 78.76%. Comparing base (beebdda) to head (eade886).
Report is 2 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8497      +/-   ##
===========================================
- Coverage    78.80%   78.76%   -0.04%     
===========================================
  Files         1728     1728              
  Lines       198853   198925      +72     
  Branches     18323    18301      -22     
===========================================
- Hits        156700   156686      -14     
- Misses       42153    42239      +86     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.