Skip to content

Commit 2e226d8

Browse files
author
Daniel Kroening
committed
use a separate message for show_goto_functions() for the console
Rationale: the messages are output into a string buffer, which does not scale well in case there are many functions. Output can be delayed substantially.
1 parent da5d4d1 commit 2e226d8

File tree

1 file changed

+14
-4
lines changed

1 file changed

+14
-4
lines changed

src/goto-programs/show_goto_functions.cpp

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -62,14 +62,24 @@ void show_goto_functions(
6262
<< (fun.second.body_available() ? ""
6363
: ", body not available")
6464
<< " */";
65+
msg.status() << messaget::eom;
6566
}
66-
67-
msg.status() << messaget::eom;
6867
}
6968
else
7069
{
71-
goto_functions.output(ns, msg.status());
72-
msg.status() << messaget::eom;
70+
auto &out = msg.status();
71+
for(const auto &fun : goto_functions.function_map)
72+
{
73+
if(fun.second.body_available())
74+
{
75+
out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
76+
77+
const symbolt &symbol = ns.lookup(fun.first);
78+
out << symbol.display_name() << " /* " << symbol.name << " */\n";
79+
fun.second.body.output(ns, symbol.name, out);
80+
msg.status() << messaget::eom;
81+
}
82+
}
7383
}
7484

7585
break;

0 commit comments

Comments
 (0)