C Semantics in K Framework

[Derek M Jones <derek AT knosof.co.uk>]

Chucky,

> The sentences you quoted seem to contradict footnote 95 in 6.5.2.3:3:
> "If the member used to read the contents of a union object is not the same
> as the member last used to store a value in the object, the appropriate part
> of the object representation of the value is reinterpreted as an object
> representation in the new type as described in 6.2.6 (a process sometimes
> called "type punning")."

DR 283 is the background.
http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_283.htm

Does this wording prevent the behavior being undefined?  Footnotes are
not normative.  I will check with WG14 people.


> -Chucky
>
> On Mon, Aug 15, 2011 at 7:40 AM, Derek M 
> Jones<derek AT knosof.co.uk>
>   wrote:
>
> > Chucky,
> >
> > > 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:
> >
> > Sentence 960 et al http://c0x.coding-guidelines.com/6.5.html
> > render it undefined.
> >
> > > 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
> > >
> > >
> > >
> > > _______________________________________________
> > > c-semantics mailing list
> > > c-semantics AT cs.illinois.edu
> > > http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
> >
> > --
> > Derek M. Jones                         tel: +44 (0) 1252 520 667
> > Knowledge Software Ltd                 
> > mailto:derek AT knosof.co.uk
> > Source code analysis                   http://www.knosof.co.uk
> > _______________________________________________
> > c-semantics mailing list
> > c-semantics AT cs.illinois.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics

--
Derek M. Jones                         tel: +44 (0) 1252 520 667
Knowledge Software Ltd                 
mailto:derek AT knosof.co.uk
Source code analysis                   http://www.knosof.co.uk