Initialise union of static lifetime with zeros #5705
Conversation
tautschnig
requested review from
chrisr-diffblue and
kroening
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5705 +/- ##
===========================================
- Coverage 69.66% 69.64% -0.02%
===========================================
Files 1248 1248
Lines 100873 100922 +49
===========================================
+ Hits 70278 70292 +14
- Misses 30595 30630 +35
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
|
It would make sense to have a warning in the manual about this one as well. |
|
Marking do-not-merge as this requires fixes in dump-c (or some approach not involving |
tautschnig
force-pushed
the
union-zero
branch
from
751dc42 to
fa43cf1
Compare
|
Looking at this, I am wondering whether or not we might want to have a 'strict mode', which would not make compiler or architecture-specific assumptions. |
Well, at least we should make sure we can configure all those architecture/compiler-specific assumptions. We have quite a lot of this in |
Even in upcoming changes there must not be a situation where such initializers cannot be dumped in a compilable fashion.
The regression test demonstrated that decoding non-null pointer-typed constants were not correctly decoded to their integer representation.
The parser unnecessarily introduced an ID_designated_initializer into offsetof when no id was required, thereby creating an expression with ID_designated_initializer that had a different shape from all other uses of ID_designated_initializer. With this cleaned up, enable expr2c to print designated-initializer expressions.
C does not have byte_update expressions.
The C standard does not specify the value of bytes that do not belong to the object representation of a member referred to in an initializer list, but compilers seem to ensure those bytes are zero (possibly by using the .bss section).
Mirror what we already did for byte extract operations.
A union_exprt can refer to components of a type that is smaller than the full bit width of the union. Consequently, bits2expr should accept bit strings for such (smaller) members.
The order of constructor arguments was wrong, resulting in 48 copies (the ASCII index of '0') instead of bit-width copies, being used.
We introduce byte updates to soundly prepare union initializers, but such byte updates are not part of the C standard and thus aren't expected by dump-c. Run simplify to clean them up, when possible.
tautschnig
force-pushed
the
union-zero
branch
from
fa43cf1 to
ac31213
Compare
tautschnig
requested review from
hannes-steffenhagen-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
|
Trying to make sure we can successfully dump union expressions after fixing zero initialisation via byte updates became quite the bug squashing party. I started out by creating a test for dump-c, which I then noticed CBMC would not produce the correct verification result for. Here is the history as it may help to understand the flood of commits:
|
| @@ -410,7 +417,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) | |||
| else if(type.id() == ID_pointer) | |||
| { | |||
| if(value == ID_NULL && config.ansi_c.NULL_is_zero) | |||
| return std::string('0', to_bitvector_type(type).get_width()); | |||
| return std::string(to_bitvector_type(type).get_width(), '0'); | |||
The C standard does not specify the value of bytes that do not belong to
the object representation of a member referred to in an initializer
list, but compilers seem to ensure those bytes are zero (possibly by
using the .bss section).