Merge pull request #4226 from peterschrammel/fix-c-enum-output

Fix C enum output

Author: peterschrammel

regression/cbmc/enum-trace1/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+enum ENUM
+{
+  E1,
+  E2,
+  E3
+};
+
+typedef enum ENUMT
+{
+  T1,
+  T2,
+  T3
+} enum_t;
+
+void test(enum ENUM e, enum_t t)
+{
+  enum ENUM ee = e;
+  enum_t tt = t;
+
+  assert(ee != tt);
+}

regression/cbmc/enum-trace1/test_json.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--json-ui --function test --trace
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+VERIFICATION FAILED
+\{\n\s*"hidden": false,\n\s*"inputID": "e",\n\s*"internal": true,\n\s*"mode": "C",\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"stepType": "input",\n\s*"thread": 0,\n\s*"values": \[\n\s*\{\n\s*"binary": "000000000000000000000000000000(0|1){2}",\n\s*"data": ".*E(1|2|3)",\n\s*"name": "integer",\n\s*"type": "enum",\n\s*"width": 32\n\s*\}\n\s*\]\n\s*\},
+\{\n\s*"hidden": false,\n\s*"inputID": "t",\n\s*"internal": true,\n\s*"mode": "C",\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"stepType": "input",\n\s*"thread": 0,\n\s*"values": \[\n\s*\{\n\s*"binary": "000000000000000000000000000000(0|1){2}",\n\s*"data": ".*T(1|2|3)",\n\s*"name": "integer",\n\s*"type": "enum",\n\s*"width": 32\n\s*\}\n\s*\]\n\s*\},
+--
+^warning: ignoring

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/json_expr.cpp

@@ -206,7 +206,11 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
 
 static std::string binary(const constant_exprt &src)
 {
-  const auto width = to_bitvector_type(src.type()).get_width();
+  std::size_t width;
+  if(src.type().id() == ID_c_enum)
+    width = to_bitvector_type(to_c_enum_type(src.type()).subtype()).get_width();
+  else
+    width = to_bitvector_type(src.type()).get_width();
   const auto int_val = bvrep2integer(src.get_value(), width, false);
   return integer2binary(int_val, width);
 }

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)
     {