C Semantics in K Framework

[CUOQ Pascal <Pascal.CUOQ AT cea.fr>]

> "A structure type describes a sequentially allocated nonempty set of
> member objects (and, in certain circumstances, an incomplete array),
> each of which has an optionally specified name and possibly distinct type."

There is also 6.7.2.1 paragraph 11:

"A bit-field declaration with no declarator, but only a colon and a width, 
indicates an unnamed bit-field"

I do not see any allusion other than the "optionally" in your paragraph
to unnamed non-bitfield members, John.
Overall, the whole matter seems a bit under-specified to me in TC2.
Does anyone know if TC3 clarifies this?

Incidentally, do you expect that there is only one correct
answer for your program? If GCC and Clang are allowed
to use the most compact layout, then surely other compilers
are allowed to insert some padding at the place where you have
left an unnamed member too (as long as they have decided to
accept the program at all)?

Pascal