about summary refs log tree commit diff homepage
path: root/lib/Solver/Z3Builder.h
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-09-16 08:47:42 +0100
committerDan Liew <delcypher@gmail.com>2017-06-01 11:36:09 +0100
commit9a73071e22b408bb9bf5c24ec2d7eeb3a8a16e96 (patch)
tree608e18daea71e838d35a2d533d509d06a7ce3cfe /lib/Solver/Z3Builder.h
parent11fd589bb7c0c075dc9c5cb1e7a0eecd9eb94ef1 (diff)
downloadklee-9a73071e22b408bb9bf5c24ec2d7eeb3a8a16e96.tar.gz
[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations
into `Z3Builder.cpp` so they can be called from in gdb.
Diffstat (limited to 'lib/Solver/Z3Builder.h')
-rw-r--r--lib/Solver/Z3Builder.h10
1 files changed, 2 insertions, 8 deletions
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> {