Merge pull request #6653 from tautschnig/bugfixes/empty-struct

Support byte-extracting empty structs

Author: kroening

regression/cbmc/empty_compound_type4/main.c

@@ -0,0 +1,21 @@
+struct empty
+{
+};
+
+struct non_empty
+{
+  int x;
+};
+
+union U
+{
+  struct empty e;
+  struct non_empty n;
+};
+
+int main()
+{
+  union U u;
+  struct empty e = u.e;
+  __CPROVER_assert(0, "dummy assertion");
+}

regression/cbmc/empty_compound_type4/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+main.c
+--trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed
+--
+Byte-extracting (which is what union operations yield) an empty struct should
+not result in a conversion warning in the flattening back-end.

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -59,9 +59,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
   #endif
 
-  if(width==0)
-    return conversion_failed(expr);
-
   // see if the byte number is constant and within bounds, else work from the
   // root object
   const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);