cprover
|
Race Detection for Threaded Goto Programs. More...
#include "race_check.h"
#include <goto-programs/remove_skip.h>
#include <linking/static_lifetime_init.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, goto_modelt &goto_model) |
Race Detection for Threaded Goto Programs.
Definition in file race_check.cpp.
#define L_M_ARG | ( | x | ) |
Definition at line 27 of file race_check.cpp.
Referenced by race_check().
#define L_M_LAST_ARG | ( | x | ) |
Definition at line 28 of file race_check.cpp.
Referenced by race_check().
std::string comment | ( | const rw_set_baset::entryt & | entry, |
bool | write | ||
) |
Definition at line 107 of file race_check.cpp.
References id2string(), and rw_set_baset::entryt::object.
Referenced by goto_checkt::add_guarded_claim(), as_string(), gcc_modet::asm_output(), json_irept::convert_from_json(), convert_properties_json(), cover_instrument_end_of_function(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), get_thread_safe_clinit_wrapper_body(), cover_instrumenter_baset::initialize_source_location(), cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_cover_instrumentert::instrument(), 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(), and show_properties().
bool has_shared_entries | ( | const namespacet & | ns, |
const rw_set_baset & | rw_set | ||
) |
Definition at line 140 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 120 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 161 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(), goto_program, has_shared_entries(), goto_programt::insert_before(), goto_programt::instructiont::is_assign(), is_shared(), L_M_LAST_ARG, goto_programt::instructiont::make_skip(), remove_skip(), source_locationt::set_comment(), exprt::source_location(), goto_programt::instructiont::source_location, and goto_programt::instructiont::swap().
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 266 of file race_check.cpp.
References w_guardst::add_initialization(), goto_program, L_M_ARG, race_check(), and goto_programt::update().
void race_check | ( | value_setst & | value_sets, |
goto_modelt & | goto_model | ||
) |
Definition at line 287 of file race_check.cpp.
References w_guardst::add_initialization(), goto_functionst::entry_point(), Forall_goto_functions, goto_functionst::function_map, goto_modelt::goto_functions, INITIALIZE_FUNCTION, L_M_ARG, main(), race_check(), goto_modelt::symbol_table, and goto_functionst::update().