#include <local_may_alias.h>
Collaboration diagram for local_may_aliast: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 |
Detailed Description
Definition at line 24 of file local_may_alias.h.
Member Typedef Documentation
◆ alias_sett
|
protected |
Definition at line 64 of file local_may_alias.h.
◆ goto_functiont
Definition at line 27 of file local_may_alias.h.
◆ loc_infost
|
protected |
Definition at line 75 of file local_may_alias.h.
◆ object_sett
|
protected |
Definition at line 84 of file local_may_alias.h.
◆ work_queuet
|
protected |
Definition at line 60 of file local_may_alias.h.
Constructor & Destructor Documentation
◆ local_may_aliast()
|
inlineexplicit |
Definition at line 29 of file local_may_alias.h.
Member Function Documentation
◆ aliases()
| 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.
◆ assign_lhs()
|
protected |
Definition at line 44 of file local_may_alias.cpp.
◆ build()
|
protected |
Definition at line 320 of file local_may_alias.cpp.
◆ get()
| 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.
◆ get_rec()
|
protected |
Definition at line 167 of file local_may_alias.cpp.
◆ output()
| 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.
Member Data Documentation
◆ cfg
| local_cfgt local_may_aliast::cfg |
Definition at line 45 of file local_may_alias.h.
◆ dirty
| dirtyt local_may_aliast::dirty |
Definition at line 43 of file local_may_alias.h.
◆ loc_infos
|
protected |
Definition at line 76 of file local_may_alias.h.
◆ locals
| localst local_may_aliast::locals |
Definition at line 44 of file local_may_alias.h.
◆ objects
|
mutableprotected |
Definition at line 62 of file local_may_alias.h.
◆ unknown_object
|
protected |
Definition at line 91 of file local_may_alias.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/local_may_alias.h
- /home/runner/work/cbmc/cbmc/src/analyses/local_may_alias.cpp
