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
#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_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::entryt &  entry, bool  write  )

static

Definition at line 108 of file race_check.cpp.

has_shared_entries()

static bool has_shared_entries ( const namespacet &  ns, const rw_set_baset &  rw_set  )

static

Definition at line 138 of file race_check.cpp.

is_shared()

static bool is_shared ( const namespacet &  ns, const symbol_exprt &  symbol_expr  )

static

Definition at line 121 of file race_check.cpp.

race_check() [1/3]

void race_check	(	value_setst &	value_sets,
		goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Definition at line 293 of file race_check.cpp.

race_check() [2/3]

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
	)

Definition at line 269 of file race_check.cpp.

race_check() [3/3]

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  )

static

Definition at line 160 of file race_check.cpp.