CBMC
Loading...
Searching...
No Matches
local_bitvector_analysis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive bitvector analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
13#define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
14
16#include <util/numbering.h>
17
18#include "locals.h"
19#include "dirty.h"
20#include "local_cfg.h"
21
23{
24public:
26
37
38 void output(
39 std::ostream &out,
40 const goto_functiont &goto_function,
41 const namespacet &ns) const;
42
46
47 // categories of things one can point to
48 struct flagst
49 {
51 {
52 }
53
54 void clear()
55 {
56 bits=0;
57 }
58
59 // the bits for the "bitvector analysis"
71
72 explicit flagst(const bitst _bits):bits(_bits)
73 {
74 }
75
76 unsigned bits;
77
78 bool merge(const flagst &other)
79 {
80 unsigned old=bits;
81 bits|=other.bits; // bit-wise or
82 return old!=bits;
83 }
84
86 {
87 return flagst(B_unknown);
88 }
89
90 bool is_unknown() const
91 {
92 return (bits&B_unknown)!=0;
93 }
94
96 {
97 return flagst(B_uninitialized);
98 }
99
100 bool is_uninitialized() const
101 {
102 return (bits&B_uninitialized)!=0;
103 }
104
106 {
107 return flagst(B_uses_offset);
108 }
109
110 bool is_uses_offset() const
111 {
112 return (bits&B_uses_offset)!=0;
113 }
114
116 {
117 return flagst(B_dynamic_local);
118 }
119
120 bool is_dynamic_local() const
121 {
122 return (bits&B_dynamic_local)!=0;
123 }
124
126 {
127 return flagst(B_dynamic_heap);
128 }
129
130 bool is_dynamic_heap() const
131 {
132 return (bits&B_dynamic_heap)!=0;
133 }
134
136 {
137 return flagst(B_null);
138 }
139
140 bool is_null() const
141 {
142 return (bits&B_null)!=0;
143 }
144
146 {
148 }
149
151 {
152 return (bits&B_static_lifetime)!=0;
153 }
154
156 {
158 }
159
161 {
162 return (bits&B_integer_address)!=0;
163 }
164
165 void print(std::ostream &) const;
166
167 flagst operator|(const flagst other) const
168 {
169 flagst result(*this);
170 result.bits|=other.bits;
171 return result;
172 }
173 };
174
175 flagst get(
177 const exprt &src);
178
179protected:
181 void build();
182
184
185 // pointers -> flagst
186 // This is a vector, so it's fast.
188
189 static bool merge(points_tot &a, points_tot &b);
190
191 typedef std::vector<points_tot> loc_infost;
193
194 void assign_lhs(
195 const exprt &lhs,
196 const exprt &rhs,
199
201 const exprt &rhs,
203
204 bool is_tracked(const irep_idt &identifier);
205};
206
207inline std::ostream &operator<<(
208 std::ostream &out,
210{
211 flags.print(out);
212 return out;
213}
214
215#endif // CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition dirty.h:28
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
std::vector< points_tot > loc_infost
expanding_vectort< flagst > points_tot
static bool merge(points_tot &a, points_tot &b)
goto_functionst::goto_functiont goto_functiont
local_bitvector_analysist(const goto_functiont &_goto_function, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
bool is_tracked(const irep_idt &identifier)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Variables whose address is taken.
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
CFG for One Function.
Local variables whose address is taken.
flagst operator|(const flagst other) const