cprover
event_grapht Class Reference

#include <event_graph.h>

Collaboration diagram for event_grapht:
[legend]

Classes

class  critical_cyclet
 
class  graph_conc_explorert
 
class  graph_explorert
 
class  graph_pensieve_explorert
 

Public Member Functions

 event_grapht (messaget &_message)
 
event_idt add_node ()
 
grapht< abstract_eventt >::nodet & operator[] (event_idt n)
 
bool has_po_edge (event_idt i, event_idt j) const
 
bool has_com_edge (event_idt i, event_idt j) const
 
std::size_t size () const
 
const wmm_grapht::edgestpo_in (event_idt n) const
 
const wmm_grapht::edgestpo_out (event_idt n) const
 
const wmm_grapht::edgestcom_in (event_idt n) const
 
const wmm_grapht::edgestcom_out (event_idt n) const
 
void add_po_edge (event_idt a, event_idt b)
 
void add_po_back_edge (event_idt a, event_idt b)
 
void add_com_edge (event_idt a, event_idt b)
 
void add_undirected_com_edge (event_idt a, event_idt b)
 
void remove_po_edge (event_idt a, event_idt b)
 
void remove_com_edge (event_idt a, event_idt b)
 
void remove_edge (event_idt a, event_idt b)
 
void explore_copy_segment (std::set< event_idt > &explored, event_idt begin, event_idt end) const
 copies the segment More...
 
event_idt copy_segment (event_idt begin, event_idt end)
 
bool is_local (event_idt a)
 
bool are_po_ordered (event_idt a, event_idt b)
 
void clear ()
 
void print_graph ()
 
void print_rec_graph (std::ofstream &file, event_idt node_id, std::set< event_idt > &visited)
 
void collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
 
void collect_cycles (std::set< critical_cyclet > &set_of_cycles, memory_modelt model)
 
void set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
 
void collect_pairs (namespacet &ns)
 
void collect_pairs_naive (namespacet &ns)
 

Public Attributes

bool filter_thin_air
 
bool filter_uniproc
 
messagetmessage
 
std::map< unsigned, data_dptmap_data_dp
 
std::list< event_idtpo_order
 
std::list< event_idtpoUrfe_order
 
std::set< std::pair< event_idt, event_idt > > loops
 
std::set< std::pair< const abstract_eventt &, const abstract_eventt & > > duplicated_bodies
 

Protected Attributes

wmm_grapht po_graph
 
wmm_grapht com_graph
 
unsigned max_var
 
unsigned max_po_trans
 
bool ignore_arrays
 

Detailed Description

Definition at line 34 of file event_graph.h.

Constructor & Destructor Documentation

§ event_grapht()

event_grapht::event_grapht ( messaget _message)
inlineexplicit

Definition at line 347 of file event_graph.h.

Member Function Documentation

§ add_com_edge()

void event_grapht::add_com_edge ( event_idt  a,
event_idt  b 
)
inline

§ add_node()

§ add_po_back_edge()

void event_grapht::add_po_back_edge ( event_idt  a,
event_idt  b 
)
inline

Definition at line 424 of file event_graph.h.

References grapht< N >::add_edge().

Referenced by instrumentert::cfg_visitort::visit_cfg_backedge().

§ add_po_edge()

§ add_undirected_com_edge()

void event_grapht::add_undirected_com_edge ( event_idt  a,
event_idt  b 
)
inline

Definition at line 442 of file event_graph.h.

References add_com_edge().

§ are_po_ordered()

bool event_grapht::are_po_ordered ( event_idt  a,
event_idt  b 
)
inline

§ clear()

void event_grapht::clear ( void  )
inline

§ collect_cycles() [1/2]

void event_grapht::collect_cycles ( std::set< critical_cyclet > &  set_of_cycles,
memory_modelt  model,
const std::set< event_idt > &  filter 
)
inline

§ collect_cycles() [2/2]

void event_grapht::collect_cycles ( std::set< critical_cyclet > &  set_of_cycles,
memory_modelt  model 
)
inline

Definition at line 521 of file event_graph.h.

References event_grapht::graph_explorert::collect_cycles().

§ collect_pairs()

void event_grapht::collect_pairs ( namespacet ns)
inline

§ collect_pairs_naive()

void event_grapht::collect_pairs_naive ( namespacet ns)
inline

§ com_in()

