Skip to content

Commit 6d5a42e

Browse files
Add and unify --show-class-hierarchy command line option
1 parent 57da328 commit 6d5a42e

File tree

8 files changed

+67
-10
lines changed

8 files changed

+67
-10
lines changed

jbmc/src/jbmc/jbmc_parse_options.cpp

+11
Original file line numberDiff line numberDiff line change
@@ -645,6 +645,16 @@ int jbmc_parse_optionst::get_goto_program(
645645
*this, options, get_message_handler());
646646
lazy_goto_model.initialize(cmdline);
647647

648+
// Show the class hierarchy
649+
if(cmdline.isset("show-class-hierarchy"))
650+
{
651+
class_hierarchyt hierarchy;
652+
hierarchy(lazy_goto_model.symbol_table);
653+
show_class_hierarchy(
654+
hierarchy, get_message_handler(), ui_message_handler.get_ui());
655+
return CPROVER_EXIT_SUCCESS;
656+
}
657+
648658
// Add failed symbols for any symbol created prior to loading any
649659
// particular function:
650660
add_failed_symbols(lazy_goto_model.symbol_table);
@@ -1079,6 +1089,7 @@ void jbmc_parse_optionst::help()
10791089
" --show-symbol-table show loaded symbol table\n"
10801090
HELP_SHOW_GOTO_FUNCTIONS
10811091
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1092+
HELP_SHOW_CLASS_HIERARCHY
10821093
"\n"
10831094
"Program instrumentation options:\n"
10841095
HELP_GOTO_CHECK

jbmc/src/jbmc/jbmc_parse_options.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,11 @@ Author: Daniel Kroening, [email protected]
2222

2323
#include <cbmc/bmc.h>
2424

25+
#include <goto-instrument/cover.h>
26+
#include <goto-programs/class_hierarchy.h>
2527
#include <goto-programs/goto_trace.h>
2628
#include <goto-programs/lazy_goto_model.h>
2729
#include <goto-programs/show_properties.h>
28-
#include <goto-instrument/cover.h>
2930

3031
#include <goto-symex/path_storage.h>
3132

@@ -60,6 +61,7 @@ class optionst;
6061
"(string-max-input-length):" \
6162
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
6263
OPT_SHOW_GOTO_FUNCTIONS \
64+
OPT_SHOW_CLASS_HIERARCHY \
6365
"(show-loops)" \
6466
"(show-symbol-table)(show-parse-tree)" \
6567
OPT_SHOW_PROPERTIES \
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--class-hierarchy --dot
3+
--show-class-hierarchy --dot
44
digraph class_hierarchy
55
^EXIT=0$
66
^SIGNAL=0$
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
22
main.c
3-
--class-hierarchy
3+
--show-class-hierarchy
44
^EXIT=0$
55
^SIGNAL=0$

src/goto-instrument/goto_instrument_parse_options.cpp

+5-4
Original file line numberDiff line numberDiff line change
@@ -652,16 +652,17 @@ int goto_instrument_parse_optionst::doit()
652652
return 0;
653653
}
654654

655-
if(cmdline.isset("class-hierarchy"))
655+
if(cmdline.isset("show-class-hierarchy"))
656656
{
657657
class_hierarchyt hierarchy;
658658
hierarchy(goto_model.symbol_table);
659659
if(cmdline.isset("dot"))
660660
hierarchy.output_dot(std::cout);
661661
else
662-
hierarchy.output(std::cout, false);
662+
show_class_hierarchy(
663+
hierarchy, get_message_handler(), ui_message_handler.get_ui());
663664

664-
return 0;
665+
return CPROVER_EXIT_SUCCESS;
665666
}
666667

667668
if(cmdline.isset("dot"))
@@ -1472,7 +1473,7 @@ void goto_instrument_parse_optionst::help()
14721473
" --call-graph show graph of function calls\n"
14731474
// NOLINTNEXTLINE(whitespace/line_length)
14741475
" --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1475-
" --class-hierarchy show class hierarchy\n"
1476+
HELP_SHOW_CLASS_HIERARCHY
14761477
// NOLINTNEXTLINE(whitespace/line_length)
14771478
" --show-threaded show instructions that may be executed by more than one thread\n"
14781479
"\n"

src/goto-instrument/goto_instrument_parse_options.h

+4-3
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,12 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/parse_options.h>
1717
#include <util/timestamper.h>
1818

19+
#include <goto-programs/class_hierarchy.h>
1920
#include <goto-programs/goto_functions.h>
20-
#include <goto-programs/show_goto_functions.h>
21-
#include <goto-programs/show_properties.h>
2221
#include <goto-programs/remove_calls_no_body.h>
2322
#include <goto-programs/remove_const_function_pointers.h>
23+
#include <goto-programs/show_goto_functions.h>
24+
#include <goto-programs/show_properties.h>
2425

2526
#include <analyses/goto_check.h>
2627

@@ -50,7 +51,7 @@ Author: Daniel Kroening, [email protected]
5051
"(max-var):(max-po-trans):(ignore-arrays)" \
5152
"(cfg-kill)(no-dependencies)(force-loop-duplication)" \
5253
"(call-graph)(reachable-call-graph)" \
53-
"(class-hierarchy)" \
54+
OPT_SHOW_CLASS_HIERARCHY \
5455
"(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
5556
"(nondet-volatile)(isr):" \
5657
"(stack-depth):(nondet-static)" \

src/goto-programs/class_hierarchy.cpp

+21
Original file line numberDiff line numberDiff line change
@@ -189,3 +189,24 @@ void class_hierarchyt::output(
189189
json_children.push_back(json_stringt(ch));
190190
}
191191
}
192+
193+
void show_class_hierarchy(
194+
const class_hierarchyt &hierarchy,
195+
message_handlert &message_handler,
196+
ui_message_handlert::uit ui,
197+
bool children_only)
198+
{
199+
messaget msg(message_handler);
200+
switch(ui)
201+
{
202+
case ui_message_handlert::uit::PLAIN:
203+
hierarchy.output(msg.result(), children_only);
204+
msg.result() << messaget::eom;
205+
break;
206+
case ui_message_handlert::uit::JSON_UI:
207+
hierarchy.output(msg.result().json_stream(), children_only);
208+
break;
209+
case ui_message_handlert::uit::XML_UI:
210+
UNIMPLEMENTED;
211+
}
212+
}

src/goto-programs/class_hierarchy.h

+21
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,19 @@ Date: April 2016
2020

2121
#include <util/graph.h>
2222
#include <util/irep.h>
23+
#include <util/ui_message.h>
24+
25+
// clang-format off
26+
#define OPT_SHOW_CLASS_HIERARCHY \
27+
"(show-class-hierarchy)"
28+
29+
#define HELP_SHOW_CLASS_HIERARCHY \
30+
" --show-class-hierarchy show the class hierarchy\n"
31+
// clang-format on
2332

2433
class symbol_tablet;
2534
class json_stream_arrayt;
35+
class message_handlert;
2636

2737
class class_hierarchyt
2838
{
@@ -96,4 +106,15 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
96106
nodes_by_namet nodes_by_name;
97107
};
98108

109+
/// Output the class hierarchy
110+
/// \param hierarchy: the class hierarchy to be printed
111+
/// \param message_handler: the message handler
112+
/// \param ui: the UI format
113+
/// \param children_only: print the children only and do not print the parents
114+
void show_class_hierarchy(
115+
const class_hierarchyt &hierarchy,
116+
message_handlert &message_handler,
117+
ui_message_handlert::uit ui,
118+
bool children_only = true);
119+
99120
#endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H

0 commit comments

Comments
 (0)