cprover
global_may_alias_domaint Class Reference

#include <global_may_alias.h>

+ Inheritance diagram for global_may_alias_domaint:
+ Collaboration diagram for global_may_alias_domaint:

Public Types

typedef union_find< irep_idtaliasest
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 

Public Member Functions

 global_may_alias_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
 Abstract Interpretation domain transform function. More...
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
 Abstract Interpretation domain output function. More...
 
bool merge (const global_may_alias_domaint &b, locationt from, locationt to)
 Abstract Interpretation domain merge function. More...
 
void make_bottom () final override
 Clear list of aliases, and mark domain as bottom. More...
 
void make_top () final override
 Clear list of aliases, and mark domain as top. More...
 
void make_entry () final override
 Make this domain a reasonable entry-point state. More...
 
bool is_bottom () const final override
 Returns true if domain is bottom. More...
 
bool is_top () const final override
 Returns false if domain is top. 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
 

Private Member Functions

void assign_lhs_aliases (const exprt &, const std::set< irep_idt > &)
 Populate list of aliases for a given identifier in a context in which an object is being written to. More...
 
void get_rhs_aliases (const exprt &, std::set< irep_idt > &)
 Populate list of aliases for a given identifier in a context in which is an object is being read. More...
 
void get_rhs_aliases_address_of (const exprt &, std::set< irep_idt > &)
 Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions. More...
 

Private Attributes

tvt has_values
 

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 global_may_alias.h.

Member Typedef Documentation

◆ aliasest

Constructor & Destructor Documentation

◆ global_may_alias_domaint()

global_may_alias_domaint::global_may_alias_domaint ( )
inline

Definition at line 27 of file global_may_alias.h.

Member Function Documentation

◆ assign_lhs_aliases()

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

Populate list of aliases for a given identifier in a context in which an object is being written to.

Parameters
lhsA left hand side expression, containing an identifier.
alias_setAn external set of aliases to populate internal aliases set.

Definition at line 19 of file global_may_alias.cpp.

◆ get_rhs_aliases()

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

Populate list of aliases for a given identifier in a context in which is an object is being read.

Parameters
rhsA right hand side expression.
alias_setA external set of aliases to populate internal aliases set.

Definition at line 41 of file global_may_alias.cpp.

◆ get_rhs_aliases_address_of()

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

Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.

Parameters
rhsA right hand side expression.
alias_setA external set of aliases to populate internal aliases set.

Definition at line 74 of file global_may_alias.cpp.

◆ is_bottom()

bool global_may_alias_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Returns true if domain is bottom.

Implements ai_domain_baset.

Definition at line 76 of file global_may_alias.h.

◆ is_top()

bool global_may_alias_domaint::is_top ( ) const
inlinefinaloverridevirtual

Returns false if domain is top.

Implements ai_domain_baset.

Definition at line 84 of file global_may_alias.h.

◆ make_bottom()

void global_may_alias_domaint::make_bottom ( )
inlinefinaloverridevirtual

Clear list of aliases, and mark domain as bottom.

Implements ai_domain_baset.

Definition at line 57 of file global_may_alias.h.

◆ make_entry()

void global_may_alias_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 70 of file global_may_alias.h.

◆ make_top()

void global_may_alias_domaint::make_top ( )
inlinefinaloverridevirtual

Clear list of aliases, and mark domain as top.

Implements ai_domain_baset.

Definition at line 64 of file global_may_alias.h.

◆ merge()

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

Abstract Interpretation domain merge function.

Definition at line 200 of file global_may_alias.cpp.

◆ output()

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

Abstract Interpretation domain output function.

Parameters
outA stream to dump domain state on.
aiA reference to the currently active abstract interpreter.
nsA namespace to resolve symbols during output.

Reimplemented from ai_domain_baset.

Definition at line 162 of file global_may_alias.cpp.

◆ transform()

void global_may_alias_domaint::transform ( const irep_idt function_from,
locationt  from,
const irep_idt function_to,
locationt  to,
ai_baset ai,
const namespacet ns 
)
finaloverridevirtual

Abstract Interpretation domain transform function.

Implements ai_domain_baset.

Definition at line 93 of file global_may_alias.cpp.

Member Data Documentation

◆ aliases

aliasest global_may_alias_domaint::aliases

Definition at line 92 of file global_may_alias.h.

◆ has_values

tvt global_may_alias_domaint::has_values
private

Definition at line 95 of file global_may_alias.h.


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