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)

void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override

bool merge (const escape_domaint &b, trace_ptrt from, trace_ptrt to)

void make_bottom () final override

no states

void make_top () final override

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

bool is_bottom () const override final

bool is_top () const override final

- 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 void make_entry ()

Make this domain a reasonable entry-point state For most domains top is sufficient.

virtual bool ai_simplify (exprt &condition, const namespacet &) const

also add

virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const

Simplifies the expression but keeps it as an l-value.

virtual exprt to_predicate (void) const

Gives a Boolean condition that is true for all values represented by the domain.

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.

ai_domain_baset (const ai_domain_baset &old)

A copy constructor is part of the domain interface.

Detailed Description

Definition at line 22 of file escape_analysis.h.

Member Typedef Documentation

◆ aliasest

typedef union_find<irep_idt> escape_domaint::aliasest

Definition at line 74 of file escape_analysis.h.

◆ cleanup_mapt

typedef std::map<irep_idt, cleanupt> escape_domaint::cleanup_mapt

Definition at line 85 of file escape_analysis.h.

Constructor & Destructor Documentation

◆ escape_domaint()

escape_domaint::escape_domaint ( )

inline

Definition at line 25 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 65 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 46 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 379 of file escape_analysis.cpp.

◆ get_function()

irep_idt escape_domaint::get_function ( const exprt & lhs )

private

Definition at line 31 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 116 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 148 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 86 of file escape_analysis.cpp.

◆ is_bottom()

bool escape_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 58 of file escape_analysis.h.

◆ is_top()

bool escape_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 66 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 44 of file escape_analysis.h.

◆ make_top()

void escape_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 51 of file escape_analysis.h.

◆ merge()

bool escape_domaint::merge ( const escape_domaint & b,

trace_ptrt from,

trace_ptrt to

)

Definition at line 326 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 280 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 167 of file escape_analysis.cpp.

Friends And Related Symbol Documentation

◆ escape_analysist

friend class escape_analysist

friend

Definition at line 98 of file escape_analysis.h.

Member Data Documentation

◆ aliases

aliasest escape_domaint::aliases

Definition at line 75 of file escape_analysis.h.

◆ cleanup_map

cleanup_mapt escape_domaint::cleanup_map

Definition at line 86 of file escape_analysis.h.

◆ has_values

tvt escape_domaint::has_values

private

Definition at line 89 of file escape_analysis.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/escape_analysis.h
/home/runner/work/cbmc/cbmc/src/analyses/escape_analysis.cpp