cprover
|
#include <local_may_alias.h>
Classes | |
class | loc_infot |
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
local_may_aliast (const goto_functiont &_goto_function) | |
void | output (std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const |
std::set< exprt > | get (const goto_programt::const_targett t, const exprt &src) const |
bool | aliases (const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const |
Public Attributes | |
dirtyt | dirty |
localst | locals |
local_cfgt | cfg |
Protected Types | |
typedef std::stack< local_cfgt::node_nrt > | work_queuet |
typedef unsigned_union_find | alias_sett |
typedef std::vector< loc_infot > | loc_infost |
typedef std::set< unsigned > | object_sett |
Protected Member Functions | |
void | build (const goto_functiont &goto_function) |
void | assign_lhs (const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest) |
void | get_rec (object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const |
Protected Attributes | |
numbering< exprt > | objects |
loc_infost | loc_infos |
unsigned | unknown_object |
Definition at line 24 of file local_may_alias.h.
|
protected |
Definition at line 64 of file local_may_alias.h.
typedef goto_functionst::goto_functiont local_may_aliast::goto_functiont |
Definition at line 27 of file local_may_alias.h.
|
protected |
Definition at line 75 of file local_may_alias.h.
|
protected |
Definition at line 84 of file local_may_alias.h.
|
protected |
Definition at line 60 of file local_may_alias.h.
|
inlineexplicit |
Definition at line 29 of file local_may_alias.h.
References build(), and output().
Referenced by local_may_alias_factoryt::operator()().
bool local_may_aliast::aliases | ( | const goto_programt::const_targett | t, |
const exprt & | src1, | ||
const exprt & | src2 | ||
) | const |
Definition at line 141 of file local_may_alias.cpp.
References cfg, get_rec(), loc_infos, local_cfgt::loc_map, and unknown_object.
|
protected |
Definition at line 44 of file local_may_alias.cpp.
References local_may_aliast::loc_infot::aliases, dirty, symbol_exprt::get_identifier(), get_rec(), irept::id(), localst::is_local(), unsigned_union_find::isolate(), locals, unsigned_union_find::make_union(), numbering< T >::number(), objects, to_if_expr(), to_index_expr(), to_member_expr(), to_symbol_expr(), to_typecast_expr(), exprt::type(), and unknown_object.
Referenced by build().
|
protected |
Definition at line 316 of file local_may_alias.cpp.
References local_may_aliast::loc_infot::aliases, ASSIGN, assign_lhs(), cfg, DEAD, DECL, dirty, FUNCTION_CALL, symbol_exprt::get_identifier(), localst::is_local(), irept::is_not_nil(), unsigned_union_find::isolate(), code_assignt::lhs(), code_function_callt::lhs(), loc_infos, locals, localst::locals_map, unsigned_union_find::make_union(), local_may_aliast::loc_infot::merge(), local_cfgt::nodes, numbering< T >::number(), objects, code_assignt::rhs(), local_cfgt::nodet::successors, code_declt::symbol(), code_deadt::symbol(), local_cfgt::nodet::t, to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_symbol_expr(), and unknown_object.
Referenced by local_may_aliast().
std::set< exprt > local_may_aliast::get | ( | const goto_programt::const_targett | t, |
const exprt & | src | ||
) | const |
Definition at line 115 of file local_may_alias.cpp.
References cfg, get_rec(), loc_infos, local_cfgt::loc_map, and objects.
Referenced by function_modifiest::get_modifies_lhs(), and get_modifies_lhs().
|
protected |
Definition at line 169 of file local_may_alias.cpp.
References local_may_aliast::loc_infot::aliases, index_exprt::array(), from_integer(), side_effect_exprt::get_statement(), irept::id(), index_exprt::index(), index_type(), irept::is_nil(), exprt::is_zero(), numbering< T >::number(), address_of_exprt::object(), objects, exprt::op0(), exprt::op1(), exprt::operands(), unsigned_union_find::same_set(), unsigned_union_find::size(), to_address_of_expr(), to_if_expr(), to_index_expr(), to_side_effect_expr(), to_typecast_expr(), exprt::type(), and unknown_object.
Referenced by aliases(), assign_lhs(), and get().
void local_may_aliast::output | ( | std::ostream & | out, |
const goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) | const |
Definition at line 437 of file local_may_alias.cpp.
References local_may_aliast::loc_infot::aliases, unsigned_union_find::count(), unsigned_union_find::find(), forall_goto_program_instructions, from_expr(), loc_infos, objects, and unsigned_union_find::size().
Referenced by goto_analyzer_parse_optionst::doit(), and local_may_aliast().
local_cfgt local_may_aliast::cfg |
Definition at line 45 of file local_may_alias.h.
dirtyt local_may_aliast::dirty |
Definition at line 43 of file local_may_alias.h.
Referenced by assign_lhs(), and build().
|
protected |
localst local_may_aliast::locals |
Definition at line 44 of file local_may_alias.h.
Referenced by assign_lhs(), and build().
Definition at line 62 of file local_may_alias.h.
Referenced by assign_lhs(), build(), get(), get_rec(), and output().
|
protected |
Definition at line 91 of file local_may_alias.h.
Referenced by aliases(), assign_lhs(), build(), and get_rec().