w_guardst Class Reference

Collaboration diagram for w_guardst:

Public Member Functions
	w_guardst (symbol_table_baset &_symbol_table)
const symbolt &	get_guard_symbol (const irep_idt &object)
const exprt	get_guard_symbol_expr (const irep_idt &object)
const exprt	get_w_guard_expr (const rw_set_baset::entryt &entry)
const exprt	get_assertion (const rw_set_baset::entryt &entry)
void	add_initialization (goto_programt &goto_program) const

Public Attributes
std::list< irep_idt >	w_guards

Protected Attributes
symbol_table_baset &	symbol_table

Detailed Description

Definition at line 33 of file race_check.cpp.

Constructor & Destructor Documentation

w_guardst()

w_guardst::w_guardst ( symbol_table_baset &  _symbol_table )

inlineexplicit

Definition at line 36 of file race_check.cpp.

Member Function Documentation

add_initialization()

void w_guardst::add_initialization

(

goto_programt &

goto_program

)

const

Definition at line 89 of file race_check.cpp.

get_assertion()

const exprt w_guardst::get_assertion ( const rw_set_baset::entryt &  entry )

inline

Definition at line 55 of file race_check.cpp.

get_guard_symbol()

const symbolt & w_guardst::get_guard_symbol

(

const irep_idt &

object

)

Definition at line 66 of file race_check.cpp.

get_guard_symbol_expr()

const exprt w_guardst::get_guard_symbol_expr ( const irep_idt &  object )

inline

Definition at line 45 of file race_check.cpp.

get_w_guard_expr()

const exprt w_guardst::get_w_guard_expr ( const rw_set_baset::entryt &  entry )

inline

Definition at line 50 of file race_check.cpp.

Member Data Documentation

symbol_table

symbol_table_baset& w_guardst::symbol_table

protected

Definition at line 63 of file race_check.cpp.

w_guards

std::list<irep_idt> w_guardst::w_guards

Definition at line 41 of file race_check.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-instrument/race_check.cpp