Skip to content

Commit 2fe43a9

Browse files
Add parameter to list goto functions without printing bodies
1 parent 5bd5962 commit 2fe43a9

File tree

4 files changed

+24
-6
lines changed

4 files changed

+24
-6
lines changed

src/goto-programs/show_goto_functions_json.cpp

+8-2
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

+4-1
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

+8-2
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

+4-1
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

0 commit comments

Comments
 (0)