cprover
rw_set.h File Reference

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 
)

§ forall_rw_set_w_entries

#define forall_rw_set_w_entries (   it,
  rw_set 
)

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().