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