#include <abstract_event.h>

Inheritance diagram for abstract_eventt:

Collaboration diagram for abstract_eventt:

Public Types
enum class	operationt { Write , Read , Fence , Lwfence , ASMfence }

Public Types inherited from graph_nodet< empty_edget >
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, irep_idt _function_id, bool _local)

	abstract_eventt (operationt _op, unsigned _th, irep_idt _var, unsigned _id, source_locationt _loc, irep_idt _function_id, 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

Public Member Functions inherited from graph_nodet< empty_edget >
void	add_in (node_indext n)

void	add_out (node_indext n)

void	erase_in (node_indext n)

void	erase_out (node_indext n)

std::string	pretty (const node_indext &idx) const

virtual	~graph_nodet ()

Public Attributes
operationt	operation

unsigned	thread

irep_idt	variable

unsigned	id

source_locationt	source_location

irep_idt	function_id

bool	local

bool	WRfence

bool	WWfence

bool	RRfence

bool	RWfence

bool	WWcumul

bool	RWcumul

bool	RRcumul

Public Attributes inherited from graph_nodet< empty_edget >
edgest	in

edgest	out

Protected Member Functions
bool	unsafe_pair_lwfence_param (const abstract_eventt &next, memory_modelt model, bool lwsync_met) const

Static Private Member Functions
static unsigned char	uc (bool truth_value)

Detailed Description

Definition at line 22 of file abstract_event.h.

Member Enumeration Documentation

◆ operationt

enum abstract_eventt::operationt

strong

Enumerator
Write
Read
Fence
Lwfence
ASMfence

Definition at line 30 of file abstract_event.h.

Constructor & Destructor Documentation

◆ abstract_eventt() [1/3]

abstract_eventt::abstract_eventt ( )

inline

Definition at line 49 of file abstract_event.h.

◆ abstract_eventt() [2/3]

abstract_eventt::abstract_eventt	(	operationt	_op,
		unsigned	_th,
		irep_idt	_var,
		unsigned	_id,
		source_locationt	_loc,
		irep_idt	_function_id,
		bool	_local
	)

inline

Definition at line 64 of file abstract_event.h.

◆ abstract_eventt() [3/3]

abstract_eventt::abstract_eventt	(	operationt	_op,
		unsigned	_th,
		irep_idt	_var,
		unsigned	_id,
		source_locationt	_loc,
		irep_idt	_function_id,
		bool	_local,
		bool	WRf,
		bool	WWf,
		bool	RRf,
		bool	RWf,
		bool	WWc,
		bool	RWc,
		bool	RRc
	)

inline

Definition at line 82 of file abstract_event.h.

Member Function Documentation

◆ fence_value()

unsigned char abstract_eventt::fence_value ( ) const

inline

Definition at line 198 of file abstract_event.h.

◆ get_operation()

std::string abstract_eventt::get_operation ( ) const

inline

Definition at line 163 of file abstract_event.h.

◆ is_corresponding_fence()

bool abstract_eventt::is_corresponding_fence	(	const abstract_eventt &	first,
		const abstract_eventt &	second
	)		const

inline

Definition at line 177 of file abstract_event.h.

◆ is_cumul()

bool abstract_eventt::is_cumul ( ) const

inline

Definition at line 196 of file abstract_event.h.

◆ is_direct()

bool abstract_eventt::is_direct ( ) const

inline

Definition at line 195 of file abstract_event.h.

◆ is_fence()

bool abstract_eventt::is_fence ( ) const

inline

Definition at line 136 of file abstract_event.h.

◆ operator()()

void abstract_eventt::operator() ( const abstract_eventt & other )

inline

Definition at line 115 of file abstract_event.h.

◆ operator<()

bool abstract_eventt::operator< ( const abstract_eventt & other ) const

inline

Definition at line 131 of file abstract_event.h.

◆ operator==()

bool abstract_eventt::operator== ( const abstract_eventt & other ) const

inline

Definition at line 126 of file abstract_event.h.

◆ uc()

static unsigned char abstract_eventt::uc ( bool truth_value )

inlinestaticprivate

Definition at line 206 of file abstract_event.h.

◆ unsafe_pair()

bool abstract_eventt::unsafe_pair	(	const abstract_eventt &	next,
		memory_modelt	model
	)		const

inline

Definition at line 146 of file abstract_event.h.

◆ unsafe_pair_asm()

bool abstract_eventt::unsafe_pair_asm	(	const abstract_eventt &	next,
		memory_modelt	model,
		unsigned char	met
	)		const

Definition at line 101 of file abstract_event.cpp.

◆ unsafe_pair_lwfence()

bool abstract_eventt::unsafe_pair_lwfence	(	const abstract_eventt &	next,
		memory_modelt	model
	)		const

inline

Definition at line 151 of file abstract_event.h.

◆ unsafe_pair_lwfence_param()

bool abstract_eventt::unsafe_pair_lwfence_param	(	const abstract_eventt &	next,
		memory_modelt	model,
		bool	lwsync_met
	)		const

protected

Definition at line 16 of file abstract_event.cpp.

Member Data Documentation

◆ function_id

irep_idt abstract_eventt::function_id

Definition at line 37 of file abstract_event.h.

◆ id

unsigned abstract_eventt::id

Definition at line 35 of file abstract_event.h.

◆ local

bool abstract_eventt::local

Definition at line 38 of file abstract_event.h.

◆ operation

operationt abstract_eventt::operation

Definition at line 32 of file abstract_event.h.

◆ RRcumul

bool abstract_eventt::RRcumul

Definition at line 47 of file abstract_event.h.

◆ RRfence

bool abstract_eventt::RRfence

Definition at line 43 of file abstract_event.h.

◆ RWcumul

bool abstract_eventt::RWcumul

Definition at line 46 of file abstract_event.h.

◆ RWfence

bool abstract_eventt::RWfence

Definition at line 44 of file abstract_event.h.

◆ source_location

source_locationt abstract_eventt::source_location

Definition at line 36 of file abstract_event.h.

◆ thread

unsigned abstract_eventt::thread

Definition at line 33 of file abstract_event.h.

◆ variable

irep_idt abstract_eventt::variable

Definition at line 34 of file abstract_event.h.

◆ WRfence

bool abstract_eventt::WRfence

Definition at line 41 of file abstract_event.h.

◆ WWcumul

bool abstract_eventt::WWcumul

Definition at line 45 of file abstract_event.h.

◆ WWfence

bool abstract_eventt::WWfence

Definition at line 42 of file abstract_event.h.

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

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

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Static Private Member Functions

Detailed Description

Member Enumeration Documentation

◆ operationt

Constructor & Destructor Documentation

◆ abstract_eventt() [1/3]

◆ abstract_eventt() [2/3]

◆ abstract_eventt() [3/3]

Member Function Documentation

◆ fence_value()

◆ get_operation()

◆ is_corresponding_fence()

◆ is_cumul()

◆ is_direct()

◆ is_fence()

◆ operator()()

◆ operator<()

◆ operator==()

◆ uc()

◆ unsafe_pair()

◆ unsafe_pair_asm()

◆ unsafe_pair_lwfence()

◆ unsafe_pair_lwfence_param()

Member Data Documentation

◆ function_id

◆ id

◆ local

◆ operation

◆ RRcumul

◆ RRfence

◆ RWcumul

◆ RWfence

◆ source_location

◆ thread

◆ variable

◆ WRfence

◆ WWcumul

◆ WWfence