Go to the documentation of this file.
51 if(lhs.
id()==ID_symbol)
53 if(lhs.
type().
id()==ID_pointer)
61 get_rec(rhs_set, rhs, loc_info_src);
64 for(object_sett::const_iterator
73 else if(lhs.
id()==ID_dereference)
78 if(lhs.
type().
id()==ID_pointer)
96 else if(lhs.
id()==ID_index)
100 else if(lhs.
id()==ID_member)
103 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
105 else if(lhs.
id()==ID_typecast)
109 else if(lhs.
id()==ID_if)
118 const exprt &rhs)
const
120 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
127 get_rec(result_tmp, rhs, loc_info_src);
129 std::set<exprt> result;
131 for(object_sett::const_iterator
132 it=result_tmp.begin();
133 it!=result_tmp.end();
146 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
153 get_rec(tmp1, src1, loc_info_src);
154 get_rec(tmp2, src2, loc_info_src);
160 std::list<unsigned> result;
162 std::set_intersection(
163 tmp1.begin(), tmp1.end(),
164 tmp2.begin(), tmp2.end(),
165 std::back_inserter(result));
167 return !result.empty();
175 if(rhs.
id()==ID_constant)
182 else if(rhs.
id()==ID_symbol)
184 if(rhs.
type().
id()==ID_pointer)
188 dest.insert(src_pointer);
190 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
197 else if(rhs.
id()==ID_if)
202 else if(rhs.
id()==ID_address_of)
206 if(
object.
id()==ID_symbol)
209 dest.insert(object_nr);
211 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
215 else if(
object.
id()==ID_index)
218 if(index_expr.
array().
id()==ID_symbol)
224 dest.insert(object_nr);
226 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
230 else if(index_expr.
array().
id()==ID_string_constant)
236 dest.insert(object_nr);
238 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
248 else if(rhs.
id()==ID_typecast)
252 else if(rhs.
id()==ID_plus)
256 if(plus_expr.operands().size() >= 3)
259 plus_expr.op0().type().id() == ID_pointer,
260 "pointer in pointer-typed sum must be op0");
261 get_rec(dest, plus_expr.op0(), loc_info_src);
263 else if(plus_expr.operands().size() == 2)
266 if(plus_expr.op0().type().id() == ID_pointer)
268 get_rec(dest, plus_expr.op0(), loc_info_src);
270 else if(plus_expr.op1().type().id() == ID_pointer)
272 get_rec(dest, plus_expr.op1(), loc_info_src);
280 else if(rhs.
id()==ID_minus)
284 if(op0.type().id() == ID_pointer)
286 get_rec(dest, op0, loc_info_src);
291 else if(rhs.
id()==ID_member)
295 else if(rhs.
id()==ID_index)
299 else if(rhs.
id()==ID_dereference)
303 else if(rhs.
id()==ID_side_effect)
308 if(statement==ID_allocate)
341 for(code_typet::parameterst::const_iterator
342 it=goto_function.type.parameters().begin();
343 it!=goto_function.type.parameters().end();
346 const irep_idt &identifier=it->get_identifier();
347 if(is_tracked(identifier))
354 for(localst::locals_mapt::const_iterator
355 l_it=
locals.locals_map.begin();
356 l_it!=
locals.locals_map.end();
359 if(is_tracked(l_it->first))
365 while(!work_queue.empty())
375 switch(instruction.
type)
381 code_assign.
lhs(), code_assign.
rhs(), loc_info_src, loc_info_dest);
401 code_function_call.
lhs(),
nil_exprt(), loc_info_src, loc_info_dest);
408 if(
objects[i].
id() == ID_symbol)
425 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
446 false,
"Unclear what is a safe over-approximation of OTHER");
451 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
455 for(local_cfgt::successorst::const_iterator
461 work_queue.push(*it);
475 out <<
"**** " << instruction.source_location <<
"\n";
479 for(std::size_t i=0; i<loc_info.
aliases.
size(); i++)
485 for(std::size_t j=0; j<loc_info.
aliases.
size(); j++)
490 if(
objects[j].
id() == ID_symbol)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
size_type find(size_type a) const
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.
goto_program_instruction_typet type
What kind of instruction?
Base class for all expressions.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
bitvector_typet index_type()
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
size_type count(size_type a) const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Field-insensitive, location-sensitive may-alias analysis.
void make_union(size_type a, size_type b)
numberingt< exprt, irep_hash > objects
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 & get_identifier() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
API to expression classes for Pointers.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
void build(const goto_functiont &goto_function)
bool is_local(const irep_idt &identifier) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
std::stack< local_cfgt::node_nrt > work_queuet
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
bool same_set(size_type a, size_type b) const
bool merge(const loc_infot &src)
const irep_idt & get_statement() const
bool is_zero() const
Return whether the expression is a constant representing 0.
instructionst instructions
The list of instructions in the goto program.
number_type number(const key_type &a)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
std::set< unsigned > object_sett
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
goto_programt::const_targett t
Operator to return the address of an object.
A codet representing an assignment in the program.
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void isolate(size_type a)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
An expression containing a side effect.
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const