#include "race_check.h"#include <util/prefix.h>#include <goto-programs/remove_skip.h>#include <linking/static_lifetime_init.h>#include <util/pointer_predicates.h>#include "rw_set.h"
Include dependency graph for race_check.cpp: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 | |
| static std::string | comment (const rw_set_baset::entryt &entry, bool write) |
| static bool | is_shared (const namespacet &ns, const symbol_exprt &symbol_expr) |
| static bool | has_shared_entries (const namespacet &ns, const rw_set_baset &rw_set) |
| static void | race_check (value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards) |
| void | race_check (value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program) |
| void | race_check (value_setst &value_sets, goto_modelt &goto_model) |
Detailed Description
Race Detection for Threaded Goto Programs
Definition in file race_check.cpp.
Macro Definition Documentation
◆ L_M_ARG
| #define L_M_ARG | ( | x | ) |
Definition at line 30 of file race_check.cpp.
◆ L_M_LAST_ARG
| #define L_M_LAST_ARG | ( | x | ) |
Definition at line 31 of file race_check.cpp.
Function Documentation
◆ comment()
|
static |
Definition at line 109 of file race_check.cpp.
◆ has_shared_entries()
|
static |
Definition at line 139 of file race_check.cpp.
◆ is_shared()
|
static |
Definition at line 122 of file race_check.cpp.
◆ race_check() [1/3]
| void race_check | ( | value_setst & | value_sets, |
| goto_modelt & | goto_model | ||
| ) |
Definition at line 292 of file race_check.cpp.
◆ race_check() [2/3]
| void race_check | ( | value_setst & | value_sets, |
| symbol_tablet & | symbol_table, | ||
| const irep_idt & | function_id, | ||
| goto_programt & | goto_program | ||
| ) |
Definition at line 270 of file race_check.cpp.
◆ race_check() [3/3]
|
static |
Definition at line 161 of file race_check.cpp.
