Loading...

Searching...

No Matches

dirtyt Class Reference

Dirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading. More...

#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 search_other (const goto_programt::instructiont &instruction)

void find_dirty (const exprt &expr)

void find_dirty_address_of (const exprt &expr)

Protected Attributes

std::unordered_set< irep_idt > dirty

Private Member Functions

void die_if_uninitialized () const

Detailed Description

Dirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading.

Definition at line 27 of file dirty.h.

Member Typedef Documentation

◆ goto_functiont

typedef goto_functionst::goto_functiont dirtyt::goto_functiont

Definition at line 41 of file dirty.h.

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 47 of file dirty.h.

◆ dirtyt() [2/3]

dirtyt::dirtyt ( const goto_functiont & goto_function )

inlineexplicit

Definition at line 51 of file dirty.h.

◆ dirtyt() [3/3]

dirtyt::dirtyt ( const goto_functionst & goto_functions )

inlineexplicit

Definition at line 57 of file dirty.h.

Member Function Documentation

◆ add_function()

void dirtyt::add_function ( const goto_functiont & goto_function )

inline

Definition at line 84 of file dirty.h.

◆ build() [1/2]

void dirtyt::build ( const goto_functionst & goto_functions )

inline

Definition at line 90 of file dirty.h.

◆ build() [2/2]

void dirtyt::build ( const goto_functiont & goto_function )

protected

Definition at line 19 of file dirty.cpp.

◆ die_if_uninitialized()

void dirtyt::die_if_uninitialized ( ) const

inlineprivate

Definition at line 30 of file dirty.h.

◆ find_dirty()

void dirtyt::find_dirty ( const exprt & expr )

protected

Definition at line 60 of file dirty.cpp.

◆ find_dirty_address_of()

void dirtyt::find_dirty_address_of ( const exprt & expr )

protected

Definition at line 73 of file dirty.cpp.

◆ get_dirty_ids()

const std::unordered_set< irep_idt > & dirtyt::get_dirty_ids ( ) const

inline

Definition at line 78 of file dirty.h.

◆ operator()() [1/2]

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

inline

Definition at line 66 of file dirty.h.

◆ operator()() [2/2]

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

inline

Definition at line 72 of file dirty.h.

◆ output()

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

Definition at line 102 of file dirty.cpp.

◆ search_other()

void dirtyt::search_other ( const goto_programt::instructiont & instruction )

protected

Definition at line 34 of file dirty.cpp.

Member Data Documentation

◆ dirty

std::unordered_set<irep_idt> dirtyt::dirty

protected

Definition at line 103 of file dirty.h.

◆ initialized

bool dirtyt::initialized

Definition at line 40 of file dirty.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/dirty.h
/home/runner/work/cbmc/cbmc/src/analyses/dirty.cpp