From 68c45ed83c04d7875749b96a87953ba3b170317f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 24 May 2018 18:03:41 +0100 Subject: [PATCH 1/3] Improve class hierarchy output more readable output, adds info whether class is abstract removes the plain text unit test which is replaced by a JBMC regression test in a later commit --- .../goto-programs/class_hierarchy_output.cpp | 20 +++++----------- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/class_hierarchy.cpp | 23 +++++++++++++------ src/goto-programs/class_hierarchy.h | 3 ++- 4 files changed, 25 insertions(+), 23 deletions(-) diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp index 75970716f91..cb8566296f8 100644 --- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp @@ -17,21 +17,15 @@ void require_parent_child_relationship( const std::string &parent_raw, const std::string &child_raw, - const std::string &output, const std::string &output_dot) { std::string parent = "java::" + parent_raw; std::string child = "java::" + child_raw; - std::stringstream - plain_child_expectation, plain_parent_expectation, dot_expectation; + std::stringstream dot_expectation; - plain_child_expectation << "Child of " << parent << ": " << child; - plain_parent_expectation << "Parent of " << child << ": " << parent; dot_expectation << "\"" << child << "\" -> \"" << parent << "\""; - REQUIRE(output.find(plain_child_expectation.str()) != std::string::npos); - REQUIRE(output.find(plain_parent_expectation.str()) != std::string::npos); REQUIRE(output_dot.find(dot_expectation.str()) != std::string::npos); } @@ -47,20 +41,18 @@ SCENARIO( std::stringstream output_dot_stream; hierarchy(symbol_table); - hierarchy.output(output_stream); hierarchy.output_dot(output_dot_stream); - std::string output = output_stream.str(); std::string output_dot = output_dot_stream.str(); require_parent_child_relationship( - "HierarchyTest", "HierarchyTestChild1", output, output_dot); + "HierarchyTest", "HierarchyTestChild1", output_dot); require_parent_child_relationship( - "HierarchyTest", "HierarchyTestChild2", output, output_dot); + "HierarchyTest", "HierarchyTestChild2", output_dot); require_parent_child_relationship( - "HierarchyTestChild1", "HierarchyTestGrandchild", output, output_dot); + "HierarchyTestChild1", "HierarchyTestGrandchild", output_dot); require_parent_child_relationship( - "HierarchyTestInterface1", "HierarchyTestGrandchild", output, output_dot); + "HierarchyTestInterface1", "HierarchyTestGrandchild", output_dot); require_parent_child_relationship( - "HierarchyTestInterface2", "HierarchyTestGrandchild", output, output_dot); + "HierarchyTestInterface2", "HierarchyTestGrandchild", output_dot); } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 66feb778817..19efe0c4db2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -659,7 +659,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("dot")) hierarchy.output_dot(std::cout); else - hierarchy.output(std::cout); + hierarchy.output(std::cout, false); return 0; } diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index 7f0e7fe558b..cdb91dbfefe 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -30,6 +30,9 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table) { const struct_typet &struct_type = to_struct_type(symbol_pair.second.type); + class_map[symbol_pair.first].is_abstract = + struct_type.get_bool(ID_abstract); + const irept::subt &bases= struct_type.find(ID_bases).get_sub(); @@ -123,17 +126,23 @@ void class_hierarchyt::get_parents_trans_rec( get_parents_trans_rec(child, dest); } -void class_hierarchyt::output(std::ostream &out) const +/// Output the class hierarchy in plain text +/// \param out: the output stream +/// \param children_only: print the children only and do not print the parents +void class_hierarchyt::output(std::ostream &out, bool children_only) const { for(const auto &c : class_map) { - for(const auto &pa : c.second.parents) - out << "Parent of " << c.first << ": " - << pa << '\n'; - + out << c.first << (c.second.is_abstract ? " (abstract)" : "") << ":\n"; + if(!children_only) + { + out << " parents:\n"; + for(const auto &pa : c.second.parents) + out << " " << pa << '\n'; + } + out << " children:\n"; for(const auto &ch : c.second.children) - out << "Child of " << c.first << ": " - << ch << '\n'; + out << " " << ch << '\n'; } } diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 1d180369765..afeb4c4e6f8 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -32,6 +32,7 @@ class class_hierarchyt { public: idst parents, children; + bool is_abstract; }; typedef std::map class_mapt; @@ -55,7 +56,7 @@ class class_hierarchyt return result; } - void output(std::ostream &) const; + void output(std::ostream &, bool children_only) const; void output_dot(std::ostream &) const; protected: From a018e2f2c451383823ed3af90deb930e8948e686 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 24 May 2018 18:12:02 +0100 Subject: [PATCH 2/3] Add JSON output for class hierarchy --- src/goto-programs/class_hierarchy.cpp | 27 +++++++++++++++++++++++++++ src/goto-programs/class_hierarchy.h | 2 ++ 2 files changed, 29 insertions(+) diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index cdb91dbfefe..efb720d32e7 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -15,6 +15,7 @@ Date: April 2016 #include +#include #include #include @@ -165,3 +166,29 @@ void class_hierarchyt::output_dot(std::ostream &ostr) const } ostr << "}\n"; } + +/// Output the class hierarchy in JSON format +/// \param json_stream: the output JSON stream array +/// \param children_only: print the children only and do not print the parents +void class_hierarchyt::output( + json_stream_arrayt &json_stream, + bool children_only) const +{ + for(const auto &c : class_map) + { + json_stream_objectt &json_class = json_stream.push_back_stream_object(); + json_class["name"] = json_stringt(c.first); + json_class["isAbstract"] = jsont::json_boolean(c.second.is_abstract); + if(!children_only) + { + json_stream_arrayt &json_parents = + json_class.push_back_stream_array("parents"); + for(const auto &pa : c.second.parents) + json_parents.push_back(json_stringt(pa)); + } + json_stream_arrayt &json_children = + json_class.push_back_stream_array("children"); + for(const auto &ch : c.second.children) + json_children.push_back(json_stringt(ch)); + } +} diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index afeb4c4e6f8..b01774b3d0d 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -22,6 +22,7 @@ Date: April 2016 #include class symbol_tablet; +class json_stream_arrayt; class class_hierarchyt { @@ -58,6 +59,7 @@ class class_hierarchyt void output(std::ostream &, bool children_only) const; void output_dot(std::ostream &) const; + void output(json_stream_arrayt &, bool children_only) const; protected: void get_children_trans_rec(const irep_idt &, idst &) const; From 2f4c6ad9b1918a79e77d93a7539b5ef1fb6c5d1c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 24 May 2018 17:17:18 +0100 Subject: [PATCH 3/3] Add and unify --show-class-hierarchy command line option --- .../jbmc/class_hierarchy/HierarchyTest.class | Bin 0 -> 300 bytes .../jbmc/class_hierarchy/HierarchyTest.java | 18 +++++++++++++++ .../class_hierarchy/HierarchyTestChild1.class | Bin 0 -> 248 bytes .../class_hierarchy/HierarchyTestChild2.class | Bin 0 -> 248 bytes .../HierarchyTestGrandchild.class | Bin 0 -> 275 bytes .../HierarchyTestInterface1.class | Bin 0 -> 127 bytes .../HierarchyTestInterface1.java | 1 + .../HierarchyTestInterface2.class | Bin 0 -> 127 bytes .../HierarchyTestInterface2.java | 1 + .../jbmc/class_hierarchy/test_json.desc | 7 ++++++ .../jbmc/class_hierarchy/test_plain.desc | 7 ++++++ jbmc/src/jbmc/jbmc_parse_options.cpp | 11 +++++++++ jbmc/src/jbmc/jbmc_parse_options.h | 4 +++- .../goto-instrument/class-hierarchy/dot.desc | 2 +- .../class-hierarchy/plain.desc | 2 +- .../goto_instrument_parse_options.cpp | 9 ++++---- .../goto_instrument_parse_options.h | 7 +++--- src/goto-programs/class_hierarchy.cpp | 21 ++++++++++++++++++ src/goto-programs/class_hierarchy.h | 21 ++++++++++++++++++ 19 files changed, 101 insertions(+), 10 deletions(-) create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestGrandchild.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class create mode 100644 jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java create mode 100644 jbmc/regression/jbmc/class_hierarchy/test_json.desc create mode 100644 jbmc/regression/jbmc/class_hierarchy/test_plain.desc diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class new file mode 100644 index 0000000000000000000000000000000000000000..26c221c378b4f8935075292fc5397558b1a77a5e GIT binary patch literal 300 zcmY+9y>7xl5QJxKV+Uh?B?^iZbRk7h5FHT>5~M&$5k!Bsk8qY_ONT+?u~H$W$OG_D zh&?0%ilkMF*-hMG(EIDv491ROPLooS(Q1vEfDlK=n! literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java new file mode 100644 index 00000000000..2379460e758 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java @@ -0,0 +1,18 @@ +public abstract class HierarchyTest { + // These fields exist only so the classloader will load all test classes: + HierarchyTestGrandchild field1; + HierarchyTestChild2 field2; + + abstract void foo(); +} + +class HierarchyTestChild1 extends HierarchyTest { + void foo() {} +} + +class HierarchyTestChild2 extends HierarchyTest { + void foo() {} +} + +class HierarchyTestGrandchild extends HierarchyTestChild1 + implements HierarchyTestInterface1, HierarchyTestInterface2 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class new file mode 100644 index 0000000000000000000000000000000000000000..4c2de35ba53158b553e56fddcd455da20b162d9d GIT binary patch literal 248 zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2y~d0sxI~Do_9b literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class new file mode 100644 index 0000000000000000000000000000000000000000..9115bd86b112f3d59d7ce5975a48252339945d7d GIT binary patch literal 248 zcmX^0Z`VEs1_l!bJ}w4k25xo+9(D#^Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2y?L8MU+8-feGjk5MTmgpgsnmYk(|SAk7G*S+%w^Fm41g7#Y}s eBpXUUmjPb_RZS1_4F}Hk-`6%o00B24)S-Fh&Lz=lqmZ zMh1SL%)C^;(%hufqL9R-9H0nSaDHh~a;jS1R71V2#Ii(225}tHj0^%G1^PLOdFlH8Nm;4MC2R}~j0{Xbt3ZH}ff-0LF|Yst DdI}-6 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java new file mode 100644 index 00000000000..47d1a8ddd62 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java @@ -0,0 +1 @@ +interface HierarchyTestInterface1 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class new file mode 100644 index 0000000000000000000000000000000000000000..14eb47f76565dcad26c0d216c92618a21b2703e0 GIT binary patch literal 127 zcmX^0Z`VEs1_l!bc6J61R3p8t#Ii(225}tHj0^%G1^PLOdFlH8Nm;4MC2R}~j0{Xbt3ZH}ff-0LF|Yst DdVL|c literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java new file mode 100644 index 00000000000..bee58260862 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java @@ -0,0 +1 @@ +interface HierarchyTestInterface2 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/test_json.desc b/jbmc/regression/jbmc/class_hierarchy/test_json.desc new file mode 100644 index 00000000000..1a61736d0b1 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/test_json.desc @@ -0,0 +1,7 @@ +CORE symex-driven-lazy-loading-expected-failure +HierarchyTest.class +--show-class-hierarchy --json-ui +activate-multi-line-match +EXIT=0 +SIGNAL=0 +\{\n *"isAbstract": true,\n *"name": "java::HierarchyTest",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestChild(1|2)",\n *"java::HierarchyTestChild(1|2)"\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestGrandchild",\n *"parents": \[\n *"java::HierarchyTestChild1",\n *"java::HierarchyTestInterface1",\n *"java::HierarchyTestInterface2"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild2",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild1",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface1",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface2",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\}, diff --git a/jbmc/regression/jbmc/class_hierarchy/test_plain.desc b/jbmc/regression/jbmc/class_hierarchy/test_plain.desc new file mode 100644 index 00000000000..fa11b97bfeb --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/test_plain.desc @@ -0,0 +1,7 @@ +CORE symex-driven-lazy-loading-expected-failure +HierarchyTest.class +--show-class-hierarchy +activate-multi-line-match +EXIT=0 +SIGNAL=0 +java::HierarchyTest \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestChild(1|2)\n *java::HierarchyTestChild(1|2)\njava::HierarchyTestGrandchild:\n *parents:\n *java::HierarchyTestChild1\n *java::HierarchyTestInterface1\n *java::HierarchyTestInterface2\n *children:\njava::HierarchyTestChild2:\n *parents:\n *java::HierarchyTest\n *children:\njava::HierarchyTestChild1:\n *parents:\n *java::HierarchyTest\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface1 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface2 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 630fc2a283a..a498ab73879 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -645,6 +645,16 @@ int jbmc_parse_optionst::get_goto_program( *this, options, get_message_handler()); lazy_goto_model.initialize(cmdline); + // Show the class hierarchy + if(cmdline.isset("show-class-hierarchy")) + { + class_hierarchyt hierarchy; + hierarchy(lazy_goto_model.symbol_table); + show_class_hierarchy( + hierarchy, get_message_handler(), ui_message_handler.get_ui()); + return CPROVER_EXIT_SUCCESS; + } + // Add failed symbols for any symbol created prior to loading any // particular function: add_failed_symbols(lazy_goto_model.symbol_table); @@ -1079,6 +1089,7 @@ void jbmc_parse_optionst::help() " --show-symbol-table show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + HELP_SHOW_CLASS_HIERARCHY "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 6de84d59d97..616b1d1b9d9 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -22,10 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include #include -#include #include @@ -60,6 +61,7 @@ class optionst; "(string-max-input-length):" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ OPT_SHOW_GOTO_FUNCTIONS \ + OPT_SHOW_CLASS_HIERARCHY \ "(show-loops)" \ "(show-symbol-table)(show-parse-tree)" \ OPT_SHOW_PROPERTIES \ diff --git a/regression/goto-instrument/class-hierarchy/dot.desc b/regression/goto-instrument/class-hierarchy/dot.desc index 77ea28c0e76..e164706a3cc 100644 --- a/regression/goto-instrument/class-hierarchy/dot.desc +++ b/regression/goto-instrument/class-hierarchy/dot.desc @@ -1,6 +1,6 @@ CORE main.c ---class-hierarchy --dot +--show-class-hierarchy --dot digraph class_hierarchy ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/class-hierarchy/plain.desc b/regression/goto-instrument/class-hierarchy/plain.desc index 52367db0168..88144582815 100644 --- a/regression/goto-instrument/class-hierarchy/plain.desc +++ b/regression/goto-instrument/class-hierarchy/plain.desc @@ -1,5 +1,5 @@ CORE main.c ---class-hierarchy +--show-class-hierarchy ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 19efe0c4db2..013a206a00b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -652,16 +652,17 @@ int goto_instrument_parse_optionst::doit() return 0; } - if(cmdline.isset("class-hierarchy")) + if(cmdline.isset("show-class-hierarchy")) { class_hierarchyt hierarchy; hierarchy(goto_model.symbol_table); if(cmdline.isset("dot")) hierarchy.output_dot(std::cout); else - hierarchy.output(std::cout, false); + show_class_hierarchy( + hierarchy, get_message_handler(), ui_message_handler.get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("dot")) @@ -1472,7 +1473,7 @@ void goto_instrument_parse_optionst::help() " --call-graph show graph of function calls\n" // NOLINTNEXTLINE(whitespace/line_length) " --reachable-call-graph show graph of function calls potentially reachable from main function\n" - " --class-hierarchy show class hierarchy\n" + HELP_SHOW_CLASS_HIERARCHY // NOLINTNEXTLINE(whitespace/line_length) " --show-threaded show instructions that may be executed by more than one thread\n" "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 185b793a3a1..60fbe8bd485 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -16,11 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include -#include #include #include +#include +#include #include @@ -50,7 +51,7 @@ Author: Daniel Kroening, kroening@kroening.com "(max-var):(max-po-trans):(ignore-arrays)" \ "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ "(call-graph)(reachable-call-graph)" \ - "(class-hierarchy)" \ + OPT_SHOW_CLASS_HIERARCHY \ "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \ "(nondet-volatile)(isr):" \ "(stack-depth):(nondet-static)" \ diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index efb720d32e7..e5fbb743019 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -192,3 +192,24 @@ void class_hierarchyt::output( json_children.push_back(json_stringt(ch)); } } + +void show_class_hierarchy( + const class_hierarchyt &hierarchy, + message_handlert &message_handler, + ui_message_handlert::uit ui, + bool children_only) +{ + messaget msg(message_handler); + switch(ui) + { + case ui_message_handlert::uit::PLAIN: + hierarchy.output(msg.result(), children_only); + msg.result() << messaget::eom; + break; + case ui_message_handlert::uit::JSON_UI: + hierarchy.output(msg.result().json_stream(), children_only); + break; + case ui_message_handlert::uit::XML_UI: + UNIMPLEMENTED; + } +} diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index b01774b3d0d..daf071451bf 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -20,9 +20,19 @@ Date: April 2016 #include #include +#include + +// clang-format off +#define OPT_SHOW_CLASS_HIERARCHY \ + "(show-class-hierarchy)" + +#define HELP_SHOW_CLASS_HIERARCHY \ + " --show-class-hierarchy show the class hierarchy\n" +// clang-format on class symbol_tablet; class json_stream_arrayt; +class message_handlert; class class_hierarchyt { @@ -96,4 +106,15 @@ class class_hierarchy_grapht : public grapht nodes_by_namet nodes_by_name; }; +/// Output the class hierarchy +/// \param hierarchy: the class hierarchy to be printed +/// \param message_handler: the message handler +/// \param ui: the UI format +/// \param children_only: print the children only and do not print the parents +void show_class_hierarchy( + const class_hierarchyt &hierarchy, + message_handlert &message_handler, + ui_message_handlert::uit ui, + bool children_only = false); + #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H