CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/race_check.cpp File Reference
Race Detection for Threaded Goto Programs. More...
Include dependency graph for race_check.cpp:
Go to the source code of this file.
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_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards, message_handlert &message_handler) |
| void | race_check (value_setst &value_sets, symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, message_handlert &message_handler) |
| void | race_check (value_setst &value_sets, goto_modelt &goto_model, message_handlert &message_handler) |
Detailed Description
Race Detection for Threaded Goto Programs.
Definition in file race_check.cpp.