diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-07-26 19:13:17 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-07-26 19:13:17 +0100 |
commit | 57129f1a3131d660c1d41ebafc864daf98192274 (patch) | |
tree | ac6644d91c014feac5528a3996deb7c05a54b844 /lib | |
parent | ee2f1f37cb113324de04d840d42bbd891e9dfd19 (diff) | |
download | klee-57129f1a3131d660c1d41ebafc864daf98192274.tar.gz |
Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::list
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 7 | ||||
-rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 8 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 30 |
3 files changed, 20 insertions, 25 deletions
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 = ""; |