Merge pull request #5687 from tautschnig/graphml-enum

graphml-witnesses should not use enum values or typedef names

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\.]*">

regression/cbmc/graphml_witness2/main.c

@@ -1,16 +1,18 @@
+#include <stdlib.h>
+
 extern void __VERIFIER_error();
 
-static float one(float *foo)
+static size_t one(size_t *foo)
 {
   return *foo;
 }
 
-static float two(float *foo)
+static size_t two(size_t *foo)
 {
   return *foo;
 }
 
-float x = 0;
+size_t x = 0;
 
 void step()
 {

regression/cbmc/graphml_witness2/test.desc

@@ -1,10 +1,13 @@
 CORE
 main.c
---graphml-witness - --unwindset main.0:1 --unwinding-assertions
+--graphml-witness - --unwindset main.0:1 --unwinding-assertions --stack-trace
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-<data key="assumption">foo = \(\(float \*\)0\);</data>
+<data key="assumption">foo = \(\(unsigned long( long)? int \*\)0\);</data>
 <data key="assumption.scope">one</data>
 --
 ^warning: ignoring
+__CPROVER_size_t
+--
+In the GraphML witness, typedef names should be expanded.

regression/memory-analyzer/cycles/test.desc

@@ -1,7 +1,7 @@
 CORE
 cycles.gb
 --breakpoint process_buffer --symbols buffer
-cycle_buffer_entry_t tmp;
+struct cycle_buffer_entry tmp;
 char tmp\$0\[\];
 struct cycle_buffer_entry tmp\$1;
 char tmp\$2\[\];

src/ansi-c/expr2c.cpp

@@ -43,7 +43,9 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   "TRUE",
   "FALSE",
-  true
+  true,
+  false,
+  false
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -53,7 +55,9 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   "1",
   "0",
-  false
+  false,
+  true,
+  true
 };
 
 // clang-format on
@@ -196,7 +200,7 @@ std::string expr2ct::convert_rec(
 
   std::string d = declarator.empty() ? declarator : " " + declarator;
 
-  if(src.find(ID_C_typedef).is_not_nil())
+  if(!configuration.expand_typedef && src.find(ID_C_typedef).is_not_nil())
   {
     return q+id2string(src.get(ID_C_typedef))+d;
   }
@@ -1709,22 +1713,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,30 @@ 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;
+
+  /// Print the expanded type instead of a typedef name, even when a typedef is
+  /// present
+  bool expand_typedef;
+
   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,
+    const bool expand_typedef)
     : 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),
+      expand_typedef(expand_typedef)
   {
   }