clang: include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9
10
11
12
13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
15
18
20
21namespace ento {
22
26
27public:
29 : EE(exprengine), SVB(SB) {}
30
32
33
34
35
36
37protected:
38
39
40
41
42
43
45 bool Assumption) = 0;
46
47
48
49
50
53 const llvm::APSInt &From,
54 const llvm::APSInt &To,
55 bool InRange) = 0;
56
57
58
61 bool Assumption) = 0;
62
63
64
65
66
67
68
70 bool Assumption) override;
71
74 const llvm::APSInt &From,
75 const llvm::APSInt &To,
76 bool InRange) override;
77
81
82private:
84
86 bool Assumption);
87};
88
89}
90
91}
92
93#endif
BasicValueFactory & getBasicValueFactory()
SymbolManager & getSymbolManager()
SymbolManager & getSymbolManager() const
ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
SValBuilder & getSValBuilder() const
virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
~SimpleConstraintManager() override
virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
BasicValueFactory & getBasicVals() const
virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
ProgramStateRef assumeInternal(ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle...
SimpleConstraintManager(ExprEngine *exprengine, SValBuilder &SB)
The JSON file list parser is used to communicate input to InstallAPI.