13 #ifndef CPROVER_ANALYSES_ESCAPE_ANALYSIS_H 14 #define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H 63 "If the domain is bottom, all maps must be empty");
71 "If the domain is top, all maps must be empty");
125 const std::set<irep_idt> &,
130 #endif // CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
void make_bottom() final override
no states
virtual void initialize(const goto_functionst &)
void make_entry() override final
a reasonable entry-point state
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
void transform(locationt from, 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 output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
numbering< irep_idt > bits
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
union_find< irep_idt > aliasest
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
instructionst::iterator targett
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
::goto_functiont goto_functiont
std::set< irep_idt > cleanup_functions
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool is_top() const override final
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
void check_lhs(const exprt &, std::set< irep_idt > &)
The basic interface of an abstract interpreter.
Base class for all expressions.
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
bool merge(const escape_domaint &b, locationt from, locationt to)
std::map< irep_idt, cleanupt > cleanup_mapt
irep_idt get_function(const exprt &)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
void instrument(goto_modelt &)
#define DATA_INVARIANT(CONDITION, REASON)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
bool is_bottom() const override final