Merge pull request #174 from delcypher/allow_stp_installed_in_root

Allow stp installed in root

7 files changed, 51 insertions, 156 deletions

diff --git a/Makefile.common b/Makefile.common
index e6de9f1e..92f5118b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -38,8 +38,8 @@ endif
 # This is filename that KLEE will look for when trying to load klee-uclibc
 KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
 
-LD.Flags += -L$(STP_ROOT)/lib
-CXX.Flags += -I$(STP_ROOT)/include
+LD.Flags += $(STP_LDFLAGS)
+CXX.Flags += $(STP_CFLAGS)
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
 CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\"
 
diff --git a/Makefile.config.in b/Makefile.config.in
index c8e2b57f..ee95c4e5 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -29,13 +29,8 @@ PROJ_INSTALL_ROOT := @prefix@
 
 KLEE_USE_CXX11 := @KLEE_USE_CXX11@
 
-STP_ROOT := @STP_ROOT@
-
-STP_NEEDS_BOOST := @STP_NEEDS_BOOST@
-
-ifeq ($(STP_NEEDS_BOOST),1)
- UPSTREAM_STP_LINK_FLAGS = @UPSTREAM_STP_LINK_FLAGS@
-endif
+STP_CFLAGS := @STP_CFLAGS@
+STP_LDFLAGS := @STP_LDFLAGS@
 
 ENABLE_METASMT := @ENABLE_METASMT@
 METASMT_ROOT := @METASMT_ROOT@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 97bd5eb6..5b9c4e58 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -552,54 +552,36 @@ dnl **************************************************************************
 
 AC_ARG_WITH(stp,
   AS_HELP_STRING([--with-stp],
-    [Location of STP installation directory]),,
-    [AC_MSG_ERROR([The --with-stp=<path> argument is mandatory where <path> is the path \
-to the root of your STP install])])
-
-#Check for empty argument
-if test "X$with_stp" = X ; then
-	AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
-else
-  stp_root=`(cd $with_stp && pwd) 2> /dev/null`
-
-  #Check for bad path
-  if test "X$stp_root" = X ; then
-  	AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
-  fi
-
-  old_CPPFLAGS="$CPPFLAGS"
-  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
-  AC_CHECK_HEADER(stp/c_interface.h,, [
-         AC_MSG_ERROR([Unable to use stp/c_interface.h header])
-  ])
-  CPPFLAGS="$old_CPPFLAGS"
+    [Location of STP installation directory]),[
+      #Check for empty argument
+      if test "X$withval" = X ; then
+	      AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
+      fi
+      stp_root=`(cd $withval && pwd) 2> /dev/null`
 
-  STP_NEEDS_BOOST=0
+      #Check for bad path
+      if test "X$stp_root" = X ; then
+	    AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
+      fi
 
-  # 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])
-  ], -L$stp_root/lib)
+      STP_CFLAGS="-I$stp_root/include"
+      STP_LDFLAGS="-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
+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])
+    ])
+CPPFLAGS="$old_CPPFLAGS"
 
-    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_CHECK_LIB(stp, vc_setInterfaceFlags,, [
+       AC_MSG_ERROR([Could not link with libstp])
+], "$STP_LDFLAGS")
 
-    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
+AC_SUBST(STP_CFLAGS)
+AC_SUBST(STP_LDFLAGS)
 
 dnl **************************************************************************
 dnl User option to enable metaSMT constraint solvers and to specify the 
diff --git a/configure b/configure
index 6db9baf0..82657008 100755
--- a/configure
+++ b/configure
@@ -626,9 +626,8 @@ ac_subst_vars='LTLIBOBJS
 LIBOBJS
 METASMT_ROOT
 ENABLE_METASMT
-STP_ROOT
-STP_NEEDS_BOOST
-UPSTREAM_STP_LINK_FLAGS
+STP_LDFLAGS
+STP_CFLAGS
 CXXCPP
 HAVE_SELINUX
 EGREP
@@ -5055,103 +5054,44 @@ fi
 # Check whether --with-stp was given.
 if test "${with_stp+set}" = set; then :
   withval=$with_stp;
-else
-  as_fn_error $? "The --with-stp=<path> argument is mandatory where <path> is the path \
-to the root of your STP install" "$LINENO" 5
-fi
-
-
-#Check for empty argument
-if test "X$with_stp" = X ; then
-	as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
-else
-  stp_root=`(cd $with_stp && pwd) 2> /dev/null`
-
-  #Check for bad path
-  if test "X$stp_root" = X ; then
-  	as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
-  fi
-
-  old_CPPFLAGS="$CPPFLAGS"
-  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
-  ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
-if test "x$ac_cv_header_stp_c_interface_h" = xyes; then :
+      #Check for empty argument
+      if test "X$withval" = X ; then
+	      as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
+      fi
+      stp_root=`(cd $withval && pwd) 2> /dev/null`
 
-else
+      #Check for bad path
+      if test "X$stp_root" = X ; then
+	    as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
+      fi
 
-         as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
+      STP_CFLAGS="-I$stp_root/include"
+      STP_LDFLAGS="-L$stp_root/lib"
 
 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 :
-  $as_echo_n "(cached) " >&6
-else
-  ac_check_lib_save_LIBS=$LIBS
-LIBS="-lstp -L$stp_root/lib $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"
+old_CPPFLAGS="$CPPFLAGS"
+CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
+ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
+if test "x$ac_cv_header_stp_c_interface_h" = xyes; then :
 
 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; }
+        as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
 
 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
+CPPFLAGS="$old_CPPFLAGS"
 
-    { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+{ $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"
+LIBS="-lstp "$STP_LDFLAGS" $LIBS"
 cat confdefs.h - <<_ACEOF >conftest.$ac_ext
 /* end confdefs.h.  */
 
@@ -5190,23 +5130,13 @@ _ACEOF
 
 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
-
-  STP_ROOT=$stp_root
-
-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