From d33628e8545d4f26036e81d034a5901412965821 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 15 Aug 2018 14:50:43 +0000
Subject: [PATCH] Fix boolbv_widtht::get_entry and fail for unknown types

It was missing the ID_symbol -> ID_symbol_type change. To guard for future bugs
of this kind, add a catch-all "UNIMPLEMENTED" as final branch.
---
 regression/cbmc/struct10/main.c         | 19 +++++++++++++++++++
 regression/cbmc/struct10/test.desc      |  8 ++++++++
 src/solvers/flattening/boolbv_width.cpp |  4 +++-
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/struct10/main.c
 create mode 100644 regression/cbmc/struct10/test.desc

diff --git a/regression/cbmc/struct10/main.c b/regression/cbmc/struct10/main.c
new file mode 100644
index 00000000000..a288fafb08f
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/struct10/test.desc b/regression/cbmc/struct10/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/struct10/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 25f7c1d29e1..16dfabf59a6 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/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;
 }