cprover
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.

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.