Merge pull request #3305 from tautschnig/expr2bits

to_bitvector_type must not be used on enum types

Author: tautschnig

regression/cbmc/enum7/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+enum E
+{
+  A = 1,
+  B = 2
+};
+
+int main()
+{
+  enum E array[2] = {A, B};
+  unsigned *p = array;
+  assert(*p == 1);
+  return 0;
+}

regression/cbmc/enum7/test.desc

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

src/util/simplify_expr.cpp

@@ -1558,25 +1558,34 @@ optionalt<std::string> simplify_exprt::expr2bits(
 
   if(expr.id()==ID_constant)
   {
+    const auto &value = to_constant_expr(expr).get_value();
+
     if(type.id()==ID_unsignedbv ||
        type.id()==ID_signedbv ||
-       type.id()==ID_c_enum ||
-       type.id()==ID_c_enum_tag ||
        type.id()==ID_floatbv ||
        type.id()==ID_fixedbv)
     {
       const auto width = to_bitvector_type(type).get_width();
-      const auto &bvrep = to_constant_expr(expr).get_value();
 
       endianness_mapt map(type, little_endian, ns);
 
       std::string result(width, ' ');
 
       for(std::string::size_type i = 0; i < width; ++i)
-        result[map.map_bit(i)] = get_bvrep_bit(bvrep, width, i) ? '1' : '0';
+        result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
 
       return result;
     }
+    else if(type.id() == ID_c_enum_tag)
+    {
+      const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
+      return expr2bits(constant_exprt(value, c_enum_type), little_endian);
+    }
+    else if(type.id() == ID_c_enum)
+    {
+      return expr2bits(
+        constant_exprt(value, to_c_enum_type(type).subtype()), little_endian);
+    }
   }
   else if(expr.id()==ID_union)
   {