Skip to content

Commit 8360233

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#1646 from peterschrammel/list-goto-functions
Option for listing the goto functions
2 parents eb5ec24 + b8cee29 commit 8360233

14 files changed

+140
-49
lines changed

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -635,9 +635,15 @@ int cbmc_parse_optionst::get_goto_program(
635635
}
636636

637637
// show it?
638-
if(cmdline.isset("show-goto-functions"))
638+
if(
639+
cmdline.isset("show-goto-functions") ||
640+
cmdline.isset("list-goto-functions"))
639641
{
640-
show_goto_functions(goto_model, ui_message_handler.get_ui());
642+
show_goto_functions(
643+
goto_model,
644+
get_message_handler(),
645+
ui_message_handler.get_ui(),
646+
cmdline.isset("list-goto-functions"));
641647
return CPROVER_EXIT_SUCCESS;
642648
}
643649

@@ -896,6 +902,7 @@ int cbmc_parse_optionst::do_bmc(bmct &bmc)
896902
/// display command line help
897903
void cbmc_parse_optionst::help()
898904
{
905+
// clang-format off
899906
std::cout <<
900907
"\n"
901908
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2017 ";
@@ -1023,4 +1030,5 @@ void cbmc_parse_optionst::help()
10231030
HELP_GOTO_TRACE
10241031
" --verbosity # verbosity level\n"
10251032
"\n";
1033+
// clang-format on
10261034
}

‎src/cbmc/cbmc_parse_options.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ class bmct;
2626
class goto_functionst;
2727
class optionst;
2828

29+
// clang-format off
2930
#define CBMC_OPTIONS \
3031
"(program-only)(preprocess)(slice-by-trace):" \
3132
OPT_FUNCTIONS \
@@ -49,7 +50,8 @@ class optionst;
4950
"(string-max-input-length):" \
5051
"(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
5152
"(little-endian)(big-endian)" \
52-
"(show-goto-functions)(show-loops)" \
53+
OPT_SHOW_GOTO_FUNCTIONS \
54+
"(show-loops)" \
5355
"(show-symbol-table)(show-parse-tree)(show-vcc)" \
5456
"(show-claims)(claim):(show-properties)" \
5557
"(drop-unused-functions)" \
@@ -68,6 +70,7 @@ class optionst;
6870
"(localize-faults)(localize-faults-method):" \
6971
OPT_GOTO_TRACE \
7072
"(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
73+
// clang-format on
7174

7275
class cbmc_parse_optionst:
7376
public parse_options_baset,

‎src/clobber/clobber_parse_options.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,9 +136,15 @@ int clobber_parse_optionst::doit()
136136
}
137137

138138
// show it?
139-
if(cmdline.isset("show-goto-functions"))
139+
if(
140+
cmdline.isset("show-goto-functions") ||
141+
cmdline.isset("list-goto-functions"))
140142
{
141-
show_goto_functions(goto_model, get_ui());
143+
show_goto_functions(
144+
goto_model,
145+
get_message_handler(),
146+
ui_message_handler.get_ui(),
147+
cmdline.isset("list-goto-functions"));
142148
return 6;
143149
}
144150

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -431,9 +431,15 @@ int goto_analyzer_parse_optionst::doit()
431431
}
432432

433433
// show it?
434-
if(cmdline.isset("show-goto-functions"))
435-
{
436-
show_goto_functions(goto_model, get_ui());
434+
if(
435+
cmdline.isset("show-goto-functions") ||
436+
cmdline.isset("list-goto-functions"))
437+
{
438+
show_goto_functions(
439+
goto_model,
440+
get_message_handler(),
441+
get_ui(),
442+
cmdline.isset("list-goto-functions"));
437443
return CPROVER_EXIT_SUCCESS;
438444
}
439445

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 20 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -280,10 +280,27 @@ int goto_diff_parse_optionst::doit()
280280
if(get_goto_program_ret!=-1)
281281
return get_goto_program_ret;
282282

283-
if(cmdline.isset("show-goto-functions"))
283+
if(cmdline.isset("show-loops"))
284284
{
285-
show_goto_functions(goto_model1, get_ui());
286-
show_goto_functions(goto_model2, get_ui());
285+
show_loop_ids(get_ui(), goto_model1);
286+
show_loop_ids(get_ui(), goto_model2);
287+
return true;
288+
}
289+
290+
if(
291+
cmdline.isset("show-goto-functions") ||
292+
cmdline.isset("list-goto-functions"))
293+
{
294+
show_goto_functions(
295+
goto_model1,
296+
get_message_handler(),
297+
ui_message_handler.get_ui(),
298+
cmdline.isset("list-goto-functions"));
299+
show_goto_functions(
300+
goto_model2,
301+
get_message_handler(),
302+
ui_message_handler.get_ui(),
303+
cmdline.isset("list-goto-functions"));
287304
return 0;
288305
}
289306

@@ -430,20 +447,6 @@ bool goto_diff_parse_optionst::process_goto_program(
430447

431448
// add loop ids
432449
goto_functions.compute_loop_numbers();
433-
434-
// show it?
435-
if(cmdline.isset("show-loops"))
436-
{
437-
show_loop_ids(get_ui(), goto_model);
438-
return true;
439-
}
440-
441-
// show it?
442-
if(cmdline.isset("show-goto-functions"))
443-
{
444-
show_goto_functions(goto_model, get_ui());
445-
return true;
446-
}
447450
}
448451

449452
catch(const char *e)

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -575,10 +575,15 @@ int goto_instrument_parse_optionst::doit()
575575
return CPROVER_EXIT_SUCCESS;
576576
}
577577

