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 = 1 ∨ main::1::e = 2 ∨ main::1::e = 4 ∨ main::1::e = 8
+^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 = 1,
+  second = 1 << 1,
+  third = 1 << 2,
+  fourth = 1 << 3,
+};
+
+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);
+}

regression/validate-trace-xml-schema/check.py

@@ -25,6 +25,7 @@
     ['integer-assignments1', 'integer-typecheck.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
+    ['enum_is_in_range', 'format.desc'],
     ['r_w_ok9', 'simplify.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
     # this one wants show-properties instead producing a trace

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();
 }