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.
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.
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.

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()

function_cfg_infot::function_cfg_infot ( const goto_functiont &  _goto_function )

inlineexplicit

Definition at line 113 of file cfg_info.h.

Member Function Documentation

is_local()

bool function_cfg_infot::is_local ( const irep_idt &  ident ) const

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()

bool function_cfg_infot::is_not_local_or_dirty_local ( const irep_idt &  ident ) const

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

const dirtyt function_cfg_infot::is_dirty

private

Definition at line 136 of file cfg_info.h.

locals

const localst function_cfg_infot::locals

private

Definition at line 137 of file cfg_info.h.

parameters

std::unordered_set<irep_idt> function_cfg_infot::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