data_dpt Class Reference

#include <data_dp.h>

Collaboration diagram for data_dpt:

Public Member Functions
void	dp_analysis (const abstract_eventt &read, const abstract_eventt &write)
void	dp_analysis (const datat &read, bool local_read, const datat &write, bool local_write)
	insertion
bool	dp (const abstract_eventt &e1, const abstract_eventt &e2) const
	search in N^2
void	dp_merge ()
	merge in N^3
void	print (messaget &message)

Private Types
typedef std::set< datat >	data_typet

Private Attributes
data_typet	data
unsigned	class_nb

Detailed Description

Definition at line 51 of file data_dp.h.

Member Typedef Documentation

data_typet

typedef std::set<datat> data_dpt::data_typet

private

Definition at line 53 of file data_dp.h.

Member Function Documentation

dp()

bool data_dpt::dp	(	const abstract_eventt &	e1,
		const abstract_eventt &	e2
	)		const

search in N^2

Definition at line 76 of file data_dp.cpp.

dp_analysis() [1/2]

void data_dpt::dp_analysis	(	const abstract_eventt &	read,
		const abstract_eventt &	write
	)

Definition at line 66 of file data_dp.cpp.

dp_analysis() [2/2]

void data_dpt::dp_analysis	(	const datat &	read,
		bool	local_read,
		const datat &	write,
		bool	local_write
	)

insertion

Definition at line 25 of file data_dp.cpp.

dp_merge()

void data_dpt::dp_merge

(

)

merge in N^3

Definition at line 121 of file data_dp.cpp.

print()

void data_dpt::print

(

messaget &

message

)

Definition at line 164 of file data_dp.cpp.

Member Data Documentation

class_nb

unsigned data_dpt::class_nb

private

Definition at line 55 of file data_dp.h.

data

data_typet data_dpt::data

private

Definition at line 54 of file data_dp.h.

---

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

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