Stores information about a goto function computed from its CFG. More...
#include <cfg_info.h>
Inheritance diagram for cfg_infot:Public Member Functions | |
| virtual bool | is_local (const irep_idt &ident) const =0 |
Returns true iff ident is locally declared. More... | |
| virtual bool | is_not_local_or_dirty_local (const irep_idt &ident) const =0 |
Returns true iff the given ident is either non-locally declared or is locally-declared but dirty. More... | |
| 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... | |
Detailed Description
Stores information about a goto function computed from its CFG.
The methods of this class provide information about identifiers to allow simplifying assigns clause checking assertions.
Definition at line 39 of file cfg_info.h.
Member Function Documentation
◆ is_local()
|
pure virtual |
Returns true iff ident is locally declared.
Implemented in goto_program_cfg_infot, loop_cfg_infot, and function_cfg_infot.
◆ is_local_composite_access()
|
inline |
Returns true iff expr is an access to a locally declared symbol and does not contain dereference or address_of operations.
Definition at line 51 of file cfg_info.h.
◆ is_not_local_or_dirty_local()
|
pure virtual |
Returns true iff the given ident is either non-locally declared or is locally-declared but dirty.
Implemented in goto_program_cfg_infot, loop_cfg_infot, and function_cfg_infot.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/cfg_info.h
