klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CommandLine.h
Go to the documentation of this file.
1 /*
2  * This header groups command line options declarations and associated data
3  * that is common for klee and kleaver.
4  */
5 
6 #ifndef KLEE_COMMANDLINE_H
7 #define KLEE_COMMANDLINE_H
8 
9 #include "llvm/Support/CommandLine.h"
10 #include "klee/Config/config.h"
11 
12 namespace klee {
13 
14 extern llvm::cl::opt<bool> UseFastCexSolver;
15 
16 extern llvm::cl::opt<bool> UseCexCache;
17 
18 extern llvm::cl::opt<bool> UseCache;
19 
20 extern llvm::cl::opt<bool> UseIndependentSolver;
21 
22 extern llvm::cl::opt<bool> DebugValidateSolver;
23 
24 extern llvm::cl::opt<int> MinQueryTimeToLog;
25 
26 extern llvm::cl::opt<double> MaxCoreSolverTime;
27 
28 extern llvm::cl::opt<bool> UseForkedCoreSolver;
29 
30 extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
31 
34 {
39 };
40 
41 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
42  * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
43  * wants to patch their copy of LLVM just for these options.
44  */
45 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
46 
47 #ifdef SUPPORT_METASMT
48 
49 enum MetaSMTBackendType
50 {
51  METASMT_BACKEND_NONE,
52  METASMT_BACKEND_STP,
53  METASMT_BACKEND_Z3,
54  METASMT_BACKEND_BOOLECTOR
55 };
56 
57 extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT;
58 
59 #endif /* SUPPORT_METASMT */
60 
61 //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
62 template <typename T>
63 static bool optionIsSet(llvm::cl::list<T> list, T option)
64 {
65  return std::find(list.begin(), list.end(), option) != list.end();
66 }
67 
68 }
69 
70 #endif /* KLEE_COMMANDLINE_H */
71 
QueryLoggingSolverType
The different query logging solvers that can switched on/off.
Definition: CommandLine.h:33
llvm::cl::opt< int > MinQueryTimeToLog
Log all queries (un-optimised) in .pc (KQuery) format.
Definition: CommandLine.h:35
Log queries passed to solver (optimised) in .pc (KQuery) format.
Definition: CommandLine.h:37
llvm::cl::opt< bool > UseCache
llvm::cl::opt< double > MaxCoreSolverTime
Log all queries (un-optimised) .smt2 (SMT-LIBv2) format.
Definition: CommandLine.h:36
llvm::cl::opt< bool > DebugValidateSolver
static bool optionIsSet(llvm::cl::list< T > list, T option)
Definition: CommandLine.h:63
llvm::cl::opt< bool > UseForkedCoreSolver
llvm::cl::list< QueryLoggingSolverType > queryLoggingOptions
llvm::cl::opt< bool > CoreSolverOptimizeDivides
llvm::cl::opt< bool > UseFastCexSolver
llvm::cl::opt< bool > UseCexCache
llvm::cl::opt< bool > UseIndependentSolver
Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format.
Definition: CommandLine.h:38