I must attest that I have been running tests based on a39f3c
since it was committed, and the issue is gone. I believe this
new question is about something else, and again, I am not
confident what is right. I have upgraded to f0ba611, the latest version.
It is again about unions and initialization.
The attached program can be reduced to the following from the
point of view of my problem:
union U3 {
const unsigned f0 : _CSMITH_BITFIELD(41);
const signed : _CSMITH_BITFIELD(0);
int8_t * const f1;
int64_t f2;
const uint32_t f3;
};
static union U3 g_142[1][1] = {{{1UL}}};
main(){
...
for (i = 0; i< 1; i++)
{
for (j = 0; j< 1; j++)
{
transparent_crc(g_142[i][j].f3, "g_142[i][j].f3",
print_hash_value);
if (print_hash_value) printf("index = [%d][%d]\n", i, j);
}
}
}
There is an assignment to g_142[0][0].f2 in the original, but you can
check by inserting exit(1); right before it that it is not reached.
So field f0 of g_142[0][0] is initialized, and much late, member f3 is
passed to transparent_crc().
Is that supposed to be defined?
I tried to get the information from C99's 6.7.8 section, but it is not
clear to me. However, objects are initialized according to their types:
pointers to NULL and integers to zero. An union can have both and
integer member and a pointer member. And NULL's representation does not
have to be the same as that of the integer zero. So I do not see how
6.7.8 could be saying that more than one member of an union should be
initialized.
What do you think?
One argument to be made is that the program is in any case safe in
practice on desktop architectures where NULL and 0 have the same
representation, made of zeroes, and static variables are mapped to a
segment that contains only zeroes. It wouldn't be to hard to have an
option in Frama-C to implement the same point of view.
Pascal