about summary refs log tree commit diff homepage
path: root/lib/Solver/Solver.cpp
diff options
context:
space:
mode:
authorPeter Collingbourne <peter@pcc.me.uk>2010-07-14 18:54:38 +0000
committerPeter Collingbourne <peter@pcc.me.uk>2010-07-14 18:54:38 +0000
commitca22c4dee94552f65e6044341b0365a21d794d65 (patch)
treed952573658c01dd894005d52afce598197e946a7 /lib/Solver/Solver.cpp
parent59c0dedbc949433afeac482e8243119240076026 (diff)
downloadklee-ca22c4dee94552f65e6044341b0365a21d794d65.tar.gz
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
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r--lib/Solver/Solver.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 1d13a11d..4059a82b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -453,6 +453,15 @@ 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
+  // In newer versions of STP, a memory management mechanism has been
+  // introduced that automatically invalidates certain C interface
+  // pointers at vc_Destroy time.  This caused double-free errors
+  // due to the ExprHandle destructor also attempting to invalidate
+  // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
+  // we restore the old behaviour.
+  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
+#endif
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {