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 39 of file race_check.cpp.
|
inlineexplicit |
Definition at line 42 of file race_check.cpp.
void w_guardst::add_initialization | ( | goto_programt & | goto_program | ) | const |
Definition at line 95 of file race_check.cpp.
References ASSIGN, goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::instructions, namespacet::lookup(), symbol_table, and w_guards.
Referenced by race_check().
|
inline |
Definition at line 60 of file race_check.cpp.
References get_guard_symbol_expr(), and rw_set_baset::entryt::object.
Referenced by race_check().
Definition at line 71 of file race_check.cpp.
References symbolt::base_name, id2string(), symbolt::is_static_lifetime, symbol_tablet::move(), symbolt::name, symbol_table, symbol_tablet::symbols, symbolt::type, symbolt::value, and w_guards.
Referenced by get_guard_symbol_expr().
Definition at line 50 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 55 of file race_check.cpp.
References get_guard_symbol_expr(), and rw_set_baset::entryt::object.
Referenced by race_check().
|
protected |
Definition at line 68 of file race_check.cpp.
Referenced by add_initialization(), and get_guard_symbol().
std::list<irep_idt> w_guardst::w_guards |
Definition at line 46 of file race_check.cpp.
Referenced by add_initialization(), and get_guard_symbol().