C Semantics in K Framework

[CUOQ Pascal <Pascal.CUOQ AT cea.fr>]

Our C auto-detection program has ceased to compile gods know when, but I'm 
thinking of putting in the following as a reminder nevertheless. Any comments?

It goes without saying that anyone using, say, -machdep x86_64, from the 
command-line, or even the default x86_32, will be completely unaware of the 
issue, so I should do something in the parser too, but I know better than 
trying to intervene there.

Pascal

Index: machdep.c
===================================================================
--- machdep.c   (revision 14601)
+++ machdep.c   (working copy)
@@ -172,6 +172,27 @@
            (int)(&((struct ptrstruct*)0)->p));
   }
 
+  // Unnamed members
+  {
+    struct S0
+    {
+      int;
+      // If you are reading this, it's probably because your C compiler
+      // rejected the above. Good for you! It is not allowed by C99.
+      // See discussion thread at:
+      // 
http://lists.cs.uiuc.edu/pipermail/c-semantics/2011-August/thread.html
+      // You can comment this block.
+      int f1;
+    };
+    if (sizeof(struct S0) != 2*sizeof(int))
+      {
+       printf("(* WARNING: This compiler handles unnamed struct members\n");
+       printf("   differently from Frama-C.\n");
+       printf("   To be analyzed correctly, your programs must *NOT* use\n");
+       printf("   this language extension. *)\n");
+      }
+   }
+
   // The alignment of a float
   {
     struct floatstruct {