cprover
global_may_alias_domaint Class Reference

#include <global_may_alias.h>

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

Public Types

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

Public Member Functions

 global_may_alias_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 global_may_alias_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
 

Private Member Functions

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 > &)
 

Private Attributes

tvt has_values
 

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

◆ get_rhs_aliases()

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

◆ 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

◆ make_bottom()

void global_may_alias_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 47 of file global_may_alias.h.

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

◆ make_entry()

void global_may_alias_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 59 of file global_may_alias.h.

References make_top().

◆ make_top()

void global_may_alias_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 53 of file global_may_alias.h.

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

Referenced by make_entry().

◆ merge()

◆ output()

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

◆ transform()

Member Data Documentation

◆ aliases

aliasest global_may_alias_domaint::aliases

◆ has_values

tvt global_may_alias_domaint::has_values
private

Definition at line 68 of file global_may_alias.h.

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


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