C Semantics in K Framework

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

Chucky,

> Moving on... since all the business with punning messes up my original
> question, here is a rewritten program:

Thanks for pointing out I missed the following.

The code below is covered by the common initial sequence rules.
Sentence 1037, 1038
http://c0x.coding-guidelines.com/6.5.2.3.html

> struct T0 {
>      char a;
> };
> struct T1 {
>      char a;
>      char b;
> };
> union U {
>      struct T0 t0;
>      struct T1 t1;
> } u;
> int main(void){
>      u.t1.a = 0;
>      u.t1.b = 0;
>      u.t0.a = 0; // A
>      return u.t1.b; // B
> }
>
> Same question again, is this unspecified according to n1570 6.2.6.1:7?  Does
> writing 0 at u.t0.a unspecify u.t1.b?
>
> -Chucky
>
> On Mon, Aug 15, 2011 at 9:45 AM, Derek M 
> Jones<derek AT knosof.co.uk>
>   wrote:
>
> > 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<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<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<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<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

--
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