cprover
escape_domaint Class Reference

#include <escape_analysis.h>

Inheritance diagram for escape_domaint:
[legend]
Collaboration diagram for escape_domaint:
[legend]

Classes

struct  cleanupt
 

Public Types

typedef union_find< irep_idtaliasest
 
typedef std::map< irep_idt, cleanuptcleanup_mapt
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Public Member Functions

 escape_domaint ()
 
void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
 
bool merge (const escape_domaint &b, locationt from, locationt to)
 
void make_bottom () final
 
void make_top () final
 
void make_entry () final
 
- Public Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
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 &ns) const
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Use the information in the domain to simplify the expression on the LHS of an assignment. 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 > &)
 
bool is_tracked (const symbol_exprt &)
 

Private Attributes

tvt has_values
 

Friends

class escape_analysist
 

Detailed Description

Definition at line 24 of file escape_analysis.h.

Member Typedef Documentation

§ aliasest

Definition at line 66 of file escape_analysis.h.

§ cleanup_mapt

Definition at line 77 of file escape_analysis.h.

Constructor & Destructor Documentation

§ escape_domaint()

escape_domaint::escape_domaint ( )
inline

Definition at line 27 of file escape_analysis.h.

References merge(), output(), and transform().

Member Function Documentation

§ assign_lhs_aliases()

void escape_domaint::assign_lhs_aliases ( const exprt lhs,
const std::set< irep_idt > &  alias_set 
)
private

§ assign_lhs_cleanup()

void escape_domaint::assign_lhs_cleanup ( const exprt lhs,
const std::set< irep_idt > &  cleanup_functions 
)
private

§ check_lhs()

void escape_domaint::check_lhs ( const exprt lhs,
std::set< irep_idt > &  cleanup_functions 
)
private

§ get_function()

irep_idt escape_domaint::get_function ( const exprt lhs)
private

§ get_rhs_aliases()

void escape_domaint::get_rhs_aliases ( const exprt rhs,
std::set< irep_idt > &  alias_set 
)
private

§ get_rhs_aliases_address_of()

void escape_domaint::get_rhs_aliases_address_of ( const exprt rhs,
std::set< irep_idt > &  alias_set 
)
private

§ get_rhs_cleanup()

void escape_domaint::get_rhs_cleanup ( const exprt rhs,
std::set< irep_idt > &  cleanup_functions 
)
private

§ is_tracked()

bool escape_domaint::is_tracked ( const symbol_exprt symbol)
private

§ make_bottom()

void escape_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 47 of file escape_analysis.h.

References aliases, cleanup_map, union_find< T >::clear(), and has_values.

§ make_entry()

void escape_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 61 of file escape_analysis.h.

References make_top().

§ make_top()

void escape_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 54 of file escape_analysis.h.

References aliases, cleanup_map, union_find< T >::clear(), and has_values.

Referenced by make_entry().

§ merge()

§ output()

void escape_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
finalvirtual

§ transform()

Friends And Related Function Documentation

§ escape_analysist

friend class escape_analysist
friend

Definition at line 90 of file escape_analysis.h.

Member Data Documentation

§ aliases

aliasest escape_domaint::aliases

§ cleanup_map

§ has_values

tvt escape_domaint::has_values
private

Definition at line 81 of file escape_analysis.h.

Referenced by make_bottom(), make_top(), merge(), output(), and transform().


The documentation for this class was generated from the following files: