diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index 1b604509632..169f57b91d1 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/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 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::sorted() const +{ + std::vector 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::sorted() +{ + std::vector 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; +} diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index a0cd4b14850..6e49f30af5c 100644 --- a/src/goto-programs/goto_functions.h +++ b/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 sorted() const; + std::vector sorted(); }; #define Forall_goto_functions(it, functions) \ diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 80c14205968..aea03ae86da 100644 --- a/src/goto-programs/goto_model.h +++ b/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() { } diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 4180e38c719..408c448d070 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -11,8 +11,6 @@ Author: Peter Schrammel #include "show_goto_functions.h" -#include - #include #include #include @@ -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; diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 49e3b08f26a..3e9fb146516 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/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(); diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index db8b17ee666..41fd545a7fe 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/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));