Expression initialiser: do not generate nil for empty union

regression/cbmc/Union_Initialization3/main.c

@@ -0,0 +1,6 @@
+union {
+} a;
+main()
+{
+  __assert_fail("", 2, __PRETTY_FUNCTION__);
+}

regression/cbmc/Union_Initialization3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+CBMC would previously report "warning: ignoring nil" and eventually fail an
+invariant in src/solvers/flattening/boolbv_width.cpp:199 function: get_entry.

regression/cbmc/Union_Initialization4/main.c

@@ -0,0 +1,16 @@
+union empty {
+};
+
+struct S
+{
+  int x;
+  union empty e;
+  int y;
+};
+
+struct S s = {1};
+
+int main()
+{
+  assert(s.x == 1 && s.y == 0);
+}

regression/cbmc/Union_Initialization4/test.desc

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

src/ansi-c/c_typecheck_initializer.cpp

@@ -953,16 +953,21 @@ exprt c_typecheck_baset::do_initializer_list(
      full_type.id()==ID_union ||
      full_type.id()==ID_vector)
   {
-    // start with zero everywhere
-    const auto zero = zero_initializer(type, value.source_location(), *this);
-    if(!zero.has_value())
+    if(
+      full_type.id() != ID_union ||
+      !to_union_type(full_type).components().empty())
     {
-      error().source_location = value.source_location();
-      error() << "cannot zero-initialize '" << to_string(full_type) << "'"
-              << eom;
-      throw 0;
+      // start with zero everywhere
+      const auto zero = zero_initializer(type, value.source_location(), *this);
+      if(!zero.has_value())
+      {
+        error().source_location = value.source_location();
+        error() << "cannot zero-initialize '" << to_string(full_type) << "'"
+                << eom;
+        throw 0;
+      }
+      result = *zero;
     }
-    result = *zero;
   }
   else if(full_type.id()==ID_array)
   {

src/linking/static_lifetime_init.cpp

@@ -65,30 +65,36 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
     return {}; // do not initialize
   }
 
-  exprt rhs;
+  optionalt<exprt> rhs;
 
   if((symbol.value.is_nil() && symbol.is_extern) ||
      symbol.value.id() == ID_nondet)
   {
     // Nondet initialise if not linked, or if explicitly requested.
     // Compilers would usually complain about the unlinked symbol case.
-    const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
-    CHECK_RETURN(nondet.has_value());
-    rhs = *nondet;
+    rhs = nondet_initializer(symbol.type, symbol.location, ns);
   }
   else if(symbol.value.is_nil())
   {
-    const auto zero = zero_initializer(symbol.type, symbol.location, ns);
-    CHECK_RETURN(zero.has_value());
-    rhs = *zero;
+    rhs = zero_initializer(symbol.type, symbol.location, ns);
   }
   else
     rhs = symbol.value;
 
-  code_assignt code(symbol.symbol_expr(), rhs);
-  code.add_source_location() = symbol.location;
+  if(rhs.has_value())
+  {
+    code_assignt code(symbol.symbol_expr(), *rhs);
+    code.add_source_location() = symbol.location;
+
+    return std::move(code);
+  }
+  else
+  {
+    code_expressiont code{typecast_exprt{symbol.symbol_expr(), empty_typet{}}};
+    code.add_source_location() = symbol.location;
 
-  return std::move(code);
+    return std::move(code);
+  }
 }
 
 void static_lifetime_init(

src/util/expr_initializer.cpp

@@ -192,6 +192,14 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
         code_value.add_source_location()=source_location;
         value.add_to_operands(std::move(code_value));
       }
+      else if(
+        c.type().id() == ID_union_tag &&
+        ns.follow_tag(to_union_tag_type(c.type())).components().empty())
+      {
+        union_exprt empty_union{irep_idt{}, nil_exprt{}, c.type()};
+        empty_union.add_source_location() = source_location;
+        value.add_to_operands(std::move(empty_union));
+      }
       else
       {
         const auto member = expr_initializer_rec(c.type(), source_location);
@@ -235,10 +243,8 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
 
     if(!found)
     {
-      // stupid empty union
-      union_exprt value(irep_idt(), nil_exprt(), type);
-      value.add_source_location() = source_location;
-      return std::move(value);
+      // empty union or no member of known size
+      return {};
     }
     else
     {