diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 16:14:41 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 16:14:41 +0000 |
| commit | bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c (patch) | |
| tree | 717d4f98ebe8d42aac3355af6b8c018485c1ac44 /lib/Core | |
| parent | 2624f435755c9de3632019fcd2ec68425a39c9e8 (diff) | |
| download | klee-bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c.tar.gz | |
Added --stp-optimize-divides flag. Patch submitted by Peter
Collingbourne: "This flag controls whether constant divides are
optimized into add/shift/multiplies before passing to STP, and is set
by default. In some circumstances the use of this optimisation can
actually slow the solver down, so it is best to allow the user to
disable it."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102069 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fd6cf441..17b87873 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -249,6 +249,11 @@ namespace { cl::opt<bool> UseForkedSTP("use-forked-stp", cl::desc("Run STP in forked process")); + + cl::opt<bool> + STPOptimizeDivides("stp-optimize-divides", + cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP"), + cl::init(true)); } @@ -314,7 +319,7 @@ Executor::Executor(const InterpreterOptions &opts, stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0 ? std::min(MaxSTPTime,MaxInstructionTime) : std::max(MaxSTPTime,MaxInstructionTime)) { - STPSolver *stpSolver = new STPSolver(UseForkedSTP); + STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides); Solver *solver = constructSolverChain(stpSolver, interpreterHandler->getOutputFilename("queries.qlog"), |