ansi_c_entry_point: avoid magic number

[tautschnig]

The code previously hard-coded an upper bound for argc that perhaps was
suitable for 32-bit systems (albeit even questionable for that case).
Replace this calculation by one that refers to configured bit widths.

• 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.

[peterschrammel]

On real systems this might be substantially lower, see getconf ARG_MAX for POSIX, for instance. Maybe we should have an instrumentation option that allows setting the value (with the system's limit as default)?

[tautschnig]

On real systems this might be substantially lower, see getconf ARG_MAX for POSIX, for instance. Maybe we should have an instrumentation option that allows setting the value (with the system's limit as default)?

Good call. I've now handled the Windows case, but for Unix it will indeed require an instrumentation option. I'm not sure how useful this even is, to be honest, so I'll not bother implementing this for now. We have --model-argc-argv in goto-instrument, which likely is more useful already.

[codecov]

Codecov Report

Merging #6007 (658de79) into develop (8aa6be8) will increase coverage by 0.01%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6007      +/-   ##
===========================================
+ Coverage    76.62%   76.64%   +0.01%     
===========================================
  Files         1578     1578              
  Lines       181180   181185       +5     
===========================================
+ Hits        138833   138865      +32     
+ Misses       42347    42320      -27     

Impacted Files	Coverage Δ
src/util/config.h	57.14% <ø> (ø)
src/ansi-c/ansi_c_entry_point.cpp	88.60% <100.00%> (-0.05%)	⬇️
src/util/config.cpp	57.85% <100.00%> (+0.36%)	⬆️
src/ansi-c/c_typecheck_expr.cpp	75.65% <0.00%> (+0.50%)	⬆️
src/solvers/smt2/smt2_conv.cpp	67.51% <0.00%> (+0.58%)	⬆️

---

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 da342c5...658de79. Read the comment docs.

[chrisr-diffblue]

Looks fine to me as is. Take my one comment as a suggestion to ponder, and not a requirement.

[chrisr-diffblue]

Much cleaner to my (biased) eye - thanks for the updates :-)