C Semantics in K Framework

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

On Jul 25, 2011, at 7:47 AM, Chucky Ellison wrote:
> One such program it catches now, which it wasn't catching before, is  
> the following:
> union U {
>     char a;
>     int b;
> } u;
> int main(void){
>     u.b = 0;
>     u.a = 0;
>     return u.b;    // error here, caught now
> }
>
> After writing to u.a, some of the bytes of u.b have become  
> unspecified.

I hear that C99 TC3 clarifies that this is more like
"implementation-defined" behavior in 6.5.2.3 footnote 82.
I do not have the exact quote (locked in a different office
in this low-activity season), but it may be worded as:

http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_283.htm

I find it amusing that the standard carefully defines
"implementation-defined", "undefined" and "unspecified"
behavior in its introduction and then leaves you guessing
all the time which one applies to difficult cases.

This said, the treatment you describe for unions seems reasonable
for an architecture-independent semantic.

Pascal