cprover
|
Public Member Functions | |
w_guardst (symbol_tablet &_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_tablet & | symbol_table |
Definition at line 31 of file race_check.cpp.
|
inlineexplicit |
Definition at line 34 of file race_check.cpp.
void w_guardst::add_initialization | ( | goto_programt & | goto_program | ) | const |
Definition at line 87 of file race_check.cpp.
References ASSIGN, goto_program, goto_programt::insert_before(), goto_programt::instructions, namespacet::lookup(), symbol_table, and w_guards.
Referenced by race_check().
|
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().
Definition at line 63 of file race_check.cpp.
References symbolt::base_name, id2string(), symbolt::is_static_lifetime, symbol_tablet::move(), symbolt::name, symbol_table, symbol_table_baset::symbols, symbolt::type, symbolt::value, and w_guards.
Referenced by get_guard_symbol_expr().
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().
|
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().
|
protected |
Definition at line 60 of file race_check.cpp.
Referenced by add_initialization(), and get_guard_symbol().
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().