The following verifies. Note that if & is applied to some part of s, the problem goes away because VCC would then have to pick which union member is active.


typedef struct S {

int x;

} S;

typedef struct T {

int y,z;

} T;

typedef union U {

S s;
T t;

} U;

void test() {

U u;
u.s.x = 1;
u.t.y = 2;
_(assert u.s.x == 1)

}

Our original plan was that when a union is made valid (e.g., as u does when it comes into scope above), we would automatically make the first union member the active one. This doesn't seem to be happening for unions, purely local or not.