cprover
w_guardst Class Reference
Collaboration diagram for w_guardst:
[legend]

Public Member Functions

 w_guardst (symbol_tablet &_symbol_table)
 
const symboltget_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_idtw_guards
 

Protected Attributes

symbol_tabletsymbol_table
 

Detailed Description

Definition at line 31 of file race_check.cpp.

Constructor & Destructor Documentation

◆ w_guardst()

w_guardst::w_guardst ( symbol_tablet _symbol_table)
inlineexplicit

Definition at line 34 of file race_check.cpp.

Member Function Documentation

◆ add_initialization()

void w_guardst::add_initialization ( goto_programt goto_program) const

◆ get_assertion()

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

Definition at line 52 of file race_check.cpp.

References get_guard_symbol_expr(), and rw_set_baset::entryt::object.

Referenced by race_check().

◆ get_guard_symbol()

◆ get_guard_symbol_expr()

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

Definition at line 42 of file race_check.cpp.

References get_guard_symbol(), and symbolt::symbol_expr().

Referenced by get_assertion(), and get_w_guard_expr().

◆ get_w_guard_expr()

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

Definition at line 47 of file race_check.cpp.

References get_guard_symbol_expr(), and rw_set_baset::entryt::object.

Referenced by race_check().

Member Data Documentation

◆ symbol_table

symbol_tablet& w_guardst::symbol_table
protected

Definition at line 60 of file race_check.cpp.

Referenced by add_initialization(), and get_guard_symbol().

◆ w_guards

std::list<irep_idt> w_guardst::w_guards

Definition at line 38 of file race_check.cpp.

Referenced by add_initialization(), and get_guard_symbol().


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