Go to the documentation of this file.
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);
260 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
276 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
281 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
299 out << cleanup.first <<
':';
300 for(
const auto &
id : cleanup.second.cleanup_functions)
320 out <<
"Aliases: " << *a_it1;
323 out <<
' ' << *a_it2;
342 const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
343 std::set<irep_idt> &a_cleanup=
cleanup_map[cleanup.first].cleanup_functions;
344 auto old_size=a_cleanup.size();
345 a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
346 if(a_cleanup.size()!=old_size)
352 for(cleanup_mapt::iterator a_it=
cleanup_map.begin();
356 if(a_it->second.cleanup_functions.empty())
390 std::set<irep_idt> &cleanup_functions)
const
392 if(lhs.
id()==ID_symbol)
397 const escape_domaint::cleanup_mapt::const_iterator m_it=
406 for(
const auto &alias :
aliases)
415 cleanup_functions.insert(
416 m_it->second.cleanup_functions.begin(),
417 m_it->second.cleanup_functions.end());
427 const std::set<irep_idt> &cleanup_functions,
433 for(
const auto &cleanup : cleanup_functions)
438 goto_function.body.insert_before_swap(location);
475 std::set<irep_idt> cleanup_functions;
478 f_it->second, i_it, code_assign.
lhs(), cleanup_functions,
false, ns);
484 std::set<irep_idt> cleanup_functions1;
488 const escape_domaint::cleanup_mapt::const_iterator m_it =
494 cleanup_functions1.insert(
495 m_it->second.cleanup_functions.begin(),
496 m_it->second.cleanup_functions.end());
499 std::set<irep_idt> cleanup_functions2;
504 f_it->second, i_it, code_dead.
symbol(), cleanup_functions1,
true, ns);
513 for(
const auto &c : cleanup_functions1)
519 for(
const auto &c : cleanup_functions2)
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void isolate(typename numbering< T >::const_iterator it)
const code_declt & to_code_decl(const codet &code)
const escape_domaint & operator[](locationt l) const
Find the analysis result for a given location.
The type of an expression, extends irept.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
goto_program_instruction_typet type
What kind of instruction?
void check_lhs(const exprt &, std::set< irep_idt > &) const
A codet representing the declaration of a local variable.
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
Base class for all expressions.
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const T & find(typename numbering< T >::const_iterator it) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt get_function(const exprt &)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
codet code
Do not read or modify directly – use get_X() instead.
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
bool same_set(const T &a, const T &b) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool merge(const escape_domaint &b, locationt from, locationt to)
const irep_idt & id() const
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
const code_function_callt & to_code_function_call(const codet &code)
const char * to_string() const
void instrument(goto_modelt &)
A codet representing the removal of a local variable going out of scope.
const parameterst & parameters() const
bool is_root(const T &a) const
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
numbering_typet::const_iterator const_iterator
goto_programt::const_targett locationt
bool make_union(const T &a, const T &b)
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
const irep_idt & get_identifier() const
Operator to return the address of an object.
source_locationt & add_source_location()
A codet representing an assignment in the program.
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
instructionst::iterator targett
bool is_tracked(const symbol_exprt &)
Field-insensitive, location-sensitive, over-approximative escape analysis.