34 if(lhs.
id()==ID_address_of)
36 else if(lhs.
id()==ID_typecast)
38 else if(lhs.
id()==ID_symbol)
49 const std::set<irep_idt> &cleanup_functions)
51 if(lhs.
id()==ID_symbol)
58 if(cleanup_functions.empty())
61 cleanup_map[identifier].cleanup_functions=cleanup_functions;
68 const std::set<irep_idt> &alias_set)
70 if(lhs.
id()==ID_symbol)
79 for(
const auto &alias : alias_set)
89 std::set<irep_idt> &cleanup_functions)
91 if(rhs.
id()==ID_symbol)
98 const escape_domaint::cleanup_mapt::const_iterator m_it=
102 cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
103 m_it->second.cleanup_functions.end());
106 else if(rhs.
id()==ID_if)
111 else if(rhs.
id()==ID_typecast)
119 std::set<irep_idt> &alias_set)
121 if(rhs.
id()==ID_symbol)
127 alias_set.insert(identifier);
129 for(
const auto &alias :
aliases)
131 alias_set.insert(alias);
134 else if(rhs.
id()==ID_if)
139 else if(rhs.
id()==ID_typecast)
143 else if(rhs.
id()==ID_address_of)
151 std::set<irep_idt> &alias_set)
153 if(rhs.
id()==ID_symbol)
156 alias_set.insert(
"&"+
id2string(identifier));
158 else if(rhs.
id()==ID_if)
163 else if(rhs.
id()==ID_dereference)
185 switch(instruction.
type)
191 std::set<irep_idt> cleanup_functions;
195 std::set<irep_idt> rhs_aliases;
223 if(
function.
id()==ID_symbol)
228 if(code_function_call.
arguments().size()==2)
235 if(!cleanup_function.
empty())
238 std::set<irep_idt> lhs_set;
241 for(
const auto &l : lhs_set)
243 cleanup_map[l].cleanup_functions.insert(cleanup_function);
275 out << cleanup.first <<
':';
276 for(
const auto &
id : cleanup.second.cleanup_functions)
296 out <<
"Aliases: " << *a_it1;
299 out <<
' ' << *a_it2;
318 const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
319 std::set<irep_idt> &a_cleanup=
cleanup_map[cleanup.first].cleanup_functions;
320 auto old_size=a_cleanup.size();
321 a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
322 if(a_cleanup.size()!=old_size)
328 for(cleanup_mapt::iterator a_it=
cleanup_map.begin();
332 if(a_it->second.cleanup_functions.empty())
366 std::set<irep_idt> &cleanup_functions)
368 if(lhs.
id()==ID_symbol)
373 const escape_domaint::cleanup_mapt::const_iterator m_it=
382 for(
const auto &alias :
aliases)
391 cleanup_functions.insert(
392 m_it->second.cleanup_functions.begin(),
393 m_it->second.cleanup_functions.end());
403 const std::set<irep_idt> &cleanup_functions,
409 for(
const auto &cleanup : cleanup_functions)
414 goto_function.body.insert_before_swap(location);
424 if(arg.
type()!=param_type)
429 location->make_function_call(code);
430 location->source_location=source_location;
447 switch(instruction.
type)
453 std::set<irep_idt> cleanup_functions;
469 std::set<irep_idt> cleanup_functions1;
473 const escape_domaint::cleanup_mapt::const_iterator m_it=
479 cleanup_functions1.insert(
480 m_it->second.cleanup_functions.begin(),
481 m_it->second.cleanup_functions.end());
484 std::set<irep_idt> cleanup_functions2;
503 for(
const auto &c : cleanup_functions1)
509 for(
const auto &c : cleanup_functions2)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The type of an expression, extends irept.
const code_declt & to_code_decl(const codet &code)
virtual statet & get_state(locationt l) override
const std::string & id2string(const irep_idt &d)
const code_deadt & to_code_dead(const codet &code)
goto_program_instruction_typet type
What kind of instruction?
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
void isolate(typename numbering< T >::const_iterator it)
typet & type()
Return the type of the expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
symbol_tablet symbol_table
Symbol table.
const T & find(typename numbering< T >::const_iterator it) const
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
This class represents an instruction in the GOTO intermediate representation.
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
const char * to_string() const
const code_assignt & to_code_assign(const codet &code)
bool same_set(const T &a, const T &b) const
const irep_idt & id() const
escape_domaint & operator[](locationt l)
instructionst::iterator targett
A codet representing the declaration of a local variable.
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
codet representation of a function call statement.
Field-insensitive, location-sensitive, over-approximative escape analysis.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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 assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &)
numbering_typet::const_iterator const_iterator
The basic interface of an abstract interpreter.
Base class for all expressions.
const parameterst & parameters() const
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
#define Forall_goto_functions(it, functions)
bool is_root(const T &a) const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool merge(const escape_domaint &b, locationt from, locationt to)
A codet representing the removal of a local variable going out of scope.
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
irep_idt get_function(const exprt &)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
bool make_union(const T &a, const T &b)
void instrument(goto_modelt &)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_identifier() const
A codet representing an assignment in the program.
const code_function_callt & to_code_function_call(const codet &code)