Replace all uses of goto_programt::output_instruction

src/analyses/ai.cpp

@@ -43,6 +43,8 @@ void ai_baset::output(
   const goto_programt &goto_program,
   std::ostream &out) const
 {
+  (void)function_id; // unused parameter
+
   forall_goto_program_instructions(i_it, goto_program)
   {
     out << "**** " << i_it->location_number << " " << i_it->source_location()
@@ -51,7 +53,7 @@ void ai_baset::output(
     abstract_state_before(i_it)->output(out, *this, ns);
     out << "\n";
     #if 1
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
     out << "\n";
     #endif
   }
@@ -84,13 +86,15 @@ jsont ai_baset::output_json(
   const irep_idt &function_id,
   const goto_programt &goto_program) const
 {
+  (void)function_id; // unused parameter
+
   json_arrayt contents;
 
   forall_goto_program_instructions(i_it, goto_program)
   {
     // Ideally we need output_instruction_json
     std::ostringstream out;
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
 
     json_objectt location{
       {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
@@ -135,6 +139,8 @@ xmlt ai_baset::output_xml(
   const irep_idt &function_id,
   const goto_programt &goto_program) const
 {
+  (void)function_id; // unused parameter
+
   xmlt function_body;
 
   forall_goto_program_instructions(i_it, goto_program)
@@ -147,7 +153,7 @@ xmlt ai_baset::output_xml(
 
     // Ideally we need output_instruction_xml
     std::ostringstream out;
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
     location.set_attribute("instruction", out.str());
 
     function_body.new_element(location);

src/analyses/flow_insensitive_analysis.cpp

@@ -173,16 +173,16 @@ bool flow_insensitive_analysis_baset::visit(
 //  if (id2string(l->function).find("debug")!=std::string::npos)
 //    std::cout << l->function << '\n'; //=="messages::debug")
 
-//  {
-//    static unsigned state_cntr=0;
-//    std::string s("pastate"); s += std::to_string(state_cntr);
-//    std::ofstream f(s.c_str());
-//    goto_program.output_instruction(ns, "", f, l);
-//    f << '\n';
-//    get_state().output(ns, f);
-//    f.close();
-//    state_cntr++;
-//  }
+  //  {
+  //    static unsigned state_cntr=0;
+  //    std::string s("pastate"); s += std::to_string(state_cntr);
+  //    std::ofstream f(s.c_str());
+  //    l->output(f);
+  //    f << '\n';
+  //    get_state().output(ns, f);
+  //    f.close();
+  //    state_cntr++;
+  //  }
 
   return new_data;
 }

src/analyses/local_bitvector_analysis.cpp

@@ -365,7 +365,7 @@ void local_bitvector_analysist::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << "\n";
 
     l++;

src/analyses/local_may_alias.cpp

@@ -497,7 +497,7 @@ void local_may_aliast::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << "\n";
 
     l++;

src/analyses/local_safe_pointers.cpp

@@ -217,7 +217,7 @@ void local_safe_pointerst::output(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << '\n';
   }
 }
@@ -268,7 +268,7 @@ void local_safe_pointerst::output_safe_dereferences(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << '\n';
   }
 }

src/analyses/sese_regions.cpp

@@ -221,7 +221,7 @@ static std::string brief_instruction_string(
     &program_relative_instruction_indices)
 {
   std::ostringstream ostr;
-  goto_program.output_instruction(ns, "", ostr, *instruction);
+  instruction->output(ostr);
   return instruction_ordinals(
            instruction, program_relative_instruction_indices) +
          " " + trimmed_last_line(ostr.str());

src/analyses/static_analysis.cpp

@@ -94,7 +94,7 @@ void static_analysis_baset::output(
     get_state(i_it).output(ns, out);
     out << "\n";
     #if 0
-    goto_program.output_instruction(ns, identifier, out, i_it);
+    i_it->output(out);
     out << "\n";
     #endif
   }

src/goto-analyzer/unreachable_instructions.cpp

@@ -75,7 +75,7 @@ static void output_dead_plain(
   for(dead_mapt::const_iterator it=dead_map.begin();
       it!=dead_map.end();
       ++it)
-    goto_program.output_instruction(ns, function_identifier, os, *it->second);
+    it->second->output(os);
 }
 
 static void add_to_xml(
@@ -136,7 +136,7 @@ static void add_to_json(
       ++it)
   {
     std::ostringstream oss;
-    goto_program.output_instruction(ns, function_identifier, oss, *it->second);
+    it->second->output(oss);
     std::string s=oss.str();
 
     std::string::size_type n=s.find('\n');

src/goto-diff/change_impact.cpp

@@ -284,7 +284,6 @@ class change_impactt
     char prefix,
     const goto_programt &goto_program,
     const namespacet &ns,
-    const irep_idt &function_id,
     goto_programt::const_targett &target) const;
 };
 
@@ -606,7 +605,7 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, ns, function_id, target);
+    output_instruction(prefix, goto_program, ns, target);
   }
 }
 
@@ -644,7 +643,7 @@ void change_impactt::output_change_impact(
 
     if(old_mod_flags&DELETED)
     {
-      output_instruction('-', goto_program, o_ns, function_id, o_target);
+      output_instruction('-', goto_program, o_ns, o_target);
       ++o_target;
       --target;
       continue;
@@ -696,7 +695,7 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, n_ns, function_id, target);
+    output_instruction(prefix, goto_program, n_ns, target);
   }
   for( ;
       o_target!=old_goto_program.instructions.end();
@@ -724,15 +723,14 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, o_ns, function_id, o_target);
+    output_instruction(prefix, goto_program, o_ns, o_target);
   }
 }
 
 void change_impactt::output_instruction(
   char prefix,
   const goto_programt &goto_program,
   const namespacet &ns,
-  const irep_idt &function_id,
   goto_programt::const_targett &target) const
 {
   if(compact_output)
@@ -748,7 +746,7 @@ void change_impactt::output_instruction(
   else
   {
     std::cout << prefix;
-    goto_program.output_instruction(ns, function_id, std::cout, *target);
+    target->output(std::cout);
   }
 }
 

src/goto-diff/unified_diff.cpp

@@ -130,15 +130,15 @@ void unified_difft::output_diff(
     {
     case differencet::SAME:
       os << ' ';
-      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      d.first->output(os);
       break;
     case differencet::DELETED:
       os << '-';
-      old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
+      d.first->output(os);
       break;
     case differencet::NEW:
       os << '+';
-      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      d.first->output(os);
       break;
     }
   }

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -51,9 +51,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       ++it)
   {
     if(loop.contains(it))
-    {
-      goto_program.output_instruction(ns, "scratch", std::cout, *it);
-    }
+      it->output(std::cout);
   }
 
   std::cout << "Modified:\n";

src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp

@@ -32,7 +32,7 @@ bool enumerating_loop_accelerationt::accelerate(
         it!=path.end();
         ++it)
     {
-      goto_program.output_instruction(ns, "OMG", std::cout, *it->loc);
+      it->loc->output(std::cout);
     }
 #endif
 

src/goto-instrument/accelerate/path.cpp

@@ -15,10 +15,8 @@ Author: Matt Lewis
 
 void output_path(
   const patht &path,
-  const goto_programt &program,
-  const namespacet &ns,
   std::ostream &str)
 {
   for(const auto &step : path)
-    program.output_instruction(ns, "path", str, *step.loc);
+    step.loc->output(str);
 }

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -62,7 +62,7 @@ bool polynomial_acceleratort::accelerate(
       it!=body.end();
       ++it)
   {
-    program.output_instruction(ns, "scratch", std::cout, *it);
+    it->output(std::cout);
   }
 
   std::cout << "Modified:\n";

src/goto-instrument/contracts/contracts.cpp

@@ -947,7 +947,11 @@ void code_contractst::apply_function_contract(
   // Kill return value variable if fresh
   if(call_ret_is_fresh_var)
   {
-    function_body.output_instruction(ns, "", log.warning(), *target);
+    log.conditional_output(
+      log.warning(), [&target](messaget::mstreamt &mstream) {
+        target->output(mstream);
+        mstream << messaget::eom;
+      });
     auto dead_inst =
       goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
     function_body.insert_before_swap(target, dead_inst);
@@ -1120,11 +1124,14 @@ void code_contractst::apply_loop_contract(
     {
       if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0)
       {
-        log.error() << "Computed loop at " << loop_head->source_location()
+        log.conditional_output(
+          log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
+            mstream << "Computed loop at " << loop_head->source_location()
                     << "contains an instruction beyond [loop_head, loop_end]:"
                     << messaget::eom;
-        goto_function.body.output_instruction(
-          ns, function_name, log.error(), *i);
+            i->output(mstream);
+            mstream << messaget::eom;
+          });
         throw 0;
       }
     }

src/goto-instrument/contracts/utils.cpp

@@ -204,16 +204,20 @@ bool is_loop_free(
     auto size = scc_size[scc_id];
     if(size > 1)
     {
-      log.error() << "Found CFG SCC with size " << size << messaget::eom;
-      for(const auto &node_id : node_to_scc)
-      {
-        if(node_to_scc[node_id] == scc_id)
-        {
-          const auto &pc = cfg[node_id].PC;
-          goto_program.output_instruction(ns, "", log.error(), *pc);
-          log.error() << messaget::eom;
-        }
-      }
+      log.conditional_output(
+        log.error(),
+        [&cfg, &node_to_scc, &scc_id, &size](messaget::mstreamt &mstream) {
+          mstream << "Found CFG SCC with size " << size << messaget::eom;
+          for(const auto &node_id : node_to_scc)
+          {
+            if(node_to_scc[node_id] == scc_id)
+            {
+              const auto &pc = cfg[node_id].PC;
+              pc->output(mstream);
+              mstream << messaget::eom;
+            }
+          }
+        });
       return false;
     }
   }

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -273,7 +273,7 @@ int goto_instrument_parse_optionst::doit()
 
         forall_goto_program_instructions(i_it, goto_program)
         {
-          goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
+          i_it->output(std::cout);
           std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
                     << "\n\n";
         }

src/goto-instrument/unwind.cpp

@@ -282,10 +282,8 @@ void goto_unwindt::unwind(
       i_it!=goto_program.instructions.end();)
   {
 #ifdef DEBUG
-    symbol_tablet st;
-    namespacet ns(st);
     std::cout << "Instruction:\n";
-    goto_program.output_instruction(ns, function_id, std::cout, *i_it);
+    i_it->output(std::cout);
 #endif
 
     if(!i_it->is_backwards_goto())

src/goto-programs/goto_inline_class.cpp

@@ -311,7 +311,7 @@ void goto_inlinet::expand_function_call(
 
 #ifdef DEBUG
   std::cout << "Expanding call:\n";
-  dest.output_instruction(ns, irep_idt(), std::cout, *target);
+  target->output(std::cout);
 #endif
 
   exprt lhs;
@@ -691,15 +691,13 @@ void goto_inlinet::output_inline_map(
         goto_function.body_available(),
         "cannot inline function with empty body");
 
-      const goto_programt &goto_program=goto_function.body;
-
       for(const auto &call : call_list)
       {
         const goto_programt::const_targett target=call.first;
         bool transitive=call.second;
 
         out << "  Call:\n";
-        goto_program.output_instruction(ns, id, out, *target);
+        target->output(out);
         out << "  Transitive: " << transitive << "\n";
       }
     }

src/goto-programs/interpreter.cpp

@@ -120,8 +120,7 @@ void interpretert::show_state()
     output.status() << "End of function '" << function->first << "'\n";
   }
   else
-    function->second.body.output_instruction(
-      ns, function->first, output.status(), *pc);
+    pc->output(output.status());
 
   output.status() << messaget::eom;
 }