Support enum-typed constants in format_expr

We should not have to fall back to irept pretty printing for these.

Author: tautschnig

regression/cbmc/enum_is_in_range/format.desc

@@ -0,0 +1,10 @@
+CORE
+no_duplicate.c
+--show-goto-functions
+main::1::e = 0 ∨ main::1::e = 1 ∨ main::1::e = 2 ∨ main::1::e = 3
+^EXIT=0$
+^SIGNAL=0$
+--
+type: c_enum_tag
+--
+This test is to show that format(expr) also works for enum-typed constants.

regression/cbmc/enum_is_in_range/no_duplicate.c

@@ -0,0 +1,19 @@
+enum enm
+{
+  first,
+  second,
+  third,
+  fourth,
+};
+
+static enum enm efunc(void)
+{
+  return second;
+}
+
+int main(void)
+{
+  enum enm e = efunc();
+  __CPROVER_assert(__CPROVER_enum_is_in_range(e), "enum failure");
+  return (e);
+}

src/util/format_expr.cpp

@@ -204,6 +204,10 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
                 << format(pointer_type.base_type()) << ')';
     }
   }
+  else if(type == ID_c_enum_tag)
+  {
+    return os << string2integer(id2string(src.get_value()), 16);
+  }
   else
     return os << src.pretty();
 }