Patch by Tomasz Kuchta that fixes the fragile way in which KLEE and Kleaver options were shared.

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

2 files changed, 58 insertions, 0 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
new file mode 100644
index 00000000..f14b813a
--- /dev/null
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -0,0 +1,57 @@
+/*
+ * This file groups command line options definitions and associated
+ * data that are common to both KLEE and Kleaver.
+ */
+
+#include "klee/CommandLine.h"
+
+namespace klee {
+
+llvm::cl::opt<bool>
+UseFastCexSolver("use-fast-cex-solver",
+		 llvm::cl::init(false),
+		 llvm::cl::desc("(default=off)"));
+
+llvm::cl::opt<bool>
+UseCexCache("use-cex-cache",
+            llvm::cl::init(true),
+            llvm::cl::desc("Use counterexample caching (default=on)"));
+
+llvm::cl::opt<bool>
+UseCache("use-cache",
+         llvm::cl::init(true),
+         llvm::cl::desc("Use validity caching (default=on)"));
+
+llvm::cl::opt<bool>
+UseIndependentSolver("use-independent-solver",
+                     llvm::cl::init(true),
+                     llvm::cl::desc("Use constraint independence (default=on)"));
+  
+llvm::cl::opt<int>
+MinQueryTimeToLog("min-query-time-to-log",
+                  llvm::cl::init(0),
+                  llvm::cl::value_desc("milliseconds"),
+                  llvm::cl::desc("Set time threshold (in ms) for queries logged in files. "
+                                 "Only queries longer than threshold will be logged. (default=0). "
+                                 "Set this param to a negative value to log timeouts only."));
+
+
+/* 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(
+    "use-query-log",
+    llvm::cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."),
+    llvm::cl::values(
+        clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
+        clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
+        clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
+        clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"),
+        clEnumValEnd
+	),
+    llvm::cl::CommaSeparated
+);
+
+}
+
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index a0c4de1c..b2ddb9b1 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -31,6 +31,7 @@
 #include "klee/Interpreter.h"
 #include "klee/TimerStatIncrementer.h"
 #include "klee/CommandLine.h"
+#include "klee/Common.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprSMTLIBLetPrinter.h"