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

- 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 67 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 48 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 385 of file escape_analysis.cpp.

◆ get_function()

irep_idt escape_domaint::get_function ( const exprt lhs)
private

Definition at line 33 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 118 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 150 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 88 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 18 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 329 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 283 of file escape_analysis.cpp.

◆ transform()

void escape_domaint::transform ( const irep_idt function_from,
trace_ptrt  from,
const irep_idt function_to,
trace_ptrt  to,
ai_baset ai,
const namespacet ns 
)
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.

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: