cprover
Loading...
Searching...
No Matches
event_grapht::critical_cyclet Class Referencefinal

#include <event_graph.h>

Collaboration diagram for event_grapht::critical_cyclet:

Classes

struct  delayt

Public Types

typedef data_typet::iterator iterator
typedef data_typet::const_iterator const_iterator
typedef data_typet::value_type value_type

Public Member Functions

iterator begin ()
const_iterator begin () const
const_iterator cbegin () const
iterator end ()
const_iterator end () const
const_iterator cend () const
template<typename T>
void push_front (T &&t)
template<typename T>
void push_back (T &&t)
value_typefront ()
const value_typefront () const
value_typeback ()
const value_typeback () const
size_t size () const
 critical_cyclet (event_grapht &_egraph, unsigned _id)
void operator() (const critical_cyclet &cyc)
bool is_cycle ()
void hide_internals (critical_cyclet &reduced) const
bool is_unsafe (memory_modelt model, bool fast=false)
 checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set
bool is_unsafe_fast (memory_modelt model)
void compute_unsafe_pairs (memory_modelt model)
bool is_unsafe_asm (memory_modelt model, bool fast=false)
 same as is_unsafe, but with ASM fences
bool is_not_uniproc (memory_modelt model) const
bool is_not_thin_air () const
std::string print () const
std::string print_events () const
std::string print_name (memory_modelt model) const
std::string print_name (memory_modelt model, bool hide_internals) const
std::string print_unsafes () const
std::string print_output () const
std::string print_all (memory_modelt model, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id, bool hide_internals) const
void print_dot (std::ostream &str, unsigned colour, memory_modelt model) const
bool operator< (const critical_cyclet &other) const

Public Attributes

unsigned id
bool has_user_defined_fence
std::set< delaytunsafe_pairs

Private Types

typedef std::list< event_idtdata_typet

Private Member Functions

bool is_not_uniproc () const
bool is_not_weak_uniproc () const
std::string print_detail (const critical_cyclet &reduced, std::map< std::string, std::string > &map_id2var, std::map< std::string, std::string > &map_var2id) const
std::string print_name (const critical_cyclet &redyced, memory_modelt model) const
bool check_AC (data_typet::const_iterator s_it, const abstract_eventt &first, const abstract_eventt &second) const
bool check_BC (data_typet::const_iterator it, const abstract_eventt &first, const abstract_eventt &second) const

Private Attributes

data_typet data
event_graphtegraph

Detailed Description

Definition at line 38 of file event_graph.h.

Member Typedef Documentation

◆ const_iterator

typedef data_typet::const_iterator event_grapht::critical_cyclet::const_iterator

Definition at line 70 of file event_graph.h.

◆ data_typet

Definition at line 40 of file event_graph.h.

◆ iterator

typedef data_typet::iterator event_grapht::critical_cyclet::iterator

Definition at line 68 of file event_graph.h.

◆ value_type

typedef data_typet::value_type event_grapht::critical_cyclet::value_type

Definition at line 72 of file event_graph.h.

Constructor & Destructor Documentation

◆ critical_cyclet()

event_grapht::critical_cyclet::critical_cyclet ( event_grapht & _egraph,
unsigned _id )
inline

Definition at line 96 of file event_graph.h.

Member Function Documentation

◆ back() [1/2]

value_type & event_grapht::critical_cyclet::back ( )
inline

Definition at line 91 of file event_graph.h.

◆ back() [2/2]

const value_type & event_grapht::critical_cyclet::back ( ) const
inline

Definition at line 92 of file event_graph.h.

◆ begin() [1/2]

iterator event_grapht::critical_cyclet::begin ( )
inline

Definition at line 74 of file event_graph.h.

◆ begin() [2/2]

const_iterator event_grapht::critical_cyclet::begin ( ) const
inline

Definition at line 75 of file event_graph.h.

◆ cbegin()

const_iterator event_grapht::critical_cyclet::cbegin ( ) const
inline

Definition at line 76 of file event_graph.h.

◆ cend()

const_iterator event_grapht::critical_cyclet::cend ( ) const
inline

Definition at line 80 of file event_graph.h.

◆ check_AC()

bool event_grapht::critical_cyclet::check_AC ( data_typet::const_iterator s_it,
const abstract_eventt & first,
const abstract_eventt & second ) const
private

Definition at line 187 of file event_graph.cpp.

◆ check_BC()

bool event_grapht::critical_cyclet::check_BC ( data_typet::const_iterator it,
const abstract_eventt & first,
const abstract_eventt & second ) const
private

Definition at line 228 of file event_graph.cpp.

◆ compute_unsafe_pairs()

void event_grapht::critical_cyclet::compute_unsafe_pairs ( memory_modelt model)
inline

Definition at line 145 of file event_graph.h.

◆ end() [1/2]

iterator event_grapht::critical_cyclet::end ( )
inline

Definition at line 78 of file event_graph.h.

◆ end() [2/2]

const_iterator event_grapht::critical_cyclet::end ( ) const
inline

Definition at line 79 of file event_graph.h.

◆ front() [1/2]

