CBMC
Classes | Public Types | Public Member Functions | Public Attributes | Private Types | Private Member Functions | Private Attributes | List of all members
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_type & front ()
 
const value_type & front () const
 
value_type & back ()
 
const value_type & back () 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 More...
 
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 More...
 
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< delayt > unsafe_pairs
 

Private Types

typedef std::list< event_idt > data_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_grapht & egraph
 

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

typedef std::list<event_idt> event_grapht::critical_cyclet::data_typet
private

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: