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:

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