Go to the documentation of this file.
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=
51 for(std::size_t i=0; i<max_index; i++)
63 localst::locals_sett::const_iterator it =
locals.
locals.find(identifier);
74 if(lhs.
id()==ID_symbol)
80 unsigned dest_pointer=
pointers.number(identifier);
82 loc_info_dest[dest_pointer]=rhs_flags;
85 else if(lhs.
id()==ID_dereference)
88 else if(lhs.
id()==ID_index)
92 else if(lhs.
id()==ID_member)
95 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
97 else if(lhs.
id()==ID_typecast)
101 else if(lhs.
id()==ID_if)
112 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
123 if(rhs.
id()==ID_constant)
130 else if(rhs.
id()==ID_symbol)
135 unsigned src_pointer=
pointers.number(identifier);
136 return loc_info_src[src_pointer];
141 else if(rhs.
id()==ID_address_of)
145 if(
object.
id()==ID_symbol)
152 else if(
object.
id()==ID_index)
155 if(index_expr.
array().
id()==ID_symbol)
169 else if(rhs.
id()==ID_typecast)
173 else if(rhs.
id()==ID_uninitialized)
177 else if(rhs.
id()==ID_plus)
181 if(plus_expr.operands().size() >= 3)
184 plus_expr.op0().type().id() == ID_pointer,
185 "pointer in pointer-typed sum must be op0");
188 else if(plus_expr.operands().size() == 2)
191 if(plus_expr.op0().type().id() == ID_pointer)
193 return get_rec(plus_expr.op0(), loc_info_src) |
196 else if(plus_expr.op1().type().id() == ID_pointer)
198 return get_rec(plus_expr.op1(), loc_info_src) |
207 else if(rhs.
id()==ID_minus)
211 if(op0.type().id() == ID_pointer)
218 else if(rhs.
id()==ID_member)
222 else if(rhs.
id()==ID_index)
226 else if(rhs.
id()==ID_dereference)
230 else if(rhs.
id()==ID_side_effect)
235 if(statement==ID_allocate)
263 while(!work_queue.empty())
265 unsigned loc_nr=work_queue.top();
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);
318 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
340 false,
"Unclear what is a safe over-approximation of OTHER");
345 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
353 work_queue.push(succ);
367 out <<
"**** " << i_it->source_location <<
"\n";
372 p_it=loc_info.begin();
373 p_it!=loc_info.end();
376 out <<
" " <<
pointers[p_it-loc_info.begin()]
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Field-insensitive, location-sensitive bitvector analysis.
const code_declt & to_code_decl(const codet &code)
static flagst mk_dynamic_local()
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
data_typet::const_iterator const_iterator
bool is_dynamic_heap() const
goto_program_instruction_typet type
What kind of instruction?
A codet representing the declaration of a local variable.
Base class for all expressions.
side_effect_exprt & to_side_effect_expr(exprt &expr)
static flagst mk_unknown()
bool is_tracked(const irep_idt &identifier)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
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().
codet representation of a function call statement.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
codet code
Do not read or modify directly – use get_X() instead.
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
static flagst mk_integer_address()
bool is_integer_address() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
bool is_local(const irep_idt &identifier) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool is_static_lifetime() const
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
A goto function, consisting of function type (see type), function body (see body),...
A codet representing the removal of a local variable going out of scope.
static flagst mk_dynamic_heap()
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
bool is_dynamic_local() const
std::stack< unsigned > work_queuet
numbering< irep_idt > pointers
const irep_idt & get_statement() const
static flagst mk_uninitialized()
bool is_uses_offset() const
bool is_zero() const
Return whether the expression is a constant representing 0.
Deprecated expression utility functions.
static flagst mk_uses_offset()
const code_assignt & to_code_assign(const codet &code)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void print(std::ostream &) const
bool is_uninitialized() const
flagst get(const goto_programt::const_targett t, const exprt &src)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
goto_programt::const_targett t
A codet representing an assignment in the program.
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
static bool merge(points_tot &a, points_tot &b)
#define forall_goto_program_instructions(it, program)
An expression containing a side effect.
static flagst mk_static_lifetime()