replace usage of format() by debug_formatter()

Author: Daniel Kroening

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/find_symbols.h>
@@ -220,7 +220,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/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';
     }
   }

src/goto-symex/equation_conversion_exceptions.h

@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 
 #include <sstream>
 
-#include <util/format_expr.h>
+#include <util/formatter.h>
 
 #include "symex_target_equation.h"
 
@@ -28,7 +28,7 @@ class equation_conversion_exceptiont : public std::runtime_error
   {
     std::ostringstream error_msg;
     error_msg << runtime_error::what();
-    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
+    error_msg << "\nSource GOTO statement: " << debug_formatter(step.source.pc->code);
     error_msg << "\nStep:\n";
     step.output(error_msg);
     error_message = error_msg.str();

src/goto-symex/slice_by_trace.cpp

@@ -21,7 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/guard.h>
-#include <util/format_expr.h>
+#include <util/formatter.h>
 
 void symex_slice_by_tracet::slice_by_trace(
   std::string trace_files,
@@ -257,10 +257,10 @@ void symex_slice_by_tracet::compute_ts_back(
 
 #if 0
       std::cout << "EVENT:  " << event << '\n';
-      std::cout << "GUARD:  " << format(guard) << '\n';
+      std::cout << "GUARD:  " << debug_formatter(guard) << '\n';
       for(size_t j=0; j < t.size(); j++)
       {
-        std::cout << "t[" << j << "]=" << format(t[j]) <<
+        std::cout << "t[" << j << "]=" << debug_formatter(t[j]) <<
           '\n';
       }
 #endif

src/goto-symex/symex_target_equation.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
-#include <util/format_expr.h>
+#include <util/formatter.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
@@ -786,10 +786,10 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
   switch(type)
   {
   case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << format(cond_expr) << '\n';
+    out << "ASSERT " << debug_formatter(cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << format(cond_expr) << '\n';
+    out << "ASSUME " << debug_formatter(cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::LOCATION:
     out << "LOCATION" << '\n';
@@ -803,7 +803,7 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
 
   case goto_trace_stept::typet::DECL:
     out << "DECL" << '\n';
-    out << format(ssa_lhs) << '\n';
+    out << debug_formatter(ssa_lhs) << '\n';
     break;
 
   case goto_trace_stept::typet::ASSIGNMENT:
@@ -867,21 +867,21 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
     out << "MEMORY_BARRIER\n";
     break;
   case goto_trace_stept::typet::GOTO:
-    out << "IF " << format(cond_expr) << " GOTO\n";
+    out << "IF " << debug_formatter(cond_expr) << " GOTO\n";
     break;
 
   default:
     UNREACHABLE;
   }
 
   if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << format(cond_expr) << '\n';
+    out << debug_formatter(cond_expr) << '\n';
 
   if(is_assert() || is_constraint())
     out << comment << '\n';
 
   if(is_shared_read() || is_shared_write())
-    out << format(ssa_lhs) << '\n';
+    out << debug_formatter(ssa_lhs) << '\n';
 
-  out << "Guard: " << format(guard) << '\n';
+  out << "Guard: " << debug_formatter(guard) << '\n';
 }

src/pointer-analysis/dereference.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
+#include <util/formatter.h>
 #endif
 
 #include <util/std_expr.h>
@@ -37,7 +37,7 @@ exprt dereferencet::operator()(const exprt &pointer)
   const typet &type=pointer.type().subtype();
 
   #ifdef DEBUG
-  std::cout << "DEREF: " << format(pointer) << '\n';
+  std::cout << "DEREF: " << debug_formatter(pointer) << '\n';
   #endif
 
   return dereference_rec(

src/pointer-analysis/value_set.cpp

@@ -24,8 +24,7 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
-#include <util/format_type.h>
+#include <util/formatter.h>
 #endif
 
 #include "add_failed_symbols.h"
@@ -327,7 +326,7 @@ void value_sett::get_value_set(
   #if 0
   for(value_setst::valuest::const_iterator it=dest.begin();
       it!=dest.end(); it++)
-    std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
+    std::cout << "GET_VALUE_SET: " << debug_formatter(*it) << '\n';
   #endif
 }
 
@@ -352,7 +351,7 @@ void value_sett::get_value_set_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr) << "\n";
+  std::cout << "GET_VALUE_SET_REC EXPR: " << debug_formatter(expr) << "\n";
   std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
   #endif
 
@@ -884,7 +883,7 @@ void value_sett::get_value_set_rec(
   for(const auto &obj : dest.read())
   {
     const exprt &e=to_expr(obj);
-    std::cout << "  " << format(e) << "\n";
+    std::cout << "  " << debug_formatter(e) << "\n";
   }
   std::cout << "\n";
   #endif
@@ -929,7 +928,7 @@ void value_sett::get_reference_set_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
+  std::cout << "GET_REFERENCE_SET_REC EXPR: " << debug_formatter(expr)
             << '\n';
   #endif
 
@@ -956,7 +955,7 @@ void value_sett::get_reference_set_rec(
     #if 0
     for(expr_sett::const_iterator it=value_set.begin();
         it!=value_set.end(); it++)
-      std::cout << "VALUE_SET: " << format(*it) << '\n';
+      std::cout << "VALUE_SET: " << debug_formatter(*it) << '\n';
     #endif
 
     return;
@@ -1093,10 +1092,10 @@ void value_sett::assign(
   bool add_to_sets)
 {
 #if 0
-  std::cout << "ASSIGN LHS: " << format(lhs) << " : "
-            << format(lhs.type()) << '\n';
-  std::cout << "ASSIGN RHS: " << format(rhs) << " : "
-            << format(rhs.type()) << '\n';
+  std::cout << "ASSIGN LHS: " << debug_formatter(lhs) << " : "
+            << debug_formatter(lhs.type()) << '\n';
+  std::cout << "ASSIGN RHS: " << debug_formatter(rhs) << " : "
+            << debug_formatter(rhs.type()) << '\n';
   std::cout << "--------------------------------------------\n";
   output(ns, std::cout);
 #endif
@@ -1301,15 +1300,15 @@ void value_sett::assign_rec(
   bool add_to_sets)
 {
   #if 0
-  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
+  std::cout << "ASSIGN_REC LHS: " << debug_formatter(lhs) << '\n';
   std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
   std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
 
   for(object_map_dt::const_iterator it=values_rhs.read().begin();
       it!=values_rhs.read().end();
       it++)
     std::cout << "ASSIGN_REC RHS: " <<
-      format(object_numbering[it->first]) << '\n';
+      debug_formatter(object_numbering[it->first]) << '\n';
   std::cout << '\n';
   #endif
 

src/pointer-analysis/value_set_dereference.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
 #endif
 
 #include <util/arith_tools.h>
@@ -23,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
-#include <util/format_type.h>
+#include <util/formatter.h>
 #include <util/guard.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
@@ -77,7 +76,7 @@ exprt value_set_dereferencet::dereference(
   const typet &type=pointer.type().subtype();
 
   #if 0
-  std::cout << "DEREF: " << format(pointer) << '\n';
+  std::cout << "DEREF: " << debug_formatter(pointer) << '\n';
   #endif
 
   // collect objects the pointer may point to
@@ -90,7 +89,7 @@ exprt value_set_dereferencet::dereference(
       it=points_to_set.begin();
       it!=points_to_set.end();
       it++)
-    std::cout << "P: " << format(*it) << '\n';
+    std::cout << "P: " << debug_formatter(*it) << '\n';
   #endif
 
   // get the values of these
@@ -105,8 +104,8 @@ exprt value_set_dereferencet::dereference(
     valuet value=build_reference_to(*it, mode, pointer, guard);
 
     #if 0
-    std::cout << "V: " << format(value.pointer_guard) << " --> ";
-    std::cout << format(value.value) << '\n';
+    std::cout << "V: " << debug_formatter(value.pointer_guard) << " --> ";
+    std::cout << debug_formatter(value.value) << '\n';
     #endif
 
     values.push_back(value);
@@ -191,7 +190,7 @@ exprt value_set_dereferencet::dereference(
   }
 
   #if 0
-  std::cout << "R: " << format(value) << "\n\n";
+  std::cout << "R: " << debug_formatter(value) << "\n\n";
   #endif
 
   return value;
@@ -281,7 +280,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &object=o.object();
 
   #if 0
-  std::cout << "O: " << format(root_object) << '\n';
+  std::cout << "O: " << debug_formatter(root_object) << '\n';
   #endif
 
   valuet result;
@@ -561,8 +560,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         {
           std::ostringstream msg;
           msg << "memory model not applicable (got `"
-              << format(result.value.type()) << "', expected `"
-              << format(dereference_type) << "')";
+              << debug_formatter(result.value.type()) << "', expected `"
+              << debug_formatter(dereference_type) << "')";
 
           dereference_callback.dereference_failure(
             "pointer dereference", msg.str(), tmp_guard);