about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.config.in6
-rw-r--r--autoconf/configure.ac29
-rwxr-xr-xconfigure74
-rw-r--r--tools/kleaver/Makefile4
-rw-r--r--tools/klee/Makefile4
-rw-r--r--unittests/Solver/Makefile4
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