Upstream STP's libstp now depends on boost. This commit updates

the configure script to detect this by first trying to link without
boost and if that fails then trying to link libstp with boost.

This also updates the relevant Makefiles so that the klee and kleaver
executables link in STP's boost dependencies if necessary.

5 files changed, 108 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