Warn when --malloc-may-fail has no effect

[tautschnig]

f7958df documented that malloc-may-fail needs to be used whenever the
library is added, but users might not actually have had a chance to read
updated documentation. Print a warning at runtime to make it more likely
that users become aware.

• 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 #6657 (274fd05) into develop (e021eef) will decrease coverage by 0.00%.
The diff coverage is 57.14%.

❗ Current head 274fd05 differs from pull request most recent head 19e6e86. Consider uploading reports for the commit 19e6e86 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6657      +/-   ##
===========================================
- Coverage    76.74%   76.74%   -0.01%     
===========================================
  Files         1579     1579              
  Lines       182171   182185      +14     
===========================================
+ Hits        139802   139811       +9     
- Misses       42369    42374       +5     

Impacted Files	Coverage Δ
.../goto-instrument/goto_instrument_parse_options.cpp	68.78% <14.28%> (-0.47%)	⬇️
src/cbmc/cbmc_parse_options.cpp	77.89% <100.00%> (+0.33%)	⬆️
src/pointer-analysis/value_set.cpp	83.29% <0.00%> (+0.12%)	⬆️

---

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 e08c77d...19e6e86. Read the comment docs.

[martin-cs]

@tautschnig Please forgive me as I am slightly behind on reviewing and so am struggling a little with context. As I understand it #6576 is moving from the "patching __CPROVER_initialize to set globals" model to "changing the symbol table and then regenerating __CPROVER_initialize" model. This sounds like a significant improvement because the patching code was always a bit flakey and being able to regenerate __CPROVER_initialize is generally useful and cool.

I don't quite get why this PR is needed though; couldn't we have these parameters as globals rather than macros and so do the "change symbol table and regenerate __CPROVER_initialize" trick for setting these?

[tautschnig]

[...]

I don't quite get why this PR is needed though; couldn't we have these parameters as globals rather than macros and so do the "change symbol table and regenerate __CPROVER_initialize" trick for setting these?

That's a fair point, and I agree this is doable. Likely this is the more user-friendly approach than adding a warning. I will, however, want to build this on top of #6590 to avoid spamming goto binaries with unnecessary global variables. I'll change this PR to "Draft" and will re-work it.