Use get_fresh_aux_symbol to construct dynamic objects

[tautschnig]

This avoids use of a global variable and reuses central infrastructure instead
of repeated local work. Note that this changes the names of dynamic objects as
the suffix now includes a $ character, and need not have any suffix, as well as
moving the counter out of the middle of C++/Java dynamic_X_array objects.

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

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 3dccbb3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99183099

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: a6180e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99244949

[peterschrammel]

Thanks, @tautschnig, for picking this up. We have to verify whether this breaks downstream consumption of traces.

[tautschnig]

Marking do-not-merge until approved by users. @peterschrammel can you please co-ordinate this?

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: a6ef0d5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99430635
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 6fa9d82).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99433156

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: bde95d0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99678277
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 375f052).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99704183

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 2e2ffd4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100068548

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: d39c8d4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100079456

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 96c4752).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100652670

[allredj]

@tautschnig is this still something you want to do?

[tautschnig]

@tautschnig is this still something you want to do?

@allredj Yes, I'd still like to get this merged at some point. Unfortunately I'm getting very little engineering time at the moment, so I'm not sure whether I can promise a rebase over the next days. But the TG debugging probably still needs to happen. I guess the next step is on me to get this rebased first?

[allredj]

@tautschnig yes a rebase will be necessary for us to look at it further. But no rush obviously! :-)

[allredj]

@tautschnig Here comes my biannual ping about this PR. It seems to me that symex has changed enough in the past year that it will be more efficient to redo this rather than try to rebase this PR. Would you agree?
Do you want to keep it open?

Btw, I wish you a great Christmas holiday!

[TGWDB]

@tautschnig This PR could be nice to rebase and merge, but maybe is too old and deprecated now? Any chance of an update on the status?

[tautschnig]

@tautschnig This PR could be nice to rebase and merge, but maybe is too old and deprecated now? Any chance of an update on the status?

Finally done. Does this still need or want some Diffblue-internal review? If so, @TGWDB can you perhaps co-ordinate for that to happen?

[codecov]

Codecov Report

Base: 78.38% // Head: 78.34% // Decreases project coverage by -0.03% ⚠️

Coverage data is based on head (9ee880b) compared to base (0841040).
Patch coverage: 76.92% of modified lines in pull request are covered.

❗ Current head 9ee880b differs from pull request most recent head e51444e. Consider uploading reports for the commit e51444e to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #3999      +/-   ##
===========================================
- Coverage    78.38%   78.34%   -0.04%     
===========================================
  Files         1647     1645       -2     
  Lines       190362   190345      -17     
===========================================
- Hits        149213   149124      -89     
- Misses       41149    41221      +72     

Impacted Files	Coverage Δ
src/ansi-c/expr2c.cpp	67.33% <ø> (-0.33%)	⬇️
src/goto-instrument/race_check.cpp	0.00% <0.00%> (ø)
src/goto-symex/goto_symex.cpp	98.64% <ø> (ø)
src/goto-symex/goto_symex.h	86.66% <ø> (ø)
src/util/pointer_predicates.h	100.00% <ø> (ø)
src/goto-symex/auto_objects.cpp	26.31% <16.66%> (+2.50%)	⬆️
src/goto-symex/symex_builtin_functions.cpp	93.12% <89.28%> (-0.23%)	⬇️
src/goto-programs/graphml_witness.cpp	53.07% <100.00%> (ø)
src/solvers/flattening/pointer_logic.cpp	95.06% <100.00%> (ø)
src/util/simplify_expr_pointer.cpp	85.83% <100.00%> (-0.76%)	⬇️
... and 74 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.