blob: 90c162ee6befa83767da37d5a4167a70322d8f43 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
//===-- SolverCmdLine.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 header groups command-line options and associated declarations
* that are common to both KLEE and Kleaver.
*/
#ifndef KLEE_SOLVERCMDLINE_H
#define KLEE_SOLVERCMDLINE_H
#include "klee/Config/config.h"
#include "klee/Support/CompilerWarning.h"
DISABLE_WARNING_PUSH
DISABLE_WARNING_DEPRECATED_DECLARATIONS
#include "llvm/ADT/ArrayRef.h"
#include "llvm/Support/CommandLine.h"
DISABLE_WARNING_POP
namespace klee {
extern llvm::cl::opt<bool> UseFastCexSolver;
extern llvm::cl::opt<bool> UseCexCache;
extern llvm::cl::opt<bool> UseBranchCache;
extern llvm::cl::opt<bool> UseIndependentSolver;
extern llvm::cl::opt<bool> DebugValidateSolver;
extern llvm::cl::opt<std::string> MinQueryTimeToLog;
extern llvm::cl::opt<bool> LogTimedOutQueries;
extern llvm::cl::opt<std::string> 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 be switched on/off
enum QueryLoggingSolverType {
ALL_KQUERY, ///< Log all queries in .kquery (KQuery) format
ALL_SMTLIB, ///< Log all queries .smt2 (SMT-LIBv2) format
SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format
SOLVER_SMTLIB ///< Log queries passed to solver 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 in the specified category
static void HideOptions(llvm::cl::OptionCategory &Category);
/// Hide all options except the ones in the specified category
static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category);
};
} // namespace klee
#endif /* KLEE_SOLVERCMDLINE_H */
|
