about summary refs log tree commit diff homepage
path: root/lib/Basic
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-07-26 19:13:17 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2017-07-26 19:13:17 +0100
commit57129f1a3131d660c1d41ebafc864daf98192274 (patch)
treeac6644d91c014feac5528a3996deb7c05a54b844 /lib/Basic
parentee2f1f37cb113324de04d840d42bbd891e9dfd19 (diff)
downloadklee-57129f1a3131d660c1d41ebafc864daf98192274.tar.gz
Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::list
Diffstat (limited to 'lib/Basic')
-rw-r--r--lib/Basic/CmdLineOptions.cpp7
-rw-r--r--lib/Basic/ConstructSolverChain.cpp8
2 files changed, 5 insertions, 10 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",