From 9a73071e22b408bb9bf5c24ec2d7eeb3a8a16e96 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 16 Sep 2016 08:47:42 +0100
Subject: [Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations
 into `Z3Builder.cpp` so they can be called from in gdb.

---
 lib/Solver/Z3Builder.cpp | 13 +++++++++++++
 lib/Solver/Z3Builder.h   | 10 ++--------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index d111c3a0..a1448415 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -28,6 +28,18 @@ llvm::cl::opt<bool> UseConstructHashZ3(
     llvm::cl::init(true));
 }
 
+namespace klee {
+
+// Declared here rather than `Z3Builder.h` so they can be called in gdb.
+template <> void Z3NodeHandle<Z3_sort>::dump() {
+  llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node)
+               << "\n";
+}
+template <> void Z3NodeHandle<Z3_ast>::dump() {
+  llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast())
+               << "\n";
+}
+
 void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) {
   ::Z3_string errorMsg =
 #ifdef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT
@@ -820,4 +832,5 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) {
     return getTrue();
   }
 }
+}
 #endif // ENABLE_Z3
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
index f3b2732b..c41eace0 100644
--- a/lib/Solver/Z3Builder.h
+++ b/lib/Solver/Z3Builder.h
@@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() {
   // instead to simplify our implementation but this seems cleaner.
   return ::Z3_sort_to_ast(context, node);
 }
-template <> inline void Z3NodeHandle<Z3_sort>::dump() {
-  llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node)
-               << "\n";
-}
 typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
+template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used));
 
 // Specialise for Z3_ast
 template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
-template <> inline void Z3NodeHandle<Z3_ast>::dump() {
-  llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast())
-               << "\n";
-}
 typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
+template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used));
 
 class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> {
 
-- 
cgit 1.4.1