Merge pull request #3195 from diffblue/goto-trace-colors

Goto trace colors

Author: tautschnig

src/goto-programs/goto_trace.cpp

@@ -82,7 +82,7 @@ void goto_trace_stept::output(
   }
 
   if(is_assert() || is_assume() || is_goto())
-    out << " (" << cond_value << ")";
+    out << " (" << cond_value << ')';
   else if(is_function_call() || is_function_return())
     out << ' ' << function_identifier;
 
@@ -233,7 +233,7 @@ std::string trace_numeric_value(
 }
 
 void trace_value(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,
@@ -245,49 +245,44 @@ void trace_value(
   if(lhs_object.has_value())
     identifier=lhs_object->get_identifier();
 
-  std::string value_string;
+  out << "  " << from_expr(ns, identifier, full_lhs) << '=';
 
   if(value.is_nil())
-    value_string="(assignment removed)";
+    out << "(assignment removed)";
   else
   {
-    value_string=from_expr(ns, identifier, value);
+    out << from_expr(ns, identifier, value);
 
     // the binary representation
-    value_string += " (" + trace_numeric_value(value, ns, options) + ")";
+    out << ' ' << messaget::faint << '('
+        << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
   }
 
-  out << "  "
-      << from_expr(ns, identifier, full_lhs)
-      << "=" << value_string
-      << "\n";
+  out << '\n';
 }
 
 void show_state_header(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const goto_trace_stept &state,
   const source_locationt &source_location,
   unsigned step_nr,
   const trace_optionst &options)
 {
-  out << "\n";
+  out << '\n';
 
   if(step_nr == 0)
     out << "Initial State";
   else
     out << "State " << step_nr;
 
-  out << " " << source_location << " thread " << state.thread_nr << "\n";
-  out << "----------------------------------------------------"
-      << "\n";
+  out << ' ' << source_location << " thread " << state.thread_nr << '\n';
+  out << "----------------------------------------------------" << '\n';
 
   if(options.show_code)
   {
-    out << as_string(ns, *state.pc)
-        << "\n";
-    out << "----------------------------------------------------"
-        << "\n";
+    out << as_string(ns, *state.pc) << '\n';
+    out << "----------------------------------------------------" << '\n';
   }
 }
 
@@ -304,7 +299,7 @@ bool is_index_member_symbol(const exprt &src)
 }
 
 void show_full_goto_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const goto_tracet &goto_trace,
   const trace_optionst &options)
@@ -324,33 +319,33 @@ void show_full_goto_trace(
     case goto_trace_stept::typet::ASSERT:
       if(!step.cond_value)
       {
-        out << "\n";
-        out << "Violated property:" << "\n";
+        out << '\n';
+        out << messaget::red << "Violated property:" << messaget::reset << '\n';
         if(!step.pc->source_location.is_nil())
-          out << "  " << step.pc->source_location << "\n";
-        out << "  " << step.comment << "\n";
+          out << "  " << step.pc->source_location << '\n';
+        out << "  " << messaget::red << step.comment << messaget::reset << '\n';
 
         if(step.pc->is_assert())
           out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
               << '\n';
 
-        out << "\n";
+        out << '\n';
       }
       break;
 
     case goto_trace_stept::typet::ASSUME:
       if(!step.cond_value)
       {
-        out << "\n";
-        out << "Violated assumption:" << "\n";
+        out << '\n';
+        out << "Violated assumption:" << '\n';
         if(!step.pc->source_location.is_nil())
-          out << "  " << step.pc->source_location << "\n";
+          out << "  " << step.pc->source_location << '\n';
 
         if(step.pc->is_assume())
           out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
               << '\n';
 
-        out << "\n";
+        out << '\n';
       }
       break;
 
@@ -403,50 +398,50 @@ void show_full_goto_trace(
         printf_formattert printf_formatter(ns);
         printf_formatter(id2string(step.format_string), step.io_args);
         printf_formatter.print(out);
-        out << "\n";
+        out << '\n';
       }
       else
       {
         show_state_header(
           out, ns, step, step.pc->source_location, step.step_nr, options);
-        out << "  OUTPUT " << step.io_id << ":";
+        out << "  OUTPUT " << step.io_id << ':';
 
         for(std::list<exprt>::const_iterator
             l_it=step.io_args.begin();
             l_it!=step.io_args.end();
             l_it++)
         {
           if(l_it!=step.io_args.begin())
-            out << ";";
-          out << " " << from_expr(ns, step.pc->function, *l_it);
+            out << ';';
+          out << ' ' << from_expr(ns, step.pc->function, *l_it);
 
           // the binary representation
-          out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
+          out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
         }
 
-        out << "\n";
+        out << '\n';
       }
       break;
 
     case goto_trace_stept::typet::INPUT:
       show_state_header(
         out, ns, step, step.pc->source_location, step.step_nr, options);
-      out << "  INPUT " << step.io_id << ":";
+      out << "  INPUT " << step.io_id << ':';
 
       for(std::list<exprt>::const_iterator
           l_it=step.io_args.begin();
           l_it!=step.io_args.end();
           l_it++)
       {
         if(l_it!=step.io_args.begin())
-          out << ";";
-        out << " " << from_expr(ns, step.pc->function, *l_it);
+          out << ';';
+        out << ' ' << from_expr(ns, step.pc->function, *l_it);
 
         // the binary representation
-        out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
+        out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
       }
 
-      out << "\n";
+      out << '\n';
       break;
 
     case goto_trace_stept::typet::FUNCTION_CALL:
@@ -497,7 +492,7 @@ void show_full_goto_trace(
 }
 
 void show_goto_stack_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const goto_tracet &goto_trace,
   const trace_optionst &options)
@@ -573,7 +568,7 @@ void show_goto_stack_trace(
 }
 
 void show_goto_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const goto_tracet &goto_trace,
   const trace_optionst &options)
@@ -585,7 +580,7 @@ void show_goto_trace(
 }
 
 void show_goto_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &ns,
   const goto_tracet &goto_trace)
 {

src/goto-programs/goto_trace.h

@@ -17,6 +17,7 @@ Date: July 2005
 #include <iosfwd>
 #include <vector>
 
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/options.h>
 #include <util/ssa_expr.h>
@@ -223,18 +224,18 @@ struct trace_optionst
 };
 
 void show_goto_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &,
   const goto_tracet &);
 
 void show_goto_trace(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &,
   const goto_tracet &,
   const trace_optionst &);
 
 void trace_value(
-  std::ostream &out,
+  messaget::mstreamt &out,
   const namespacet &,
   const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,