C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

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")."

-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