30 out <<
"+uninitialized";
32 out <<
"+uses_offset";
34 out <<
"+dynamic_local";
36 out <<
"+dynamic_heap";
40 out <<
"+static_lifetime";
42 out <<
"+integer_address";
49 std::size_t max_index=
52 for(std::size_t i=0; i<max_index; i++)
64 localst::locals_sett::const_iterator it =
locals.
locals.find(identifier);
75 if(lhs.
id()==ID_symbol)
83 loc_info_dest[dest_pointer]=rhs_flags;
86 else if(lhs.
id()==ID_dereference)
89 else if(lhs.
id()==ID_index)
93 else if(lhs.
id()==ID_member)
96 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
98 else if(lhs.
id()==ID_typecast)
102 else if(lhs.
id()==ID_if)
113 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
124 if(rhs.
id()==ID_constant)
131 else if(rhs.
id()==ID_symbol)
137 return loc_info_src[src_pointer];
142 else if(rhs.
id()==ID_address_of)
146 if(
object.
id()==ID_symbol)
153 else if(
object.
id()==ID_index)
156 if(index_expr.
array().
id()==ID_symbol)
170 else if(rhs.
id()==ID_typecast)
174 else if(rhs.
id()==ID_uninitialized)
178 else if(rhs.
id()==ID_plus)
182 if(plus_expr.operands().size() >= 3)
185 plus_expr.op0().type().id() == ID_pointer,
186 "pointer in pointer-typed sum must be op0");
189 else if(plus_expr.operands().size() == 2)
192 if(plus_expr.op0().type().id() == ID_pointer)
194 return get_rec(plus_expr.op0(), loc_info_src) |
197 else if(plus_expr.op1().type().id() == ID_pointer)
199 return get_rec(plus_expr.op1(), loc_info_src) |
208 else if(rhs.
id()==ID_minus)
212 if(op0.type().id() == ID_pointer)
219 else if(rhs.
id()==ID_member)
223 else if(rhs.
id()==ID_index)
227 else if(rhs.
id()==ID_dereference)
231 else if(rhs.
id()==ID_side_effect)
236 if(statement==ID_allocate)
264 while(!work_queue.empty())
266 unsigned loc_nr=work_queue.top();
274 switch(instruction.
type)
280 code_assign.
lhs(), code_assign.
rhs(), loc_info_src, loc_info_dest);
287 exprt(ID_uninitialized),
295 exprt(ID_uninitialized),
306 code_function_call.
lhs(),
nil_exprt(), loc_info_src, loc_info_dest);
313 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
335 false,
"Unclear what is a safe over-approximation of OTHER");
340 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
348 work_queue.push(succ);
362 out <<
"**** " << instruction.source_location <<
"\n";
367 p_it=loc_info.begin();
368 p_it!=loc_info.end();
371 out <<
" " <<
pointers[p_it-loc_info.begin()]
A codet representing an assignment in the program.
codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
data_typet::const_iterator const_iterator
Base class for all expressions.
bool is_zero() const
Return whether the expression is a constant representing 0.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
goto_program_instruction_typet type
What kind of instruction?
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
const irep_idt & id() const
std::stack< unsigned > work_queuet
static bool merge(points_tot &a, points_tot &b)
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)
numberingt< irep_idt > pointers
goto_programt::const_targett t
bool is_local(const irep_idt &identifier) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
number_type number(const key_type &a)
An expression containing a side effect.
const irep_idt & get_statement() const
const irep_idt & get_identifier() const
Deprecated expression utility functions.
Field-insensitive, location-sensitive bitvector analysis.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
static flagst mk_uses_offset()
static flagst mk_integer_address()
static flagst mk_dynamic_heap()
static flagst mk_static_lifetime()
static flagst mk_unknown()
static flagst mk_dynamic_local()
bool is_static_lifetime() const
bool is_dynamic_local() const
void print(std::ostream &) const
bool is_dynamic_heap() const
bool is_uses_offset() const
bool is_uninitialized() const
bool is_integer_address() const
static flagst mk_uninitialized()