clang: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9
10
11
12
13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
15
20#include "llvm/Support/SaveAndRestore.h"
21#include
22#include
23#include
24
25namespace llvm {
26
28
29}
30
32namespace ento {
33
34class ProgramStateManager;
35class ExprEngine;
36class SymbolReaper;
37
39 std::optional Val;
40
41public:
42
43
45
46
48
49
50
52 return *Val;
53 }
54
55
57
58
60
61
63
64
65
67};
68
70public:
73
76
78 bool Assumption);
79
81
82
83
84
85
86
88
90 const llvm::APSInt &From,
91 const llvm::APSInt &To, bool InBound);
92
93
94
95
96
97
99 const llvm::APSInt &From,
100 const llvm::APSInt &To);
101
102
103
104
105
106
107
110 return nullptr;
111 }
112
113
114
115
118 return nullptr;
119 }
120
121
122
123
126 return nullptr;
127 }
128
129
130
133
135 const char *NL, unsigned int Space,
136 bool IsDot) const = 0;
137
140
141
142
145 }
146
147protected:
148
150 public:
152 void pop() { Aux.pop_back(); }
154 return llvm::is_contained(Aux, S);
155 }
156
157 private:
159 };
161
164
167 const llvm::APSInt &From,
168 const llvm::APSInt &To,
169 bool InBound) = 0;
170
171
172
173
174
175
177
178
179
181
182 template
184 AssumeFunction &Assume);
185};
186
187std::unique_ptr
190
191std::unique_ptr
194
195}
196}
197
198#endif
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
bool isUnderconstrained() const
Return true if the constrained is underconstrained and we do not know if the constraint is true of va...
ConditionTruthVal()=default
Construct a ConstraintVal indicating the constraint is underconstrained.
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
bool isConstrained() const
Return true if the constrained is perfectly constrained.
ConditionTruthVal(bool constraint)
Construct a ConditionTruthVal indicating the constraint is constrained to either true or false,...
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to 'true'.
A helper class to simulate the call stack of nested assume calls.
bool contains(const ProgramState *S) const
void push(const ProgramState *S)
virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0
virtual const llvm::APSInt * getSymMaxVal(ProgramStateRef state, SymbolRef sym) const
Attempt to return the minimal possible value for a given symbol.
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)
virtual const llvm::APSInt * getSymVal(ProgramStateRef state, SymbolRef sym) const
If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
virtual void printValue(raw_ostream &Out, ProgramStateRef State, SymbolRef Sym)
virtual bool canReasonAbout(SVal X) const =0
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond)
Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false,...
ConstraintManager()=default
virtual ~ConstraintManager()
virtual void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym)
Convenience method to query the state to see if a symbol is null or not null, or if neither assumptio...
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, SymbolReaper &SymReaper)=0
Scan all symbols referenced by the constraints.
AssumeStackTy AssumeStack
virtual const llvm::APSInt * getSymMinVal(ProgramStateRef state, SymbolRef sym) const
Attempt to return the minimal possible value for a given symbol.
ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
Returns a pair of states (StInRange, StOutOfRange) where the given value is assumed to be in the rang...
std::pair< ProgramStateRef, ProgramStateRef > ProgramStatePair
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption)
ProgramStatePair assumeDualImpl(ProgramStateRef &State, AssumeFunction &Assume)
virtual ProgramStateRef assumeInternal(ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
virtual bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const =0
virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym)
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"),...
ProgramState - This class encapsulates:
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
A class responsible for cleaning up unused symbols.
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
std::unique_ptr< ConstraintManager > CreateRangeConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
The JSON file list parser is used to communicate input to InstallAPI.
Diagnostic wrappers for TextAPI types for error reporting.