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)
126 if(aliases.same_set(alias, identifier))
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)
177 const goto_programt::instructiont &instruction=*from;
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)
275 for(aliasest::const_iterator a_it1=
aliases.begin();
281 for(aliasest::const_iterator a_it2=
aliases.begin();
290 out <<
"Aliases: " << *a_it1;
293 out <<
' ' << *a_it2;
320 const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
321 std::set<irep_idt> &a_cleanup=
cleanup_map[cleanup.first].cleanup_functions;
322 unsigned old_size=a_cleanup.size();
323 a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
324 if(a_cleanup.size()!=old_size)
330 for(cleanup_mapt::iterator a_it=
cleanup_map.begin();
334 if(a_it->second.cleanup_functions.empty())
341 for(aliasest::const_iterator it=b.
aliases.begin();
355 for(aliasest::const_iterator it=
aliases.begin();
368 std::set<irep_idt> &cleanup_functions)
370 if(lhs.
id()==ID_symbol)
375 const escape_domaint::cleanup_mapt::const_iterator m_it=
384 for(
const auto &alias :
aliases)
386 if(alias!=identifier && aliases.same_set(alias, identifier))
393 cleanup_functions.insert(
394 m_it->second.cleanup_functions.begin(),
395 m_it->second.cleanup_functions.end());
405 const std::set<irep_idt> &cleanup_functions,
411 for(
const auto &cleanup : cleanup_functions)
416 goto_function.body.insert_before_swap(location);
428 if(arg.
type()!=param_type)
433 location->make_function_call(code);
434 location->source_location=source_location;
448 const goto_programt::instructiont &instruction=*i_it;
450 switch(instruction.type)
456 std::set<irep_idt> cleanup_functions;
457 operator[](i_it).check_lhs(code_assign.
lhs(), cleanup_functions);
472 std::set<irep_idt> cleanup_functions1;
476 const escape_domaint::cleanup_mapt::const_iterator m_it=
482 cleanup_functions1.insert(
483 m_it->second.cleanup_functions.begin(),
484 m_it->second.cleanup_functions.end());
487 std::set<irep_idt> cleanup_functions2;
506 for(
const auto &c : cleanup_functions1)
512 for(
const auto &c : cleanup_functions2)
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const code_declt & to_code_decl(const codet &code)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
const code_deadt & to_code_dead(const codet &code)
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
const irep_idt & get_identifier() const
void isolate(typename numbering< T >::const_iterator it)
const T & find(typename numbering< T >::const_iterator it) const
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
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
A declaration of a local variable.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
const irep_idt & get_identifier() const
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
Field-insensitive, location-sensitive, over-approximative escape analysis.
goto_function_templatet< goto_programt > goto_functiont
void instrument(goto_functionst &, const namespacet &)
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 > &)
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
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
bool merge(const escape_domaint &b, locationt from, locationt to)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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 assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
void make_typecast(const typet &_type)
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett