typedef union _ut
{
int x;
int y;
int *ox;
/*@dependent@*/ int *dx;
struct { int a; int b; int *ip; } st;
} *ut;
extern /*@only@*/ /*@out@*/ void *smalloc (size_t);
ut ut_create1 (/*@unused@*/ int a)
{
ut u = (ut) smalloc (sizeof (*u));
return u; /* 1. Returned union u contains no defined field */
}
ut ut_create2 (int a)
{
ut u = (ut) smalloc (sizeof (*u));
u->x = a;
return u;
}
ut ut_create3 (int a)
{
ut u = (ut) smalloc (sizeof (*u));
u->x = a;
u->y = a;
return u; /* [Not anymore. Returned union u has 2 defined fields: x, y */
}
ut ut_create4 (int *t)
{
ut u = (ut) smalloc (sizeof (*u));
u->ox = t; /* 2. Implicitly temp storage t assigned to implicitly only */
return u;
}
ut ut_create5 (int *t)
{
ut u = (ut) smalloc (sizeof (*u));
u->dx = t; /* 3. Implicitly temp storage t assigned to dependent: u->dx = t */
return u;
}
ut ut_create6 (void)
{
ut u = (ut) smalloc (sizeof (*u));
u->st.a = 3;
return u; /* 4. Returned storage u->st contains 2 undefined fields: b, ip */
}
ut ut_create7 (int *p)
{
ut u = (ut) smalloc (sizeof (*u));
u->st.a = 3;
u->st.b = 4;
u->st.ip = p; /* 5. Implicitly temp storage p assigned to implicitly only */
return u;
}
void ut_mangle1 (ut u)
{
free (u->ox);
} /* 6. Released storage u->ox reachable from parameter */
void ut_mangle2 (ut u)
{
free (u->st.ip);
} /* 7. Released storage u->st.ip reachable from parameter */
void ut_mangle3 (ut u)
{
free (u->st.ip);
u->x = 3; /* This one's a toughy... */
} /* 8. Released storage u->st.ip reachable from parameter */
syntax highlighted by Code2HTML, v. 0.9.1