63 for(object_sett::const_iterator
117 const exprt &rhs)
const
127 std::set<exprt> result;
129 for(object_sett::const_iterator
157 std::list<unsigned> result;
159 std::set_intersection(
162 std::back_inserter(result));
164 return !result.empty();
187 for(std::size_t i=0; i<
loc_info_src.aliases.size(); i++)
208 for(std::size_t i=0; i<
loc_info_src.aliases.size(); i++)
223 for(std::size_t i=0; i<
loc_info_src.aliases.size(); i++)
235 for(std::size_t i=0; i<
loc_info_src.aliases.size(); i++)
257 "pointer in pointer-typed sum must be op0");
260 else if(
plus_expr.operands().size() == 2)
338 for(code_typet::parameterst::const_iterator
339 it=goto_function.type.parameters().begin();
340 it!=goto_function.type.parameters().end();
343 const irep_idt &identifier=it->get_identifier();
344 if(is_tracked(identifier))
351 for(localst::locals_mapt::const_iterator
356 if(is_tracked(
l_it->first))
372 switch(instruction.
type())
396 const auto &lhs = instruction.
call_lhs();
422 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
426 DATA_INVARIANT(
false,
"SET_RETURN_VALUE must be removed before analysis");
443 false,
"Unclear what is a safe over-approximation of OTHER");
448 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
452 for(local_cfgt::successorst::const_iterator
472 out <<
"**** " << instruction.source_location() <<
"\n";
476 for(std::size_t i=0; i<
loc_info.aliases.size(); i++)
482 for(std::size_t j=0; j<
loc_info.aliases.size(); j++)
498 instruction.output(out);
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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 symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
goto_program_instruction_typet type() const
What kind of instruction?
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
const irep_idt & id() const
goto_programt::const_targett t
bool merge(const loc_infot &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
void build(const goto_functiont &goto_function)
numberingt< exprt, irep_hash > objects
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
std::stack< local_cfgt::node_nrt > work_queuet
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
std::set< unsigned > object_sett
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...
number_type number(const key_type &a)
An expression containing a side effect.
size_type find(size_type a) const
void make_union(size_type a, size_type b)
bool same_set(size_type a, size_type b) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Field-insensitive, location-sensitive may-alias 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 CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.