50 if(lhs.
id()==ID_symbol)
52 if(lhs.
type().
id()==ID_pointer)
54 unsigned dest_pointer=
objects.number(lhs);
60 get_rec(rhs_set, rhs, loc_info_src);
63 for(object_sett::const_iterator
72 else if(lhs.
id()==ID_dereference)
77 if(lhs.
type().
id()==ID_pointer)
79 for(std::size_t i=0; i<
objects.size(); i++)
95 else if(lhs.
id()==ID_index)
99 else if(lhs.
id()==ID_member)
102 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
104 else if(lhs.
id()==ID_typecast)
108 else if(lhs.
id()==ID_if)
117 const exprt &rhs)
const 119 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
126 get_rec(result_tmp, rhs, loc_info_src);
128 std::set<exprt> result;
130 for(object_sett::const_iterator
131 it=result_tmp.begin();
132 it!=result_tmp.end();
145 local_cfgt::loc_mapt::const_iterator loc_it=
cfg.
loc_map.find(t);
152 get_rec(tmp1, src1, loc_info_src);
153 get_rec(tmp2, src2, loc_info_src);
159 std::list<unsigned> result;
161 std::set_intersection(
162 tmp1.begin(), tmp1.end(),
163 tmp2.begin(), tmp2.end(),
164 std::back_inserter(result));
166 return !result.empty();
174 if(rhs.
id()==ID_constant)
179 dest.insert(
objects.number(
exprt(ID_integer_address_object)));
181 else if(rhs.
id()==ID_symbol)
183 if(rhs.
type().
id()==ID_pointer)
185 unsigned src_pointer=
objects.number(rhs);
187 dest.insert(src_pointer);
189 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
196 else if(rhs.
id()==ID_if)
201 else if(rhs.
id()==ID_address_of)
205 if(
object.
id()==ID_symbol)
207 unsigned object_nr=
objects.number(rhs);
208 dest.insert(object_nr);
210 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
214 else if(
object.
id()==ID_index)
217 if(index_expr.
array().
id()==ID_symbol)
222 unsigned object_nr=
objects.number(tmp2);
223 dest.insert(object_nr);
225 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
229 else if(index_expr.
array().
id()==ID_string_constant)
234 unsigned object_nr=
objects.number(tmp2);
235 dest.insert(object_nr);
237 for(std::size_t i=0; i<loc_info_src.
aliases.
size(); i++)
247 else if(rhs.
id()==ID_typecast)
251 else if(rhs.
id()==ID_plus)
255 assert(rhs.
op0().
type().
id()==ID_pointer);
265 else if(rhs.
op1().
type().
id()==ID_pointer)
275 else if(rhs.
id()==ID_minus)
284 else if(rhs.
id()==ID_member)
288 else if(rhs.
id()==ID_index)
292 else if(rhs.
id()==ID_dereference)
296 else if(rhs.
id()==ID_side_effect)
301 if(statement==ID_allocate)
334 for(code_typet::parameterst::const_iterator
339 const irep_idt &identifier=it->get_identifier();
340 if(is_tracked(identifier))
347 for(localst::locals_mapt::const_iterator
352 if(is_tracked(l_it->first))
358 while(!work_queue.empty())
368 switch(instruction.
type)
374 code_assign.
lhs(), code_assign.
rhs(), loc_info_src, loc_info_dest);
400 code_function_call.
lhs(),
nil_exprt(), loc_info_src, loc_info_dest);
405 for(std::size_t i=0; i<
objects.size(); i++)
427 for(local_cfgt::successorst::const_iterator
433 work_queue.push(*it);
447 out <<
"**** " << i_it->source_location <<
"\n";
451 for(std::size_t i=0; i<loc_info.
aliases.
size(); i++)
457 for(std::size_t j=0; j<loc_info.
aliases.
size(); j++)
462 if(
objects[j].
id() == ID_symbol)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const code_declt & to_code_decl(const codet &code)
const code_deadt & to_code_dead(const codet &code)
goto_program_instruction_typet type
What kind of instruction?
std::set< unsigned > object_sett
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::stack< local_cfgt::node_nrt > work_queuet
typet & type()
Return the type of the expression.
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
bool merge(const loc_infot &src)
side_effect_exprt & to_side_effect_expr(exprt &expr)
This class represents an instruction in the GOTO intermediate representation.
void make_union(size_type a, size_type b)
bool is_local(const irep_idt &identifier) const
const code_assignt & to_code_assign(const codet &code)
void build(const goto_functiont &goto_function)
size_type find(size_type a) const
const irep_idt & id() const
A codet representing the declaration of a local variable.
API to expression classes.
size_type count(size_type a) const
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
codet representation of a function call statement.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
code_typet type
The type of the function, indicating the return type and parameter types.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Operator to return the address of an object.
void isolate(size_type a)
A goto function, consisting of function type (see type), function body (see body),...
goto_programt::const_targett t
Base class for all expressions.
const parameterst & parameters() const
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
A codet representing the removal of a local variable going out of scope.
bool is_zero() const
Return whether the expression is a constant representing 0.
numbering< exprt > objects
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
An expression containing a side effect.
#define forall_goto_program_instructions(it, program)
bool same_set(size_type a, size_type b) const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
A codet representing an assignment in the program.
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
const irep_idt & get_statement() const
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)