diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Solver/Z3Builder.cpp | 13 | ||||
-rw-r--r-- | 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> { |