cprover
escape_domaint Class Reference

#include <escape_analysis.h>

+ Inheritance diagram for escape_domaint:
+ Collaboration diagram for escape_domaint:

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
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 

Public Member Functions

 escape_domaint ()
 
void transform (const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
 
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...
 
- Public Member Functions inherited from ai_domain_baset
virtual ~ai_domain_baset ()
 
virtual void transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
 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...
 
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

- Protected Member Functions inherited from ai_domain_baset
 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...
 

Detailed Description

Definition at line 24 of file escape_analysis.h.

Member Typedef Documentation

◆ aliasest

Definition at line 84 of file escape_analysis.h.

◆ cleanup_mapt

Definition at line 95 of file escape_analysis.h.

Constructor & Destructor Documentation

◆ escape_domaint()

escape_domaint::escape_domaint ( )
inline

Definition at line 27 of file escape_analysis.h.

Member Function Documentation

◆ assign_lhs_aliases()

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

Definition at line 66 of file escape_analysis.cpp.

◆ assign_lhs_cleanup()

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

Definition at line 47 of file escape_analysis.cpp.

◆ check_lhs()

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

Definition at line 388 of file escape_analysis.cpp.

◆ get_function()

irep_idt escape_domaint::get_function ( const exprt lhs)
private

Definition at line 32 of file escape_analysis.cpp.

◆ get_rhs_aliases()

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

Definition at line 117 of file escape_analysis.cpp.

◆ get_rhs_aliases_address_of()

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

Definition at line 149 of file escape_analysis.cpp.

◆ get_rhs_cleanup()

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

Definition at line 87 of file escape_analysis.cpp.

◆ is_bottom()

bool escape_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 63 of file escape_analysis.h.

◆ is_top()

bool escape_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 71 of file escape_analysis.h.

◆ is_tracked()

bool escape_domaint::is_tracked ( const symbol_exprt symbol)
private

Definition at line 17 of file escape_analysis.cpp.

◆ make_bottom()

void escape_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 49 of file escape_analysis.h.

◆ make_entry()

void escape_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 79 of file escape_analysis.h.

◆ make_top()

void escape_domaint::make_top ( )
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.

◆ merge()

bool escape_domaint::merge ( const escape_domaint b,
locationt  from,
locationt  to 
)

Definition at line 332 of file escape_analysis.cpp.

◆ output()

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

Reimplemented from ai_domain_baset.

Definition at line 286 of file escape_analysis.cpp.

◆ transform()

void escape_domaint::transform ( const irep_idt function_from,
locationt  from,
const irep_idt function_to,
locationt  to,
ai_baset ai,
const namespacet ns 
)
finaloverridevirtual
Deprecated:
SINCE(2019, 08, 01, "use the history signature instead")

Implements ai_domain_baset.

Definition at line 168 of file escape_analysis.cpp.

Friends And Related Function Documentation

◆ escape_analysist

friend class escape_analysist
friend

Definition at line 108 of file escape_analysis.h.

Member Data Documentation

◆ aliases

aliasest escape_domaint::aliases

Definition at line 85 of file escape_analysis.h.

◆ cleanup_map

cleanup_mapt escape_domaint::cleanup_map

Definition at line 96 of file escape_analysis.h.

◆ has_values

tvt escape_domaint::has_values
private

Definition at line 99 of file escape_analysis.h.


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