Field sensitivity: fully expand nested objects

[tautschnig]

When applying field sensitivity to an expression we must expand all levels. In the included test we previously constructed a member symbol (var_11..value) as right-hand side that still was of struct type. Instead, we must create a struct expression composed of all its members (here: { var_11..value.._0 }).

Also, we must not keep nested expandable members in the propagation map for phi nodes don't merge on them.

Fixes: #7462

• 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

Base: 78.48% // Head: 78.48% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (1658ee4) compared to base (7a9398d).
Patch coverage: 43.24% of modified lines in pull request are covered.

❗ Current head 1658ee4 differs from pull request most recent head ad8086f. Consider uploading reports for the commit ad8086f to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7472      +/-   ##
===========================================
- Coverage    78.48%   78.48%   -0.01%     
===========================================
  Files         1663     1663              
  Lines       191151   191180      +29     
===========================================
+ Hits        150032   150039       +7     
- Misses       41119    41141      +22     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_expr.cpp	76.06% <ø> (ø)
src/ansi-c/expr2c_class.h	100.00% <ø> (ø)
src/goto-symex/symex_assign.cpp	81.15% <ø> (-0.41%)	⬇️
src/util/pointer_expr.h	96.72% <0.00%> (-2.32%)	⬇️
src/ansi-c/expr2c.cpp	67.71% <7.69%> (-0.37%)	⬇️
src/goto-symex/field_sensitivity.cpp	93.28% <83.33%> (+0.24%)	⬆️

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.