578-
if(cmdline.isset("show-goto-functions"))
578+
if(
579+
cmdline.isset("show-goto-functions") ||
580+
cmdline.isset("list-goto-functions"))
579581
{
580-
namespacet ns(goto_model.symbol_table);
581-
show_goto_functions(goto_model, get_ui());
582+
show_goto_functions(
583+
goto_model,
584+
get_message_handler(),
585+
ui_message_handler.get_ui(),
586+
cmdline.isset("list-goto-functions"));
582587
return CPROVER_EXIT_SUCCESS;
583588
}
584589

‎src/goto-programs/show_goto_functions.cpp

Lines changed: 33 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -29,35 +29,60 @@ Author: Peter Schrammel
2929

3030
void show_goto_functions(
3131
const namespacet &ns,
32+
message_handlert &message_handler,
3233
ui_message_handlert::uit ui,
33-
const goto_functionst &goto_functions)
34+
const goto_functionst &goto_functions,
35+
bool list_only)
3436
{
37+
messaget msg(message_handler);
3538
switch(ui)
3639
{
3740
case ui_message_handlert::uit::XML_UI:
3841
{
39-
show_goto_functions_xmlt xml_show_functions(ns);
40-
xml_show_functions(goto_functions, std::cout);
42+
show_goto_functions_xmlt xml_show_functions(ns, list_only);
43+
msg.status() << xml_show_functions.convert(goto_functions);
4144
}
4245
break;
4346

4447
case ui_message_handlert::uit::JSON_UI:
4548
{
46-
show_goto_functions_jsont json_show_functions(ns);
47-
json_show_functions(goto_functions, std::cout);
49+
show_goto_functions_jsont json_show_functions(ns, list_only);
50+
msg.status() << json_show_functions.convert(goto_functions);
4851
}
4952
break;
5053

5154
case ui_message_handlert::uit::PLAIN:
52-
goto_functions.output(ns, std::cout);
55+
if(list_only)
56+
{
57+
for(const auto &fun : goto_functions.function_map)
58+
{
59+
const symbolt &symbol = ns.lookup(fun.first);
60+
msg.status() << '\n'
61+
<< symbol.display_name() << " /* " << symbol.name
62+
<< (fun.second.body_available() ? ""
63+
: ", body not available")
64+
<< " */";
65+
}
66+
67+
msg.status() << messaget::eom;
68+
}
69+
else
70+
{
71+
goto_functions.output(ns, msg.status());
72+
msg.status() << messaget::eom;
73+
}
74+
5375
break;
5476
}
5577
}
5678

5779
void show_goto_functions(
5880
const goto_modelt &goto_model,
59-
ui_message_handlert::uit ui)
81+
message_handlert &message_handler,
82+
ui_message_handlert::uit ui,
83+
bool list_only)
6084
{
6185
const namespacet ns(goto_model.symbol_table);
62-
show_goto_functions(ns, ui, goto_model.goto_functions);
86+
show_goto_functions(
87+
ns, message_handler, ui, goto_model.goto_functions, list_only);
6388
}

‎src/goto-programs/show_goto_functions.h

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,19 +18,27 @@ 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,
33+
message_handlert &message_handler,
2934
ui_message_handlert::uit ui,
30-
const goto_functionst &goto_functions);
35+
const goto_functionst &goto_functions,
36+
bool list_only = false);
3137

3238
void show_goto_functions(
3339
const goto_modelt &,
34-
ui_message_handlert::uit ui);
40+
message_handlert &message_handler,
41+
ui_message_handlert::uit ui,
42+
bool list_only = false);
3543

3644
#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H

‎src/goto-programs/show_goto_functions_json.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,11 @@ Author: Thomas Kiley
2626

2727
/// For outputting the GOTO program in a readable JSON format.
2828
/// \param ns: the namespace to use to resolve names with
29-
show_goto_functions_jsont::show_goto_functions_jsont(const namespacet &ns):
30-
ns(ns)
29+
/// \param list_only: output only list of functions, but not their bodies
30+
show_goto_functions_jsont::show_goto_functions_jsont(
31+
const namespacet &_ns,
32+
bool _list_only)
33+
: ns(_ns), list_only(_list_only)
3134
{}
3235

