about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/CommandLine.h12
-rw-r--r--lib/Basic/CmdLineOptions.cpp7
-rw-r--r--lib/Basic/ConstructSolverChain.cpp8
-rw-r--r--lib/Core/Executor.cpp30
4 files changed, 21 insertions, 36 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 6a72692d..64930bb2 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -40,11 +40,7 @@ enum QueryLoggingSolverType
     SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
 };
 
-/* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
- * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
- * wants to patch their copy of LLVM just for these options.
- */
-extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
+extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;
 
 enum CoreSolverType {
   STP_SOLVER,
@@ -70,12 +66,6 @@ extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
 #endif /* ENABLE_METASMT */
 
-//A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
-template <typename T>
-static bool optionIsSet(llvm::cl::list<T> &list, T option) {
-    return std::find(list.begin(), list.end(), option) != list.end();
-}
-
 }
 
 #endif	/* KLEE_COMMANDLINE_H */
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 54087c21..324f349e 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -65,12 +65,7 @@ CoreSolverOptimizeDivides("solver-optimize-divides",
                  llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"),
                  llvm::cl::init(false));
 
-
-/* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
- * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
- * wants to patch their copy of LLVM just for these options.
- */
-llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
+llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions(
     "use-query-log",
     llvm::cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."),
     llvm::cl::values(
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index d00fcec1..50d81a25 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -23,14 +23,14 @@ Solver *constructSolverChain(Solver *coreSolver,
                              std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
+  if (queryLoggingOptions.isSet(SOLVER_KQUERY)) {
     solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
                                    MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .kquery format to %s\n",
                  baseSolverQueryKQueryLogPath.c_str());
   }
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
+  if (queryLoggingOptions.isSet(SOLVER_SMTLIB)) {
     solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
                                        MinQueryTimeToLog);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
@@ -55,14 +55,14 @@ Solver *constructSolverChain(Solver *coreSolver,
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, coreSolver);
 
-  if (optionIsSet(queryLoggingOptions, ALL_KQUERY)) {
+  if (queryLoggingOptions.isSet(ALL_KQUERY)) {
     solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
                                        MinQueryTimeToLog);
     klee_message("Logging all queries in .kquery format to %s\n",
                  queryKQueryLogPath.c_str());
   }
 
-  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
+  if (queryLoggingOptions.isSet(ALL_SMTLIB)) {
     solver =
         createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
     klee_message("Logging all queries in .smt2 format to %s\n",
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dd4c8f47..fac68b8d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -120,7 +120,7 @@ namespace {
     FILE_COMPACT ///
   };
 
-  llvm::cl::list<PrintDebugInstructionsType> DebugPrintInstructions(
+  llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions(
       "debug-print-instructions",
       llvm::cl::desc("Log instructions during execution."),
       llvm::cl::values(
@@ -352,9 +352,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
 
-  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
-      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+  if (DebugPrintInstructions.isSet(FILE_ALL) ||
+      DebugPrintInstructions.isSet(FILE_COMPACT) ||
+      DebugPrintInstructions.isSet(FILE_SRC)) {
     std::string debug_file_name =
         interpreterHandler->getOutputFilename("instructions.txt");
     std::string ErrorInfo;
@@ -1136,19 +1136,19 @@ void Executor::executeGetValue(ExecutionState &state,
 
 void Executor::printDebugInstructions(ExecutionState &state) {
   // check do not print
-  if (DebugPrintInstructions.size() == 0)
+  if (DebugPrintInstructions.getBits() == 0)
 	  return;
 
   llvm::raw_ostream *stream = 0;
-  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
-      optionIsSet(DebugPrintInstructions, STDERR_SRC) ||
-      optionIsSet(DebugPrintInstructions, STDERR_COMPACT))
+  if (DebugPrintInstructions.isSet(STDERR_ALL) ||
+      DebugPrintInstructions.isSet(STDERR_SRC) ||
+      DebugPrintInstructions.isSet(STDERR_COMPACT))
     stream = &llvm::errs();
   else
     stream = &debugLogBuffer;
 
-  if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) &&
-      !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) {
+  if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
+      !DebugPrintInstructions.isSet(FILE_COMPACT)) {
     (*stream) << "     ";
     state.pc->printFileLine(*stream);
     (*stream) << ":";
@@ -1156,14 +1156,14 @@ void Executor::printDebugInstructions(ExecutionState &state) {
 
   (*stream) << state.pc->info->assemblyLine;
 
-  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_ALL))
+  if (DebugPrintInstructions.isSet(STDERR_ALL) ||
+      DebugPrintInstructions.isSet(FILE_ALL))
     (*stream) << ":" << *(state.pc->inst);
   (*stream) << "\n";
 
-  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
-      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
-      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+  if (DebugPrintInstructions.isSet(FILE_ALL) ||
+      DebugPrintInstructions.isSet(FILE_COMPACT) ||
+      DebugPrintInstructions.isSet(FILE_SRC)) {
     debugLogBuffer.flush();
     (*debugInstFile) << debugLogBuffer.str();
     debugBufferString = "";
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 13:36:55 +0000