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.
---
Makefile | 8 +-
Makefile.common | 9 +-
Makefile.config.in | 3 +
autoconf/configure.ac | 25 ++++
configure | 294 ++++++++++++++++++++++++++++++++++++++-
include/klee/Config/config.h.in | 6 +
lib/Solver/STPBuilder.h | 4 +
lib/Solver/Solver.cpp | 3 +
tools/kleaver/Makefile | 13 ++-
tools/klee/Makefile | 13 ++-
www/GetStarted.html | 34 +++++
11 files changed, 404 insertions(+), 8 deletions(-)
diff --git a/Makefile b/Makefile
index 2c3ab72..44a9b83 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,13 @@
#
LEVEL = .
-DIRS = stp lib tools runtime
+include $(LEVEL)/Makefile.config
+
+DIRS = lib
+ifeq ($(ENABLE_EXT_STP),0)
+ DIRS += stp
+endif
+DIRS += tools runtime
EXTRA_DIST = include
# Only build support directories when building unittests.
diff --git a/Makefile.common b/Makefile.common
index f3a8f8b..ff83602 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -26,8 +26,13 @@ LLVMCC := $(LLVMGCC)
LLVMCXX := $(LLVMGXX)
endif
-LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
-CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+ifeq ($(ENABLE_EXT_STP),1)
+ LD.Flags += -L$(STP_ROOT)/lib
+ CXX.Flags += -I$(STP_ROOT)/include
+else
+ LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
+ CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+endif
CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\"
# For STP.
diff --git a/Makefile.config.in b/Makefile.config.in
index 0b85883..4d9718d 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -20,6 +20,9 @@ PROJ_OBJ_ROOT := $(subst //,/, at abs_top_objdir@)
# Set the root directory of this project's install prefix
PROJ_INSTALL_ROOT := @prefix@
+ENABLE_EXT_STP := @ENABLE_EXT_STP@
+STP_ROOT := @STP_ROOT@
+
ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
ENABLE_STPLOG := @ENABLE_STPLOG@
ENABLE_UCLIBC := @ENABLE_UCLIBC@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 4266ac4..015c4f4 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -262,6 +262,31 @@ AC_CHECK_HEADERS([selinux/selinux.h],
AC_SUBST(HAVE_SELINUX, 1),
AC_SUBST(HAVE_SELINUX, 0))
+AC_ARG_WITH(stp,
+ AS_HELP_STRING([--with-stp],
+ [Location of STP installation directory]),,)
+
+if test X$with_stp = X ; then
+ AC_SUBST(ENABLE_EXT_STP,[[0]])
+else
+ stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+ 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"
+
+ AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
+ AC_MSG_ERROR([Unable to link with libstp])
+ ], -L$stp_root/lib)
+
+ AC_DEFINE(HAVE_EXT_STP, 1, [Using external STP])
+ AC_SUBST(ENABLE_EXT_STP,[[1]])
+ AC_SUBST(STP_ROOT,$stp_root)
+fi
+
dnl **************************************************************************
dnl * Create the output files
dnl **************************************************************************
diff --git a/configure b/configure
index 4f24a6b..e162245 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 at 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
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 88f92d9..653b27a 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -3,9 +3,15 @@
/* Does the platform use __ctype_b_loc, etc. */
#undef HAVE_CTYPE_EXTERNALS
+/* Using external STP */
+#undef HAVE_EXT_STP
+
/* Define to 1 if you have the <inttypes.h> header file. */
#undef HAVE_INTTYPES_H
+/* Define to 1 if you have the `stp' library (-lstp). */
+#undef HAVE_LIBSTP
+
/* Define to 1 if you have the <memory.h> header file. */
#undef HAVE_MEMORY_H
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 3071325..4353857 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,7 +17,11 @@
#include <map>
#define Expr VCExpr
+#ifdef HAVE_EXT_STP
+#include <stp/c_interface.h>
+#else
#include "../../stp/c_interface/c_interface.h"
+#endif
#if ENABLE_STPLOG == 1
#include "stp/stplog.h"
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 1d13a11..2815875 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -453,6 +453,9 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool
_useForkedSTP, bool _optim
assert(vc && "unable to create validity checker");
assert(builder && "unable to create STPBuilder");
+#ifdef HAVE_EXT_STP
+ vc_setInterfaceFlags(vc, EXPRDELETE, 0);
+#endif
vc_registerErrorHandler(::stp_error_handler);
if (useForkedSTP) {
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index d9c417c..21d84cb 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -9,12 +9,21 @@
LEVEL=../..
TOOLNAME = kleaver
+
+include $(LEVEL)/Makefile.config
+
STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a
stp_sat.a \
stp_simplifier.a
# FIXME: Ideally we wouldn't have any LLVM dependencies here, which
# means kicking out klee's Support.
-USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a \
- $(STP_LIBS)
+USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+ifeq ($(ENABLE_EXT_STP),0)
+ USEDLIBS += $(STP_LIBS)
+endif
LINK_COMPONENTS = support
include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_EXT_STP),1)
+ LIBS += -lstp
+endif
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 72188b7..23c8f1d 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -9,10 +9,19 @@
LEVEL=../..
TOOLNAME = klee
+
+include $(LEVEL)/Makefile.config
+
STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a
stp_sat.a \
stp_simplifier.a
-USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a
kleeBasic.a \
- $(STP_LIBS)
+USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a
kleeBasic.a
+ifeq ($(ENABLE_EXT_STP),0)
+ USEDLIBS += $(STP_LIBS)
+endif
LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_EXT_STP),1)
+ LIBS += -lstp
+endif
diff --git a/www/GetStarted.html b/www/GetStarted.html
index 2008660..84b3667 100644
--- a/www/GetStarted.html
+++ b/www/GetStarted.html
@@ -142,6 +142,40 @@ library.</p>
</li>
</ol>
+<h2 id="stp">Building KLEE with a more recent version of STP</h2>
+
+<p>If your benchmarks are running slowly or not terminating it may
+be worth trying a more recent version of KLEE's constraint solver
+<a href="http://sites.google.com/site/stpfastprover/";>STP</a>,
+which offers performance improvements over the version supplied
+with KLEE.</p>
+
+<p>STP does not make frequent releases, and its Subversion repository
+is under constant development and may be unstable. The instructions
+below are for a particular revision which is known to pass the KLEE
+test suite, but you can try a more recent revision (at your own risk)
+by changing or removing the <tt>-r</tt> argument to the <tt>svn
+co</tt> command.</p>
+
+<ol>
+ <li>Download and build STP.
+ <div class="instr">
+ $ svn co -r 940
https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
stp <br>
+ $ cd stp <br>
+ $ scripts/configure --with-prefix=<i>path/to/stp/inst</i>
--with-cryptominisat2 <br>
+ $ make OPTIMIZE=-O2 CFLAGS_M32= install
+ </div>
+ </li>
+
+ <li>Configure KLEE:
+ <div class="instr">
+ $ ./configure --with-llvm=<i>path/to/llvm</i>
--with-stp=<i>path/to/stp/inst</i>
+ </div>
+ </li>
+
+ <li>Rebuild KLEE.</li>
+</ol>
+
</div>
</body>
</html>
--
1.6.5
--UugvWAfsgieZRqgk--
