cprover
|
#include <escape_analysis.h>
Classes | |
struct | cleanupt |
Public Types | |
typedef union_find< irep_idt > | aliasest |
typedef std::map< irep_idt, cleanupt > | cleanup_mapt |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef ai_history_baset::trace_ptrt | trace_ptrt |
Public Member Functions | |
escape_domaint () | |
void | transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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 is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More... | |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override |
bool | merge (const escape_domaint &b, locationt from, locationt to) |
void | make_bottom () final override |
no states More... | |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
bool | is_bottom () const override final |
bool | is_top () const override final |
void | make_entry () override final |
Make this domain a reasonable entry-point state. More... | |
![]() | |
virtual | ~ai_domain_baset () |
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify (exprt &condition, const namespacet &) const |
also add More... | |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Simplifies the expression but keeps it as an l-value. More... | |
virtual exprt | to_predicate (void) const |
Gives a Boolean condition that is true for all values represented by the domain. More... | |
Public Attributes | |
aliasest | aliases |
cleanup_mapt | cleanup_map |
Private Member Functions | |
void | assign_lhs_cleanup (const exprt &, const std::set< irep_idt > &) |
void | get_rhs_cleanup (const exprt &, std::set< irep_idt > &) |
void | assign_lhs_aliases (const exprt &, const std::set< irep_idt > &) |
void | get_rhs_aliases (const exprt &, std::set< irep_idt > &) |
void | get_rhs_aliases_address_of (const exprt &, std::set< irep_idt > &) |
irep_idt | get_function (const exprt &) |
void | check_lhs (const exprt &, std::set< irep_idt > &) const |
bool | is_tracked (const symbol_exprt &) |
Private Attributes | |
tvt | has_values |
Friends | |
class | escape_analysist |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More... | |
ai_domain_baset (const ai_domain_baset &old) | |
A copy constructor is part of the domain interface. More... | |
Definition at line 24 of file escape_analysis.h.
typedef union_find<irep_idt> escape_domaint::aliasest |
Definition at line 84 of file escape_analysis.h.
typedef std::map<irep_idt, cleanupt> escape_domaint::cleanup_mapt |
Definition at line 95 of file escape_analysis.h.
|
inline |
Definition at line 27 of file escape_analysis.h.
|
private |
Definition at line 67 of file escape_analysis.cpp.
|
private |
Definition at line 48 of file escape_analysis.cpp.
|
private |
Definition at line 385 of file escape_analysis.cpp.
Definition at line 33 of file escape_analysis.cpp.
|
private |
Definition at line 118 of file escape_analysis.cpp.
|
private |
Definition at line 150 of file escape_analysis.cpp.
|
private |
Definition at line 88 of file escape_analysis.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 63 of file escape_analysis.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 71 of file escape_analysis.h.
|
private |
Definition at line 18 of file escape_analysis.cpp.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 79 of file escape_analysis.h.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 56 of file escape_analysis.h.
bool escape_domaint::merge | ( | const escape_domaint & | b, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 329 of file escape_analysis.cpp.
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 283 of file escape_analysis.cpp.
|
finaloverridevirtual |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after
"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature
Implements ai_domain_baset.
Definition at line 169 of file escape_analysis.cpp.
|
friend |
Definition at line 108 of file escape_analysis.h.
aliasest escape_domaint::aliases |
Definition at line 85 of file escape_analysis.h.
cleanup_mapt escape_domaint::cleanup_map |
Definition at line 96 of file escape_analysis.h.
|
private |
Definition at line 99 of file escape_analysis.h.