Fix C enum XML output

bvrep2integer must be used.

Author: peterschrammel

regression/cbmc/enum-trace1/test_xml.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--xml-ui --function test --trace
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+VERIFICATION FAILED
+<input hidden="false" step_nr="\d+" thread="0">\n\s*<input_id>e</input_id>\n\s*<value>.*E(1|2|3)</value>\n\s*<value_expression>\n\s*<integer binary="000000000000000000000000000000(0|1){2}" c_type="enum" width="32">(0|1|2)</integer>\n\s*</value_expression>
+<input hidden="false" step_nr="\d+" thread="0">\n\s*<input_id>t</input_id>\n\s*<value>.*T(1|2|3)</value>\n\s*<value_expression>\n\s*<integer binary="000000000000000000000000000000(0|1){2}" c_type="enum" width="32">(0|1|2)</integer>\n\s*</value_expression>
+--
+^warning: ignoring

src/goto-programs/xml_expr.cpp

@@ -179,16 +179,13 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       const auto width =
         to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
 
+      const auto integer_value = bvrep2integer(value, width, false);
       result.name = "integer";
-      result.set_attribute(
-        "binary",
-        integer2binary(numeric_cast_v<mp_integer>(constant_expr), width));
+      result.set_attribute("binary", integer2binary(integer_value, width));
       result.set_attribute("width", width);
       result.set_attribute("c_type", "enum");
 
-      mp_integer i;
-      if(!to_integer(constant_expr, i))
-        result.data = integer2string(i);
+      result.data = integer2string(integer_value);
     }
     else if(type.id() == ID_c_enum_tag)
     {