Merge pull request #5688 from tautschnig/anonymous-members

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

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,29 @@
+#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,21 @@
+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

@@ -6,7 +6,7 @@ else()
 add_test_pl_profile(
     "cbmc-library"
     "$<TARGET_FILE:cbmc>"
-    "-C;-X;unix"
+    "-C;-X;unix;-X;gcc-only"
     "CORE"
 )
 endif()

regression/cbmc-library/Makefile

@@ -5,13 +5,14 @@ include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 	unix_only = -X unix
+	gcc_only = -X gcc-only
 endif
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

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-library/memcpy-09/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^VERIFICATION SUCCESSFUL$

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
+CORE 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/Empty_struct3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --json-ui
 VERIFICATION FAILED

regression/cbmc/Malloc10/main.c

@@ -1,3 +1,4 @@
+#include <assert.h>
 #include <stdlib.h>
 
 void __blast_assert()
@@ -7,6 +8,7 @@ void __blast_assert()
 
 struct list_head
 {
+  int dummy;
 };
 
 struct list_head *elem = (struct list_head *)((void *)0);

regression/cbmc/Union_Initialization2/test.desc

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

regression/cbmc/atomic_section_seq1/main.c

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

regression/cbmc/atomic_section_seq1/test.desc

@@ -1,11 +1,8 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
---
-This test involves empty structs, which the SMT2 back-end does not currently
-support.

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
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/empty_compound_type3/test.desc

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

regression/cbmc/empty_compound_type4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --trace
 ^VERIFICATION FAILED$

regression/cbmc/struct1/test.desc

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

regression/cbmc/union/union_member.c

@@ -2,7 +2,7 @@
 
 struct s
 {
-  union U
+  union
   {
     char b[2];
   };

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c

@@ -17,6 +17,7 @@ struct s2n_evp_digest
   const void *ctx;
 };
 union s2n_hash_low_level_digest {
+  void *dummy; // for MSVC compatibility
 };
 struct s2n_hash_evp_digest
 {