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 25 of file local_may_alias.h.
|
protected |
Definition at line 65 of file local_may_alias.h.
Definition at line 28 of file local_may_alias.h.
|
protected |
Definition at line 76 of file local_may_alias.h.
|
protected |
Definition at line 85 of file local_may_alias.h.
|
protected |
Definition at line 61 of file local_may_alias.h.
|
inlineexplicit |
Definition at line 30 of file local_may_alias.h.
References build().
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.
Referenced by build().
|
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(), 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 aliases(), local_may_aliast::loc_infot::aliases, ASSIGN, assign_lhs(), cfg, goto_programt::instructiont::code, 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_cfgt::nodes, objects, code_typet::parameters(), 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(), goto_functiont::type, goto_programt::instructiont::type, 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(), 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, goto_functiont::body, unsigned_union_find::count(), unsigned_union_find::find(), forall_goto_program_instructions, from_expr(), symbol_exprt::get_identifier(), loc_infos, objects, goto_programt::output_instruction(), unsigned_union_find::size(), and to_symbol_expr().
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
local_cfgt local_may_aliast::cfg |
Definition at line 46 of file local_may_alias.h.
dirtyt local_may_aliast::dirty |
Definition at line 44 of file local_may_alias.h.
Referenced by assign_lhs(), and build().
|
protected |
localst local_may_aliast::locals |
Definition at line 45 of file local_may_alias.h.
Referenced by assign_lhs(), and build().
Definition at line 63 of file local_may_alias.h.
Referenced by assign_lhs(), build(), get(), get_rec(), and output().
|
protected |
Definition at line 92 of file local_may_alias.h.
Referenced by aliases(), assign_lhs(), build(), and get_rec().