From 1402e6018fc47cd7041eb6fc37f59218ace235e5 Mon Sep 17 00:00:00 2001
From: Marek Trtik <trtik@diffblue.com>
Date: Wed, 15 Mar 2017 11:10:25 +0000
Subject: [PATCH 1/3] Added output in DOT format.

---
 src/goto-programs/class_hierarchy.cpp | 15 +++++++++++++++
 src/goto-programs/class_hierarchy.h   | 15 +++++++++++++++
 2 files changed, 30 insertions(+)

diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp
index 1311a3e7fdc..285aff2bc54 100644
--- a/src/goto-programs/class_hierarchy.cpp
+++ b/src/goto-programs/class_hierarchy.cpp
@@ -135,3 +135,18 @@ void class_hierarchyt::output(std::ostream &out) const
           << ch << '\n';
   }
 }
+
+std::ostream &output_dot(std::ostream &ostr, const class_hierarchyt &hierarchy)
+{
+  ostr << "digraph call_graph {\n"
+       << "  rankdir=BT;\n"
+       << "  node [fontsize=12 shape=box];\n";
+  for(const auto &c : hierarchy.class_map)
+    for(const auto &ch : c.second.parents)
+      ostr << "  \"" << c.first << "\" -> "
+           << "\"" << ch << "\" "
+           << " [arrowhead=\"vee\"];"
+           << "\n";
+  ostr << "}\n";
+  return ostr;
+}
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index bef2c7ec7eb..81a575e5aa1 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -55,4 +55,19 @@ class class_hierarchyt
   void get_parents_trans_rec(const irep_idt &, idst &) const;
 };
 
+
+/*******************************************************************\
+
+Function: output_dot
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+std::ostream &output_dot(std::ostream &ostr, const class_hierarchyt &hierarchy);
+
+
 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H

From 58ea4b09bc425227ac07aed6b9ec284606dee461 Mon Sep 17 00:00:00 2001
From: Marek Trtik <trtik@diffblue.com>
Date: Thu, 16 Mar 2017 12:26:37 +0000
Subject: [PATCH 2/3] Unimportant: moved empty comment from one place to
 another.

---
 src/goto-programs/class_hierarchy.cpp | 12 ++++++++++++
 src/goto-programs/class_hierarchy.h   | 11 -----------
 2 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp
index 285aff2bc54..14e8cdadee9 100644
--- a/src/goto-programs/class_hierarchy.cpp
+++ b/src/goto-programs/class_hierarchy.cpp
@@ -136,6 +136,18 @@ void class_hierarchyt::output(std::ostream &out) const
   }
 }
 
+/*******************************************************************\
+
+Function: output_dot
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 std::ostream &output_dot(std::ostream &ostr, const class_hierarchyt &hierarchy)
 {
   ostr << "digraph call_graph {\n"
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index 81a575e5aa1..c75f0e487e7 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -56,17 +56,6 @@ class class_hierarchyt
 };
 
 
-/*******************************************************************\
-
-Function: output_dot
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
 std::ostream &output_dot(std::ostream &ostr, const class_hierarchyt &hierarchy);
 
 

From 3df5732effc314b5e3bbe9fa1d68a4053f047e41 Mon Sep 17 00:00:00 2001
From: Marek Trtik <trtik@diffblue.com>
Date: Tue, 21 Mar 2017 10:17:26 +0000
Subject: [PATCH 3/3] Updates requested in PR #642: Removal of blank lines.

---
 src/goto-programs/class_hierarchy.h | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index c75f0e487e7..d124c66e558 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -55,8 +55,6 @@ class class_hierarchyt
   void get_parents_trans_rec(const irep_idt &, idst &) const;
 };
 
-
 std::ostream &output_dot(std::ostream &ostr, const class_hierarchyt &hierarchy);
 
-
 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H