CBMC
|
#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 | |
numberingt< exprt, irep_hash > | 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.
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.
bool local_may_aliast::aliases | ( | const goto_programt::const_targett | t, |
const exprt & | src1, | ||
const exprt & | src2 | ||
) | const |
Definition at line 140 of file local_may_alias.cpp.
|
protected |
Definition at line 44 of file local_may_alias.cpp.
|
protected |
Definition at line 320 of file local_may_alias.cpp.
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.
|
protected |
Definition at line 167 of file local_may_alias.cpp.
void local_may_aliast::output | ( | std::ostream & | out, |
const goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) | const |
Definition at line 463 of file local_may_alias.cpp.
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.
|
protected |
Definition at line 76 of file local_may_alias.h.
localst local_may_aliast::locals |
Definition at line 44 of file local_may_alias.h.
|
mutableprotected |
Definition at line 62 of file local_may_alias.h.
|
protected |
Definition at line 91 of file local_may_alias.h.