const wmm_grapht::edgest& event_grapht::com_in ( event_idt  n) const
inline

Definition at line 405 of file event_graph.h.

References grapht< N >::in().

§ com_out()

§ copy_segment()

§ explore_copy_segment()

void event_grapht::explore_copy_segment ( std::set< event_idt > &  explored,
event_idt  begin,
event_idt  end 
) const

copies the segment

Parameters
begintop of the subgraph
endbottom of the subgraph

Definition at line 72 of file event_graph.cpp.

References po_out().

Referenced by copy_segment(), and remove_edge().

§ has_com_edge()

bool event_grapht::has_com_edge ( event_idt  i,
event_idt  j 
) const
inline

Definition at line 385 of file event_graph.h.

References grapht< N >::has_edge().

Referenced by copy_segment().

§ has_po_edge()

bool event_grapht::has_po_edge ( event_idt  i,
event_idt  j 
) const
inline

§ is_local()

bool event_grapht::is_local ( event_idt  a)
inline

Definition at line 475 of file event_graph.h.

References operator[]().

§ operator[]()

grapht<abstract_eventt>::nodet& event_grapht::operator[] ( event_idt  n)
inline

Definition at line 375 of file event_graph.h.

Referenced by copy_segment(), is_local(), and print_rec_graph().

§ po_in()

§ po_out()

§ print_graph()

void event_grapht::print_graph ( )

Definition at line 56 of file event_graph.cpp.

References po_order, and print_rec_graph().

Referenced by clear(), and fence_weak_memory().

§ print_rec_graph()

void event_grapht::print_rec_graph ( std::ofstream &  file,
event_idt  node_id,
std::set< event_idt > &  visited 
)

Definition at line 28 of file event_graph.cpp.

References com_out(), operator[](), po_out(), and abstract_eventt::source_location.

Referenced by clear(), and print_graph().

§ remove_com_edge()

void event_grapht::remove_com_edge ( event_idt  a,
event_idt  b 
)
inline

Definition at line 454 of file event_graph.h.

References grapht< N >::remove_edge().

Referenced by event_grapht::graph_explorert::backtrack(), and remove_edge().

§ remove_edge()

void event_grapht::remove_edge ( event_idt  a,
event_idt  b 
)
inline

§ remove_po_edge()

void event_grapht::remove_po_edge ( event_idt  a,
event_idt  b 
)
inline

Definition at line 449 of file event_graph.h.

References grapht< N >::remove_edge().

Referenced by remove_edge().

§ set_parameters_collection()

void event_grapht::set_parameters_collection ( unsigned  _max_var = 0,
unsigned  _max_po_trans = 0,
bool  _ignore_arrays = false 
)
inline

Definition at line 528 of file event_graph.h.

Referenced by instrumentert::set_parameters_collection().

§ size()

Member Data Documentation

§ com_graph

wmm_grapht event_grapht::com_graph
protected

Definition at line 206 of file event_graph.h.

§ duplicated_bodies

std::set<std::pair<const abstract_eventt&, const abstract_eventt&> > event_grapht::duplicated_bodies

Definition at line 473 of file event_graph.h.

Referenced by copy_segment().

§ filter_thin_air

bool event_grapht::filter_thin_air

§ filter_uniproc

bool event_grapht::filter_uniproc

Definition at line 355 of file event_graph.h.

Referenced by event_grapht::graph_explorert::backtrack().

§ ignore_arrays

bool event_grapht::ignore_arrays
protected

Definition at line 211 of file event_graph.h.

Referenced by event_grapht::graph_explorert::backtrack().

§ loops

std::set<std::pair<event_idt, event_idt> > event_grapht::loops

Definition at line 365 of file event_graph.h.

§ map_data_dp

std::map<unsigned, data_dpt> event_grapht::map_data_dp

§ max_po_trans

unsigned event_grapht::max_po_trans
protected

Definition at line 210 of file event_graph.h.

§ max_var

unsigned event_grapht::max_var
protected

Definition at line 209 of file event_graph.h.

§ message

§ po_graph

wmm_grapht event_grapht::po_graph
protected

Definition at line 205 of file event_graph.h.

§ po_order

§ poUrfe_order

std::list<event_idt> event_grapht::poUrfe_order

Definition at line 363 of file event_graph.h.

Referenced by event_grapht::graph_explorert::collect_cycles().


The documentation for this class was generated from the following files: