diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index abb5be7d..c7d88c2c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -48,6 +48,7 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" #include "klee/Internal/System/MemoryUsage.h" +#include "klee/OptionCategories.h" #include "klee/SolverStats.h" #include "../Expr/ArrayExprOptimizer.h" @@ -121,21 +122,25 @@ namespace { + /* Constraint solving options */ + + cl::opt<unsigned> + MaxSymArraySize("max-sym-array-size", + cl::desc("If a symbolic array exceeds this size (in bytes), symbolic addresses into this array are concretized. Set to 0 to disable (default=0)"), + cl::init(0), + cl::cat(SolvingCat)); cl::opt<bool> SimplifySymIndices("simplify-sym-indices", cl::init(false), - cl::desc("Simplify symbolic accesses using equalities from other constraints (default=false)")); + cl::desc("Simplify symbolic accesses using equalities from other constraints (default=false)"), + cl::cat(SolvingCat)); cl::opt<bool> EqualitySubstitution("equality-substitution", cl::init(true), - cl::desc("Simplify equality expressions before querying the solver (default=true).")); - - cl::opt<unsigned> - MaxSymArraySize("max-sym-array-size", - cl::init(0)); - + cl::desc("Simplify equality expressions before querying the solver (default=true)"), + cl::cat(SolvingCat)); /*** External call policy options ***/ @@ -317,7 +322,6 @@ namespace { cl::cat(TerminationCat)); - /*** Debugging options ***/ cl::OptionCategory DebugCat("Debugging options", @@ -3560,7 +3564,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (success) { const MemoryObject *mo = op.first; - if (MaxSymArraySize && mo->size>=MaxSymArraySize) { + if (MaxSymArraySize && mo->size >= MaxSymArraySize) { address = toConstant(state, address, "max-sym-array-size"); } |