cprover
data_dpt Class Referencefinal

#include <data_dp.h>

Collaboration diagram for data_dpt:
[legend]

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 More...
 
bool dp (const abstract_eventt &e1, const abstract_eventt &e2) const
 search in N^2 More...
 
void dp_merge ()
 merge in N^3 More...
 
void print (messaget &message)
 

Private Types

typedef std::set< datatdata_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()

◆ dp_analysis() [1/2]

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

◆ 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 22 of file data_dp.cpp.

References class_nb, datat::id, and datat::loc.

◆ dp_merge()

void data_dpt::dp_merge ( )

merge in N^3

Definition at line 118 of file data_dp.cpp.

References INVARIANT, and data::size.

◆ print()

void data_dpt::print ( messaget message)

Definition at line 161 of file data_dp.cpp.

References messaget::debug(), and messaget::eom().

Member Data Documentation

◆ class_nb

unsigned data_dpt::class_nb
private

Definition at line 55 of file data_dp.h.

Referenced by dp_analysis().

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