Add option to use an external version of STP

This patch adds a new configure option, --with-stp, which configures
KLEE to use an external version of STP instead of the version in the
source tree.  It includes documentation referring users to the STP
download location.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 293 insertions, 1 deletions

diff --git a/configure b/configure
index 4f24a6b6..e1622458 100755
--- a/configure
+++ b/configure
@@ -674,6 +674,8 @@ CXX
 CXXFLAGS
 ac_ct_CXX
 CXXCPP
+ENABLE_EXT_STP
+STP_ROOT
 LIBOBJS
 LTLIBOBJS'
 ac_subst_files=''
@@ -1275,6 +1277,7 @@ Optional Packages:
   --with-uclibc           Enable use of the klee uclibc at the given path
   --with-runtime          Select build configuration for runtime libraries
                           (default Release)
+  --with-stp              Location of STP installation directory
 
 Some influential environment variables:
   CC          C compiler command
@@ -4952,6 +4955,293 @@ done
 
 
 
+# Check whether --with-stp was given.
+if test "${with_stp+set}" = set; then
+  withval=$with_stp;
+fi
+
+
+if test X$with_stp = X ; then
+  ENABLE_EXT_STP=0
+
+else
+  stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+  old_CPPFLAGS="$CPPFLAGS"
+  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
+  if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  { echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+else
+  # Is the header compilable?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h usability" >&5
+echo $ECHO_N "checking stp/c_interface.h usability... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h.  */
+$ac_includes_default
+#include <stp/c_interface.h>
+_ACEOF
+rm -f conftest.$ac_objext
+if { (ac_try="$ac_compile"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_compile") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } &&
+	 { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; } &&
+	 { ac_try='test -s conftest.$ac_objext'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; }; then
+  ac_header_compiler=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	ac_header_compiler=no
+fi
+
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_compiler" >&5
+echo "${ECHO_T}$ac_header_compiler" >&6; }
+
+# Is the header present?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h presence" >&5
+echo $ECHO_N "checking stp/c_interface.h presence... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h.  */
+#include <stp/c_interface.h>
+_ACEOF
+if { (ac_try="$ac_cpp conftest.$ac_ext"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_cpp conftest.$ac_ext") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } >/dev/null; then
+  if test -s conftest.err; then
+    ac_cpp_err=$ac_cxx_preproc_warn_flag
+    ac_cpp_err=$ac_cpp_err$ac_cxx_werror_flag
+  else
+    ac_cpp_err=
+  fi
+else
+  ac_cpp_err=yes
+fi
+if test -z "$ac_cpp_err"; then
+  ac_header_preproc=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+  ac_header_preproc=no
+fi
+
+rm -f conftest.err conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_preproc" >&5
+echo "${ECHO_T}$ac_header_preproc" >&6; }
+
+# So?  What about this header?
+case $ac_header_compiler:$ac_header_preproc:$ac_cxx_preproc_warn_flag in
+  yes:no: )
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&5
+echo "$as_me: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&2;}
+    ac_header_preproc=yes
+    ;;
+  no:yes:* )
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: present but cannot be compiled" >&5
+echo "$as_me: WARNING: stp/c_interface.h: present but cannot be compiled" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h:     check for missing prerequisite headers?" >&5
+echo "$as_me: WARNING: stp/c_interface.h:     check for missing prerequisite headers?" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: see the Autoconf documentation" >&5
+echo "$as_me: WARNING: stp/c_interface.h: see the Autoconf documentation" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h:     section \"Present But Cannot Be Compiled\"" >&5
+echo "$as_me: WARNING: stp/c_interface.h:     section \"Present But Cannot Be Compiled\"" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&5
+echo "$as_me: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&2;}
+    ( cat <<\_ASBOX
+## ------------------------------------- ##
+## Report this to daniel@minormatter.com ##
+## ------------------------------------- ##
+_ASBOX
+     ) | sed "s/^/$as_me: WARNING:     /" >&2
+    ;;
+esac
+{ echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+  ac_cv_header_stp_c_interface_h=$ac_header_preproc
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+
+fi
+if test $ac_cv_header_stp_c_interface_h = yes; then
+  :
+else
+
+         { { echo "$as_me:$LINENO: error: Unable to use stp/c_interface.h header" >&5
+echo "$as_me: error: Unable to use stp/c_interface.h header" >&2;}
+   { (exit 1); exit 1; }; }
+
+fi
+
+
+  CPPFLAGS="$old_CPPFLAGS"
+
+
+{ echo "$as_me:$LINENO: checking for vc_setInterfaceFlags in -lstp" >&5
+echo $ECHO_N "checking for vc_setInterfaceFlags in -lstp... $ECHO_C" >&6; }
+if test "${ac_cv_lib_stp_vc_setInterfaceFlags+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lstp -L$stp_root/lib $LIBS"
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* 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
+rm -f conftest.$ac_objext conftest$ac_exeext
+if { (ac_try="$ac_link"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_link") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } &&
+	 { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; } &&
+	 { ac_try='test -s conftest$ac_exeext'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; }; then
+  ac_cv_lib_stp_vc_setInterfaceFlags=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	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
+{ echo "$as_me:$LINENO: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
+echo "${ECHO_T}$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
+if test $ac_cv_lib_stp_vc_setInterfaceFlags = yes; then
+  cat >>confdefs.h <<_ACEOF
+#define HAVE_LIBSTP 1
+_ACEOF
+
+  LIBS="-lstp $LIBS"
+
+else
+
+         { { echo "$as_me:$LINENO: error: Unable to link with libstp" >&5
+echo "$as_me: error: Unable to link with libstp" >&2;}
+   { (exit 1); exit 1; }; }
+
+fi
+
+
+
+cat >>confdefs.h <<\_ACEOF
+#define HAVE_EXT_STP 1
+_ACEOF
+
+  ENABLE_EXT_STP=1
+
+  STP_ROOT=$stp_root
+
+fi
+
+
 ac_config_commands="$ac_config_commands Makefile"
 
 
@@ -5676,11 +5966,13 @@ CXX!$CXX$ac_delim
 CXXFLAGS!$CXXFLAGS$ac_delim
 ac_ct_CXX!$ac_ct_CXX$ac_delim
 CXXCPP!$CXXCPP$ac_delim
+ENABLE_EXT_STP!$ENABLE_EXT_STP$ac_delim
+STP_ROOT!$STP_ROOT$ac_delim
 LIBOBJS!$LIBOBJS$ac_delim
 LTLIBOBJS!$LTLIBOBJS$ac_delim
 _ACEOF
 
-  if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 76; then
+  if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 78; then
     break
   elif $ac_last_try; then
     { { echo "$as_me:$LINENO: error: could not make $CONFIG_STATUS" >&5