C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

I want to make sure I understand what is going on with unions before I go and add more checks.  I would like some feedback about what people think about the following program.  It's not crystal clear to me whether this program is unspecified:

union T {
    char a;
};
union U {
    union T t;
    int b;
} u;
int main(void){
    u.b = 0;
    u.t.a = 0;      // A
    return u.b;    // B
}

(n1570 6.2.6.1:7) "When a value is stored in a member of an object of union type, the bytes of the object representation that do not correspond to that member but do correspond to other members take unspecified values."

At line A, a value is clearly being "stored in a member of" u.t.  It is unclear to me if it is also "storing a value in a member of" u.  If so, some of the bytes of u corresponding to u.b are made unspecified by 6.2.6.1:7.  If not, it is defined to read from u.b at line B.  What do you think about this?  Are there any other reasons this program would be unspecified or undefined?

-Chucky

On Mon, Jul 25, 2011 at 8:47 AM, Chucky Ellison <celliso2 AT illinois.edu> wrote:

Everybody,

The latest version of kcc (r941) should be catching some new kinds of union errors I was missing before.  As usual, you'll need to update K too.

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.  Basically, any program where you say union.field=foo will invalidate the bytes of the union not belonging to the field.  However, this version won't catch structs or unions nested in unions (example below).  I'm still trying to figure out a generic solution to this, but I thought this improvement might be useful in the meanwhile.

An example of an unspecified program program kcc still fails to detect is the following:
union T {
    char a;
};
union U {
    union T t;
    int b;
} u;
int main(void){
    u.b = 0;
    u.t.a = 0;
    return u.b;    // error here, still not caught
}


This version includes a reworking of the way types are represented in kcc to allow more flexibility.  This was a huge change, so if you see anything funky, let me know.

-Chucky