Merge pull request #5702 from tautschnig/union-excess

C front-end: ignore or reject excess union initializers

Author: tautschnig

regression/cbmc/Union_Initialization5/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+#ifndef _MSC_VER
+union U {
+  int x;
+  int y;
+} u = {1, 2};
+
+int main()
+{
+  // the excess initializer (2) is ignored
+  assert(u.x == 1);
+}
+#else
+int main()
+{
+}
+#endif

regression/cbmc/Union_Initialization5/test.desc

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

scripts/expected_doxygen_warnings.txt

@@ -85,7 +85,7 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (83), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (84), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/ansi-c/c_typecheck_initializer.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_initializer.h>
 #include <util/prefix.h>
@@ -484,6 +485,22 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         error() << "union member designator found for empty union" << eom;
         throw 0;
       }
+      else if(init_it != initializer_list.operands().begin())
+      {
+        if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+        {
+          error().source_location = value.source_location();
+          error() << "too many initializers" << eom;
+          throw 0;
+        }
+        else
+        {
+          warning().source_location = value.source_location();
+          warning() << "excess elements in union initializer" << eom;
+
+          return ++init_it;
+        }
+      }
       else if(index >= components.size())
       {
         error().source_location = value.source_location();
@@ -494,16 +511,20 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
       const union_typet::componentt &component = components[index];
 
-      if(dest->id()==ID_union &&
-         dest->get(ID_component_name)==component.get_name())
+      DATA_INVARIANT(
+        dest->id() == ID_union, "union should be zero initialized");
+
+      if(dest->get(ID_component_name) == component.get_name())
       {
         // Already right union component. We can initialize multiple submembers,
         // so do not overwrite this.
       }
       else
       {
-        // Note that gcc issues a warning if the union component is switched.
-        // Build a union expression from given component.
+        // The first component is not the maximum member, which the (default)
+        // zero initializer prepared. Replace this by a component-specific
+        // initializer; other bytes have an unspecified value (C Standard
+        // 6.2.6.1(7)).
         const auto zero =
           zero_initializer(component.type(), value.source_location(), *this);
         if(!zero.has_value())