From 1b3290215a9b6f0c2017f0af5824413e77ce6d7b Mon Sep 17 00:00:00 2001 From: Cristian Cadar 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 +++++++++++++++++++++++++++++++++++++ lib/Basic/CmdLineOptions.cpp | 2 +- lib/Basic/ConstructSolverChain.cpp | 2 +- lib/Core/Executor.cpp | 2 +- lib/Core/SpecialFunctionHandler.cpp | 2 +- lib/Core/UserSearcher.cpp | 2 +- lib/Solver/CoreSolver.cpp | 2 +- tools/kleaver/main.cpp | 2 +- unittests/Solver/SolverTest.cpp | 2 +- 11 files changed, 93 insertions(+), 93 deletions(-) delete mode 100644 include/klee/CommandLine.h create mode 100644 include/klee/SolverCmdLine.h 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 UseFastCexSolver; - -extern llvm::cl::opt UseCexCache; - -extern llvm::cl::opt UseCache; - -extern llvm::cl::opt UseIndependentSolver; - -extern llvm::cl::opt DebugValidateSolver; - -extern llvm::cl::opt MinQueryTimeToLog; - -extern llvm::cl::opt MaxCoreSolverTime; - -extern llvm::cl::opt UseForkedCoreSolver; - -extern llvm::cl::opt CoreSolverOptimizeDivides; - -extern llvm::cl::opt 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 queryLoggingOptions; - -enum CoreSolverType { - STP_SOLVER, - METASMT_SOLVER, - DUMMY_SOLVER, - Z3_SOLVER, - NO_SOLVER -}; -extern llvm::cl::opt CoreSolverToUse; - -extern llvm::cl::opt 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 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 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 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 UseFastCexSolver; + +extern llvm::cl::opt UseCexCache; + +extern llvm::cl::opt UseCache; + +extern llvm::cl::opt UseIndependentSolver; + +extern llvm::cl::opt DebugValidateSolver; + +extern llvm::cl::opt MinQueryTimeToLog; + +extern llvm::cl::opt MaxCoreSolverTime; + +extern llvm::cl::opt UseForkedCoreSolver; + +extern llvm::cl::opt CoreSolverOptimizeDivides; + +extern llvm::cl::opt 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 queryLoggingOptions; + +enum CoreSolverType { + STP_SOLVER, + METASMT_SOLVER, + DUMMY_SOLVER, + Z3_SOLVER, + NO_SOLVER +}; +extern llvm::cl::opt CoreSolverToUse; + +extern llvm::cl::opt 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 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 Categories); +}; +} + +#endif /* KLEE_COMMANDLINE_H */ diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 3c117db9..b4517d47 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -12,7 +12,7 @@ * data that are common to both KLEE and Kleaver. */ -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Config/Version.h" #include "llvm/ADT/ArrayRef.h" diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 50d81a25..5880ad59 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -11,7 +11,7 @@ * This file groups declarations that are common to both KLEE and Kleaver. */ #include "klee/Common.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3e37a6c6..4b57ccf9 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -28,7 +28,7 @@ #include "klee/Expr.h" #include "klee/Interpreter.h" #include "klee/TimerStatIncrementer.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Common.h" #include "klee/util/Assignment.h" #include "klee/util/ExprPPrinter.h" diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 3b281d66..8752c2c8 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -22,7 +22,7 @@ #include "Executor.h" #include "MemoryManager.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "llvm/IR/Module.h" #include "llvm/ADT/Twine.h" diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 5e88df7c..aa90c401 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -13,7 +13,7 @@ #include "Executor.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/MergeHandler.h" diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 438f38f6..774f52a7 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -10,7 +10,7 @@ #include "STPSolver.h" #include "Z3Solver.h" #include "MetaSMTSolver.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "llvm/Support/ErrorHandling.h" diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 800cece9..3ce414a2 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -17,7 +17,7 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/Statistics.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Common.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 38e055cd..b178ced3 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -10,7 +10,7 @@ #include #include "gtest/gtest.h" -#include "klee/CommandLine.h" +#include "klee/SolverCmdLine.h" #include "klee/Constraints.h" #include "klee/Expr.h" #include "klee/Solver.h" -- cgit 1.4.1