value_type & event_grapht::critical_cyclet::front ( )
inline

Definition at line 88 of file event_graph.h.

◆ front() [2/2]

const value_type & event_grapht::critical_cyclet::front ( ) const
inline

Definition at line 89 of file event_graph.h.

◆ hide_internals()

void event_grapht::critical_cyclet::hide_internals ( critical_cyclet & reduced) const

Definition at line 1157 of file event_graph.cpp.

◆ is_cycle()

bool event_grapht::critical_cyclet::is_cycle ( )
inline

Definition at line 111 of file event_graph.h.

◆ is_not_thin_air()

bool event_grapht::critical_cyclet::is_not_thin_air ( ) const

Definition at line 971 of file event_graph.cpp.

◆ is_not_uniproc() [1/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( ) const
private

Definition at line 896 of file event_graph.cpp.

◆ is_not_uniproc() [2/2]

bool event_grapht::critical_cyclet::is_not_uniproc ( memory_modelt model) const
inline

Definition at line 152 of file event_graph.h.

◆ is_not_weak_uniproc()

bool event_grapht::critical_cyclet::is_not_weak_uniproc ( ) const
private

Definition at line 934 of file event_graph.cpp.

◆ is_unsafe()

bool event_grapht::critical_cyclet::is_unsafe ( memory_modelt model,
bool fast = false )

checks whether there is at least one pair which is unsafe (takes fences and dependencies into account), and adds the unsafe pairs in the set

Definition at line 281 of file event_graph.cpp.

◆ is_unsafe_asm()

bool event_grapht::critical_cyclet::is_unsafe_asm ( memory_modelt model,
bool fast = false )

same as is_unsafe, but with ASM fences

Definition at line 563 of file event_graph.cpp.

◆ is_unsafe_fast()

bool event_grapht::critical_cyclet::is_unsafe_fast ( memory_modelt model)
inline

Definition at line 140 of file event_graph.h.

◆ operator()()

void event_grapht::critical_cyclet::operator() ( const critical_cyclet & cyc)
inline

Definition at line 101 of file event_graph.h.

◆ operator<()

bool event_grapht::critical_cyclet::operator< ( const critical_cyclet & other) const
inline

Definition at line 232 of file event_graph.h.

◆ print()

std::string event_grapht::critical_cyclet::print ( ) const

Definition at line 1019 of file event_graph.cpp.

◆ print_all()

std::string event_grapht::critical_cyclet::print_all ( memory_modelt model,
std::map< std::string, std::string > & map_id2var,
std::map< std::string, std::string > & map_var2id,
bool hide_internals ) const

Definition at line 1127 of file event_graph.cpp.

◆ print_detail()

std::string event_grapht::critical_cyclet::print_detail ( const critical_cyclet & reduced,
std::map< std::string, std::string > & map_id2var,
std::map< std::string, std::string > & map_var2id ) const
private

Definition at line 1099 of file event_graph.cpp.

◆ print_dot()

void event_grapht::critical_cyclet::print_dot ( std::ostream & str,
unsigned colour,
memory_modelt model ) const

Definition at line 1548 of file event_graph.cpp.

◆ print_events()

std::string event_grapht::critical_cyclet::print_events ( ) const

Definition at line 1074 of file event_graph.cpp.

◆ print_name() [1/3]

std::string event_grapht::critical_cyclet::print_name ( const critical_cyclet & redyced,
memory_modelt model ) const
private

Definition at line 1233 of file event_graph.cpp.

◆ print_name() [2/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt model) const
inline

Definition at line 205 of file event_graph.h.

◆ print_name() [3/3]

std::string event_grapht::critical_cyclet::print_name ( memory_modelt model,
bool hide_internals ) const
inline

Definition at line 209 of file event_graph.h.

◆ print_output()

std::string event_grapht::critical_cyclet::print_output ( ) const

Definition at line 1086 of file event_graph.cpp.

◆ print_unsafes()

std::string event_grapht::critical_cyclet::print_unsafes ( ) const

Definition at line 1027 of file event_graph.cpp.

◆ push_back()

template<typename T>
void event_grapht::critical_cyclet::push_back ( T && t)
inline

Definition at line 86 of file event_graph.h.

◆ push_front()

template<typename T>
void event_grapht::critical_cyclet::push_front ( T && t)
inline

Definition at line 83 of file event_graph.h.

◆ size()

size_t event_grapht::critical_cyclet::size ( ) const
inline

Definition at line 94 of file event_graph.h.

Member Data Documentation

◆ data

data_typet event_grapht::critical_cyclet::data
private

Definition at line 41 of file event_graph.h.

◆ egraph

event_grapht& event_grapht::critical_cyclet::egraph
private

Definition at line 43 of file event_graph.h.

◆ has_user_defined_fence

bool event_grapht::critical_cyclet::has_user_defined_fence

Definition at line 65 of file event_graph.h.

◆ id

unsigned event_grapht::critical_cyclet::id

Definition at line 64 of file event_graph.h.

◆ unsafe_pairs

std::set<delayt> event_grapht::critical_cyclet::unsafe_pairs

Definition at line 198 of file event_graph.h.


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