ai_baset: output now requires function identifier

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.

Author: Daniel Kroening

src/analyses/ai.cpp

@@ -42,7 +42,7 @@ void ai_baset::output(
 
 void ai_baset::output(
   const namespacet &ns,
-  const irep_idt &identifier,
+  const irep_idt &function_identifier,
   const goto_programt &goto_program,
   std::ostream &out) const
 {
@@ -54,7 +54,7 @@ void ai_baset::output(
     abstract_state_before(i_it)->output(out, *this, ns);
     out << "\n";
     #if 1
-    goto_program.output_instruction(ns, identifier, out, *i_it);
+    goto_program.output_instruction(ns, function_identifier, out, *i_it);
     out << "\n";
     #endif
   }
@@ -82,15 +82,9 @@ jsont ai_baset::output_json(
   return std::move(result);
 }
 
-/// Output the domains for a single function as JSON
-/// \param ns: The namespace
-/// \param goto_program: The goto program
-/// \param identifier: The identifier used to find a symbol to identify the
-///   source language
-/// \return The JSON object
 jsont ai_baset::output_json(
   const namespacet &ns,
-  const irep_idt &identifier,
+  const irep_idt &function_identifier,
   const goto_programt &goto_program) const
 {
   json_arrayt contents;
@@ -99,7 +93,7 @@ jsont ai_baset::output_json(
   {
     // Ideally we need output_instruction_json
     std::ostringstream out;
-    goto_program.output_instruction(ns, identifier, out, *i_it);
+    goto_program.output_instruction(ns, function_identifier, out, *i_it);
 
     json_objectt location(
       {{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
@@ -138,15 +132,9 @@ xmlt ai_baset::output_xml(
   return program;
 }
 
-/// Output the domains for a single function as XML
-/// \param ns: The namespace
-/// \param goto_program: The goto program
-/// \param identifier: The identifier used to find a symbol to identify the
-///   source language
-/// \return The XML object
 xmlt ai_baset::output_xml(
   const namespacet &ns,
-  const irep_idt &identifier,
+  const irep_idt &function_identifier,
   const goto_programt &goto_program) const
 {
   xmlt function_body;
@@ -161,7 +149,7 @@ xmlt ai_baset::output_xml(
 
     // Ideally we need output_instruction_xml
     std::ostringstream out;
-    goto_program.output_instruction(ns, identifier, out, *i_it);
+    goto_program.output_instruction(ns, function_identifier, out, *i_it);
     location.set_attribute("instruction", out.str());
 
     function_body.new_element(location);

src/analyses/ai.h

@@ -124,6 +124,18 @@ class ai_baset
   {
   }
 
+  /// Output the abstract states for a single function
+  /// \param ns: The namespace
+  /// \param function_identifier: The identifier used to find a symbol to
+  ///   identify the \p goto_program's source language
+  /// \param goto_program: The goto program
+  /// \param out: The ostream to direct output to
+  virtual void output(
+    const namespacet &ns,
+    const irep_idt &function_identifier,
+    const goto_programt &goto_program,
+    std::ostream &out) const;
+
   /// Output the abstract states for a whole program
   virtual void output(
     const namespacet &ns,
@@ -139,15 +151,6 @@ class ai_baset
     output(ns, goto_model.goto_functions, out);
   }
 
-  /// Output the abstract states for a function
-  void output(
-    const namespacet &ns,
-    const goto_programt &goto_program,
-    std::ostream &out) const
-  {
-    output(ns, "", goto_program, out);
-  }
-
   /// Output the abstract states for a function
   void output(
     const namespacet &ns,
@@ -243,38 +246,26 @@ class ai_baset
   /// entry state required by the analysis
   void entry_state(const goto_functionst &goto_functions);
 
-  /// Output the abstract states for a single function
-  /// \param ns: The namespace
-  /// \param goto_program: The goto program
-  /// \param identifier: The identifier used to find a symbol to identify the
-  ///   source language
-  /// \param out: The ostream to direct output to
-  virtual void output(
-    const namespacet &ns,
-    const goto_programt &goto_program,
-    const irep_idt &identifier,
-    std::ostream &out) const;
-
   /// Output the abstract states for a single function as JSON
   /// \param ns: The namespace
   /// \param goto_program: The goto program
-  /// \param identifier: The identifier used to find a symbol to identify the
-  ///   source language
+  /// \param function_identifier: The identifier used to find a symbol to
+  ///   identify the source language
   /// \return The JSON object
   virtual jsont output_json(
     const namespacet &ns,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const goto_programt &goto_program) const;
 
   /// Output the abstract states for a single function as XML
   /// \param ns: The namespace
   /// \param goto_program: The goto program
-  /// \param identifier: The identifier used to find a symbol to identify the
-  ///   source language
+  /// \param function_identifier: The identifier used to find a symbol to
+  ///   identify the source language
   /// \return The XML object
   virtual xmlt output_xml(
     const namespacet &ns,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const goto_programt &goto_program) const;
 
   /// The work queue, sorted by location number

src/goto-instrument/uninitialized.cpp

@@ -223,7 +223,7 @@ void show_uninitialized(
       out << "////\n\n";
       uninitialized_analysist uninitialized_analysis;
       uninitialized_analysis(f_it->first, f_it->second.body, ns);
-      uninitialized_analysis.output(ns, f_it->second.body, out);
+      uninitialized_analysis.output(ns, f_it->first, f_it->second.body, out);
     }
   }
 }