Expression initialiser: do not generate nil for empty union

Empty unions do not have a meaningful union_exprt as an initialiser, and
thus the expression initialiser should make use of returning an
optionalt{} instead.

This test was generated using C-Reduce based on an example initially
generated by CSmith.

Author: tautschnig

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,17 @@
+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/linking/static_lifetime_init.cpp

@@ -68,30 +68,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

@@ -193,6 +193,13 @@ 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);
@@ -236,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
     {