C Semantics in K Framework

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

John,

> The C99 standard seems to make it clear that structs may contain unnamed
> members.  This argues that KCC and CompCert are correct.

Unnamed BIT-FIELD members.

> Both Clang and GCC (even when given the --std=c99 flag) complain that
> line 5 does not declare anything, and their output is consistent with
> this claim.

This is correct.

> Anyone know what's going on?

The code is making use of an extension to C.

> Thanks,
>
> John
>
>
>
> int printf (const char *, ...);
>
> struct S0
> {
>     int;
>     int f1;
> };
>
> struct S3
> {
>     int f2;
>     int f3;
> };
>
> union U4
> {
>     struct S3 f0;
>     struct S0 f3;
> };
>
> union U4 g_110;
>
> int main (void)
> {
>     g_110.f3.f1 = 1;
>     printf ("%d\n", g_110.f0.f2);
>     return 0;
> }
> _______________________________________________
> 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