CBMC
|
#include <cfg_info.h>
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) |
![]() | |
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.