cprover
dirtyt Class Reference

#include <dirty.h>

Collaboration diagram for dirtyt:
[legend]

Public Types

typedef std::unordered_set< irep_idt, irep_id_hashid_sett
 
typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 dirtyt (const goto_functiont &goto_function)
 
 dirtyt (const goto_functionst &goto_functions)
 
void output (std::ostream &out) const
 
bool operator() (const irep_idt &id) const
 
bool operator() (const symbol_exprt &expr) const
 
const id_settget_dirty_ids () const
 

Protected Member Functions

void build (const goto_functiont &goto_function)
 
void find_dirty (const exprt &expr)
 
void find_dirty_address_of (const exprt &expr)
 

Protected Attributes

id_sett dirty
 

Detailed Description

Definition at line 22 of file dirty.h.

Member Typedef Documentation

◆ goto_functiont

typedef goto_functionst::goto_functiont dirtyt::goto_functiont

Definition at line 26 of file dirty.h.

◆ id_sett

typedef std::unordered_set<irep_idt, irep_id_hash> dirtyt::id_sett

Definition at line 25 of file dirty.h.

Constructor & Destructor Documentation

◆ dirtyt() [1/2]

dirtyt::dirtyt ( const goto_functiont goto_function)
inlineexplicit

Definition at line 28 of file dirty.h.

References build().

◆ dirtyt() [2/2]

dirtyt::dirtyt ( const goto_functionst goto_functions)
inlineexplicit

Definition at line 33 of file dirty.h.

References build(), and forall_goto_functions.

Member Function Documentation

◆ build()

void dirtyt::build ( const goto_functiont goto_function)
protected

Definition at line 18 of file dirty.cpp.

References find_dirty(), and forall_goto_program_instructions.

Referenced by dirtyt().

◆ find_dirty()

void dirtyt::find_dirty ( const exprt expr)
protected

◆ find_dirty_address_of()

void dirtyt::find_dirty_address_of ( const exprt expr)
protected

◆ get_dirty_ids()

const id_sett& dirtyt::get_dirty_ids ( ) const
inline

Definition at line 51 of file dirty.h.

References dirty.

◆ operator()() [1/2]

bool dirtyt::operator() ( const irep_idt id) const
inline

Definition at line 41 of file dirty.h.

References dirty.

Referenced by operator()().

◆ operator()() [2/2]

bool dirtyt::operator() ( const symbol_exprt expr) const
inline

Definition at line 46 of file dirty.h.

References symbol_exprt::get_identifier(), and operator()().

◆ output()

void dirtyt::output ( std::ostream &  out) const

Definition at line 70 of file dirty.cpp.

References dirty.

Referenced by operator<<().

Member Data Documentation

◆ dirty

id_sett dirtyt::dirty
protected

Definition at line 60 of file dirty.h.

Referenced by find_dirty_address_of(), get_dirty_ids(), operator()(), and output().


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