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 35 of file event_graph.h.
|
inlineexplicit |
Definition at line 383 of file event_graph.h.
Definition at line 474 of file event_graph.h.
References grapht< N >::add_edge(), com_graph, and poUrfe_order.
Referenced by add_undirected_com_edge(), copy_segment(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
inline |
Definition at line 406 of file event_graph.h.
References grapht< N >::add_node(), com_graph, INVARIANT, and po_graph.
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 463 of file event_graph.h.
References grapht< N >::add_edge(), loops, po_graph, po_order, and poUrfe_order.
Referenced by instrumentert::cfg_visitort::visit_cfg_backedge().
Definition at line 454 of file event_graph.h.
References grapht< N >::add_edge(), po_graph, po_order, and poUrfe_order.
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 481 of file event_graph.h.
References add_com_edge().
Definition at line 520 of file event_graph.h.
References loops, and po_order.
Referenced by event_grapht::critical_cyclet::is_cycle().
|
inline |
Definition at line 539 of file event_graph.h.
References grapht< N >::clear(), com_graph, map_data_dp, and po_graph.
|
inline |
Definition at line 552 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles(), max_po_trans, and max_var.
Referenced by instrumentert::collect_cycles(), and instrumentert::collect_cycles_by_SCCs().
|
inline |
Definition at line 560 of file event_graph.h.
References event_grapht::graph_explorert::collect_cycles(), max_po_trans, and max_var.
|
inline |
Definition at line 579 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs(), max_po_trans, and max_var.
Referenced by instrumenter_pensievet::collect_pairs().
|
inline |
Definition at line 585 of file event_graph.h.
References event_grapht::graph_pensieve_explorert::collect_pairs(), max_po_trans, max_var, and event_grapht::graph_pensieve_explorert::set_naive().
Referenced by instrumenter_pensievet::collect_pairs_naive().
|
inline |
Definition at line 444 of file event_graph.h.
References com_graph, and grapht< N >::in().
|
inline |
Definition at line 449 of file event_graph.h.
References com_graph, and grapht< N >::out().
Referenced by event_grapht::graph_pensieve_explorert::collect_pairs(), 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 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().
Definition at line 424 of file event_graph.h.
References com_graph, and grapht< N >::has_edge().
Referenced by copy_segment().
Definition at line 419 of file event_graph.h.
References grapht< N >::has_edge(), and po_graph.
Referenced by copy_segment().
|
inline |
Definition at line 514 of file event_graph.h.
References operator[]().
|
inline |
Definition at line 414 of file event_graph.h.
References po_graph.
Referenced by copy_segment(), is_local(), and print_rec_graph().
|
inline |
Definition at line 434 of file event_graph.h.
References grapht< N >::in(), and po_graph.
|
inline |
Definition at line 439 of file event_graph.h.
References grapht< N >::out(), and po_graph.
Referenced by explore_copy_segment(), instrumentert::is_cfg_spurious(), and print_rec_graph().
void event_grapht::print_graph | ( | ) |
Definition at line 56 of file event_graph.cpp.
References po_order, and 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 print_graph().
Definition at line 493 of file event_graph.h.
References com_graph, and grapht< N >::remove_edge().
Referenced by remove_edge().
Definition at line 498 of file event_graph.h.
References remove_com_edge(), and remove_po_edge().
Definition at line 488 of file event_graph.h.
References po_graph, and grapht< N >::remove_edge().
Referenced by remove_edge().
|
inline |
Definition at line 567 of file event_graph.h.
References ignore_arrays, max_po_trans, and max_var.
Referenced by instrumentert::set_parameters_collection().
|
inline |
Definition at line 429 of file event_graph.h.
References po_graph, and grapht< N >::size().
Referenced by copy_segment(), 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 242 of file event_graph.h.
Referenced by add_com_edge(), add_node(), clear(), com_in(), com_out(), has_com_edge(), and remove_com_edge().
std::set<std::pair<const abstract_eventt&, const abstract_eventt&> > event_grapht::duplicated_bodies |
Definition at line 512 of file event_graph.h.
Referenced by copy_segment().
bool event_grapht::filter_thin_air |
Definition at line 393 of file event_graph.h.
Referenced by event_grapht::graph_explorert::collect_cycles().
bool event_grapht::filter_uniproc |
Definition at line 394 of file event_graph.h.
|
protected |
Definition at line 247 of file event_graph.h.
Referenced by set_parameters_collection().
Definition at line 404 of file event_graph.h.
Referenced by add_po_back_edge(), and are_po_ordered().
std::map<unsigned, data_dpt> event_grapht::map_data_dp |
Definition at line 398 of file event_graph.h.
Referenced by clear(), and instrumentert::cfg_visitort::visit_cfg_function().
|
protected |
Definition at line 246 of file event_graph.h.
Referenced by event_grapht::graph_explorert::collect_cycles(), collect_cycles(), collect_pairs(), collect_pairs_naive(), and set_parameters_collection().
|
protected |
Definition at line 245 of file event_graph.h.
Referenced by event_grapht::graph_explorert::backtrack(), collect_cycles(), collect_pairs(), collect_pairs_naive(), and set_parameters_collection().
messaget& event_grapht::message |
Definition at line 395 of file event_graph.h.
Referenced by event_grapht::graph_pensieve_explorert::collect_pairs(), copy_segment(), event_grapht::graph_explorert::filter_thin_air(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
protected |
Definition at line 241 of file event_graph.h.
Referenced by add_node(), add_po_back_edge(), add_po_edge(), clear(), has_po_edge(), operator[](), po_in(), po_out(), remove_po_edge(), and size().
std::list<event_idt> event_grapht::po_order |
Definition at line 401 of file event_graph.h.
Referenced by add_po_back_edge(), add_po_edge(), are_po_ordered(), event_grapht::graph_pensieve_explorert::collect_pairs(), and print_graph().
std::list<event_idt> event_grapht::poUrfe_order |
Definition at line 402 of file event_graph.h.
Referenced by add_com_edge(), add_po_back_edge(), and add_po_edge().