CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
data_dp.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: data dependencies
4
5Author: Vincent Nimal
6
7Date: 2012
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
15#define CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
16
17#include <set>
18
20
21class abstract_eventt;
22class messaget;
23
24struct datat
25{
28 mutable unsigned eq_class;
29
34
39
40 bool operator==(const datat &d) const
41 {
42 return id==d.id && loc==d.loc;
43 }
44
45 bool operator<(const datat &d2) const
46 {
47 return id<d2.id || (id==d2.id && loc<d2.loc);
48 }
49};
50
51class data_dpt final
52{
53 typedef std::set<datat> data_typet;
55 unsigned class_nb;
56
57public:
58 /* add this dependency in the structure */
60 void dp_analysis(
61 const datat &read,
62 bool local_read,
63 const datat &write,
64 bool local_write);
65
66 /* are these two events with a data dependency ? */
67 bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const;
68
69 /* routine to maintain partitioning */
70 void dp_merge();
71
72 /* printing */
73 void print(messaget &message);
74};
75
76#endif // CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
data_typet data
Definition data_dp.h:54
void dp_merge()
merge in N^3
Definition data_dp.cpp:121
void print(messaget &message)
Definition data_dp.cpp:164
std::set< datat > data_typet
Definition data_dp.h:53
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
Definition data_dp.cpp:76
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Definition data_dp.cpp:66
unsigned class_nb
Definition data_dp.h:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
datat(irep_idt _id, source_locationt _loc, unsigned _eq_class)
Definition data_dp.h:30
unsigned eq_class
Definition data_dp.h:28
irep_idt id
Definition data_dp.h:26
bool operator==(const datat &d) const
Definition data_dp.h:40
datat(irep_idt _id, source_locationt _loc)
Definition data_dp.h:35
bool operator<(const datat &d2) const
Definition data_dp.h:45
source_locationt loc
Definition data_dp.h:27
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition unistd.c:195