cprover
Loading...
Searching...
No Matches
loop_cfg_infot Class Reference

#include <cfg_info.h>

Inheritance diagram for loop_cfg_infot:
Collaboration diagram for loop_cfg_infot:

Public Member Functions

 loop_cfg_infot (goto_functiont &_goto_function, const loopt &loop)
bool is_local (const irep_idt &ident) const override
 Returns true iff ident is a loop local.
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.
void erase_locals (std::set< exprt > &exprs)
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
std::unordered_set< irep_idtlocals

Detailed Description

Definition at line 142 of file cfg_info.h.

Constructor & Destructor Documentation

◆ loop_cfg_infot()

loop_cfg_infot::loop_cfg_infot ( goto_functiont & _goto_function,
const loopt & loop )
inline

Definition at line 145 of file cfg_info.h.

Member Function Documentation

◆ erase_locals()

void loop_cfg_infot::erase_locals ( std::set< exprt > & exprs)
inline

Definition at line 171 of file cfg_info.h.

◆ is_local()

bool loop_cfg_infot::is_local ( const irep_idt & ident) const
inlineoverridevirtual

Returns true iff ident is a loop local.

Implements cfg_infot.

Definition at line 156 of file cfg_info.h.

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

Member Data Documentation

◆ is_dirty

const dirtyt loop_cfg_infot::is_dirty
private

Definition at line 193 of file cfg_info.h.

◆ locals

std::unordered_set<irep_idt> loop_cfg_infot::locals
private

Definition at line 194 of file cfg_info.h.


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