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"
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 | |
| 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) |
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 27 of file race_check.cpp.
◆ L_M_LAST_ARG
| #define L_M_LAST_ARG | ( | x | ) |
Definition at line 28 of file race_check.cpp.
Function Documentation
◆ comment()
| std::string comment | ( | const rw_set_baset::entryt & | entry, |
| bool | write | ||
| ) |
Definition at line 107 of file race_check.cpp.
◆ has_shared_entries()
| bool has_shared_entries | ( | const namespacet & | ns, |
| const rw_set_baset & | rw_set | ||
| ) |
Definition at line 140 of file race_check.cpp.
◆ is_shared()
| bool is_shared | ( | const namespacet & | ns, |
| const symbol_exprt & | symbol_expr | ||
| ) |
Definition at line 120 of file race_check.cpp.
◆ race_check() [1/3]
| 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.
◆ race_check() [2/3]
| void race_check | ( | value_setst & | value_sets, |
| symbol_tablet & | symbol_table, | ||
| goto_programt & | goto_program | ||
| ) |
Definition at line 266 of file race_check.cpp.
◆ race_check() [3/3]
| void race_check | ( | value_setst & | value_sets, |
| goto_modelt & | goto_model | ||
| ) |
Definition at line 287 of file race_check.cpp.
