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 |
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 |
![]() | |
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 | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
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 |
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.
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 57 of file global_may_alias.h.
References 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().
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 |
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.
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().