cprover
|
#include <global_may_alias.h>
Public Types | |
typedef union_find< irep_idt > | aliasest |
![]() | |
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 |
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 |
void | make_top () final override |
void | make_entry () final override |
bool | is_bottom () const final override |
bool | is_top () const final override |
![]() | |
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 |
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 |
Definition at line 24 of file global_may_alias.h.
Definition at line 76 of file global_may_alias.h.
|
inline |
Definition at line 27 of file global_may_alias.h.
|
private |
Definition at line 14 of file global_may_alias.cpp.
References aliases, symbol_exprt::get_identifier(), irept::id(), union_find< T >::isolate(), union_find< T >::make_union(), and to_symbol_expr().
Referenced by transform().
|
private |
Definition at line 31 of file global_may_alias.cpp.
References aliases, symbol_exprt::get_identifier(), get_rhs_aliases_address_of(), irept::id(), union_find< T >::same_set(), to_address_of_expr(), to_if_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by transform().
|
private |
Definition at line 59 of file global_may_alias.cpp.
References symbol_exprt::get_identifier(), irept::id(), id2string(), to_if_expr(), and to_symbol_expr().
Referenced by get_rhs_aliases().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 62 of file global_may_alias.h.
References aliases, DATA_INVARIANT, has_values, tvt::is_false(), and union_find< T >::size().
|
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().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 45 of file global_may_alias.h.
References aliases, union_find< T >::clear(), and has_values.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 57 of file global_may_alias.h.
References make_top().
|
inlinefinaloverridevirtual |
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().
bool global_may_alias_domaint::merge | ( | const global_may_alias_domaint & | b, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 159 of file global_may_alias.cpp.
References aliases, union_find< T >::begin(), union_find< T >::end(), union_find< T >::find(), has_values, tvt::is_false(), union_find< T >::isolate(), union_find< T >::make_union(), union_find< T >::same_set(), and tvt::unknown().
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 121 of file global_may_alias.cpp.
References aliases, union_find< T >::begin(), union_find< T >::end(), has_values, tvt::is_known(), union_find< T >::is_root(), union_find< T >::same_set(), and tvt::to_string().
|
finaloverridevirtual |
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.
aliasest global_may_alias_domaint::aliases |
Definition at line 77 of file global_may_alias.h.
Referenced by assign_lhs_aliases(), get_rhs_aliases(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().
|
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().