Skip to content

Commit da2e737

Browse files
Add and unify --show-class-hierarchy command line option
1 parent a7e55aa commit da2e737

File tree

6 files changed

+59
-7
lines changed

6 files changed

+59
-7
lines changed

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 11 additions & 0 deletions
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 0;
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

Lines changed: 3 additions & 1 deletion
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 \

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -652,14 +652,15 @@ 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

664665
return 0;
665666
}
@@ -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

Lines changed: 4 additions & 3 deletions
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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,3 +178,24 @@ void class_hierarchyt::output(json_stream_arrayt &json_stream, bool children_onl
178178
json_children.push_back(json_stringt(ch));
179179
}
180180
}
181+
182+
void show_class_hierarchy(
183+
const class_hierarchyt &hierarchy,
184+
message_handlert &message_handler,
185+
ui_message_handlert::uit ui,
186+
bool children_only)
187+
{
188+
messaget msg(message_handler);
189+
switch(ui)
190+
{
191+
case ui_message_handlert::uit::PLAIN:
192+
hierarchy.output(msg.result(), children_only);
193+
msg.result() << messaget::eom;
194+
break;
195+
case ui_message_handlert::uit::JSON_UI:
196+
hierarchy.output(msg.result().json_stream(), children_only);
197+
break;
198+
case ui_message_handlert::uit::XML_UI:
199+
UNIMPLEMENTED;
200+
}
201+
}

src/goto-programs/class_hierarchy.h

Lines changed: 16 additions & 0 deletions
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,10 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
96106
nodes_by_namet nodes_by_name;
97107
};
98108

109+
void show_class_hierarchy(
110+
const class_hierarchyt &hierarchy,
111+
message_handlert &message_handler,
112+
ui_message_handlert::uit ui,
113+
bool children_only = true);
114+
99115
#endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H

0 commit comments

Comments
 (0)