diff options
-rwxr-xr-x | .travis/stp.sh | 12 | ||||
-rw-r--r-- | Makefile.common | 1 | ||||
-rw-r--r-- | autoconf/configure.ac | 19 | ||||
-rwxr-xr-x | configure | 64 | ||||
-rw-r--r-- | tools/kleaver/Makefile | 2 | ||||
-rw-r--r-- | tools/klee/Makefile | 2 | ||||
-rw-r--r-- | unittests/Expr/Makefile | 2 | ||||
-rw-r--r-- | unittests/Ref/Makefile | 2 | ||||
-rw-r--r-- | unittests/Solver/Makefile | 2 |
9 files changed, 98 insertions, 8 deletions
diff --git a/.travis/stp.sh b/.travis/stp.sh index abc4e566..1c8fdb48 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -6,6 +6,18 @@ set -e STP_LOG="$(pwd)/stp-build.log" if [ "${STP_VERSION}" == "UPSTREAM" ]; then + # Build minisat + git clone https://github.com/niklasso/minisat + cd minisat + mkdir build + cd build + MINISAT_DIR=`pwd` + cmake -DCMAKE_INSTALL_PREFIX=/usr .. + make + sudo make install + cd ../../ + + # Build STP git clone --depth 1 git://github.com/stp/stp.git src mkdir build cd build diff --git a/Makefile.common b/Makefile.common index 92f5118b..964a7475 100644 --- a/Makefile.common +++ b/Makefile.common @@ -38,7 +38,6 @@ endif # This is filename that KLEE will look for when trying to load klee-uclibc KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca" -LD.Flags += $(STP_LDFLAGS) CXX.Flags += $(STP_CFLAGS) CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\" CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\" diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 5b9c4e58..8d4f465c 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -576,10 +576,27 @@ AC_CHECK_HEADER(stp/c_interface.h,, ]) CPPFLAGS="$old_CPPFLAGS" +STP_NEEDS_MINISAT=0 AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [ - AC_MSG_ERROR([Could not link with libstp]) + STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp]) ], "$STP_LDFLAGS") +dnl Try linking again with minisat if necessary +if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags + + AC_CHECK_LIB(stp, + vc_setInterfaceFlags,, [ + AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong]) + ], "$STP_LDFLAGS" "-lminisat" ) + + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" +else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" +fi + + AC_SUBST(STP_CFLAGS) AC_SUBST(STP_LDFLAGS) diff --git a/configure b/configure index 82657008..85d10756 100755 --- a/configure +++ b/configure @@ -5085,6 +5085,7 @@ fi CPPFLAGS="$old_CPPFLAGS" +STP_NEEDS_MINISAT=0 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : @@ -5130,11 +5131,72 @@ _ACEOF else - as_fn_error $? "Could not link with libstp" "$LINENO" 5 + STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5 +$as_echo "Could not link with libstp" >&6; } fi +if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags + + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 +$as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } +if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_check_lib_save_LIBS=$LIBS +LIBS="-lstp "$STP_LDFLAGS" "-lminisat" $LIBS" +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char vc_setInterfaceFlags (); +int +main () +{ +return vc_setInterfaceFlags (); + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + ac_cv_lib_stp_vc_setInterfaceFlags=yes +else + ac_cv_lib_stp_vc_setInterfaceFlags=no +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext +LIBS=$ac_check_lib_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5 +$as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; } +if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_LIBSTP 1 +_ACEOF + + LIBS="-lstp $LIBS" + +else + + as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5 + +fi + + + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" +else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" +fi + + diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index f66d0598..10b19a20 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -19,7 +19,7 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common -LIBS += -lstp +LIBS += $(STP_LDFLAGS) ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/tools/klee/Makefile b/tools/klee/Makefile index b9506b47..eb80d845 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -20,7 +20,7 @@ LINK_COMPONENTS += irreader endif include $(LEVEL)/Makefile.common -LIBS += -lstp +LIBS += $(STP_LDFLAGS) ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile index a9bfeda1..e52aea31 100644 --- a/unittests/Expr/Makefile +++ b/unittests/Expr/Makefile @@ -10,4 +10,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest CXXFLAGS += -DLLVM_29_UNITTEST -LIBS += -lstp +LIBS += $(STP_LDFLAGS) diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile index 94bbb83c..14dcc8bd 100644 --- a/unittests/Ref/Makefile +++ b/unittests/Ref/Makefile @@ -9,4 +9,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest -LIBS += -lstp +LIBS += $(STP_LDFLAGS) diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index 00713691..aeac34ac 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -9,4 +9,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest -LIBS += -lstp +LIBS += $(STP_LDFLAGS) |