Merge pull request #3165 from diffblue/goto_functions_message

use a separate message for show_goto_functions() for the console

Author: Daniel Kroening

src/goto-programs/goto_functions.cpp

@@ -13,24 +13,7 @@ Date: June 2003
 
 #include "goto_functions.h"
 
-void goto_functionst::output(
-  const namespacet &ns,
-  std::ostream &out) const
-{
-  for(const auto &fun : function_map)
-  {
-    if(fun.second.body_available())
-    {
-      out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
-
-      const symbolt &symbol=ns.lookup(fun.first);
-      out << symbol.display_name() << " /* " << symbol.name << " */\n";
-      fun.second.body.output(ns, symbol.name, out);
-
-      out << std::flush;
-    }
-  }
-}
+#include <algorithm>
 
 void goto_functionst::compute_location_numbers()
 {
@@ -73,3 +56,44 @@ void goto_functionst::compute_loop_numbers()
     func.second.body.compute_loop_numbers();
   }
 }
+
+/// returns a vector of the iterators in alphabetical order
+std::vector<goto_functionst::function_mapt::const_iterator>
+goto_functionst::sorted() const
+{
+  std::vector<function_mapt::const_iterator> result;
+
+  result.reserve(function_map.size());
+
+  for(auto it = function_map.begin(); it != function_map.end(); it++)
+    result.push_back(it);
+
+  std::sort(
+    result.begin(),
+    result.end(),
+    [](function_mapt::const_iterator a, function_mapt::const_iterator b) {
+      return id2string(a->first) < id2string(b->first);
+    });
+
+  return result;
+}
+
+/// returns a vector of the iterators in alphabetical order
+std::vector<goto_functionst::function_mapt::iterator> goto_functionst::sorted()
+{
+  std::vector<function_mapt::iterator> result;
+
+  result.reserve(function_map.size());
+
+  for(auto it = function_map.begin(); it != function_map.end(); it++)
+    result.push_back(it);
+
+  std::sort(
+    result.begin(),
+    result.end(),
+    [](function_mapt::iterator a, function_mapt::iterator b) {
+      return id2string(a->first) < id2string(b->first);
+    });
+
+  return result;
+}

src/goto-programs/goto_functions.h

@@ -72,10 +72,6 @@ class goto_functionst
     function_map.clear();
   }
 
-  void output(
-    const namespacet &ns,
-    std::ostream &out) const;
-
   void compute_location_numbers();
   void compute_location_numbers(goto_programt &);
   void compute_loop_numbers();
@@ -118,6 +114,9 @@ class goto_functionst
     for(const auto &fun : other.function_map)
       function_map[fun.first].copy_from(fun.second);
   }
+
+  std::vector<function_mapt::const_iterator> sorted() const;
+  std::vector<function_mapt::iterator> sorted();
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_model.h

@@ -37,12 +37,6 @@ class goto_modelt : public abstract_goto_modelt
     goto_functions.clear();
   }
 
-  void output(std::ostream &out) const
-  {
-    namespacet ns(symbol_table);
-    goto_functions.output(ns, out);
-  }
-
   goto_modelt()
   {
   }

src/goto-programs/show_goto_functions.cpp

@@ -11,8 +11,6 @@ Author: Peter Schrammel
 
 #include "show_goto_functions.h"
 
-#include <iostream>
-
 #include <util/xml.h>
 #include <util/json.h>
 #include <util/json_expr.h>
@@ -52,24 +50,32 @@ void show_goto_functions(
   break;
 
   case ui_message_handlert::uit::PLAIN:
-    if(list_only)
     {
-      for(const auto &fun : goto_functions.function_map)
+      // sort alphabetically
+      const auto sorted = goto_functions.sorted();
+
+      for(const auto &fun : sorted)
       {
-        const symbolt &symbol = ns.lookup(fun.first);
-        msg.status() << '\n'
-                     << symbol.display_name() << " /* " << symbol.name
-                     << (fun.second.body_available() ? ""
-                                                     : ", body not available")
-                     << " */";
-      }
+        const symbolt &symbol = ns.lookup(fun->first);
+        const bool has_body = fun->second.body_available();
 
-      msg.status() << messaget::eom;
-    }
-    else
-    {
-      goto_functions.output(ns, msg.status());
-      msg.status() << messaget::eom;
+        if(list_only)
+        {
+          msg.status() << '\n'
+                       << symbol.display_name() << " /* " << symbol.name
+                       << (has_body ? "" : ", body not available") << " */";
+          msg.status() << messaget::eom;
+        }
+        else if(has_body)
+        {
+          msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
+
+          msg.status() << messaget::bold << symbol.display_name()
+                       << messaget::reset << " /* " << symbol.name << " */\n";
+          fun->second.body.output(ns, symbol.name, msg.status());
+          msg.status() << messaget::eom;
+        }
+      }
     }
 
     break;

src/goto-programs/show_goto_functions_json.cpp

@@ -41,10 +41,13 @@ json_objectt show_goto_functions_jsont::convert(
 {
   json_arrayt json_functions;
   const json_irept no_comments_irep_converter(false);
-  for(const auto &function_entry : goto_functions.function_map)
+
+  const auto sorted = goto_functions.sorted();
+
+  for(const auto &function_entry : sorted)
   {
-    const irep_idt &function_name=function_entry.first;
-    const goto_functionst::goto_functiont &function=function_entry.second;
+    const irep_idt &function_name = function_entry->first;
+    const goto_functionst::goto_functiont &function = function_entry->second;
 
     json_objectt &json_function=
       json_functions.push_back(jsont()).make_object();

src/goto-programs/show_goto_functions_xml.cpp

@@ -43,10 +43,13 @@ xmlt show_goto_functions_xmlt::convert(
   const goto_functionst &goto_functions)
 {
   xmlt xml_functions=xmlt("functions");
-  for(const auto &function_entry : goto_functions.function_map)
+
+  const auto sorted = goto_functions.sorted();
+
+  for(const auto &function_entry : sorted)
   {
-    const irep_idt &function_name=function_entry.first;
-    const goto_functionst::goto_functiont &function=function_entry.second;
+    const irep_idt &function_name = function_entry->first;
+    const goto_functionst::goto_functiont &function = function_entry->second;
 
     xmlt &xml_function=xml_functions.new_element("function");
     xml_function.set_attribute("name", id2string(function_name));