diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-11-01 21:51:52 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-11-01 21:51:52 +0000 |
commit | 5c692a7feb6a378e83de58927556ff587e7d2e47 (patch) | |
tree | 5fd7d80e2367ff07476f90128484c946ecbcae51 | |
parent | 155eae5f80b83786daf693c92f787ccd2a51af10 (diff) | |
download | klee-5c692a7feb6a378e83de58927556ff587e7d2e47.tar.gz |
Upstream libstp is no longer dependent on Boost so remove the
configure/Makefile code that adds Boost as a depdendency because We don't need to support old versions of STP that needed Boost.
-rw-r--r-- | Makefile.config.in | 6 | ||||
-rw-r--r-- | autoconf/configure.ac | 29 | ||||
-rwxr-xr-x | configure | 74 | ||||
-rw-r--r-- | tools/kleaver/Makefile | 4 | ||||
-rw-r--r-- | tools/klee/Makefile | 4 | ||||
-rw-r--r-- | unittests/Solver/Makefile | 4 |
6 files changed, 7 insertions, 114 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index b2474849..ee95c4e5 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -32,12 +32,6 @@ KLEE_USE_CXX11 := @KLEE_USE_CXX11@ STP_CFLAGS := @STP_CFLAGS@ STP_LDFLAGS := @STP_LDFLAGS@ -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 a5f12c5f..5b9c4e58 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -570,35 +570,16 @@ AC_ARG_WITH(stp, old_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS $STP_CFLAGS" -AC_CHECK_HEADER(stp/c_interface.h,, [ - AC_MSG_ERROR([Unable to use stp/c_interface.h header]) -]) +AC_CHECK_HEADER(stp/c_interface.h,, + [ + AC_MSG_ERROR([Unable to use stp/c_interface.h header]) + ]) CPPFLAGS="$old_CPPFLAGS" -STP_NEEDS_BOOST=0 - -# Try old STP AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [ - STP_NEEDS_BOOST=1 ; AC_MSG_RESULT([Could not link with libstp. Checking if newer STP is being used]) + AC_MSG_ERROR([Could not link with libstp]) ], "$STP_LDFLAGS") -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]) - ], "$STP_LDFLAGS" $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_CFLAGS) AC_SUBST(STP_LDFLAGS) diff --git a/configure b/configure index ae7ae0b0..82657008 100755 --- a/configure +++ b/configure @@ -628,8 +628,6 @@ METASMT_ROOT ENABLE_METASMT STP_LDFLAGS STP_CFLAGS -STP_NEEDS_BOOST -UPSTREAM_STP_LINK_FLAGS CXXCPP HAVE_SELINUX EGREP @@ -5080,16 +5078,13 @@ if test "x$ac_cv_header_stp_c_interface_h" = xyes; then : else - as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5 + as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5 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 : @@ -5135,76 +5130,11 @@ _ACEOF else - 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 "$STP_LDFLAGS" $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 + as_fn_error $? "Could not link with libstp" "$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 - diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index 656ffeae..f66d0598 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -31,7 +31,3 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lrt -lboolector -lminisat_core endif - -ifeq ($(STP_NEEDS_BOOST),1) - LIBS += $(UPSTREAM_STP_LINK_FLAGS) -endif diff --git a/tools/klee/Makefile b/tools/klee/Makefile index 03b387c0..b9506b47 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -32,7 +32,3 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lrt -lboolector -lminisat_core endif - -ifeq ($(STP_NEEDS_BOOST),1) - LIBS += $(UPSTREAM_STP_LINK_FLAGS) -endif diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index 83427795..00713691 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -10,7 +10,3 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest LIBS += -lstp - -ifeq ($(STP_NEEDS_BOOST),1) - LIBS += $(UPSTREAM_STP_LINK_FLAGS) -endif |