CBMC
goto_program_cfg_infot Class Reference

For a goto program. More...

#include <cfg_info.h>

+ Inheritance diagram for goto_program_cfg_infot:
+ Collaboration diagram for goto_program_cfg_infot:

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_idtlocals
 
std::set< irep_idtdirty
 

Detailed Description

For a goto program.

locals and dirty locals are inferred directly from the instruction sequence.

Definition at line 199 of file cfg_info.h.

Constructor & Destructor Documentation

◆ goto_program_cfg_infot()

goto_program_cfg_infot::goto_program_cfg_infot ( const goto_programt goto_program)
inlineexplicit

Definition at line 202 of file cfg_info.h.

Member Function Documentation

◆ is_local()

bool goto_program_cfg_infot::is_local ( const irep_idt ident) const
inlineoverridevirtual

Returns true iff ident is a loop local.

Implements cfg_infot.

Definition at line 217 of file cfg_info.h.

◆ is_not_local_or_dirty_local()

bool goto_program_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 224 of file cfg_info.h.

Member Data Documentation

◆ dirty

std::set<irep_idt> goto_program_cfg_infot::dirty
protected

Definition at line 234 of file cfg_info.h.

◆ locals

std::set<irep_idt> goto_program_cfg_infot::locals
protected

Definition at line 233 of file cfg_info.h.


The documentation for this class was generated from the following file: