function_cfg_infot Class Reference
#include <cfg_info.h>
Inheritance diagram for function_cfg_infot: Collaboration diagram for function_cfg_infot:Public Member Functions | |
| function_cfg_infot (const goto_functiont &_goto_function) | |
| bool | is_local (const irep_idt &ident) const override |
Returns true iff ident is a local or parameter of the goto_function. More... | |
| bool | is_not_local_or_dirty_local (const irep_idt &ident) const override |
Returns true iff the given ident is either not a goto_function local or is a 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... | |
Private Attributes | |
| const dirtyt | is_dirty |
| const localst | locals |
| std::unordered_set< irep_idt > | parameters |
Detailed Description
Definition at line 110 of file cfg_info.h.
Constructor & Destructor Documentation
◆ function_cfg_infot()
|
inlineexplicit |
Definition at line 113 of file cfg_info.h.
Member Function Documentation
◆ is_local()
|
inlineoverridevirtual |
Returns true iff ident is a local or parameter of the goto_function.
Implements cfg_infot.
Definition at line 122 of file cfg_info.h.
◆ is_not_local_or_dirty_local()
|
inlineoverridevirtual |
Returns true iff the given ident is either not a goto_function local or is a local that is dirty.
Implements cfg_infot.
Definition at line 130 of file cfg_info.h.
Member Data Documentation
◆ is_dirty
|
private |
Definition at line 136 of file cfg_info.h.
◆ locals
|
private |
Definition at line 137 of file cfg_info.h.
◆ parameters
|
private |
Definition at line 138 of file cfg_info.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/cfg_info.h
