Fix C enum JSON output

The subtype must be used.

Author: peterschrammel

regression/cbmc/enum-trace1/main.c

@@ -0,0 +1,18 @@
+#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

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