Race Detection for Threaded Goto Programs. More...

#include <iosfwd>
#include <vector>
#include <set>
#include <util/guard.h>
#include <util/std_code.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <goto-programs/goto_functions.h>
#include <pointer-analysis/value_sets.h>

Include dependency graph for rw_set.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	rw_set_baset

struct	rw_set_baset::entryt

class	_rw_set_loct

class	rw_set_loct

class	rw_set_functiont

class	rw_set_with_trackt

Macros
#define	forall_rw_set_r_entries(it, rw_set)

#define	forall_rw_set_w_entries(it, rw_set)

Functions
std::ostream &	operator<< (std::ostream &out, const rw_set_baset &rw_set)

Detailed Description

Race Detection for Threaded Goto Programs.

Definition in file rw_set.h.

Macro Definition Documentation

◆ forall_rw_set_r_entries

#define forall_rw_set_r_entries	(	it,
		rw_set
	)

Value:

for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \

it!=(rw_set).r_entries.end(); it++)

Definition at line 104 of file rw_set.h.

Referenced by shared_bufferst::affected_by_delay(), fence_all_sharedt::compute(), fence_volatilet::compute(), instrumentert::cfg_visitort::contains_shared_array(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), potential_race_on_read(), race_check(), instrumentert::cfg_visitort::visit_cfg_assign(), and shared_bufferst::cfg_visitort::weak_memory().

◆ forall_rw_set_w_entries

#define forall_rw_set_w_entries	(	it,
		rw_set
	)

Value:

for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \

it!=(rw_set).w_entries.end(); it++)

Definition at line 108 of file rw_set.h.

Referenced by shared_bufferst::affected_by_delay(), fence_all_sharedt::compute(), fence_volatilet::compute(), instrumentert::cfg_visitort::contains_shared_array(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), potential_race_on_write(), race_check(), instrumentert::cfg_visitort::visit_cfg_assign(), and shared_bufferst::cfg_visitort::weak_memory().

Function Documentation

◆ operator<<()

std::ostream& operator<<	(	std::ostream &	out,
		const rw_set_baset &	rw_set
	)

inline

Definition at line 97 of file rw_set.h.

References rw_set_baset::output().

Classes