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 |
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 |
![]() | |
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 |
Definition at line 24 of file global_may_alias.h.
Definition at line 64 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().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 47 of file global_may_alias.h.
References aliases, union_find< T >::clear(), and has_values.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 59 of file global_may_alias.h.
References 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().
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 >::find(), has_values, tvt::is_false(), union_find< T >::isolate(), union_find< T >::make_union(), union_find< T >::same_set(), and tvt::unknown().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 121 of file global_may_alias.cpp.
References aliases, has_values, tvt::is_known(), union_find< T >::is_root(), union_find< T >::same_set(), and tvt::to_string().
|
final |
Definition at line 78 of file global_may_alias.cpp.
References aliases, ASSIGN, assign_lhs_aliases(), 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(), and to_code_decl().
aliasest global_may_alias_domaint::aliases |
Definition at line 65 of file global_may_alias.h.
Referenced by assign_lhs_aliases(), get_rhs_aliases(), make_bottom(), make_top(), merge(), output(), and transform().
|
private |
Definition at line 68 of file global_may_alias.h.
Referenced by make_bottom(), make_top(), merge(), output(), and transform().