#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:

/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/event_graph.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/event_graph.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ data_typet

◆ iterator

◆ value_type

Constructor & Destructor Documentation

◆ critical_cyclet()

Member Function Documentation

◆ back() [1/2]

◆ back() [2/2]

◆ begin() [1/2]

◆ begin() [2/2]

◆ cbegin()

◆ cend()

◆ check_AC()

◆ check_BC()

◆ compute_unsafe_pairs()

◆ end() [1/2]

◆ end() [2/2]

◆ front() [1/2]

◆ front() [2/2]

◆ hide_internals()

◆ is_cycle()

◆ is_not_thin_air()

◆ is_not_uniproc() [1/2]

◆ is_not_uniproc() [2/2]

◆ is_not_weak_uniproc()

◆ is_unsafe()

◆ is_unsafe_asm()

◆ is_unsafe_fast()

◆ operator()()

◆ operator<()

◆ print()

◆ print_all()

◆ print_detail()

◆ print_dot()

◆ print_events()

◆ print_name() [1/3]

◆ print_name() [2/3]

◆ print_name() [3/3]

◆ print_output()

◆ print_unsafes()

◆ push_back()

◆ push_front()

◆ size()

Member Data Documentation

◆ data

◆ egraph

◆ has_user_defined_fence

◆ id

◆ unsafe_pairs