Introduce expression/type formatting functor

src/analyses/constant_propagator.cpp

@@ -13,7 +13,7 @@ Author: Peter Schrammel
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
+#include <util/formatter.h>
 #endif
 
 #include <util/ieee_float.h>
@@ -223,7 +223,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
   const namespacet &ns)
 {
 #ifdef DEBUG
-  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
+  std::cout << "two_way_propagate_rec: " << debug_formatter(expr) << '\n';
 #endif
 
   bool change=false;

src/ansi-c/Makefile

@@ -2,6 +2,7 @@ SRC = anonymous_member.cpp \
       ansi_c_convert_type.cpp \
       ansi_c_declaration.cpp \
       ansi_c_entry_point.cpp \
+      ansi_c_formatter.cpp \
       ansi_c_internal_additions.cpp \
       ansi_c_language.cpp \
       ansi_c_lex.yy.cpp \

src/ansi-c/ansi_c_formatter.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "ansi_c_formatter.h"
+
+#include "expr2c.h"
+
+#include <ostream>
+
+std::ostream &ansi_c_formattert::format(std::ostream &os, const exprt &expr)
+{
+  return os << expr2c(expr, ns);
+}
+
+std::ostream &ansi_c_formattert::format(std::ostream &os, const typet &type)
+{
+  return os << type2c(type, ns);
+}
+
+std::ostream &
+ansi_c_formattert::format(std::ostream &os, const source_locationt &loc)
+{
+  return os << loc;
+}

src/ansi-c/ansi_c_formatter.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_FORMATTER_H
+#define CPROVER_ANSI_C_FORMATTER_H
+
+#include <util/formatter.h>
+
+class ansi_c_formattert : public formattert
+{
+public:
+  explicit ansi_c_formattert(const namespacet &_ns) : ns(_ns)
+  {
+  }
+
+  std::ostream &format(std::ostream &, const exprt &) override;
+  std::ostream &format(std::ostream &, const typet &) override;
+  std::ostream &format(std::ostream &, const source_locationt &) override;
+
+  const namespacet &ns;
+};
+
+#endif // CPROVER_ANSI_C_FORMATTER_H

src/cbmc/cbmc_parse_options.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include <ansi-c/c_preprocess.h>
+#include <ansi-c/ansi_c_formatter.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -595,7 +596,9 @@ int cbmc_parse_optionst::get_goto_program(
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      namespacet ns(goto_model.symbol_table);
+      ansi_c_formattert formatter(ns);
+      show_symbol_table(goto_model, ui_message_handler.get_ui(), formatter);
       return CPROVER_EXIT_SUCCESS;
     }
 

src/cpp/Makefile

@@ -6,6 +6,7 @@ SRC = cpp_constructor.cpp \
       cpp_destructor.cpp \
       cpp_enum_type.cpp \
       cpp_exception_id.cpp \
+      cpp_formatter.cpp \
       cpp_id.cpp \
       cpp_instantiate_template.cpp \
       cpp_internal_additions.cpp \

src/cpp/cpp_formatter.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "cpp_formatter.h"
+
+#include "expr2cpp.h"
+
+#include <ostream>
+
+std::ostream &cpp_formattert::format(std::ostream &os, const exprt &expr)
+{
+  return os << expr2cpp(expr, ns);
+}
+
+std::ostream &cpp_formattert::format(std::ostream &os, const typet &type)
+{
+  return os << type2cpp(type, ns);
+}
+
+std::ostream &
+cpp_formattert::format(std::ostream &os, const source_locationt &loc)
+{
+  return os << loc;
+}

src/cpp/cpp_formatter.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPP_FORMATTER_H
+#define CPROVER_CPP_FORMATTER_H
+
+#include <util/formatter.h>
+
+class cpp_formattert : public formattert
+{
+public:
+  explicit cpp_formattert(const namespacet &_ns) : ns(_ns)
+  {
+  }
+
+  std::ostream &format(std::ostream &, const exprt &) override;
+  std::ostream &format(std::ostream &, const typet &) override;
+  std::ostream &format(std::ostream &, const source_locationt &) override;
+
+  const namespacet &ns;
+};
+
+#endif // CPROVER_CPP_FORMATTER_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/json.h>
 #include <util/exit_codes.h>
 
+#include <ansi-c/ansi_c_formatter.h>
+
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_calls_no_body.h>
@@ -463,7 +465,9 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-symbol-table"))
     {
-      ::show_symbol_table(goto_model, get_ui());
+      namespacet ns(goto_model.symbol_table);
+      ansi_c_formattert formatter(ns);
+      ::show_symbol_table(goto_model, get_ui(), formatter);
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-programs/generate_function_bodies.cpp

@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 #include "generate_function_bodies.h"
 
 #include <util/arith_tools.h>
-#include <util/format_expr.h>
+#include <util/formatter.h>
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
@@ -102,7 +102,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
     const namespacet ns(symbol_table);
     std::ostringstream comment_stream;
     comment_stream << id2string(ID_assertion) << " "
-                   << format(assert_instruction->guard);
+                   << debug_formatter(assert_instruction->guard);
     assert_instruction->source_location.set_comment(comment_stream.str());
     assert_instruction->source_location.set_property_class(ID_assertion);
     auto end_instruction = add_instruction();
@@ -134,7 +134,7 @@ class assert_false_then_assume_false_generate_function_bodiest
     const namespacet ns(symbol_table);
     std::ostringstream comment_stream;
     comment_stream << id2string(ID_assertion) << " "
-                   << format(assert_instruction->guard);
+                   << debug_formatter(assert_instruction->guard);
     assert_instruction->source_location.set_comment(comment_stream.str());
     assert_instruction->source_location.set_property_class(ID_assertion);
     auto assume_instruction = add_instruction();
@@ -203,7 +203,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
           bool constant_known_array_size = lhs_array_type.size().is_constant();
           if(!constant_known_array_size)
           {
-            warning() << "Cannot havoc non-const array " << format(lhs)
+            warning() << "Cannot havoc non-const array " << debug_formatter(lhs)
                       << " in function " << function_name
                       << ": Unknown array size" << eom;
           }
@@ -219,7 +219,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
               // Pretty much the same thing as a unknown size array
               // Technically not allowed by the C standard, but we model
               // unknown size arrays in structs this way
-              warning() << "Cannot havoc non-const array " << format(lhs)
+              warning() << "Cannot havoc non-const array " << debug_formatter(lhs)
                         << " in function " << function_name << ": Array size 0"
                         << eom;
             }

src/goto-programs/goto_trace.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening
 #include <ostream>
 
 #include <util/arith_tools.h>
-#include <util/format_expr.h>
+#include <util/formatter.h>
 #include <util/symbol.h>
 
 #include <ansi-c/printf_formatter.h>
@@ -74,8 +74,8 @@ void goto_trace_stept::output(
 
   if(is_assignment())
   {
-    out << "  " << format(full_lhs)
-        << " = " << format(full_lhs_value)
+    out << "  " << debug_formatter(full_lhs)
+        << " = " << debug_formatter(full_lhs_value)
         << '\n';
   }
 
@@ -95,7 +95,7 @@ void goto_trace_stept::output(
       if(!comment.empty())
         out << "  " << comment << '\n';
 
-      out << "  " << format(pc->guard) << '\n';
+      out << "  " << debug_formatter(pc->guard) << '\n';
       out << '\n';
     }
   }