graphml-witnesses should not use enum values

Make the "clean" configuration produce integers instead.

Author: tautschnig

regression/cbmc/graphml_witness1/test.desc

@@ -49,6 +49,7 @@ main.c
     <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">15</data>
+      <data key="assumption">next_field = [01];</data>
       <data key="assumption.scope">remove_one</data>
     </edge>
     <node id="[0-9\.]*">

src/ansi-c/expr2c.cpp

@@ -43,7 +43,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   "TRUE",
   "FALSE",
-  true
+  true,
+  false
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -53,7 +54,8 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   "1",
   "0",
-  false
+  false,
+  true
 };
 
 // clang-format on
@@ -1709,22 +1711,29 @@ std::string expr2ct::convert_constant(
     if(c_enum_type.id()!=ID_c_enum)
       return convert_norep(src, precedence);
 
-    const c_enum_typet::memberst &members=
-      to_c_enum_type(c_enum_type).members();
-
-    for(const auto &member : members)
+    if(!configuration.print_enum_int_value)
     {
-      if(member.get_value() == value)
-        return "/*enum*/" + id2string(member.get_base_name());
+      const c_enum_typet::memberst &members =
+        to_c_enum_type(c_enum_type).members();
+
+      for(const auto &member : members)
+      {
+        if(member.get_value() == value)
+          return "/*enum*/" + id2string(member.get_base_name());
+      }
     }
 
-    // failed...
+    // lookup failed or enum is to be output as integer
     const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
     const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
 
-    mp_integer int_value = bvrep2integer(value, width, is_signed);
+    std::string value_as_string =
+      integer2string(bvrep2integer(value, width, is_signed));
 
-    return "/*enum*/"+integer2string(int_value);
+    if(configuration.print_enum_int_value)
+      return value_as_string;
+    else
+      return "/*enum*/" + value_as_string;
   }
   else if(type.id()==ID_rational)
     return convert_norep(src, precedence);

src/ansi-c/expr2c.h

@@ -39,19 +39,24 @@ struct expr2c_configurationt final
   /// This is the string that will be printed for null pointers
   bool use_library_macros;
 
+  /// When printing an enum-typed constant, print the integer representation
+  bool print_enum_int_value;
+
   expr2c_configurationt(
     const bool include_struct_padding_components,
     const bool print_struct_body_in_type,
     const bool include_array_size,
     const std::string &true_string,
     const std::string &false_string,
-    const bool use_library_macros)
+    const bool use_library_macros,
+    const bool print_enum_int_value)
     : include_struct_padding_components(include_struct_padding_components),
       print_struct_body_in_type(print_struct_body_in_type),
       include_array_size(include_array_size),
       true_string(true_string),
       false_string(false_string),
-      use_library_macros(use_library_macros)
+      use_library_macros(use_library_macros),
+      print_enum_int_value(print_enum_int_value)
   {
   }