#include <cfg_info.h>
Definition at line 142 of file cfg_info.h.
◆ loop_cfg_infot()
◆ erase_locals()
void loop_cfg_infot::erase_locals |
( |
std::set< exprt > & |
exprs | ) |
|
|
inline |
◆ is_local()
bool loop_cfg_infot::is_local |
( |
const irep_idt & |
ident | ) |
const |
|
inlineoverridevirtual |
◆ is_not_local_or_dirty_local()
bool loop_cfg_infot::is_not_local_or_dirty_local |
( |
const irep_idt & |
ident | ) |
const |
|
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.
◆ is_dirty
const dirtyt loop_cfg_infot::is_dirty |
|
private |
◆ locals
std::unordered_set<irep_idt> loop_cfg_infot::locals |
|
private |
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/cfg_info.h