From 5766e55b1ff24aef508b7c2a257725e66af24b99 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Mon, 11 Mar 2019 10:45:02 +0000 Subject: Added options in ArrayExprOptimizer.cpp to the constraint solving category --- lib/Expr/ArrayExprOptimizer.cpp | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index e911e197..d043783a 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -15,6 +15,7 @@ #include "klee/Config/Version.h" #include "klee/ExprBuilder.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/OptionCategories.h" #include "klee/util/Assignment.h" #include "klee/util/BitArray.h" @@ -32,28 +33,32 @@ using namespace klee; namespace klee { llvm::cl::opt OptimizeArray( "optimize-array", - llvm::cl::values( - clEnumValN(ALL, "all", "Combining index and value transformations"), - clEnumValN(INDEX, "index", "Index-based transformation"), - clEnumValN(VALUE, "value", "Value-based transformation at branch (both " - "concrete and concrete/symbolic)") - KLEE_LLVM_CL_VAL_END), + llvm::cl::values(clEnumValN(ALL, "all", + "Combining index and value transformations"), + clEnumValN(INDEX, "index", "Index-based transformation"), + clEnumValN(VALUE, "value", + "Value-based transformation at branch (both " + "concrete and concrete/symbolic)") + KLEE_LLVM_CL_VAL_END), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " - "arrays. (default=off)")); + "arrays. (default=off)"), + llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt ArrayValueRatio( "array-value-ratio", llvm::cl::desc("Maximum ratio of unique values to array size for which the " "value-based transformations are applied."), - llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size")); + llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size"), + llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt ArrayValueSymbRatio( "array-value-symb-ratio", llvm::cl::desc("Maximum ratio of symbolic values to array size for which " "the mixed value-based transformations are applied."), - llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size")); -}; + llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size"), + llvm::cl::cat(klee::SolvingCat)); +}; // namespace klee ref extendRead(const UpdateList &ul, const ref index, Expr::Width w) { -- cgit 1.4.1