From d8b34f25c84358738994bf45b374527080a049bf Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 17 Feb 2019 11:23:03 +0000
Subject: [PATCH 1/2] Fix C enum JSON output

The subtype must be used.
---
 regression/cbmc/enum-trace1/main.c         | 23 ++++++++++++++++++++++
 regression/cbmc/enum-trace1/test_json.desc | 11 +++++++++++
 src/goto-programs/json_expr.cpp            |  6 +++++-
 3 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/enum-trace1/main.c
 create mode 100644 regression/cbmc/enum-trace1/test_json.desc

diff --git a/regression/cbmc/enum-trace1/main.c b/regression/cbmc/enum-trace1/main.c
new file mode 100644
index 00000000000..b4e8ce48d74
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc
new file mode 100644
index 00000000000..e26c6134123
--- /dev/null
+++ b/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
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 85784628334..161ffcc63d2 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/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);
 }

From 7fa0f97715a1a4a4f859d8f6195213f42b1cfcf5 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 17 Feb 2019 11:23:21 +0000
Subject: [PATCH 2/2] Fix C enum XML output

bvrep2integer must be used.
---
 regression/cbmc/enum-trace1/test_xml.desc | 11 +++++++++++
 src/goto-programs/xml_expr.cpp            |  9 +++------
 2 files changed, 14 insertions(+), 6 deletions(-)
 create mode 100644 regression/cbmc/enum-trace1/test_xml.desc

diff --git a/regression/cbmc/enum-trace1/test_xml.desc b/regression/cbmc/enum-trace1/test_xml.desc
new file mode 100644
index 00000000000..47e98cf549d
--- /dev/null
+++ b/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
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index 91ea790fada..0d419150429 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/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)
     {