19 if(identifier==
"__CPROVER_memory_leak" ||
20 identifier==
"__CPROVER_malloc_object" ||
21 identifier==
"__CPROVER_dead_object" ||
22 identifier==
"__CPROVER_deallocated")
30 if(lhs.
id()==ID_address_of)
32 else if(lhs.
id()==ID_typecast)
34 else if(lhs.
id()==ID_symbol)
45 const std::set<irep_idt> &cleanup_functions)
47 if(lhs.
id()==ID_symbol)
54 if(cleanup_functions.empty())
57 cleanup_map[identifier].cleanup_functions=cleanup_functions;
64 const std::set<irep_idt> &alias_set)
66 if(lhs.
id()==ID_symbol)
75 for(
const auto &alias : alias_set)
85 std::set<irep_idt> &cleanup_functions)
87 if(rhs.
id()==ID_symbol)
94 const escape_domaint::cleanup_mapt::const_iterator m_it=
98 cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
99 m_it->second.cleanup_functions.end());
102 else if(rhs.
id()==ID_if)
107 else if(rhs.
id()==ID_typecast)
115 std::set<irep_idt> &alias_set)
117 if(rhs.
id()==ID_symbol)
123 alias_set.insert(identifier);
125 for(
const auto &alias :
aliases)
127 alias_set.insert(alias);
130 else if(rhs.
id()==ID_if)
135 else if(rhs.
id()==ID_typecast)
139 else if(rhs.
id()==ID_address_of)
147 std::set<irep_idt> &alias_set)
149 if(rhs.
id()==ID_symbol)
152 alias_set.insert(
"&"+
id2string(identifier));
154 else if(rhs.
id()==ID_if)
159 else if(rhs.
id()==ID_dereference)
179 switch(instruction.
type)
185 std::set<irep_idt> cleanup_functions;
217 if(
function.
id()==ID_symbol)
220 if(identifier==
"__CPROVER_cleanup")
222 if(code_function_call.
arguments().size()==2)
229 if(!cleanup_function.
empty())
232 std::set<irep_idt> lhs_set;
235 for(
const auto &lhs : lhs_set)
237 cleanup_map[lhs].cleanup_functions.insert(cleanup_function);
269 out << cleanup.first <<
':';
270 for(
const auto &
id : cleanup.second.cleanup_functions)
290 out <<
"Aliases: " << *a_it1;
293 out <<
' ' << *a_it2;
312 const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
313 std::set<irep_idt> &a_cleanup=
cleanup_map[cleanup.first].cleanup_functions;
314 auto old_size=a_cleanup.size();
315 a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
316 if(a_cleanup.size()!=old_size)
322 for(cleanup_mapt::iterator a_it=
cleanup_map.begin();
326 if(a_it->second.cleanup_functions.empty())
360 std::set<irep_idt> &cleanup_functions)
362 if(lhs.
id()==ID_symbol)
367 const escape_domaint::cleanup_mapt::const_iterator m_it=
376 for(
const auto &alias :
aliases)
385 cleanup_functions.insert(
386 m_it->second.cleanup_functions.begin(),
387 m_it->second.cleanup_functions.end());
397 const std::set<irep_idt> &cleanup_functions,
403 for(
const auto &cleanup : cleanup_functions)
408 goto_function.body.insert_before_swap(location);
420 if(arg.
type()!=param_type)
425 location->make_function_call(code);
426 location->source_location=source_location;
443 switch(instruction.
type)
449 std::set<irep_idt> cleanup_functions;
465 std::set<irep_idt> cleanup_functions1;
469 const escape_domaint::cleanup_mapt::const_iterator m_it=
475 cleanup_functions1.insert(
476 m_it->second.cleanup_functions.begin(),
477 m_it->second.cleanup_functions.end());
480 std::set<irep_idt> cleanup_functions2;
499 for(
const auto &c : cleanup_functions1)
505 for(
const auto &c : cleanup_functions2)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
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 irep_idt & get_identifier() const
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 generic typet to a code_typet.
const irep_idt & get_identifier() const
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
void isolate(typename numbering< T >::const_iterator it)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic 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 declaration of a local variable.
const irep_idt & get_identifier() const
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
::goto_functiont goto_functiont
Field-insensitive, location-sensitive, over-approximative escape analysis.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
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
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 a generic exprt to a typecast_exprt.
bool merge(const escape_domaint &b, locationt from, locationt to)
A removal of a local variable.
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)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)