CBMC
|
For a goto program. More...
#include <cfg_info.h>
Public Member Functions | |
goto_program_cfg_infot (const goto_programt &goto_program) | |
bool | is_local (const irep_idt &ident) const override |
Returns true iff ident is a loop local. More... | |
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. More... | |
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. More... | |
Protected Attributes | |
std::set< irep_idt > | locals |
std::set< irep_idt > | dirty |
For a goto program.
locals and dirty locals are inferred directly from the instruction sequence.
Definition at line 199 of file cfg_info.h.
|
inlineexplicit |
Definition at line 202 of file cfg_info.h.
|
inlineoverridevirtual |
Returns true iff ident
is a loop local.
Implements cfg_infot.
Definition at line 217 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 224 of file cfg_info.h.
|
protected |
Definition at line 234 of file cfg_info.h.
|
protected |
Definition at line 233 of file cfg_info.h.