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 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 global_may_alias_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...
 
void make_entry () final override
 a reasonable entry-point state More...
 
bool is_bottom () const final override
 
bool is_top () const final override
 
- 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 &ns) 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 > &)
 
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
 

Additional Inherited Members

- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. 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

◆ 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

◆ is_bottom()

bool global_may_alias_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

◆ is_top()

bool global_may_alias_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 69 of file global_may_alias.h.

References aliases, DATA_INVARIANT, has_values, tvt::is_true(), and union_find< T >::size().

◆ make_bottom()

void global_may_alias_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 45 of file global_may_alias.h.

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

◆ make_entry()

void global_may_alias_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 57 of file global_may_alias.h.

References make_top().

◆ make_top()

void global_may_alias_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 51 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
finaloverridevirtual

◆ transform()

void global_may_alias_domaint::transform ( locationt  from,
locationt  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)

"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "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())

Implements ai_domain_baset.

Definition at line 78 of file global_may_alias.cpp.

References aliases, ASSIGN, assign_lhs_aliases(), goto_programt::instructiont::code, DEAD, DECL, code_declt::get_identifier(), code_deadt::get_identifier(), get_rhs_aliases(), has_values, tvt::is_false(), union_find< T >::isolate(), code_assignt::lhs(), code_assignt::rhs(), to_code_assign(), to_code_dead(), to_code_decl(), and goto_programt::instructiont::type.

Member Data Documentation

◆ aliases

aliasest global_may_alias_domaint::aliases

◆ has_values

tvt global_may_alias_domaint::has_values
private

Definition at line 80 of file global_may_alias.h.

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


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