CBMC
Public Member Functions | Private Attributes | List of all members
incremental_dirtyt Class Reference

Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once. More...

#include <dirty.h>

+ Collaboration diagram for incremental_dirtyt:

Public Member Functions

void populate_dirty_for_function (const irep_idt &id, const goto_functionst::goto_functiont &function)
 Analyse the given function with dirtyt if it hasn't been seen before. More...
 
bool operator() (const irep_idt &id) const
 
bool operator() (const symbol_exprt &expr) const
 

Private Attributes

dirtyt dirty
 
std::unordered_set< irep_idt > dirty_processed_functions
 

Detailed Description

Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once.

Definition at line 117 of file dirty.h.

Member Function Documentation

◆ operator()() [1/2]

bool incremental_dirtyt::operator() ( const irep_idt &  id) const
inline

Definition at line 124 of file dirty.h.

◆ operator()() [2/2]

bool incremental_dirtyt::operator() ( const symbol_exprt &  expr) const
inline

Definition at line 129 of file dirty.h.

◆ populate_dirty_for_function()

void incremental_dirtyt::populate_dirty_for_function ( const irep_idt &  id,
const goto_functionst::goto_functiont &  function 
)

Analyse the given function with dirtyt if it hasn't been seen before.

Parameters
idfunction id to analyse
functionfunction to analyse

Definition at line 112 of file dirty.cpp.

Member Data Documentation

◆ dirty

dirtyt incremental_dirtyt::dirty
private

Definition at line 135 of file dirty.h.

◆ dirty_processed_functions

std::unordered_set<irep_idt> incremental_dirtyt::dirty_processed_functions
private

Definition at line 136 of file dirty.h.

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