Skip to content

Commit ebd8248

Browse files
Add list-goto-functions command line option
1 parent 2fe43a9 commit ebd8248

File tree

2 files changed

+34
-10
lines changed

2 files changed

+34
-10
lines changed

src/goto-programs/show_goto_functions.cpp

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,34 +30,52 @@ Author: Peter Schrammel
3030
void show_goto_functions(
3131
const namespacet &ns,
3232
ui_message_handlert::uit ui,
33-
const goto_functionst &goto_functions)
33+
const goto_functionst &goto_functions,
34+
bool list_only)
3435
{
3536
switch(ui)
3637
{
3738
case ui_message_handlert::uit::XML_UI:
3839
{
39-
show_goto_functions_xmlt xml_show_functions(ns);
40+
show_goto_functions_xmlt xml_show_functions(ns, list_only);
4041
xml_show_functions(goto_functions, std::cout);
4142
}
4243
break;
4344

4445
case ui_message_handlert::uit::JSON_UI:
4546
{
46-
show_goto_functions_jsont json_show_functions(ns);
47+
show_goto_functions_jsont json_show_functions(ns, list_only);
4748
json_show_functions(goto_functions, std::cout);
4849
}
4950
break;
5051

5152
case ui_message_handlert::uit::PLAIN:
52-
goto_functions.output(ns, std::cout);
53+
if(list_only)
54+
{
55+
for(const auto &fun : goto_functions.function_map)
56+
{
57+
const symbolt &symbol = ns.lookup(fun.first);
58+
std::cout << '\n'
59+
<< symbol.display_name() << " /* " << symbol.name
60+
<< (fun.second.body_available() ? ""
61+
: ", body not available")
62+
<< " */";
63+
}
64+
65+
std::cout << std::endl;
66+
}
67+
else
68+
goto_functions.output(ns, std::cout);
69+
5370
break;
5471
}
5572
}
5673

5774
void show_goto_functions(
5875
const goto_modelt &goto_model,
59-
ui_message_handlert::uit ui)
76+
ui_message_handlert::uit ui,
77+
bool list_only)
6078
{
6179
const namespacet ns(goto_model.symbol_table);
62-
show_goto_functions(ns, ui, goto_model.goto_functions);
80+
show_goto_functions(ns, ui, goto_model.goto_functions, list_only);
6381
}

src/goto-programs/show_goto_functions.h

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,19 +18,25 @@ class namespacet;
1818
class goto_modelt;
1919
class goto_functionst;
2020

21+
// clang-format off
2122
#define OPT_SHOW_GOTO_FUNCTIONS \
22-
"(show-goto-functions)"
23+
"(show-goto-functions)" \
24+
"(list-goto-functions)"
2325

2426
#define HELP_SHOW_GOTO_FUNCTIONS \
25-
" --show-goto-functions show goto program\n"
27+
" --show-goto-functions show goto program\n" \
28+
" --list-goto-functions list goto functions\n"
29+
// clang-format on
2630

2731
void show_goto_functions(
2832
const namespacet &ns,
2933
ui_message_handlert::uit ui,
30-
const goto_functionst &goto_functions);
34+
const goto_functionst &goto_functions,
35+
bool list_only = false);
3136

3237
void show_goto_functions(
3338
const goto_modelt &,
34-
ui_message_handlert::uit ui);
39+
ui_message_handlert::uit ui,
40+
bool list_only = false);
3541

3642
#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H

0 commit comments

Comments
 (0)