3336
/// Walks through all of the functions in the program and returns a JSON object
@@ -55,6 +58,9 @@ json_objectt show_goto_functions_jsont::convert(
5558
has_prefix(id2string(function_name), "java::java");
5659
json_function["isInternal"]=jsont::json_boolean(is_internal);
5760

61+
if(list_only)
62+
continue;
63+
5864
if(function.body_available())
5965
{
6066
json_arrayt json_instruction_array=json_arrayt();

‎src/goto-programs/show_goto_functions_json.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,17 @@ class namespacet;
2020
class show_goto_functions_jsont
2121
{
2222
public:
23-
explicit show_goto_functions_jsont(const namespacet &ns);
23+
explicit show_goto_functions_jsont(
24+
const namespacet &_ns,
25+
bool _list_only = false);
2426

2527
json_objectt convert(const goto_functionst &goto_functions);
2628
void operator()(
2729
const goto_functionst &goto_functions, std::ostream &out, bool append=true);
2830

2931
private:
3032
const namespacet &ns;
33+
bool list_only;
3134
};
3235

3336
#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_JSON_H

‎src/goto-programs/show_goto_functions_xml.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,11 @@ Author: Thomas Kiley
2525

2626
/// For outputting the GOTO program in a readable xml format.
2727
/// \param ns: the namespace to use to resolve names with
28-
show_goto_functions_xmlt::show_goto_functions_xmlt(const namespacet &ns):
29-
ns(ns)
28+
/// \param list_only: output only list of functions, but not their bodies
29+
show_goto_functions_xmlt::show_goto_functions_xmlt(
30+
const namespacet &_ns,
31+
bool _list_only)
32+
: ns(_ns), list_only(_list_only)
3033
{}
3134

3235
/// Walks through all of the functions in the program and returns an xml object
@@ -56,6 +59,9 @@ xmlt show_goto_functions_xmlt::convert(
5659
has_prefix(id2string(function_name), "java::java");
5760
xml_function.set_attribute_bool("is_internal", is_internal);
5861

62+
if(list_only)
63+
continue;
64+
5965
if(function.body_available())
6066
{
6167
xmlt &xml_instructions=xml_function.new_element("instructions");

‎src/goto-programs/show_goto_functions_xml.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,17 @@ class namespacet;
2020
class show_goto_functions_xmlt
2121
{
2222
public:
23-
explicit show_goto_functions_xmlt(const namespacet &ns);
23+
explicit show_goto_functions_xmlt(
24+
const namespacet &_ns,
25+
bool _list_only = false);
2426

2527
xmlt convert(const goto_functionst &goto_functions);
2628
void operator()(
2729
const goto_functionst &goto_functions, std::ostream &out, bool append=true);
2830

2931
private:
3032
const namespacet &ns;
33+
bool list_only;
3134
};
3235

3336
#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H

‎src/jbmc/jbmc_parse_options.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -600,9 +600,15 @@ int jbmc_parse_optionst::get_goto_program(
600600
}
601601

602602
// show it?
603-
if(cmdline.isset("show-goto-functions"))
603+
if(
604+
cmdline.isset("show-goto-functions") ||
605+
cmdline.isset("list-goto-functions"))
604606
{
605-
show_goto_functions(*goto_model, ui_message_handler.get_ui());
607+
show_goto_functions(
608+
*goto_model,
609+
get_message_handler(),
610+
ui_message_handler.get_ui(),
611+
cmdline.isset("list-goto-functions"));
606612
return 0;
607613
}
608614

‎src/jbmc/jbmc_parse_options.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ class bmct;
2626
class goto_functionst;
2727
class optionst;
2828

29+
// clang-format off
2930
#define JBMC_OPTIONS \
3031
"(program-only)(preprocess)(slice-by-trace):" \
3132
OPT_FUNCTIONS \
@@ -48,7 +49,8 @@ class optionst;
4849
"(string-max-length):" \
4950
"(string-max-input-length):" \
5051
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
51-
"(show-goto-functions)(show-loops)" \
52+
OPT_SHOW_GOTO_FUNCTIONS \
53+
"(show-loops)" \
5254
"(show-symbol-table)(show-parse-tree)(show-vcc)" \
5355
"(show-properties)" \
5456
"(drop-unused-functions)" \
@@ -65,6 +67,7 @@ class optionst;
6567
"(java-unwind-enum-static)" \
6668
"(localize-faults)(localize-faults-method):" \
6769
OPT_GOTO_TRACE
70+
// clang-format on
6871

6972
class jbmc_parse_optionst:
7073
public parse_options_baset,

0 commit comments

Comments
 (0)