pointer_logic: use mp_integer for numbering objects

[kroening]

Replacing std::size_t by mp_integer makes the code more platform-independent
and easier to use as overflow is no longer a concern.

• 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.
• 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 #6833 (c89b4f4) into develop (09cc397) will decrease coverage by 0.00%.
The diff coverage is 90.74%.

@@             Coverage Diff             @@
##           develop    #6833      +/-   ##
===========================================
- Coverage    77.03%   77.02%   -0.01%     
===========================================
  Files         1594     1594              
  Lines       185016   184999      -17     
===========================================
- Hits        142520   142502      -18     
- Misses       42496    42497       +1     

Impacted Files	Coverage Δ
src/solvers/flattening/bv_pointers.h	100.00% <ø> (ø)
...smt2_incremental/construct_value_expr_from_smt.cpp	100.00% <ø> (ø)
src/solvers/flattening/pointer_logic.h	72.72% <50.00%> (-7.28%)	⬇️
src/solvers/flattening/pointer_logic.cpp	91.35% <85.71%> (+1.23%)	⬆️
src/solvers/flattening/bv_pointers.cpp	85.16% <93.75%> (-0.18%)	⬇️
src/solvers/smt2/smt2_conv.cpp	67.47% <100.00%> (ø)
...smt2_incremental/construct_value_expr_from_smt.cpp	100.00% <100.00%> (ø)

---

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 e3dd810...c89b4f4. Read the comment docs.

[thomasspriggs]

Under what circumstances is it possible to overflow the size of std::size_t here?

My understanding is that in practical terms std::size_t is always sufficiently wide to support addressing all bytes of memory on the architecture for which cbmc is being compiled. Therefore assuming that each object we are dealing with requires 1 or more bytes of memory to track and that objects are assigned numbers sequentially, we will run out of memory before overflowing std::size_t.

[kroening]

std::size_t might be 32 bits, but we are verifying code for a 64-bit architecture.