From 155eae5f80b83786daf693c92f787ccd2a51af10 Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Wed, 22 Oct 2014 10:28:46 +0200 Subject: configure: allow stp being installed in / I have stp in standard paths: /usr/include and /usr/lib64. Allow that by correct STP_CFLAGS + STP_LDFLAGS instead of STP_ROOT. Those are empty when --with-stp is not passed. configure is regenerated by autoconf too. Signed-off-by: Jiri Slaby --- Makefile.common | 4 +-- Makefile.config.in | 3 +- autoconf/configure.ac | 91 ++++++++++++++++++++++++++------------------------- configure | 76 +++++++++++++++++++++--------------------- 4 files changed, 88 insertions(+), 86 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..b2474849 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -29,7 +29,8 @@ PROJ_INSTALL_ROOT := @prefix@ KLEE_USE_CXX11 := @KLEE_USE_CXX11@ -STP_ROOT := @STP_ROOT@ +STP_CFLAGS := @STP_CFLAGS@ +STP_LDFLAGS := @STP_LDFLAGS@ STP_NEEDS_BOOST := @STP_NEEDS_BOOST@ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 97bd5eb6..a5f12c5f 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -552,55 +552,56 @@ dnl ************************************************************************** AC_ARG_WITH(stp, AS_HELP_STRING([--with-stp], - [Location of STP installation directory]),, - [AC_MSG_ERROR([The --with-stp= argument is mandatory where is the path \ -to the root of your STP install])]) - -#Check for empty argument -if test "X$with_stp" = X ; then - AC_MSG_ERROR([ cannot be empty in --with-stp=]) -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" - - 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]) - ], -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 ) + [Location of STP installation directory]),[ + #Check for empty argument + if test "X$withval" = X ; then + AC_MSG_ERROR([ cannot be empty in --with-stp=]) + fi + stp_root=`(cd $withval && pwd) 2> /dev/null` - 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 + #Check for bad path + if test "X$stp_root" = X ; then + AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp]) + fi - AC_SUBST(STP_ROOT,$stp_root) + STP_CFLAGS="-I$stp_root/include" + STP_LDFLAGS="-L$stp_root/lib" + ]) + +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" + +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]) +], "$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) + dnl ************************************************************************** dnl User option to enable metaSMT constraint solvers and to specify the dnl the location of the metaSMT root directory diff --git a/configure b/configure index 6db9baf0..ae7ae0b0 100755 --- a/configure +++ b/configure @@ -626,7 +626,8 @@ ac_subst_vars='LTLIBOBJS LIBOBJS METASMT_ROOT ENABLE_METASMT -STP_ROOT +STP_LDFLAGS +STP_CFLAGS STP_NEEDS_BOOST UPSTREAM_STP_LINK_FLAGS CXXCPP @@ -5055,47 +5056,47 @@ fi # Check whether --with-stp was given. if test "${with_stp+set}" = set; then : withval=$with_stp; -else - as_fn_error $? "The --with-stp= argument is mandatory where is the path \ -to the root of your STP install" "$LINENO" 5 -fi + #Check for empty argument + if test "X$withval" = X ; then + as_fn_error $? " cannot be empty in --with-stp=" "$LINENO" 5 + fi + stp_root=`(cd $withval && 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 -#Check for empty argument -if test "X$with_stp" = X ; then - as_fn_error $? " cannot be empty in --with-stp=" "$LINENO" 5 -else - stp_root=`(cd $with_stp && pwd) 2> /dev/null` + STP_CFLAGS="-I$stp_root/include" + STP_LDFLAGS="-L$stp_root/lib" - #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 +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" + +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 - 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" +CPPFLAGS="$old_CPPFLAGS" - STP_NEEDS_BOOST=0 +STP_NEEDS_BOOST=0 - # Try old STP - { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 +# 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" +LIBS="-lstp "$STP_LDFLAGS" $LIBS" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ @@ -5134,24 +5135,24 @@ _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 + 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 +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 "$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" $UPSTREAM_STP_LINK_FLAGS $LIBS" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ @@ -5190,23 +5191,22 @@ _ACEOF else - as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5 + 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 + UPSTREAM_STP_LINK_FLAGS=$UPSTREAM_STP_LINK_FLAGS - STP_NEEDS_BOOST=$STP_NEEDS_BOOST + STP_NEEDS_BOOST=$STP_NEEDS_BOOST - else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: Using old STP" >&5 +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Using old STP" >&5 $as_echo "Using old STP" >&6; } - fi +fi + - STP_ROOT=$stp_root -fi -- cgit 1.4.1 From 5c692a7feb6a378e83de58927556ff587e7d2e47 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 1 Nov 2014 21:51:52 +0000 Subject: 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. --- Makefile.config.in | 6 ---- autoconf/configure.ac | 29 ++++--------------- configure | 74 ++--------------------------------------------- tools/kleaver/Makefile | 4 --- tools/klee/Makefile | 4 --- 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 -- cgit 1.4.1