C front-end: initializer lists do not initialise anonymous members

Compilers differ in their handling of anonymous members, also depending
on the type of the anonymous member. Make sure we accurately model this
while type checking. Consequently, regression tests need to be amened to
either be compiler-specific or not rely on anonymous or empty compound
types, which dump-c also must not spuriously generate (from incomplete
structs or unions).

New tests are based on a case found by C-Reduce when starting from an
SV-COMP task. Behaviour across different compilers confirmed with
Compiler Explorer (https://godbolt.org/).

Author: tautschnig

regression/ansi-c/Empty_Declaration1/main.c

@@ -1,10 +1,12 @@
 int blah(void);
 ; // empty!
 
+#ifndef _MSC_VER
 struct some
 {
   ; // empty
 };
+#endif
 
 int main() {
 }

regression/ansi-c/Union_Initialization2/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 
-union member designator found for empty union
+(union member designator found for empty union|C requires that a struct or union has at least one member)
 ^SIGNAL=0$
 ^EXIT=(1|64)$
 --

regression/ansi-c/_Generic1/main.c

@@ -13,6 +13,7 @@
                 struct some: 5 \
              )
 
+#ifdef __GNUC__
 struct some
 {
 } s;
@@ -22,7 +23,6 @@ char ch;
 long double ld;
 short sh;
 
-#ifdef __GNUC__
 STATIC_ASSERT(G(i)==3);
 STATIC_ASSERT(G(sh)==10);
 STATIC_ASSERT(G(ld)==1);

regression/ansi-c/anonymous_member1/main.c

@@ -1,15 +1,39 @@
+#ifdef _MSC_VER
+// No _Static_assert in Visual Studio
+#  define _Static_assert(condition, message) static_assert(condition, message)
+#endif
+
 struct S
 {
   struct
   {
     int : 1;
+#ifndef _MSC_VER
     int;
+#endif
     int named;
   };
 };
 
+_Static_assert(sizeof(struct S) == sizeof(int) * 2, "ignore int;");
+
 struct S s = {.named = 0};
 
+struct S1
+{
+  struct S2
+  {
+    int : 1;
+    int named;
+  };
+};
+
+#ifdef _MSC_VER
+_Static_assert(sizeof(struct S1) == sizeof(int) * 2, "");
+#else
+_Static_assert(sizeof(struct S1) == 0, "");
+#endif
+
 int main()
 {
 }

regression/ansi-c/anonymous_member2/main.c

@@ -0,0 +1,25 @@
+#define static_assert(x) struct {char some[(x) ? 1 : -1]; }
+
+struct a
+{
+};
+struct c
+{
+  struct a;
+  void *d;
+} e =
+  {
+#ifdef not_permitted
+    {},
+#endif
+    0},
+  e2;
+struct
+{
+  struct c f;
+} * g;
+int main()
+{
+  g->f;
+  static_assert(sizeof(e) == sizeof(void *));
+}

regression/ansi-c/anonymous_member2/not_permitted.desc

@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+-Dnot_permitted
+cannot initialize 'void \*' with an initializer list
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ansi-c/anonymous_member2/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/anonymous_member3/main.c

@@ -0,0 +1,20 @@
+typedef void(keyhandler_fn_t)(void);
+typedef void(irq_keyhandler_fn_t)(int);
+
+void foo()
+{
+}
+
+struct keyhandler
+{
+  union {
+    keyhandler_fn_t *fn;
+    irq_keyhandler_fn_t *irq_fn;
+  };
+  const char *desc;
+  _Bool x, y;
+} key_table[3] = {[0] = {{(keyhandler_fn_t *)(foo)}, "text", 1, 0}};
+
+int main()
+{
+}

regression/ansi-c/anonymous_member3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/sizeof3/main.c

@@ -4,6 +4,7 @@
 #define STATIC_ASSERT(condition)                                               \
   int CONCAT2(some_array, __LINE__)[(condition) ? 1 : -1]
 
+#ifndef _MSC_VER
 struct empty_struct { };
 union empty_union { };
 
