Merge pull request #2743 from tautschnig/boolbv-width

Fix boolbv_widtht::get_entry and fail for unknown types

Author: kroening

regression/cbmc/struct10/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct S
+{
+  int x;
+};
+
+struct T
+{
+  struct S a[2];
+};
+
+int main()
+{
+  struct T t;
+  t.a[1].x = 42;
+  assert(t.a[1].x == 42);
+  return 0;
+}

regression/cbmc/struct10/test.desc

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

src/solvers/flattening/boolbv_width.cpp

@@ -195,7 +195,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   }
   else if(type_id==ID_pointer)
     entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
-  else if(type_id==ID_symbol)
+  else if(type_id == ID_symbol_type)
     entry=get_entry(ns.follow(type));
   else if(type_id==ID_struct_tag)
     entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
@@ -209,6 +209,8 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   }
   else if(type_id==ID_string)
     entry.total_width=32;
+  else if(type_id != ID_empty)
+    UNIMPLEMENTED;
 
   return entry;
 }