|
CBMC
|
#include <cfg_info.h>
Inheritance diagram for loop_cfg_infot:
Collaboration diagram for loop_cfg_infot:Public Member Functions | |
| loop_cfg_infot (goto_functiont &_goto_function, const loopt &loop) | |
| bool | is_local (const irep_idt &ident) const override |
Returns true iff ident is a loop local. | |
| bool | is_not_local_or_dirty_local (const irep_idt &ident) const override |
Returns true iff the given ident is either not a loop local or is a loop local that is dirty. | |
| void | erase_locals (std::set< exprt > &exprs) |
Public Member Functions inherited from cfg_infot | |
| bool | is_local_composite_access (const exprt &expr) const |
Returns true iff expr is an access to a locally declared symbol and does not contain dereference or address_of operations. | |
Private Attributes | |
| const dirtyt | is_dirty |
| std::unordered_set< irep_idt > | locals |
Definition at line 142 of file cfg_info.h.
|
inline |
Definition at line 145 of file cfg_info.h.
Definition at line 171 of file cfg_info.h.
Returns true iff ident is a loop local.
Implements cfg_infot.
Definition at line 156 of file cfg_info.h.
|
inlineoverridevirtual |
Returns true iff the given ident is either not a loop local or is a loop local that is dirty.
Implements cfg_infot.
Definition at line 163 of file cfg_info.h.
Definition at line 193 of file cfg_info.h.
|
private |
Definition at line 194 of file cfg_info.h.