29 out <<
"+uninitialized";
31 out <<
"+uses_offset";
33 out <<
"+dynamic_local";
35 out <<
"+dynamic_heap";
39 out <<
"+static_lifetime";
41 out <<
"+integer_address";
48 std::size_t max_index=
49 std::max(src.
points_to.size(), points_to.size());
51 for(std::size_t i=0; i<max_index; i++)
65 it->second.id()!=ID_pointer ||
78 if(lhs.
id()==ID_symbol)
86 loc_info_dest.
points_to[dest_pointer]=rhs_flags;
89 else if(lhs.
id()==ID_dereference)
92 else if(lhs.
id()==ID_index)
96 else if(lhs.
id()==ID_member)
99 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
101 else if(lhs.
id()==ID_typecast)
105 else if(lhs.
id()==ID_if)
116 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
122 return get_rec(rhs, loc_info_src);
129 if(rhs.
id()==ID_constant)
136 else if(rhs.
id()==ID_symbol)
142 return loc_info_src.
points_to[src_pointer];
147 else if(rhs.
id()==ID_address_of)
151 if(
object.
id()==ID_symbol)
158 else if(
object.
id()==ID_index)
161 if(index_expr.
array().
id()==ID_symbol)
175 else if(rhs.
id()==ID_typecast)
179 else if(rhs.
id()==ID_uninitialized)
183 else if(rhs.
id()==ID_plus)
187 assert(rhs.
op0().
type().
id()==ID_pointer);
199 else if(rhs.
op1().
type().
id()==ID_pointer)
210 else if(rhs.
id()==ID_minus)
220 else if(rhs.
id()==ID_member)
224 else if(rhs.
id()==ID_index)
228 else if(rhs.
id()==ID_dereference)
232 else if(rhs.
id()==ID_side_effect)
237 if(statement==ID_malloc)
263 while(!work_queue.empty())
265 unsigned loc_nr=work_queue.top();
267 const goto_programt::instructiont &instruction=*node.
t;
273 switch(instruction.type)
279 code_assign.
lhs(), code_assign.
rhs(), loc_info_src, loc_info_dest);
288 exprt(ID_uninitialized),
299 exprt(ID_uninitialized),
311 code_function_call.
lhs(),
nil_exprt(), loc_info_src, loc_info_dest);
324 work_queue.push(succ);
338 out <<
"**** " << i_it->source_location <<
"\n";
342 for(points_tot::const_iterator
354 goto_function.body.output_instruction(ns,
"", out, i_it);
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const code_declt & to_code_decl(const codet &code)
static flagst mk_unknown()
bool is_uninitialized() const
bool is_dynamic_heap() const
bool is_static_lifetime() const
void build(const goto_functiont &goto_function)
const code_deadt & to_code_dead(const codet &code)
void print(std::ostream &) const
bool is_tracked(const irep_idt &identifier)
Deprecated expression utility functions.
goto_functionst::goto_functiont goto_functiont
const irep_idt & get_identifier() const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
static flagst mk_static_lifetime()
Field-insensitive, location-sensitive bitvector analysis.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
static flagst mk_integer_address()
bool is_local(const irep_idt &identifier) const
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
A declaration of a local variable.
bool is_integer_address() const
static flagst mk_dynamic_local()
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
API to expression classes.
bool is_dynamic_local() const
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
bool merge(const flagst &other)
goto_programt::const_targett t
flagst get(const goto_programt::const_targett t, const exprt &src)
bool is_uses_offset() const
numbering< irep_idt > pointers
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
static flagst mk_uses_offset()
static flagst mk_dynamic_heap()
A removal of a local variable.
flagst get_rec(const exprt &rhs, const loc_infot &loc_info_src)
static flagst mk_uninitialized()
number_type number(const T &a)
An expression containing a side effect.
std::stack< unsigned > work_queuet
#define forall_goto_program_instructions(it, program)
bool merge(const loc_infot &src)
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)