diff options
| -rw-r--r-- | autoconf/configure.ac | 16 | ||||
| -rwxr-xr-x | configure | 33 | ||||
| -rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
| -rw-r--r-- | lib/Solver/Z3Builder.cpp | 9 |
4 files changed, 60 insertions, 1 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 94928fcc..617469e6 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -651,6 +651,22 @@ if test "X$ENABLE_Z3" != X0 ; then AC_MSG_ERROR([Unable to link against z3]) ], "$Z3_LDFLAGS") + # Test which function signature of ``Z3_get_error_msg()`` we need to use. + # There's an API break between Z3 4.4.1 and the master branch + AC_MSG_CHECKING([if Z3_get_error_msg() requires Z3_context]) + AC_COMPILE_IFELSE( + [AC_LANG_PROGRAM([[#include "z3.h"]], + [[Z3_context c = Z3_mk_context(0); Z3_get_error_msg(c, Z3_OK);]])], + [Z3_HAS_ERROR_MSG_CONTEXT=1], + [Z3_HAS_ERROR_MSG_CONTEXT=0]) + + if test "X$Z3_HAS_ERROR_MSG_CONTEXT" == X1; then + AC_DEFINE(HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT, [1], [Z3 needs a Z3_context passed to Z3_get_error_msg()]) + AC_MSG_RESULT([yes]) + else + AC_MSG_RESULT([no]) + fi + Z3_LDFLAGS="${Z3_LDFLAGS} -lz3" AC_MSG_NOTICE([Using Z3 solver backend]) CPPFLAGS="$old_CPPFLAGS" diff --git a/configure b/configure index 571c4338..4da72718 100755 --- a/configure +++ b/configure @@ -5109,6 +5109,39 @@ else fi + # Test which function signature of ``Z3_get_error_msg()`` we need to use. + # There's an API break between Z3 4.4.1 and the master branch + { $as_echo "$as_me:${as_lineno-$LINENO}: checking if Z3_get_error_msg() requires Z3_context" >&5 +$as_echo_n "checking if Z3_get_error_msg() requires Z3_context... " >&6; } + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ +#include "z3.h" +int +main () +{ +Z3_context c = Z3_mk_context(0); Z3_get_error_msg(c, Z3_OK); + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_compile "$LINENO"; then : + Z3_HAS_ERROR_MSG_CONTEXT=1 +else + Z3_HAS_ERROR_MSG_CONTEXT=0 +fi +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext + + if test "X$Z3_HAS_ERROR_MSG_CONTEXT" == X1; then + +$as_echo "#define HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT 1" >>confdefs.h + + { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5 +$as_echo "yes" >&6; } + else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } + fi + Z3_LDFLAGS="${Z3_LDFLAGS} -lz3" { $as_echo "$as_me:${as_lineno-$LINENO}: Using Z3 solver backend" >&5 $as_echo "$as_me: Using Z3 solver backend" >&6;} diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 28eefcb6..66bf31cb 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -63,6 +63,9 @@ /* Define to 1 if you have the <unistd.h> header file. */ #undef HAVE_UNISTD_H +/* Z3 needs a Z3_context passed to Z3_get_error_msg() */ +#undef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT + /* LLVM version is release (instead of development) */ #undef LLVM_IS_RELEASE diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index f928c927..ae78c21c 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -27,7 +27,14 @@ llvm::cl::opt<bool> UseConstructHashZ3( } void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { - ::Z3_string errorMsg = Z3_get_error_msg(ctx, ec); + ::Z3_string errorMsg = +#ifdef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT + // Z3 > 4.4.1 + Z3_get_error_msg(ctx, ec); +#else + // Z3 4.4.1 + Z3_get_error_msg(ec); +#endif // FIXME: This is kind of a hack. The value comes from the enum // Z3_CANCELED_MSG but this isn't currently exposed by Z3's C API if (strcmp(errorMsg, "canceled") == 0) { |