]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000. | |
3 | ** See ../LICENSE for license information. | |
4 | */ | |
5 | /* | |
6 | ** specialClauses.h | |
7 | */ | |
8 | ||
9 | # ifndef SPECIALCLAUSES_H | |
10 | # define SPECIALCLAUSES_H | |
11 | ||
12 | typedef enum | |
13 | { | |
14 | SP_USES, | |
15 | SP_DEFINES, | |
16 | SP_ALLOCATES, | |
17 | SP_RELEASES, | |
18 | SP_SETS, | |
19 | SP_ISNULL, | |
20 | SP_ISNOTNULL, | |
21 | SP_ISONLY, | |
22 | SP_ISSHARED, | |
23 | SP_ISDEPENDENT, | |
24 | SP_ISOWNED, | |
25 | SP_ISOBSERVER, | |
26 | SP_ISEXPOSED | |
27 | } specialClauseKind ; | |
28 | ||
29 | typedef enum | |
30 | { | |
31 | TK_BEFORE, | |
32 | TK_AFTER, | |
33 | TK_BOTH | |
34 | } stateConstraint; | |
35 | ||
36 | abst_typedef struct | |
37 | { | |
38 | stateConstraint state; | |
39 | specialClauseKind kind; | |
40 | sRefSet refs; | |
41 | } *specialClause ; | |
42 | ||
43 | typedef /*@only@*/ specialClause o_specialClause; | |
44 | ||
45 | extern /*@unused@*/ cstring specialClause_unparse (specialClause p_s) /*@*/ ; | |
46 | ||
47 | extern /*@null@*/ sRefMod | |
48 | specialClause_getEffectFunction (specialClause p_cl) /*@*/ ; | |
49 | ||
50 | extern /*@null@*/ sRefMod | |
51 | specialClause_getReturnEffectFunction (specialClause p_cl) /*@*/ ; | |
52 | ||
53 | extern /*@null@*/ sRefMod | |
54 | specialClause_getEntryFunction (specialClause p_cl) /*@*/ ; | |
55 | ||
56 | extern bool specialClause_isBefore (specialClause p_cl) /*@*/ ; | |
57 | extern bool specialClause_isAfter (specialClause p_cl) /*@*/ ; | |
58 | ||
59 | extern /*@observer@*/ sRefSet specialClause_getRefs (specialClause p_cl) /*@*/ ; | |
60 | # define specialClause_getRefs(cl) ((cl)->refs) | |
61 | ||
62 | abst_typedef /*@null@*/ struct | |
63 | { | |
64 | int nelements; | |
65 | int nspace; | |
66 | /*@relnull@*/ /*@reldef@*/ o_specialClause *elements; | |
67 | } *specialClauses ; | |
68 | ||
69 | /*@iter specialClauses_elements (sef specialClauses x, yield exposed specialClause el); @*/ | |
70 | # define specialClauses_elements(x, m_el) \ | |
71 | { if (!specialClauses_isUndefined(x)) \ | |
72 | { int m_ind; specialClause *m_elements = &((x)->elements[0]); \ | |
73 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
74 | { specialClause m_el = *(m_elements++); | |
75 | ||
76 | # define end_specialClauses_elements }}} | |
77 | ||
78 | /*@iter specialClauses_preElements (sef specialClauses x, yield exposed specialClause el); @*/ | |
79 | # define specialClauses_preElements(x, m_el) \ | |
80 | { if (!specialClauses_isUndefined(x)) \ | |
81 | { int m_ind; specialClause *m_elements = &((x)->elements[0]); \ | |
82 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
83 | { specialClause m_el = *(m_elements++); if (specialClause_isBefore (m_el)) { \ | |
84 | ||
85 | # define end_specialClauses_preElements }}}} | |
86 | ||
87 | /*@iter specialClauses_postElements (sef specialClauses x, yield exposed specialClause el); @*/ | |
88 | # define specialClauses_postElements(x, m_el) \ | |
89 | { if (!specialClauses_isUndefined(x)) \ | |
90 | { int m_ind; specialClause *m_elements = &((x)->elements[0]); \ | |
91 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
92 | { specialClause m_el = *(m_elements++); if (specialClause_isAfter (m_el)) { \ | |
93 | ||
94 | # define end_specialClauses_postElements }}}} | |
95 | ||
96 | extern void specialClauses_checkAll (uentry p_ue) | |
97 | /*@modifies p_ue, g_msgstream@*/ ; | |
98 | ||
99 | extern flagcode specialClause_preErrorCode (specialClause p_cl) /*@*/ ; | |
100 | extern /*@observer@*/ cstring | |
101 | specialClause_preErrorString (specialClause p_cl, sRef p_sr) /*@*/ ; | |
102 | ||
103 | extern flagcode specialClause_postErrorCode (specialClause p_cl) /*@*/ ; | |
104 | extern /*@observer@*/ cstring | |
105 | specialClause_postErrorString (specialClause p_cl, sRef p_sr) /*@*/ ; | |
106 | ||
107 | extern sRefTest specialClause_getPreTestFunction (specialClause p_cl) /*@*/ ; | |
108 | ||
109 | extern sRefTest specialClause_getPostTestFunction (specialClause p_cl) /*@*/ ; | |
110 | extern sRefShower specialClause_getPostTestShower (specialClause p_cl) /*@*/ ; | |
111 | ||
112 | extern specialClause | |
113 | specialClause_create (stateConstraint p_st, specialClauseKind p_k, /*@only@*/ sRefSet p_s) | |
114 | /*@*/ ; | |
115 | ||
116 | extern specialClause specialClause_createDefines (/*@only@*/ sRefSet p_s) /*@*/ ; | |
117 | extern specialClause specialClause_createUses (/*@only@*/ sRefSet p_s) /*@*/ ; | |
118 | extern specialClause specialClause_createAllocates (/*@only@*/ sRefSet p_s) /*@*/ ; | |
119 | extern specialClause specialClause_createReleases (/*@only@*/ sRefSet p_s) /*@*/ ; | |
120 | extern specialClause specialClause_createSets (/*@only@*/ sRefSet p_s) /*@*/ ; | |
121 | ||
122 | /*@constant null specialClauses specialClauses_undefined@*/ | |
123 | # define specialClauses_undefined ((specialClauses) 0) | |
124 | ||
125 | extern /*@falsenull@*/ bool specialClauses_isDefined (specialClauses p_s) /*@*/ ; | |
126 | # define specialClauses_isDefined(s) ((s) != specialClauses_undefined) | |
127 | ||
128 | extern /*@truenull@*/ bool specialClauses_isUndefined (specialClauses p_s) /*@*/ ; | |
129 | # define specialClauses_isUndefined(s) ((s) == specialClauses_undefined) | |
130 | ||
131 | extern /*@unused@*/ int | |
132 | specialClauses_size (/*@sef@*/ specialClauses p_s) /*@*/ ; | |
133 | # define specialClauses_size(s) (specialClauses_isDefined (s) ? (s)->nelements : 0) | |
134 | ||
135 | extern cstring specialClause_unparseKind (specialClause p_s) /*@*/ ; | |
136 | ||
137 | extern specialClauses | |
138 | specialClauses_add (/*@returned@*/ specialClauses p_s, | |
139 | /*@only@*/ specialClause p_el) | |
140 | /*@modifies p_s@*/ ; | |
141 | ||
142 | extern /*@unused@*/ cstring specialClauses_unparse (specialClauses p_s) /*@*/ ; | |
143 | extern void specialClauses_free (/*@only@*/ specialClauses p_s) ; | |
144 | ||
145 | extern /*@only@*/ specialClauses specialClauses_copy (specialClauses p_s) /*@*/ ; | |
146 | ||
147 | extern cstring specialClauses_dump (specialClauses p_s) /*@*/ ; | |
148 | extern specialClauses specialClauses_undump (char **p_s) /*@modifies *p_s@*/ ; | |
149 | ||
150 | /*@constant int specialClausesBASESIZE;@*/ | |
151 | # define specialClausesBASESIZE MIDBASESIZE | |
152 | ||
153 | extern void specialClauses_checkEqual (uentry p_old, uentry p_unew) | |
154 | /*@modifies g_msgstream@*/ ; | |
155 | ||
156 | # else | |
157 | # error "Multiple include" | |
158 | # endif | |
159 | ||
160 |