Merge pull request #5611 from tautschnig/enum-dump-c

C front-end: printing enum type declarations with bitvector awareness

Author: kroening

regression/goto-instrument/dump-enum/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+enum hex
+{
+  V1 = 0x1,
+  V10 = 0xA,
+  V11 = 11
+};
+
+int main()
+{
+  enum hex h = V10;
+  assert(0xca == (unsigned char)(char)0b11001010);
+}

regression/goto-instrument/dump-enum/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dump-c
+enum hex \{ .* \};
+h=/\*enum\*/V10;
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test must pass running CBMC on the output generated using dump-c to
+demonstrate that the enum output wouldn't generate A and B (just those
+characters, no quotes or 0x prefix) instead of 10 and 11, respectively.

src/ansi-c/expr2c.cpp

@@ -378,21 +378,27 @@ std::string expr2ct::convert_rec(
 
     if(!to_c_enum_type(src).is_incomplete())
     {
+      const c_enum_typet &c_enum_type = to_c_enum_type(src);
+      const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
+      const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
+
       result += '{';
 
       // add members
-      const c_enum_typet::memberst &members = to_c_enum_type(src).members();
+      const c_enum_typet::memberst &members = c_enum_type.members();
 
       for(c_enum_typet::memberst::const_iterator it = members.begin();
           it != members.end();
           it++)
       {
+        mp_integer int_value = bvrep2integer(it->get_value(), width, is_signed);
+
         if(it != members.begin())
           result += ',';
         result += ' ';
         result += id2string(it->get_base_name());
         result += '=';
-        result += id2string(it->get_value());
+        result += integer2string(int_value);
       }
 
       result += " }";
@@ -1703,24 +1709,21 @@ std::string expr2ct::convert_constant(
     if(c_enum_type.id()!=ID_c_enum)
       return convert_norep(src, precedence);
 
-    const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
-    const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
-
-    mp_integer int_value = bvrep2integer(value, width, is_signed);
-    mp_integer i=0;
-
-    irep_idt int_value_string=integer2string(int_value);
-
     const c_enum_typet::memberst &members=
       to_c_enum_type(c_enum_type).members();
 
     for(const auto &member : members)
     {
-      if(member.get_value() == int_value_string)
+      if(member.get_value() == value)
         return "/*enum*/" + id2string(member.get_base_name());
     }
 
     // failed...
+    const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
+    const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
+
+    mp_integer int_value = bvrep2integer(value, width, is_signed);
+
     return "/*enum*/"+integer2string(int_value);
   }
   else if(type.id()==ID_rational)