C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

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