Do not attempt to compute union sizes when not required

Packed unions/structs without alignment specification may use fields of
dynamic size. It is then unnecessary to compute their full size as it
would never be used anyway.

Author: Daniel Kroening

regression/ansi-c/Union_Padding2/main.c

@@ -0,0 +1,34 @@
+static unsigned bar()
+{
+  unsigned r;
+  return r;
+}
+
+#ifdef _MSC_VER
+
+static void foo()
+{
+}
+
+#else
+
+static void foo()
+{
+ unsigned len=bar();
+ struct {
+   int a;
+   union {
+     int s;
+     unsigned char b[len];
+   } __attribute__ (( packed )) S;
+   int c;
+ } __attribute__ (( packed )) *l;
+}
+
+#endif
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/ansi-c/Union_Padding2/test.desc

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

regression/cbmc/dynamic_sizeof1/main.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+
+  if(x>=0 && x<=1000)
+  {
+    struct
+    {
+      int asd;
+
+      union {
+        int i;
+        char array[x];
+      };
+    } *ptr;
+
+    if(x<=sizeof(int))
+      assert(sizeof(*ptr)==sizeof(int)*2);
+    else
+      assert(sizeof(*ptr)==sizeof(int)+x);
+  }
+}

regression/cbmc/dynamic_sizeof1/test.desc

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

src/ansi-c/padding.cpp

@@ -303,36 +303,40 @@ void add_padding(struct_typet &type, const namespacet &ns)
 
 void add_padding(union_typet &type, const namespacet &ns)
 {
-  mp_integer max_alignment=alignment(type, ns)*8;
-  mp_integer size_bits=pointer_offset_bits(type, ns);
+  mp_integer max_alignment_bits=alignment(type, ns)*8;
+  mp_integer size_bits=0;
 
-  if(size_bits<0)
-    throw "type of unknown size:\n"+type.pretty();
-
-  union_typet::componentst &components=type.components();
+  // check per component, and ignore those without fixed size
+  for(const auto &c : type.components())
+  {
+    mp_integer s=pointer_offset_bits(c.type(), ns);
+    if(s>0)
+      size_bits=std::max(size_bits, s);
+  }
 
   // Is the union packed?
   if(type.get_bool(ID_C_packed))
   {
-    // The size needs to be a multiple of 8 only.
-    max_alignment=8;
+    // The size needs to be a multiple of 8 bits only.
+    max_alignment_bits=8;
   }
 
   // The size must be a multiple of the alignment, or
   // we add a padding member to the union.
 
-  if(size_bits%max_alignment!=0)
+  if(size_bits%max_alignment_bits!=0)
   {
-    mp_integer padding=max_alignment-(size_bits%max_alignment);
+    mp_integer padding_bits=
+      max_alignment_bits-(size_bits%max_alignment_bits);
 
     unsignedbv_typet padding_type;
-    padding_type.set_width(integer2unsigned(size_bits+padding));
+    padding_type.set_width(integer2size_t(size_bits+padding_bits));
 
     struct_typet::componentt component;
     component.type()=padding_type;
     component.set_name("$pad");
     component.set_is_padding(true);
 
-    components.push_back(component);
+    type.components().push_back(component);
   }
 }