Minor initialization issue with unions

[monniaux]

#include <stdint.h>
#include <stdio.h>

union {
  int8_t;
  uint32_t c;
} toto = { 730 };

int main() {
  printf("%d\n", toto.c);
  return 0;
}

According to C17 6.7.9.17 "When no designations are present, subobjects of the current object are initialized in order according to the type of the current object: [...] the first named member of a union."

Accordingly, gcc considers that the initializer initializes c to 730. In contrast, CompCert considers that it initializes the unnamed field to 730, which gets truncated to 218. So it seems CompCert's behavior is incorrect.

I don't think this is something likely to show up in real code, except perhaps if the unnamed field is meant as some form of padding.

[m-schmidt]

Just for completeness: C99 and C11 also state "...first named member of a union".

[monniaux]

Note: in C11 and C17, anonymous fields that have union or structure type are treated specially, they expose their subfields (transitively) as though they were fields of the outer object. This is not the case here, but you may want to look into this.

[xavierleroy]

For the record, a full analysis of this issue:

• A declaration such as union { int8_t; uint32_t c; } is not allowed by the C99 grammar. The C11 grammar allows it (so as to support anonymous structs and unions) but gives it a meaning only if the type (here int8_t) is a struct or a union.
• GCC and Clang both accept this declaration, even in strict C99 mode, and just ignore the int8_t member. For GCC compatibility, the CompCert parser accepts the declaration, but the elaborator was not ignoring it like it should. This is fixed in 2892e2c .
• The "first named member of a union" prescription addresses unnamed bit-fields, as in union { int : 16; uint32_t c; }, which is legal C99 and C11. This is taken care of in 6ede270.