cprover
rw_set.h File Reference

Race Detection for Threaded Goto Programs. More...

#include <iosfwd>
#include <vector>
#include <set>
#include <util/std_expr.h>
#include <goto-programs/goto_model.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 110 of file rw_set.h.

◆ 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 114 of file rw_set.h.

Function Documentation

◆ operator<<()

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

Definition at line 103 of file rw_set.h.