Added several options in Executor.cpp to the constraint solving category

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");
     }