Refactoring patch by Tomasz Kuchta that moves options shared by KLEE and Kleaver to a separate file.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171395 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 4 insertions, 23 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 1a4663a1..00034eb1 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -10,6 +10,7 @@
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 #include "klee/Statistics.h"
+#include "klee/CommandLine.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
 
@@ -90,24 +91,6 @@ namespace {
   UseDummySolver("use-dummy-solver",
 		   cl::init(false));
 
-  cl::opt<bool>
-  UseFastCexSolver("use-fast-cex-solver",
-		   cl::init(false));
-  
-  // FIXME: Command line argument modified in Executor.cpp of Klee. Different
-  // output file name used.
-  cl::opt<bool>
-  UseSTPQueryPCLog("use-stp-query-pc-log",
-                   cl::init(false));
-   
-  // FIXME: Command line argument duplicated in Executor.cpp of Klee
-  cl::opt<unsigned int>
-  MinQueryTimeToLog("min-query-time-to-log",
-                    cl::init(0),
-                    cl::value_desc("milliseconds"),
-                    cl::desc("Set time threshold (in ms) for queries logged in files. "
-                             "Only queries longer than threshold will be logged. (default=0)"));
-  
 }
 
 static std::string escapedString(const char *start, unsigned length) {
@@ -197,8 +180,8 @@ static bool EvaluateInputAST(const char *Filename,
   // FIXME: Support choice of solver.
   Solver *S, *STP = S = 
     UseDummySolver ? createDummySolver() : new STPSolver(true);
-  if (UseSTPQueryPCLog)
-    S = createPCLoggingSolver(S, "stp-queries.pc", MinQueryTimeToLog);
+  if (true == optionIsSet(queryLoggingOptions, SOLVER_PC))
+    S = createPCLoggingSolver(S, SOLVER_QUERIES_PC_FILE_NAME, MinQueryTimeToLog);
   if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);
@@ -265,9 +248,7 @@ static bool EvaluateInputAST(const char *Filename,
               std::cout << "\n";
           }
         } else {
-          std::cout << "FAIL (reason: " 
-                    << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
-                    << ")";
+          std::cout << "VALID (counterexample request ignored)";
         }
       }