cprover
|
Race Detection for Threaded Goto Programs. More...
#include "race_check.h"
#include <util/std_expr.h>
#include <util/guard.h>
#include <util/symbol_table.h>
#include <util/prefix.h>
#include <util/cprover_prefix.h>
#include <goto-programs/goto_program.h>
#include <goto-programs/goto_functions.h>
#include <pointer-analysis/value_sets.h>
#include <goto-programs/remove_skip.h>
#include "rw_set.h"
Go to the source code of this file.
Classes | |
class | w_guardst |
Macros | |
#define | L_M_ARG(x) |
#define | L_M_LAST_ARG(x) |
Functions | |
std::string | comment (const rw_set_baset::entryt &entry, bool write) |
bool | is_shared (const namespacet &ns, const symbol_exprt &symbol_expr) |
bool | has_shared_entries (const namespacet &ns, const rw_set_baset &rw_set) |
void | race_check (value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards) |
void | race_check (value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program) |
void | race_check (value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions) |
Race Detection for Threaded Goto Programs.
Definition in file race_check.cpp.
#define L_M_ARG | ( | x | ) |
Definition at line 35 of file race_check.cpp.
Referenced by race_check().
#define L_M_LAST_ARG | ( | x | ) |
Definition at line 36 of file race_check.cpp.
Referenced by race_check().
std::string comment | ( | const rw_set_baset::entryt & | entry, |
bool | write | ||
) |
Definition at line 115 of file race_check.cpp.
References id2string(), and rw_set_baset::entryt::object.
Referenced by as_string(), gcc_modet::asm_output(), build_goto_trace(), convert(), xml_goto_program_convertt::convert(), json_irept::convert_from_json(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), instrument_cover_goals(), goto_trace_stept::output(), symex_target_equationt::SSA_stept::output(), goto_programt::output_instruction(), race_check(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), replace_location(), source_locationt::set_comment(), show_properties(), and show_properties_json().
bool has_shared_entries | ( | const namespacet & | ns, |
const rw_set_baset & | rw_set | ||
) |
Definition at line 148 of file race_check.cpp.
References is_shared(), rw_set_baset::r_entries, and rw_set_baset::w_entries.
Referenced by race_check().
bool is_shared | ( | const namespacet & | ns, |
const symbol_exprt & | symbol_expr | ||
) |
Definition at line 128 of file race_check.cpp.
References CPROVER_PREFIX, symbol_exprt::get_identifier(), has_prefix(), id2string(), symbolt::is_shared(), and namespacet::lookup().
Referenced by goto_symex_statet::assignment(), has_shared_entries(), and race_check().
void race_check | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
goto_programt & | goto_program, | ||
w_guardst & | w_guards | ||
) |
Definition at line 169 of file race_check.cpp.
References ASSIGN, comment(), Forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, w_guardst::get_assertion(), w_guardst::get_w_guard_expr(), has_shared_entries(), is_shared(), L_M_LAST_ARG, remove_skip(), and exprt::source_location().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and race_check().
void race_check | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
goto_programt & | goto_program | ||
) |
Definition at line 274 of file race_check.cpp.
References w_guardst::add_initialization(), L_M_ARG, race_check(), and w_guardst::w_guards.
void race_check | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions | ||
) |
Definition at line 295 of file race_check.cpp.
References w_guardst::add_initialization(), CPROVER_PREFIX, goto_functions_templatet< bodyT >::entry_point(), goto_functions_templatet< goto_programt >::entry_point(), Forall_goto_functions, goto_functions_templatet< bodyT >::function_map, L_M_ARG, main(), race_check(), goto_functions_templatet< bodyT >::update(), and w_guardst::w_guards.