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, 48 insertions, 57 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index c8397cf1..39290e7b 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -1,55 +1,31 @@
 /*
- * FIXME: This is a temporary solution.
- * This header groups command line options and associated data that is common
- * for klee and kleaver.
+ * This header groups command line options declarations and associated data
+ * that is common for klee and kleaver.
  */
 
-#ifndef COMMANDLINE_H
-#define	COMMANDLINE_H
+#ifndef KLEE_COMMANDLINE_H
+#define KLEE_COMMANDLINE_H
 
 #include "llvm/Support/CommandLine.h"
 
-namespace {
+namespace klee {
 
-#define ALL_QUERIES_SMT2_FILE_NAME      "all-queries.smt2"
-#define SOLVER_QUERIES_SMT2_FILE_NAME   "solver-queries.smt2"
-#define ALL_QUERIES_PC_FILE_NAME        "all-queries.pc"
-#define SOLVER_QUERIES_PC_FILE_NAME     "solver-queries.pc"
-    
-llvm::cl::opt<bool>
-UseFastCexSolver("use-fast-cex-solver",
-		 llvm::cl::init(false),
-		 llvm::cl::desc("(default=off)"));
+extern llvm::cl::opt<bool> UseFastCexSolver;
 
-llvm::cl::opt<bool>
-UseCexCache("use-cex-cache",
-            llvm::cl::init(true),
-            llvm::cl::desc("Use counterexample caching (default=on)"));
+extern llvm::cl::opt<bool> UseCexCache;
 
-llvm::cl::opt<bool>
-UseCache("use-cache",
-         llvm::cl::init(true),
-         llvm::cl::desc("Use validity caching (default=on)"));
+extern llvm::cl::opt<bool> UseCache;
 
-llvm::cl::opt<bool>
-UseIndependentSolver("use-independent-solver",
-                     llvm::cl::init(true),
-                     llvm::cl::desc("Use constraint independence (default=on)"));
+extern llvm::cl::opt<bool> UseIndependentSolver; 
   
-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."));
+extern llvm::cl::opt<int> MinQueryTimeToLog;
 
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
 {
-    ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format
-    ALL_SMTLIB, ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
-    SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format
+    ALL_PC,       ///< Log all queries (un-optimised) in .pc (KQuery) format
+    ALL_SMTLIB,   ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
+    SOLVER_PC,    ///< Log queries passed to solver (optimised) in .pc (KQuery) format
     SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
 };
 
@@ -57,29 +33,17 @@ enum QueryLoggingSolverType
  * 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
-);
+extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
+
+//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();
 }
 
-namespace klee { 
-  //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	/* COMMANDLINE_H */
+#endif	/* KLEE_COMMANDLINE_H */
 
diff --git a/include/klee/Common.h b/include/klee/Common.h
new file mode 100644
index 00000000..657b9341
--- /dev/null
+++ b/include/klee/Common.h
@@ -0,0 +1,27 @@
+//===-- Common.h ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/*
+ * This file groups declarations that are common to both KLEE and Kleaver.
+ */
+
+#ifndef KLEE_COMMON_H
+#define KLEE_COMMON_H
+
+namespace klee {
+
+#define ALL_QUERIES_SMT2_FILE_NAME      "all-queries.smt2"
+#define SOLVER_QUERIES_SMT2_FILE_NAME   "solver-queries.smt2"
+#define ALL_QUERIES_PC_FILE_NAME        "all-queries.pc"
+#define SOLVER_QUERIES_PC_FILE_NAME     "solver-queries.pc"
+
+}
+
+#endif /* KLEE_COMMON_H */
+