cprover
dirtyt Class Reference

#include <dirty.h>

Collaboration diagram for dirtyt:
[legend]

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 dirtyt ()
 
 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 std::unordered_set< irep_idt > & get_dirty_ids () const
 
void add_function (const goto_functiont &goto_function)
 
void build (const goto_functionst &goto_functions)
 

Public Attributes

bool initialized
 

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

std::unordered_set< irep_idtdirty
 

Private Member Functions

void die_if_uninitialized () const
 

Detailed Description

Definition at line 23 of file dirty.h.

Member Typedef Documentation

◆ goto_functiont

Constructor & Destructor Documentation

◆ dirtyt() [1/3]

dirtyt::dirtyt ( )
inline
Postcondition
dirtyt objects that are created through this constructor are not safe to use. If you copied a dirtyt (for example, by adding an object that owns a dirtyt to a container and then copying it back out), you will need to re-initialize the dirtyt by calling dirtyt::build().

Definition at line 43 of file dirty.h.

◆ dirtyt() [2/3]

dirtyt::dirtyt ( const goto_functiont goto_function)
inlineexplicit

Definition at line 47 of file dirty.h.

References build(), and initialized.

◆ dirtyt() [3/3]

dirtyt::dirtyt ( const goto_functionst goto_functions)
inlineexplicit

Definition at line 53 of file dirty.h.

References build().

Member Function Documentation

◆ add_function()

void dirtyt::add_function ( const goto_functiont goto_function)
inline

Definition at line 80 of file dirty.h.

References build(), and initialized.

Referenced by incremental_dirtyt::populate_dirty_for_function().

◆ build() [1/2]

void dirtyt::build ( const goto_functionst goto_functions)
inline

Definition at line 86 of file dirty.h.

References forall_goto_functions, initialized, and PRECONDITION.

Referenced by add_function(), and dirtyt().

◆ build() [2/2]

void dirtyt::build ( const goto_functiont goto_function)
protected

Definition at line 18 of file dirty.cpp.

References goto_functiont::body, find_dirty(), and forall_goto_program_instructions.

◆ die_if_uninitialized()

void dirtyt::die_if_uninitialized ( ) const
inlineprivate

Definition at line 26 of file dirty.h.

References initialized, and INVARIANT.

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

◆ 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 std::unordered_set<irep_idt>& dirtyt::get_dirty_ids ( ) const
inline

Definition at line 74 of file dirty.h.

References die_if_uninitialized(), and dirty.

◆ operator()() [1/2]

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

Definition at line 62 of file dirty.h.

References die_if_uninitialized(), and dirty.

Referenced by operator()().

◆ operator()() [2/2]

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

Definition at line 68 of file dirty.h.

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

◆ output()

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

Definition at line 70 of file dirty.cpp.

References die_if_uninitialized(), and dirty.

Referenced by operator<<().

Member Data Documentation

◆ dirty

std::unordered_set<irep_idt> dirtyt::dirty
protected

Definition at line 99 of file dirty.h.

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

◆ initialized

bool dirtyt::initialized

Definition at line 36 of file dirty.h.

Referenced by add_function(), build(), die_if_uninitialized(), and dirtyt().


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