25 out <<
"+uninitialized";
27 out <<
"+uses_offset";
29 out <<
"+dynamic_local";
31 out <<
"+dynamic_heap";
35 out <<
"+static_lifetime";
37 out <<
"+integer_address";
44 std::size_t max_index=
47 for(std::size_t i=0; i<max_index; i++)
59 localst::locals_sett::const_iterator it =
locals.
locals.find(identifier);
70 if(lhs.
id()==ID_symbol)
78 loc_info_dest[dest_pointer]=rhs_flags;
81 else if(lhs.
id()==ID_dereference)
84 else if(lhs.
id()==ID_index)
88 else if(lhs.
id()==ID_member)
91 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
93 else if(lhs.
id()==ID_typecast)
97 else if(lhs.
id()==ID_if)
108 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
119 if(rhs.
id()==ID_constant)
126 else if(rhs.
id()==ID_symbol)
132 return loc_info_src[src_pointer];
137 else if(rhs.
id()==ID_address_of)
141 if(
object.
id()==ID_symbol)
148 else if(
object.
id()==ID_index)
151 if(index_expr.
array().
id()==ID_symbol)
165 else if(rhs.
id()==ID_typecast)
169 else if(rhs.
id()==ID_uninitialized)
173 else if(rhs.
id()==ID_plus)
177 if(plus_expr.operands().size() >= 3)
180 plus_expr.op0().type().id() == ID_pointer,
181 "pointer in pointer-typed sum must be op0");
184 else if(plus_expr.operands().size() == 2)
187 if(plus_expr.op0().type().id() == ID_pointer)
189 return get_rec(plus_expr.op0(), loc_info_src) |
192 else if(plus_expr.op1().type().id() == ID_pointer)
194 return get_rec(plus_expr.op1(), loc_info_src) |
203 else if(rhs.
id()==ID_minus)
207 if(op0.type().id() == ID_pointer)
214 else if(rhs.
id()==ID_member)
218 else if(rhs.
id()==ID_index)
222 else if(rhs.
id()==ID_dereference)
226 else if(rhs.
id()==ID_side_effect)
231 if(statement==ID_allocate)
259 while(!work_queue.empty())
261 unsigned loc_nr=work_queue.top();
269 switch(instruction.
type)
275 code_assign.
lhs(), code_assign.
rhs(), loc_info_src, loc_info_dest);
282 exprt(ID_uninitialized),
290 exprt(ID_uninitialized),
297 const auto &lhs = instruction.
call_lhs();
306 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
311 DATA_INVARIANT(
false,
"SET_RETURN_VALUE must be removed before analysis");
328 false,
"Unclear what is a safe over-approximation of OTHER");
333 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
341 work_queue.push(succ);
355 out <<
"**** " << instruction.source_location <<
"\n";
360 p_it=loc_info.begin();
361 p_it!=loc_info.end();
364 out <<
" " <<
pointers[p_it-loc_info.begin()]
A codet representing an assignment in the program.
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.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
goto_program_instruction_typet type
What kind of instruction?
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
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
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 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()