CBMC
Loading...
Searching...
No Matches
Classes | Macros | Functions
race_check.cpp File Reference

Race Detection for Threaded Goto Programs. More...

#include "race_check.h"
#include <util/pointer_predicates.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

 
 

Functions

 
 
 
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.

Macro Definition Documentation

◆  L_M_ARG

#define L_M_ARG (   x )

Definition at line 29 of file race_check.cpp.

◆  L_M_LAST_ARG

#define L_M_LAST_ARG (   x )

Definition at line 30 of file race_check.cpp.

Function Documentation

◆  comment()

static std::string comment ( const rw_set_baset::entrytentry,
bool  write 
)
static

Definition at line 108 of file race_check.cpp.

◆  has_shared_entries()

static bool has_shared_entries ( const namespacetns,
const rw_set_basetrw_set 
)
static

Definition at line 138 of file race_check.cpp.

◆  is_shared()

static bool is_shared ( const namespacetns,
const symbol_exprtsymbol_expr 
)
static

Definition at line 121 of file race_check.cpp.

◆  race_check() [1/3]

void race_check ( value_setstvalue_sets,
goto_modeltgoto_model,
message_handlertmessage_handler 
)

Definition at line 293 of file race_check.cpp.

◆  race_check() [2/3]

void race_check ( value_setstvalue_sets,
symbol_table_basetsymbol_table,
const irep_idtfunction_id,
goto_programtgoto_program,
message_handlertmessage_handler 
)

Definition at line 269 of file race_check.cpp.

◆  race_check() [3/3]

static void race_check ( value_setstvalue_sets,
symbol_table_basetsymbol_table,
const irep_idtfunction_id,
goto_programtgoto_program,
w_guardstw_guards,
message_handlertmessage_handler 
)
static

Definition at line 160 of file race_check.cpp.

AltStyle によって変換されたページ (->オリジナル) /