Merge pull request #3829 from tautschnig/function-dot

dot: use irep_idt for function identifier [blocks: #3126]

Author: tautschnig

src/goto-instrument/dot.cpp

@@ -44,10 +44,8 @@ class dott
   std::list<exprt> function_calls;
   std::list<exprt> clusters;
 
-  void write_dot_subgraph(
-    std::ostream &,
-    const std::string &,
-    const goto_programt &);
+  void
+  write_dot_subgraph(std::ostream &, const irep_idt &, const goto_programt &);
 
   void do_dot_function_calls(std::ostream &);
 
@@ -64,21 +62,23 @@ class dott
                  std::set<goto_programt::const_targett> &);
 };
 
-/// writes the dot graph that corresponds to the goto program to the output
+/// Write the dot graph that corresponds to the goto program to the output
 /// stream.
-/// \par parameters: output stream, name and goto program
+/// \param out: output stream
+/// \param function_id: name of \p goto_program
+/// \param goto_program: goto program the dot graph of which is written
 /// \return true on error, false otherwise
 void dott::write_dot_subgraph(
   std::ostream &out,
-  const std::string &name,
+  const irep_idt &function_id,
   const goto_programt &goto_program)
 {
   clusters.push_back(exprt("cluster"));
-  clusters.back().set("name", name);
+  clusters.back().set("name", function_id);
   clusters.back().set("nr", subgraphscount);
 
-  out << "subgraph \"cluster_" << name << "\" {\n";
-  out << "label=\"" << name << "\";\n";
+  out << "subgraph \"cluster_" << function_id << "\" {\n";
+  out << "label=\"" << function_id << "\";\n";
 
   const goto_programt::instructionst &instructions =
     goto_program.instructions;
@@ -111,22 +111,22 @@ void dott::write_dot_subgraph(
           tmp.str("Goto");
         else
         {
-          std::string t = from_expr(ns, it->function, it->guard);
+          std::string t = from_expr(ns, function_id, it->guard);
           while(t[ t.size()-1 ]=='\n')
             t = t.substr(0, t.size()-1);
           tmp << escape(t) << "?";
         }
       }
       else if(it->is_assume())
       {
-        std::string t = from_expr(ns, it->function, it->guard);
+        std::string t = from_expr(ns, function_id, it->guard);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp << "Assume\\n(" << escape(t) << ")";
       }
       else if(it->is_assert())
       {
-        std::string t = from_expr(ns, it->function, it->guard);
+        std::string t = from_expr(ns, function_id, it->guard);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp << "Assert\\n(" << escape(t) << ")";
@@ -145,7 +145,7 @@ void dott::write_dot_subgraph(
         tmp.str("Atomic End");
       else if(it->is_function_call())
       {
-        std::string t = from_expr(ns, it->function, it->code);
+        std::string t = from_expr(ns, function_id, it->code);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp.str(escape(t));
@@ -162,7 +162,7 @@ void dott::write_dot_subgraph(
               it->is_return() ||
               it->is_other())
       {
-        std::string t = from_expr(ns, it->function, it->code);
+        std::string t = from_expr(ns, function_id, it->code);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp.str(escape(t));
@@ -266,7 +266,7 @@ void dott::output(std::ostream &out)
 
   forall_goto_functions(it, goto_model.goto_functions)
     if(it->second.body_available())
-      write_dot_subgraph(out, id2string(it->first), it->second.body);
+      write_dot_subgraph(out, it->first, it->second.body);
 
   do_dot_function_calls(out);