diff options
-rw-r--r-- | Makefile.config.in | 6 | ||||
-rw-r--r-- | autoconf/configure.ac | 22 | ||||
-rwxr-xr-x | configure | 72 | ||||
-rw-r--r-- | tools/kleaver/Makefile | 6 | ||||
-rw-r--r-- | tools/klee/Makefile | 6 | ||||
-rw-r--r-- | unittests/Solver/Makefile | 4 |
6 files changed, 112 insertions, 4 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 35f7bcfe..a6dcdcaa 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -29,6 +29,12 @@ PROJ_INSTALL_ROOT := @prefix@ STP_ROOT := @STP_ROOT@ +STP_NEEDS_BOOST := @STP_NEEDS_BOOST@ + +ifeq ($(STP_NEEDS_BOOST),1) + UPSTREAM_STP_LINK_FLAGS = @UPSTREAM_STP_LINK_FLAGS@ +endif + ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index af5affc0..7d4ff994 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -523,10 +523,30 @@ else ]) CPPFLAGS="$old_CPPFLAGS" + STP_NEEDS_BOOST=0 + + # Try old STP AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [ - AC_MSG_ERROR([Unable to link with libstp]) + STP_NEEDS_BOOST=1 ; AC_MSG_RESULT([Could not link with libstp. Checking if newer STP is being used]) ], -L$stp_root/lib) + dnl Flags for upstream STP which has boost dependency + UPSTREAM_STP_LINK_FLAGS="-lboost_system -lboost_program_options" + if test "X$STP_NEEDS_BOOST" != 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]) + ], -L$stp_root/lib $UPSTREAM_STP_LINK_FLAGS ) + + AC_SUBST(UPSTREAM_STP_LINK_FLAGS, $UPSTREAM_STP_LINK_FLAGS) + AC_SUBST(STP_NEEDS_BOOST, $STP_NEEDS_BOOST) + else + AC_MSG_RESULT([Using old STP]) + fi + AC_SUBST(STP_ROOT,$stp_root) fi diff --git a/configure b/configure index d343ac69..55497c3a 100755 --- a/configure +++ b/configure @@ -627,6 +627,8 @@ LIBOBJS METASMT_ROOT ENABLE_METASMT STP_ROOT +STP_NEEDS_BOOST +UPSTREAM_STP_LINK_FLAGS CXXCPP ac_ct_CXX CXXFLAGS @@ -4868,6 +4870,9 @@ fi CPPFLAGS="$old_CPPFLAGS" + STP_NEEDS_BOOST=0 + + # Try old STP { $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 : @@ -4913,11 +4918,76 @@ _ACEOF else - as_fn_error $? "Unable to link with libstp" "$LINENO" 5 + STP_NEEDS_BOOST=1 ; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp. Checking if newer STP is being used" >&5 +$as_echo "Could not link with libstp. Checking if newer STP is being used" >&6; } + +fi + + + UPSTREAM_STP_LINK_FLAGS="-lboost_system -lboost_program_options" + if test "X$STP_NEEDS_BOOST" != 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 -L$stp_root/lib $UPSTREAM_STP_LINK_FLAGS $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 + UPSTREAM_STP_LINK_FLAGS=$UPSTREAM_STP_LINK_FLAGS + + STP_NEEDS_BOOST=$STP_NEEDS_BOOST + + else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Using old STP" >&5 +$as_echo "Using old STP" >&6; } + fi + STP_ROOT=$stp_root fi diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index b93e361d..39ba8fdb 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -30,4 +30,8 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags += -DBOOST_HAS_GCC_TR1 CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core -endif \ No newline at end of file +endif + +ifeq ($(STP_NEEDS_BOOST),1) + LIBS += $(UPSTREAM_STP_LINK_FLAGS) +endif diff --git a/tools/klee/Makefile b/tools/klee/Makefile index f050bf74..ce5a21e6 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -31,4 +31,8 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags += -DBOOST_HAS_GCC_TR1 CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core -endif \ No newline at end of file +endif + +ifeq ($(STP_NEEDS_BOOST),1) + LIBS += $(UPSTREAM_STP_LINK_FLAGS) +endif diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index 00713691..83427795 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -10,3 +10,7 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest LIBS += -lstp + +ifeq ($(STP_NEEDS_BOOST),1) + LIBS += $(UPSTREAM_STP_LINK_FLAGS) +endif |