From 1b3290215a9b6f0c2017f0af5824413e77ce6d7b Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Wed, 3 Oct 2018 23:10:19 +0100
Subject: Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file
 is meant to have only solver options.

---
 include/klee/CommandLine.h   | 84 --------------------------------------------
 include/klee/Solver.h        |  2 +-
 include/klee/SolverCmdLine.h | 84 ++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 85 deletions(-)
 delete mode 100644 include/klee/CommandLine.h
 create mode 100644 include/klee/SolverCmdLine.h

(limited to 'include')

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
deleted file mode 100644
index 9668d00b..00000000
--- a/include/klee/CommandLine.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/*
- * This header groups command line options declarations and associated data
- * that is common for klee and kleaver.
- */
-
-#ifndef KLEE_COMMANDLINE_H
-#define KLEE_COMMANDLINE_H
-
-#include "klee/Config/config.h"
-
-#include "llvm/ADT/ArrayRef.h"
-#include "llvm/Support/CommandLine.h"
-
-namespace klee {
-
-extern llvm::cl::opt<bool> UseFastCexSolver;
-
-extern llvm::cl::opt<bool> UseCexCache;
-
-extern llvm::cl::opt<bool> UseCache;
-
-extern llvm::cl::opt<bool> UseIndependentSolver; 
-
-extern llvm::cl::opt<bool> DebugValidateSolver;
-  
-extern llvm::cl::opt<int> MinQueryTimeToLog;
-
-extern llvm::cl::opt<double> MaxCoreSolverTime;
-
-extern llvm::cl::opt<bool> UseForkedCoreSolver;
-
-extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
-
-extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
-
-///The different query logging solvers that can switched on/off
-enum QueryLoggingSolverType
-{
-    ALL_KQUERY,   ///< Log all queries (un-optimised) in .kquery (KQuery) format
-    ALL_SMTLIB,   ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
-    SOLVER_KQUERY,///< Log queries passed to solver (optimised) in .kquery (KQuery) format
-    SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
-};
-
-extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;
-
-enum CoreSolverType {
-  STP_SOLVER,
-  METASMT_SOLVER,
-  DUMMY_SOLVER,
-  Z3_SOLVER,
-  NO_SOLVER
-};
-extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
-
-extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
-
-#ifdef ENABLE_METASMT
-
-enum MetaSMTBackendType
-{
-    METASMT_BACKEND_STP,
-    METASMT_BACKEND_Z3,
-    METASMT_BACKEND_BOOLECTOR,
-    METASMT_BACKEND_CVC4,
-    METASMT_BACKEND_YICES2
-};
-
-extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
-
-#endif /* ENABLE_METASMT */
-
-class KCommandLine {
-public:
-  /// Hide all options except the ones in the specified category
-  static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category);
-
-  /// Hide all options except the ones in the specified categories
-  static void HideUnrelatedOptions(
-      llvm::ArrayRef<const llvm::cl::OptionCategory *> Categories);
-};
-}
-
-#endif	/* KLEE_COMMANDLINE_H */
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index e669c6f4..e4762ae2 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
-#include "klee/CommandLine.h" // FIXME: This is just for CoreSolverType
+#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType
 #include "klee/Expr.h"
 
 #include <vector>
diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h
new file mode 100644
index 00000000..9668d00b
--- /dev/null
+++ b/include/klee/SolverCmdLine.h
@@ -0,0 +1,84 @@
+/*
+ * This header groups command line options declarations and associated data
+ * that is common for klee and kleaver.
+ */
+
+#ifndef KLEE_COMMANDLINE_H
+#define KLEE_COMMANDLINE_H
+
+#include "klee/Config/config.h"
+
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/Support/CommandLine.h"
+
+namespace klee {
+
+extern llvm::cl::opt<bool> UseFastCexSolver;
+
+extern llvm::cl::opt<bool> UseCexCache;
+
+extern llvm::cl::opt<bool> UseCache;
+
+extern llvm::cl::opt<bool> UseIndependentSolver; 
+
+extern llvm::cl::opt<bool> DebugValidateSolver;
+  
+extern llvm::cl::opt<int> MinQueryTimeToLog;
+
+extern llvm::cl::opt<double> MaxCoreSolverTime;
+
+extern llvm::cl::opt<bool> UseForkedCoreSolver;
+
+extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
+
+extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
+
+///The different query logging solvers that can switched on/off
+enum QueryLoggingSolverType
+{
+    ALL_KQUERY,   ///< Log all queries (un-optimised) in .kquery (KQuery) format
+    ALL_SMTLIB,   ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
+    SOLVER_KQUERY,///< Log queries passed to solver (optimised) in .kquery (KQuery) format
+    SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
+};
+
+extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;
+
+enum CoreSolverType {
+  STP_SOLVER,
+  METASMT_SOLVER,
+  DUMMY_SOLVER,
+  Z3_SOLVER,
+  NO_SOLVER
+};
+extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
+
+extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
+
+#ifdef ENABLE_METASMT
+
+enum MetaSMTBackendType
+{
+    METASMT_BACKEND_STP,
+    METASMT_BACKEND_Z3,
+    METASMT_BACKEND_BOOLECTOR,
+    METASMT_BACKEND_CVC4,
+    METASMT_BACKEND_YICES2
+};
+
+extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
+
+#endif /* ENABLE_METASMT */
+
+class KCommandLine {
+public:
+  /// Hide all options except the ones in the specified category
+  static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category);
+
+  /// Hide all options except the ones in the specified categories
+  static void HideUnrelatedOptions(
+      llvm::ArrayRef<const llvm::cl::OptionCategory *> Categories);
+};
+}
+
+#endif	/* KLEE_COMMANDLINE_H */
-- 
cgit 1.4.1