@@ -16,6 +17,7 @@ struct combination {
 STATIC_ASSERT(sizeof(struct empty_struct)==0);
 STATIC_ASSERT(sizeof(union empty_union)==0);
 STATIC_ASSERT(sizeof(struct combination)==sizeof(int));
+#endif
 
 int main()
 {

regression/ansi-c/struct5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--i386-win32
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-concurrency/invalid_object1/main.c

@@ -134,6 +134,7 @@ struct OpenEthState
 
 struct device
 {
+  int dummy;
 };
 
 struct napi_struct

regression/cbmc-library/CMakeLists.txt

@@ -7,7 +7,7 @@ add_test_pl_tests(
     "$<TARGET_FILE:cbmc>"
     "cbmc-library"
     "$<TARGET_FILE:cbmc>"
-    "-C;-X;pthread"
+    "-C;-X;pthread;-X;gcc-only"
     "CORE"
 )
 endif()

regression/cbmc-library/Makefile

@@ -5,13 +5,14 @@ include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 	no_pthread = -X pthread
+	gcc_only = -X gcc-only
 endif
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread) $(gcc_only)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread) $(gcc_only)
 
 show:
 	@for dir in *; do \

regression/cbmc-library/memcpy-06/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 function 'memcpy' is not declared
@@ -8,3 +8,6 @@ parameter "memcpy::dst" type mismatch
 --
 ^warning: ignoring
 Invariant check failed
+--
+This test requires support for empty structs, which aren't supported by Visual
+Studio.

regression/cbmc/Anonymous_Struct2/main.c

@@ -1,6 +1,9 @@
 // The member without name is a Visual Studio feature
 // https://msdn.microsoft.com/en-us/library/z2cx9y4f.aspx
 
+#ifdef _MSC_VER
+#  include <assert.h>
+
 struct X
 {
   struct
@@ -47,3 +50,8 @@ int main()
   assert(s2.y==1);
   assert(s2.z==1);
 }
+#else
+int main()
+{
+}
+#endif

regression/cbmc/Anonymous_Struct3/main.c

@@ -1,5 +1,3 @@
-#include <assert.h>
-
 // The member without name is a Visual Studio feature
 // https://msdn.microsoft.com/en-us/library/z2cx9y4f.aspx
 typedef union my_U {
@@ -19,7 +17,7 @@ int main()
   x.f1 = 1;
 
   if(*(char *)&word==1)
-    assert(x.raw==2); // little endian
+    __CPROVER_assert(x.raw == 2, "little endian");
   else
-    assert(x.raw==64); // big endian
+    __CPROVER_assert(x.raw == 64, "big endian");
 }

regression/cbmc/Anonymous_Struct3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+-win32
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Empty_struct1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 
 ^EXIT=0$

regression/cbmc/Empty_struct2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/cbmc/atomic_section_seq1/main.c

@@ -200,6 +200,7 @@ struct OpenEthState$link4
 
 struct device
 {
+  int dummy;
 };
 
 struct napi_struct

regression/cbmc/empty_compound_type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/cbmc/empty_compound_type2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

src/ansi-c/c_typecheck_initializer.cpp

@@ -285,7 +285,9 @@ void c_typecheck_baset::designator_enter(
 
     for(const auto &c : struct_type.components())
     {
-      if(c.type().id() != ID_code && !c.get_is_padding())
+      if(
+        c.type().id() != ID_code && !c.get_is_padding() &&
+        (c.type().id() != ID_c_bit_field || !c.get_anonymous()))
       {
         entry.subtype = c.type();
         break;
@@ -721,12 +723,11 @@ void c_typecheck_baset::increment_designator(designatort &designator)
       assert(components.size()==entry.size);
 
       // we skip over any padding or code
-      // we also skip over anonymous members
+      // we also skip over anonymous members bit fields
       while(entry.index < entry.size &&
             (components[entry.index].get_is_padding() ||
              (components[entry.index].get_anonymous() &&
-              components[entry.index].type().id() != ID_struct_tag &&
-              components[entry.index].type().id() != ID_union_tag) ||
+              components[entry.index].type().id() == ID_c_bit_field) ||
              components[entry.index].type().id() == ID_code))
       {
         entry.index++;
@@ -826,8 +827,9 @@ designatort c_typecheck_baset::make_designator(
       }
       else
       {
-        // We will search for anonymous members,
-        // in a loop. This isn't supported by gcc, but icc does allow it.
+        // We will search for anonymous members, in a loop. This isn't supported
+        // by GCC (unless the anonymous member is within an unnamed union or
+        // struct), but Visual Studio does allow it.
 
         bool found=false, repeat;
         typet tmp_type=entry.type;
@@ -853,6 +855,9 @@ designatort c_typecheck_baset::make_designator(
               c.get_anonymous() &&
               (c.type().id() == ID_struct_tag ||
                c.type().id() == ID_union_tag) &&
+              (config.ansi_c.mode ==
+                 configt::ansi_ct::flavourt::VISUAL_STUDIO ||
+               follow(c.type()).find(ID_tag).is_nil()) &&
               has_component_rec(c.type(), component_name, *this))
             {
               entry.index=number;