show flow-insensitive value set

[polgreen]

Adds command line argument to goto-instrument to show the flow insensitive value set. Previously only possible to show the flow sensitive value set. Does not add this command line argument to help file, to be consistent with the original flow sensitive value set

• Each commit message has a non-empty body, explaining why the change was made.
• 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/

None of the existing similar goto-instrument options are documented, or in the help file so I assume these are not meant to be publicly advertised features

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

I haven't added new features, just the ability to print the result

• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #5414 into develop will decrease coverage by 0.84%.
The diff coverage is 25.00%.

@@             Coverage Diff             @@
##           develop    #5414      +/-   ##
===========================================
- Coverage    68.19%   67.34%   -0.85%     
===========================================
  Files         1176     1176              
  Lines        97527    97531       +4     
===========================================
- Hits         66510    65686     -824     
- Misses       31017    31845     +828     

Flag	Coverage Δ
#cproversmt2	?
#regression	65.37% <25.00%> (-0.01%)	⬇️
#unit	32.24% <ø> (ø)

Impacted Files	Coverage Δ
...rc/goto-instrument/goto_instrument_parse_options.h	100.00% <ø> (ø)
.../goto-instrument/goto_instrument_parse_options.cpp	58.29% <25.00%> (-0.19%)	⬇️
src/solvers/smt2/smt2irep.cpp	32.00% <0.00%> (-56.00%)	⬇️
src/solvers/smt2/smt2_conv.cpp	31.46% <0.00%> (-26.23%)	⬇️
src/solvers/floatbv/float_bv.cpp	55.25% <0.00%> (-18.88%)	⬇️
src/solvers/smt2/smt2_dec.cpp	61.53% <0.00%> (-16.93%)	⬇️
src/solvers/smt2/smt2_tokenizer.cpp	69.02% <0.00%> (-16.82%)	⬇️
src/solvers/flattening/pointer_logic.cpp	81.81% <0.00%> (-10.61%)	⬇️
src/solvers/smt2/smt2_parser.cpp	58.91% <0.00%> (-8.07%)	⬇️
src/util/expr_util.cpp	80.50% <0.00%> (-4.24%)	⬇️
... and 12 more

---

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 d453933...f789092. Read the comment docs.

[hannes-steffenhagen-diffblue]

❓

Does not add this command line argument to help file, to be consistent with the original flow sensitive value set

I really don’t believe this is the sort of thing we want to be consistent about. Having one undocumented option is already bad, adding another and not documenting that either just because the other one isn’t is just making it worse.

Also, would you mind adding some tests that show what kind of output you’re expecting from this option to regression/goto-instrument?

[martin-cs]

Code change is fine. Please get the consistency in the help file by documenting more not less! Also a regression test would be good; goto-instrument's functionality is woefully under tested.

[martin-cs]

General aspirational ramble. I would like to get us down to just one abstract interpretation framework, rather than the current three. As part of that I would like to move this kind of functionality out of goto-instrument and into goto-analyser --show because ... it's really not instrumentation or even program transformation. To do this we need to:

1. refactor how function pointer removal works.
2. be able to do return removal with function pointers in.
3. modify the ait framework to tolerate function pointers.
4. flow-insensitive ait_storage.
5. migrate over the pointer analysis and other bits.

3-5 I am happy to do and are not actually much work. I have been working with @chrisr-diffblue to do 1 and 2 for ... a year or two but it has stalled a number of times. @NlightNFotis has written at least two full PRs to do this.

If you care about this kind of functionality, maybe we could get this moving again? @chrisr-diffblue ?