cprover
|
#include <event_graph.h>
Classes | |
class | critical_cyclet |
class | graph_conc_explorert |
class | graph_explorert |
class | graph_pensieve_explorert |
Public Attributes | |
bool | filter_thin_air |
bool | filter_uniproc |
messaget & | message |
std::map< unsigned, data_dpt > | map_data_dp |
std::list< event_idt > | po_order |
std::list< event_idt > | poUrfe_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 |
Definition at line 34 of file event_graph.h.
|
inlineexplicit |
Definition at line 347 of file event_graph.h.
Definition at line 435 of file event_graph.h.
References grapht< N >::add_edge().
Referenced by add_undirected_com_edge(), copy_segment(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
inline |
Definition at line 367 of file event_graph.h.
References grapht< N >::add_node().
Referenced by copy_segment(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
Definition at line 424 of file event_graph.h.
References grapht< N >::add_edge().
Referenced by instrumentert::cfg_visitort::visit_cfg_backedge().
Definition at line 415 of file event_graph.h.
References grapht< N >::add_edge().
Referenced by copy_segment(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), and instrumentert::cfg_visitort::visit_cfg_lwfence().
Definition at line 442 of file event_graph.h.
References add_com_edge().
Definition at line 481 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::critical_cyclet::is_cycle(), and cycles_visitort::po_edges().
|
inline |
Definition at line 500 of file event_graph.h.
References grapht< N >::clear(), print_graph(), and print_rec_graph().
Referenced by event_grapht::critical_cyclet::operator()().
|
inline |
Definition at line 513 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles().
Referenced by instrumentert::collect_cycles(), and instrumentert::collect_cycles_by_SCCs().
|
inline |
Definition at line 521 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles().
|
inline |
Definition at line 540 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs().
Referenced by instrumenter_pensievet::collect_pairs(), and event_grapht::graph_pensieve_explorert::set_naive().
|
inline |
Definition at line 546 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs(), and event_grapht::graph_pensieve_explorert::set_naive().
Referenced by instrumenter_pensievet::collect_pairs_naive().
|
inline |
Definition at line 405 of file event_graph.h.
References grapht< N >::in().
|
inline |
Definition at line 410 of file event_graph.h.
References grapht< N >::out().
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::graph_pensieve_explorert::collect_pairs(), event_grapht::graph_pensieve_explorert::find_second_event(), and print_rec_graph().
Definition at line 90 of file event_graph.cpp.
References add_com_edge(), add_node(), add_po_edge(), duplicated_bodies, messaget::eom(), explore_copy_segment(), source_locationt::get_file(), source_locationt::get_function(), has_com_edge(), has_po_edge(), message, operator[](), size(), abstract_eventt::source_location, and messaget::status().
Referenced by remove_edge(), and instrumentert::cfg_visitort::visit_cfg_duplicate().
void event_grapht::explore_copy_segment | ( | std::set< event_idt > & | explored, |
event_idt | begin, | ||
event_idt | end | ||
) | const |
copies the segment
begin | top of the subgraph |
end | bottom of the subgraph |
Definition at line 72 of file event_graph.cpp.
References po_out().
Referenced by copy_segment(), and remove_edge().
Definition at line 385 of file event_graph.h.
References grapht< N >::has_edge().
Referenced by copy_segment().
Definition at line 380 of file event_graph.h.
References grapht< N >::has_edge().
Referenced by const_graph_visitort::const_graph_explore(), copy_segment(), and const_graph_visitort::graph_explore().
|
inline |
Definition at line 475 of file event_graph.h.
References operator[]().
|
inline |
Definition at line 375 of file event_graph.h.
Referenced by copy_segment(), is_local(), and print_rec_graph().
|
inline |
Definition at line 395 of file event_graph.h.
References grapht< N >::in().
Referenced by const_graph_visitort::const_graph_explore_AC(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), const_graph_visitort::graph_explore_AC(), and cycles_visitort::po_edges().
|
inline |
Definition at line 400 of file event_graph.h.
References grapht< N >::out().
Referenced by event_grapht::graph_explorert::backtrack(), const_graph_visitort::const_graph_explore(), const_graph_visitort::const_graph_explore_BC(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), explore_copy_segment(), event_grapht::graph_pensieve_explorert::find_second_event(), const_graph_visitort::graph_explore(), const_graph_visitort::graph_explore_BC(), instrumentert::is_cfg_spurious(), cycles_visitort::po_edges(), print_rec_graph(), and const_graph_visitort::PT().
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().
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().
Definition at line 454 of file event_graph.h.
References grapht< N >::remove_edge().
Referenced by event_grapht::graph_explorert::backtrack(), and remove_edge().
Definition at line 459 of file event_graph.h.
References copy_segment(), explore_copy_segment(), remove_com_edge(), and remove_po_edge().
Definition at line 449 of file event_graph.h.
References grapht< N >::remove_edge().
Referenced by remove_edge().
|
inline |
Definition at line 528 of file event_graph.h.
Referenced by instrumentert::set_parameters_collection().
|
inline |
Definition at line 390 of file event_graph.h.
References grapht< N >::size().
Referenced by event_grapht::graph_explorert::collect_cycles(), copy_segment(), event_grapht::critical_cyclet::is_cycle(), event_grapht::critical_cyclet::is_not_thin_air(), event_grapht::critical_cyclet::is_unsafe(), event_grapht::critical_cyclet::is_unsafe_asm(), and event_grapht::critical_cyclet::print_all().
|
protected |
Definition at line 206 of file event_graph.h.
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().
bool event_grapht::filter_thin_air |
Definition at line 354 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), and event_grapht::graph_explorert::collect_cycles().
bool event_grapht::filter_uniproc |
Definition at line 355 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack().
|
protected |
Definition at line 211 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack().
Definition at line 365 of file event_graph.h.
std::map<unsigned, data_dpt> event_grapht::map_data_dp |
Definition at line 359 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), and instrumentert::cfg_visitort::visit_cfg_function().
|
protected |
Definition at line 210 of file event_graph.h.
|
protected |
Definition at line 209 of file event_graph.h.
messaget& event_grapht::message |
Definition at line 356 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::graph_explorert::collect_cycles(), event_grapht::graph_pensieve_explorert::collect_pairs(), copy_segment(), event_grapht::graph_explorert::extract_cycle(), event_grapht::graph_explorert::filter_thin_air(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
protected |
Definition at line 205 of file event_graph.h.
std::list<event_idt> event_grapht::po_order |
Definition at line 362 of file event_graph.h.
Referenced by event_grapht::graph_explorert::collect_cycles(), event_grapht::graph_pensieve_explorert::collect_pairs(), and print_graph().
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().