klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CmdLineOptions.cpp
Go to the documentation of this file.
1 /*
2  * This file groups command line options definitions and associated
3  * data that are common to both KLEE and Kleaver.
4  */
5 
6 #include "klee/CommandLine.h"
7 
8 namespace klee {
9 
10 llvm::cl::opt<bool>
11 UseFastCexSolver("use-fast-cex-solver",
12  llvm::cl::init(false),
13  llvm::cl::desc("(default=off)"));
14 
15 llvm::cl::opt<bool>
16 UseCexCache("use-cex-cache",
17  llvm::cl::init(true),
18  llvm::cl::desc("Use counterexample caching (default=on)"));
19 
20 llvm::cl::opt<bool>
21 UseCache("use-cache",
22  llvm::cl::init(true),
23  llvm::cl::desc("Use validity caching (default=on)"));
24 
25 llvm::cl::opt<bool>
26 UseIndependentSolver("use-independent-solver",
27  llvm::cl::init(true),
28  llvm::cl::desc("Use constraint independence (default=on)"));
29 
30 llvm::cl::opt<bool>
31 DebugValidateSolver("debug-validate-solver",
32  llvm::cl::init(false));
33 
34 llvm::cl::opt<int>
35 MinQueryTimeToLog("min-query-time-to-log",
36  llvm::cl::init(0),
37  llvm::cl::value_desc("milliseconds"),
38  llvm::cl::desc("Set time threshold (in ms) for queries logged in files. "
39  "Only queries longer than threshold will be logged. (default=0). "
40  "Set this param to a negative value to log timeouts only."));
41 
42 llvm::cl::opt<double>
43 MaxCoreSolverTime("max-solver-time",
44  llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"),
45  llvm::cl::init(0.0),
46  llvm::cl::value_desc("seconds"));
47 
48 llvm::cl::opt<bool>
49 UseForkedCoreSolver("use-forked-solver",
50  llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"),
51  llvm::cl::init(true));
52 
53 llvm::cl::opt<bool>
54 CoreSolverOptimizeDivides("solver-optimize-divides",
55  llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"),
56  llvm::cl::init(true));
57 
58 
59 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
60  * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
61  * wants to patch their copy of LLVM just for these options.
62  */
63 llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
64  "use-query-log",
65  llvm::cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."),
66  llvm::cl::values(
67  clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
68  clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
69  clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
70  clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"),
71  clEnumValEnd
72  ),
73  llvm::cl::CommaSeparated
74 );
75 
76 #ifdef SUPPORT_METASMT
77 
78 llvm::cl::opt<klee::MetaSMTBackendType>
79 UseMetaSMT("use-metasmt",
80  llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."),
81  llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"),
82  clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
83  clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
84  clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"),
85  clEnumValEnd),
86  llvm::cl::init(METASMT_BACKEND_NONE));
87 
88 #endif /* SUPPORT_METASMT */
89 
90 }
91 
92 
93 
94 
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
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