23 const std::set<irep_idt> &alias_set)
25 if(lhs.
id()==ID_symbol)
31 for(
const auto &alias : alias_set)
33 aliases.make_union(identifier, alias);
45 std::set<irep_idt> &alias_set)
47 if(rhs.
id()==ID_symbol)
50 alias_set.insert(identifier);
52 for(
const auto &alias : alias_set)
53 if(
aliases.same_set(alias, identifier))
54 alias_set.insert(alias);
56 else if(rhs.
id()==ID_if)
61 else if(rhs.
id()==ID_typecast)
65 else if(rhs.
id()==ID_address_of)
78 std::set<irep_idt> &alias_set)
80 if(rhs.
id()==ID_symbol)
83 alias_set.insert(
"&"+
id2string(identifier));
85 else if(rhs.
id()==ID_if)
90 else if(rhs.
id()==ID_dereference)
110 switch(instruction.
type())
114 std::set<irep_idt> rhs_aliases;
133 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
136 DATA_INVARIANT(
false,
"SET_RETURN_VALUE must be removed before analysis");
149 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
153 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
179 if(
aliases.is_root(a_it1) && a_it1!=a_it2 &&
180 aliases.same_set(a_it1, a_it2))
184 out <<
"Aliases: " << *a_it1;
187 out <<
' ' << *a_it2;
210 if(!
aliases.same_set(*it, b_root))
212 aliases.make_union(*it, b_root);
222 if(cleanup_map.find(*it)==cleanup_map.end())
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
Base class for all expressions.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Abstract Interpretation domain transform function.
global_may_alias_domaint()
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.
bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
Abstract Interpretation domain merge function.
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which is an object is being read.
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which an object is being written to.
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
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?
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
const T & find(const_iterator it) const
typename numbering_typet::const_iterator const_iterator
Field-insensitive, location-sensitive, over-approximative escape analysis.
const std::string & id2string(const irep_idt &d)
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,...
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
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.