Dirty locals analysis: consume goto_programt instead of goto_functiont

[tautschnig]

The analysis does not use any information contained in a goto_functiont that's not already available in a goto_programt. Using this more specific type avoids any (future) use building unnecessary wrappers.

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

[tautschnig]

@kroening @martin-cs @peterschrammel There may be a point in not making this change to keep analysis APIs more consistent. Please let me know.

[codecov]

Codecov Report

Base: 78.28% // Head: 78.28% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (4004524) compared to base (2890f74).
Patch coverage: 100.00% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7244   +/-   ##
========================================
  Coverage    78.28%   78.28%           
========================================
  Files         1642     1642           
  Lines       189980   190002   +22     
========================================
+ Hits        148720   148742   +22     
  Misses       41260    41260           

Impacted Files	Coverage Δ
src/analyses/constant_propagator.h	82.00% <100.00%> (-0.36%)	⬇️
src/analyses/dirty.cpp	84.61% <100.00%> (ø)
src/analyses/dirty.h	100.00% <100.00%> (ø)
src/analyses/local_bitvector_analysis.h	90.00% <100.00%> (-0.20%)	⬇️
src/analyses/local_may_alias.h	100.00% <100.00%> (ø)
src/goto-instrument/contracts/cfg_info.h	87.50% <100.00%> (-0.34%)	⬇️
src/goto-symex/symex_function_call.cpp	95.63% <100.00%> (+0.02%)	⬆️
src/goto-symex/symex_main.cpp	87.07% <100.00%> (+0.03%)	⬆️
unit/goto-symex/goto_symex_state.cpp	100.00% <100.00%> (ø)
unit/goto-symex/symex_assign.cpp	100.00% <100.00%> (ø)
... and 2 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[kroening]

The key difference between the two data structures are the identifiers of the parameters. Which analyses need those?

[kroening]

Further to this, a parameter may become dirty if you take its address. Unless we use goto_functionst, we don't have the identifiers.

[tautschnig]

Further to this, a parameter may become dirty if you take its address. Unless we use goto_functionst, we don't have the identifiers.

Yes, but we don't even bother looking at whether a symbol has local scope or not: the analysis collects all symbols the address of which is taken. We could, arguably, refine that.

[kroening]

This still bugs me a bit; it would seem that it may be preferable to have a common argument to procedure-local analyses, and goto_functiont would seem to be the right choice.

[peterschrammel]

I'm not entirely convinced that this refactoring has huge value, but nothing blocking.

We could, arguably, refine that.

Any plans to do that soon?

[tautschnig]

Despite having approvals here: I will refrain from merging as the feedback suggests we might make better use of the existing signature in future, and the code churn just isn't really helpful.