value sets: do not try to access components of an empty struct/union

[tautschnig]

This avoids a segmentation fault while running on
c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lustre--mdc--mdc.ko-entry_point.cil.out.i
with options --pointer-check --bounds-check --unwind 2. This benchmark
includes the empty union __anonunion_u_rpc_386. While the patch does
address the problem on this benchmark, I failed to come up with a small
regression test.

• 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 #5659 (eade88f) into develop (c9c3ca6) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #5659   +/-   ##
========================================
  Coverage    69.42%   69.42%           
========================================
  Files         1243     1243           
  Lines       100632   100633    +1     
========================================
+ Hits         69861    69864    +3     
+ Misses       30771    30769    -2     

Flag	Coverage Δ
cproversmt2	43.14% <66.66%> (+<0.01%)	⬆️
regression	66.32% <66.66%> (+<0.01%)	⬆️
unit	32.26% <100.00%> (+<0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/pointer-analysis/value_set.cpp	78.39% <100.00%> (+0.03%)	⬆️
src/goto-symex/renaming_level.cpp	98.98% <0.00%> (+1.01%)	⬆️
src/util/expr_initializer.cpp	86.51% <0.00%> (+1.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 c9c3ca6...eade88f. Read the comment docs.

[hannes-steffenhagen-diffblue]

Could you come up with a test case for this for our regression tests?

[tautschnig]

Could you come up with a test case for this for our regression tests?

I tried, and I'll keep trying, but it seems one has to craft code that does invalid pointer dereferences and perhaps other questionable things.

[martin-cs]

Change seems reasonable. I agree with @hannes-steffenhagen-diffblue that a test case would be good. Have you tried https://github.com/csmith-project/creduce ?

[tautschnig]

Have you tried https://github.com/csmith-project/creduce ?

Ah, of course! Thank you for reminding me!! That did the trick, a tiny regression test is now included. (And, yes, it does involve invalid pointer dereferencing.)

[martin-cs]

Much better! Thanks.