Expand typedef names in GraphML output

typedefs are not meaningful when taken out of context.

Author: tautschnig

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

@@ -44,6 +44,7 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   "TRUE",
   "FALSE",
   true,
+  false,
   false
 };
 
@@ -55,6 +56,7 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   "1",
   "0",
   false,
+  true,
   true
 };
 
@@ -198,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;
   }

src/ansi-c/expr2c.h

@@ -42,21 +42,27 @@ struct expr2c_configurationt final
   /// 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 print_enum_int_value)
+    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),
-      print_enum_int_value(print_enum_int_value)
+      print_enum_int_value(print_enum_int_value),
+      expand_typedef(expand_typedef)
   {
   }