cprover
|
#include <abstract_event.h>
Public Types | |
enum | operationt { operationt::Write, operationt::Read, operationt::Fence, operationt::Lwfence, operationt::ASMfence } |
![]() | |
typedef std::size_t | node_indext |
typedef empty_edget | edget |
typedef std::map< node_indext, edget > | edgest |
Public Member Functions | |
abstract_eventt () | |
abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local) | |
abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, bool _local, bool WRf, bool WWf, bool RRf, bool RWf, bool WWc, bool RWc, bool RRc) | |
void | operator() (const abstract_eventt &other) |
bool | operator== (const abstract_eventt &other) const |
bool | operator< (const abstract_eventt &other) const |
bool | is_fence () const |
bool | unsafe_pair (const abstract_eventt &next, memory_modelt model) const |
bool | unsafe_pair_lwfence (const abstract_eventt &next, memory_modelt model) const |
bool | unsafe_pair_asm (const abstract_eventt &next, memory_modelt model, unsigned char met) const |
std::string | get_operation () const |
bool | is_corresponding_fence (const abstract_eventt &first, const abstract_eventt &second) const |
bool | is_direct () const |
bool | is_cumul () const |
unsigned char | fence_value () const |
![]() | |
void | add_in (node_indext n) |
void | add_out (node_indext n) |
void | erase_in (node_indext n) |
void | erase_out (node_indext n) |
Public Attributes | |
operationt | operation |
unsigned | thread |
irep_idt | variable |
unsigned | id |
source_locationt | source_location |
bool | local |
bool | WRfence |
bool | WWfence |
bool | RRfence |
bool | RWfence |
bool | WWcumul |
bool | RWcumul |
bool | RRcumul |
![]() | |
edgest | in |
edgest | out |
Protected Member Functions | |
bool | unsafe_pair_lwfence_param (const abstract_eventt &next, memory_modelt model, bool lwsync_met) const |
Definition at line 22 of file abstract_event.h.
|
strong |
Enumerator | |
---|---|
Write | |
Read | |
Fence | |
Lwfence | |
ASMfence |
Definition at line 30 of file abstract_event.h.
|
inline |
Definition at line 48 of file abstract_event.h.
|
inline |
Definition at line 52 of file abstract_event.h.
|
inline |
Definition at line 60 of file abstract_event.h.
|
inline |
Definition at line 173 of file abstract_event.h.
References RRcumul, RRfence, RWcumul, RWfence, WRfence, WWcumul, and WWfence.
Referenced by event_grapht::critical_cyclet::print_name().
|
inline |
Definition at line 138 of file abstract_event.h.
References ASMfence, Fence, Lwfence, operation, Read, and Write.
Referenced by operator<<(), event_grapht::critical_cyclet::print_dot(), event_grapht::critical_cyclet::print_events(), event_grapht::critical_cyclet::print_name(), instrumentert::print_outputs_local(), and event_grapht::critical_cyclet::print_unsafes().
|
inline |
|
inline |
Definition at line 171 of file abstract_event.h.
|
inline |
|
inline |
Definition at line 111 of file abstract_event.h.
References ASMfence, Fence, Lwfence, and operation.
Referenced by event_grapht::critical_cyclet::hide_internals().
|
inline |
Definition at line 91 of file abstract_event.h.
References id, local, operation, source_location, thread, and variable.
|
inline |
Definition at line 106 of file abstract_event.h.
References id.
|
inline |
Definition at line 101 of file abstract_event.h.
References id.
|
inline |
Definition at line 121 of file abstract_event.h.
References unsafe_pair_lwfence_param().
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::critical_cyclet::is_unsafe(), and event_grapht::critical_cyclet::is_unsafe_asm().
bool abstract_eventt::unsafe_pair_asm | ( | const abstract_eventt & | next, |
memory_modelt | model, | ||
unsigned char | met | ||
) | const |
|
inline |
Definition at line 126 of file abstract_event.h.
References unsafe_pair_lwfence_param().
Referenced by event_grapht::critical_cyclet::is_unsafe().
|
protected |
unsigned abstract_eventt::id |
Definition at line 35 of file abstract_event.h.
Referenced by operator()(), operator<(), operator==(), event_grapht::critical_cyclet::print_dot(), and instrumentert::print_outputs_local().
bool abstract_eventt::local |
Definition at line 37 of file abstract_event.h.
Referenced by event_grapht::graph_explorert::backtrack(), data_dpt::dp(), data_dpt::dp_analysis(), operator()(), unsafe_pair_asm(), and unsafe_pair_lwfence_param().
operationt abstract_eventt::operation |
Definition at line 32 of file abstract_event.h.
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::critical_cyclet::check_AC(), event_grapht::critical_cyclet::check_BC(), event_grapht::graph_pensieve_explorert::collect_pairs(), cycles_visitort::com_constraint(), const_graph_visitort::const_graph_explore_AC(), const_graph_visitort::const_graph_explore_BC(), const_graph_visitort::CT(), const_graph_visitort::CT_not_powr(), get_operation(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), is_corresponding_fence(), is_fence(), event_grapht::critical_cyclet::is_not_thin_air(), event_grapht::critical_cyclet::is_not_uniproc(), event_grapht::critical_cyclet::is_not_weak_uniproc(), event_grapht::critical_cyclet::is_unsafe(), operator()(), event_grapht::critical_cyclet::print_dot(), event_grapht::critical_cyclet::print_name(), event_grapht::critical_cyclet::print_unsafes(), unsafe_pair_asm(), and unsafe_pair_lwfence_param().
bool abstract_eventt::RRcumul |
Definition at line 46 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_cumul().
bool abstract_eventt::RRfence |
Definition at line 42 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_direct().
bool abstract_eventt::RWcumul |
Definition at line 45 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_cumul().
bool abstract_eventt::RWfence |
Definition at line 43 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_direct().
source_locationt abstract_eventt::source_location |
Definition at line 36 of file abstract_event.h.
Referenced by event_grapht::graph_pensieve_explorert::collect_pairs(), event_grapht::copy_segment(), data_dpt::dp(), data_dpt::dp_analysis(), instrumentert::instrument_all_inserter(), instrumentert::instrument_minimum_interference_inserter(), instrumentert::instrument_my_events_inserter(), instrumentert::instrument_one_event_per_cycle_inserter(), instrumentert::is_cfg_spurious(), operator()(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_output(), instrumentert::print_outputs_local(), event_grapht::print_rec_graph(), fence_insertert::print_to_file(), fence_insertert::print_to_file_2(), fence_insertert::print_to_file_3(), and fence_insertert::print_to_file_4().
unsigned abstract_eventt::thread |
Definition at line 33 of file abstract_event.h.
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::critical_cyclet::check_AC(), event_grapht::critical_cyclet::check_BC(), cycles_visitort::com_constraint(), event_grapht::critical_cyclet::hide_internals(), event_grapht::critical_cyclet::is_not_thin_air(), event_grapht::critical_cyclet::is_unsafe(), event_grapht::critical_cyclet::is_unsafe_asm(), operator()(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_dot(), event_grapht::critical_cyclet::print_name(), event_grapht::critical_cyclet::print_output(), instrumentert::print_outputs_local(), event_grapht::critical_cyclet::print_unsafes(), unsafe_pair_asm(), unsafe_pair_lwfence_param(), and instrumentert::cfg_visitort::visit_cfg_assign().
irep_idt abstract_eventt::variable |
Definition at line 34 of file abstract_event.h.
Referenced by event_grapht::graph_explorert::backtrack(), event_grapht::graph_pensieve_explorert::collect_pairs(), data_dpt::dp(), data_dpt::dp_analysis(), instrumentert::instrument_all_inserter(), instrumentert::instrument_minimum_interference_inserter(), instrumentert::instrument_my_events_inserter(), instrumentert::instrument_one_event_per_cycle_inserter(), event_grapht::critical_cyclet::is_not_uniproc(), event_grapht::critical_cyclet::is_not_weak_uniproc(), event_grapht::critical_cyclet::is_unsafe(), operator()(), operator<<(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_dot(), event_grapht::critical_cyclet::print_events(), event_grapht::critical_cyclet::print_name(), event_grapht::critical_cyclet::print_output(), instrumentert::print_outputs_local(), fence_insertert::print_to_file_3(), fence_insertert::print_to_file_4(), event_grapht::critical_cyclet::print_unsafes(), unsafe_pair_asm(), and unsafe_pair_lwfence_param().
bool abstract_eventt::WRfence |
Definition at line 40 of file abstract_event.h.
Referenced by event_grapht::graph_explorert::backtrack(), fence_value(), is_corresponding_fence(), and is_direct().
bool abstract_eventt::WWcumul |
Definition at line 44 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_cumul().
bool abstract_eventt::WWfence |
Definition at line 41 of file abstract_event.h.
Referenced by fence_value(), is_corresponding_fence(), and is_direct().