]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** varKinds.h | |
3 | */ | |
4 | ||
5 | # ifndef VARKINDSH | |
6 | # define VARKINDSH | |
7 | ||
8 | /* | |
9 | ** states of storage | |
10 | */ | |
11 | ||
12 | typedef enum { | |
13 | SS_UNKNOWN, | |
14 | SS_UNUSEABLE, /* cannot use (unallocated pointer reference) */ | |
15 | SS_UNDEFINED, /* cannot use value (e.g., unbound variable) */ | |
16 | SS_MUNDEFINED,/* maybe undefined */ | |
17 | SS_ALLOCATED, /* allocated pointer */ | |
18 | SS_PDEFINED, /* partially defined: must check reachable values */ | |
19 | SS_DEFINED, /* completely defined: can use value and all reachable values */ | |
20 | SS_PARTIAL, /* defined, but can be bashed without error (partial structure returned) */ | |
21 | SS_DEAD, /* cannot use (after giving aways as only) | |
22 | * same meaning as UNUSEABLE, except that we | |
23 | * want to generate better error messages. */ | |
24 | SS_HOFFA, /* "probably dead" */ | |
25 | SS_FIXED, /* cannot modify */ | |
26 | SS_RELDEF, /* a structure field that may or may not be defined (up to | |
27 | * programmer to worry about it. */ | |
28 | ||
29 | SS_UNDEFGLOB, /* global only: undefined before call */ | |
30 | SS_KILLED, /* global only: undefined after call */ | |
31 | SS_UNDEFKILLED, /* global only: undefined before and after call */ | |
32 | ||
33 | SS_SPECIAL, /* marker for uses/defines/allocates/releases-specified */ | |
34 | ||
35 | SS_LAST | |
36 | } sstate; | |
37 | ||
6483a926 | 38 | extern bool sstate_isValid (/*@sef@*/ sstate) /*@*/ ; |
39 | # define sstate_isValid(s) ((s) >= SS_UNKNOWN && (s) <= SS_LAST) | |
40 | ||
885824d3 | 41 | typedef enum { |
42 | SCNONE, | |
43 | SCEXTERN, | |
44 | SCSTATIC | |
45 | } storageClassCode ; | |
46 | ||
28bf4b0b | 47 | typedef enum { |
885824d3 | 48 | NS_ERROR = -1, /* error (suppress messages) */ |
49 | NS_UNKNOWN = 0, /* no annotation */ | |
50 | NS_NOTNULL, /* definitely not null */ | |
51 | NS_MNOTNULL, /* marked with notnull */ | |
52 | ||
53 | /* perhaps null */ | |
54 | NS_RELNULL, /* relaxed null --- okay null for set, not null for checking */ | |
55 | NS_CONSTNULL, /* null constant (for abstract types) */ | |
56 | ||
57 | /* don't change the order! */ /* possibly null */ | |
58 | NS_POSNULL, /* possibly null */ | |
59 | NS_DEFNULL, /* definitely null */ | |
60 | NS_ABSNULL /* null from abstract type definition (concrete type unknown) */ | |
61 | } nstate; | |
62 | ||
63 | extern bool nstate_isKnown (nstate p_n) /*@*/ ; | |
64 | # define nstate_isKnown(n) ((n) != NS_UNKNOWN) | |
65 | ||
28bf4b0b | 66 | extern bool nstate_isValid (/*@sef@*/ nstate p_n) /*@*/ ; |
67 | # define nstate_isValid(n) ((n) >= NS_ERROR && (n) <= NS_ABSNULL) | |
68 | ||
885824d3 | 69 | /* |
70 | ** aliasing states | |
71 | */ | |
72 | ||
73 | /* | |
74 | ** HEY STUPID! Don't switch around the order! | |
75 | ** | |
76 | ** These numbers are fixed into the library format. If the order | |
77 | ** changes, remember to remake all libraries! | |
78 | */ | |
79 | ||
80 | typedef enum { | |
81 | AK_UNKNOWN = 0, /* AK_UNKNOWN must be first */ | |
82 | AK_ERROR, | |
83 | AK_ONLY, | |
84 | AK_IMPONLY, | |
85 | AK_KEEP, | |
86 | AK_KEPT, | |
28bf4b0b | 87 | AK_TEMP, /* 6 */ |
885824d3 | 88 | AK_IMPTEMP, |
89 | AK_SHARED, | |
90 | AK_UNIQUE, | |
28bf4b0b | 91 | AK_RETURNED, /* 10 */ |
885824d3 | 92 | AK_FRESH, /* local only storage (may be shared) */ |
93 | AK_STACK, /* allocated on local stack */ | |
94 | AK_REFCOUNTED, | |
95 | AK_REFS, | |
96 | AK_KILLREF, | |
97 | AK_NEWREF, | |
98 | AK_OWNED, | |
28bf4b0b | 99 | AK_DEPENDENT, /* 18 */ |
885824d3 | 100 | AK_IMPDEPENDENT, |
101 | AK_STATIC, | |
102 | AK_LOCAL /* AK_LOCAL must be last */ | |
103 | } alkind; | |
104 | ||
105 | typedef enum { | |
106 | XO_UNKNOWN, | |
107 | XO_NORMAL, | |
108 | XO_EXPOSED, | |
109 | XO_OBSERVER | |
110 | } exkind; | |
111 | ||
112 | extern bool sstate_isKnown (sstate p_s) /*@*/ ; | |
113 | # define sstate_isKnown(s) ((s) != SS_UNKNOWN) | |
114 | ||
115 | extern bool sstate_isUnknown (sstate p_s) /*@*/ ; | |
116 | # define sstate_isUnknown(s) ((s) == SS_UNKNOWN) | |
117 | ||
118 | extern bool exkind_isUnknown (exkind p_e) /*@*/ ; | |
119 | # define exkind_isUnknown(e) ((e) == XO_UNKNOWN) | |
120 | ||
121 | extern bool exkind_isKnown (/*@sef@*/ exkind p_e) /*@*/ ; | |
122 | # define exkind_isKnown(e) ((e) != XO_UNKNOWN && (e) != XO_NORMAL) | |
123 | ||
6483a926 | 124 | extern bool exkind_isValid (/*@sef@*/ exkind p_e) /*@*/ ; |
125 | # define exkind_isValid(e) ((e) >= XO_UNKNOWN && (e) <= XO_OBSERVER) | |
126 | ||
28bf4b0b | 127 | extern bool alkind_isValid (/*@sef@*/ alkind p_a) /*@*/ ; |
128 | # define alkind_isValid(a) ((a) >= AK_UNKNOWN && (a) <= AK_LOCAL) | |
129 | ||
885824d3 | 130 | extern bool alkind_isImplicit (/*@sef@*/ alkind p_a) /*@*/ ; |
131 | extern bool alkind_isDependent (/*@sef@*/ alkind p_a) /*@*/ ; | |
132 | extern bool alkind_isOnly (/*@sef@*/ alkind p_a) /*@*/ ; | |
133 | extern bool alkind_isTemp (/*@sef@*/ alkind p_a) /*@*/ ; | |
134 | ||
135 | # define alkind_isImplicit(a) (((a) == AK_IMPONLY || (a) == AK_IMPDEPENDENT \ | |
136 | || (a) == AK_IMPTEMP)) | |
137 | # define alkind_isDependent(a) (((a) == AK_DEPENDENT || (a) == AK_IMPDEPENDENT)) | |
138 | # define alkind_isOnly(a) ((a) == AK_ONLY || (a) == AK_IMPONLY) | |
139 | # define alkind_isTemp(a) (((a) == AK_TEMP || (a) == AK_IMPTEMP)) | |
140 | ||
141 | extern bool alkind_equal (alkind p_a1, alkind p_a2) /*@*/ ; | |
142 | ||
143 | extern bool alkind_isOwned (alkind p_a) /*@*/ ; | |
144 | extern bool alkind_isStack (alkind p_a) /*@*/ ; | |
145 | extern bool alkind_isStatic (alkind p_a) /*@*/ ; | |
146 | extern bool alkind_isKeep (alkind p_a) /*@*/ ; | |
147 | extern bool alkind_isKept (alkind p_a) /*@*/ ; | |
148 | extern bool alkind_isUnique (alkind p_a) /*@*/ ; | |
149 | extern bool alkind_isError (alkind p_a) /*@*/ ; | |
150 | extern bool alkind_isFresh (alkind p_a) /*@*/ ; | |
151 | extern bool alkind_isShared (alkind p_a) /*@*/ ; | |
152 | extern bool alkind_isLocal (alkind p_a) /*@*/ ; | |
153 | extern bool alkind_isKnown (alkind p_a) /*@*/ ; | |
154 | extern bool alkind_isUnknown (alkind p_a) /*@*/ ; | |
155 | extern bool alkind_isRefCounted (alkind p_a) /*@*/ ; | |
156 | extern /*@unused@*/ bool alkind_isRefs (alkind p_a) /*@*/ ; | |
157 | extern bool alkind_isNewRef (alkind p_a) /*@*/ ; | |
158 | extern bool alkind_isKillRef (alkind p_a) /*@*/ ; | |
159 | ||
2e127cb8 | 160 | extern alkind alkind_resolve (alkind p_a1, alkind p_a2) /*@*/ ; |
161 | ||
885824d3 | 162 | # define alkind_isOwned(a) ((a) == AK_OWNED) |
163 | # define alkind_isStack(a) ((a) == AK_STACK) | |
164 | # define alkind_isStatic(a) ((a) == AK_STATIC) | |
165 | # define alkind_isKeep(a) ((a) == AK_KEEP) | |
166 | # define alkind_isKept(a) ((a) == AK_KEPT) | |
167 | # define alkind_isUnique(a) ((a) == AK_UNIQUE) | |
168 | # define alkind_isError(a) ((a) == AK_ERROR) | |
169 | # define alkind_isFresh(a) ((a) == AK_FRESH) | |
170 | # define alkind_isShared(a) ((a) == AK_SHARED) | |
171 | # define alkind_isLocal(a) ((a) == AK_LOCAL) | |
172 | # define alkind_isKnown(a) ((a) != AK_UNKNOWN) | |
173 | # define alkind_isUnknown(a) ((a) == AK_UNKNOWN) | |
174 | # define alkind_isRefCounted(a) ((a) == AK_REFCOUNTED) | |
175 | # define alkind_isRefs(a) ((a) == AK_REFS) | |
176 | # define alkind_isNewRef(a) ((a) == AK_NEWREF) | |
177 | # define alkind_isKillRef(a) ((a) == AK_KILLREF) | |
178 | ||
179 | extern /*@observer@*/ cstring sstate_unparse (sstate p_s) /*@*/ ; | |
180 | ||
181 | extern alkind alkind_fromQual (qual p_q) /*@*/ ; | |
182 | extern alkind alkind_derive (alkind p_outer, alkind p_inner) /*@*/ ; | |
183 | extern /*@observer@*/ cstring alkind_unparse (alkind p_a) /*@*/ ; | |
184 | extern /*@observer@*/ cstring alkind_capName (alkind p_a) /*@*/ ; | |
185 | extern alkind alkind_fromInt (int p_n) /*@*/ ; | |
186 | extern nstate nstate_fromInt (int p_n) /*@*/ ; | |
187 | extern /*@observer@*/ cstring nstate_unparse (nstate p_n) /*@*/ ; | |
188 | extern int nstate_compare (nstate p_n1, nstate p_n2) /*@*/ ; | |
189 | extern bool nstate_possiblyNull (nstate p_n) /*@*/ ; | |
190 | extern bool nstate_perhapsNull (nstate p_n) /*@*/ ; | |
191 | extern sstate sstate_fromInt (int p_n) /*@*/ ; | |
192 | extern exkind exkind_fromInt (int p_n) /*@*/ ; | |
193 | extern exkind exkind_fromQual (qual p_q) /*@*/ ; | |
194 | extern /*@observer@*/ cstring exkind_unparse (exkind p_a) /*@*/ ; | |
195 | extern /*@observer@*/ cstring exkind_capName (exkind p_a) /*@*/ ; | |
196 | extern /*@observer@*/ cstring exkind_unparseError (exkind p_a) /*@*/ ; | |
197 | extern sstate sstate_fromQual (qual p_q) /*@*/ ; | |
198 | extern bool alkind_compatible (alkind p_a1, alkind p_a2) /*@*/ ; | |
199 | extern alkind alkind_fixImplicit (alkind p_a) /*@*/ ; | |
200 | ||
28bf4b0b | 201 | typedef enum |
885824d3 | 202 | { |
203 | XK_ERROR, | |
204 | XK_UNKNOWN, | |
205 | XK_NEVERESCAPE, | |
206 | XK_GOTO, | |
207 | XK_MAYGOTO, | |
208 | XK_MAYEXIT, | |
209 | XK_MUSTEXIT, | |
210 | XK_TRUEEXIT, | |
211 | XK_FALSEEXIT, | |
212 | XK_MUSTRETURN, | |
213 | XK_MAYRETURN, | |
214 | XK_MAYRETURNEXIT, | |
215 | XK_MUSTRETURNEXIT /* must return or exit */ | |
216 | } exitkind; | |
217 | ||
218 | /*@constant exitkind XK_LAST; @*/ | |
219 | # define XK_LAST XK_MUSTRETURNEXIT | |
220 | ||
221 | extern exitkind exitkind_fromQual (qual p_q) /*@*/ ; | |
222 | extern /*@unused@*/ bool exitkind_isMustExit (exitkind p_e) /*@*/ ; | |
223 | # define exitkind_isMustExit(e) ((e) == XK_MUSTEXIT) | |
224 | ||
225 | extern bool exitkind_equal (exitkind p_e1, exitkind p_e2) /*@*/ ; | |
226 | # define exitkind_equal(e1,e2) ((e1) == (e2)) | |
227 | ||
228 | extern bool exitkind_couldExit (exitkind p_e) /*@*/ ; | |
229 | extern bool exitkind_couldEscape (exitkind p_e) /*@*/ ; | |
230 | extern exitkind exitkind_fromInt (int p_x) /*@*/ ; | |
231 | extern /*@observer@*/ cstring exitkind_unparse (exitkind p_k) /*@*/ ; | |
232 | ||
233 | extern bool exitkind_isKnown (exitkind p_e) /*@*/ ; | |
234 | # define exitkind_isKnown(e) ((e) != XK_UNKNOWN) | |
235 | ||
236 | extern bool exitkind_isTrueExit (exitkind p_e) /*@*/ ; | |
237 | # define exitkind_isTrueExit(e) \ | |
238 | ((e) == XK_TRUEEXIT) | |
239 | ||
240 | extern bool exitkind_isConditionalExit (/*@sef@*/ exitkind p_e) /*@*/ ; | |
241 | # define exitkind_isConditionalExit(e) \ | |
242 | ((e) == XK_TRUEEXIT || (e) == XK_FALSEEXIT) | |
243 | ||
244 | extern bool exitkind_isError (/*@sef@*/ exitkind p_e) /*@*/ ; | |
245 | # define exitkind_isError(e) ((e) == XK_ERROR) | |
246 | ||
247 | extern bool exitkind_mustExit (/*@sef@*/ exitkind p_e) /*@*/ ; | |
248 | # define exitkind_mustExit(e) ((e) == XK_MUSTEXIT) | |
249 | ||
250 | extern bool exitkind_mustEscape (/*@sef@*/ exitkind p_e) /*@*/ ; | |
251 | # define exitkind_mustEscape(e) \ | |
252 | ((e) == XK_MUSTEXIT || (e) == XK_MUSTRETURN \ | |
253 | || (e) == XK_MUSTRETURNEXIT || (e) == XK_GOTO) | |
254 | ||
255 | extern exitkind exitkind_makeConditional (exitkind p_k) /*@*/ ; | |
256 | extern exitkind exitkind_combine (exitkind p_k1, exitkind p_k2) /*@*/ ; | |
257 | ||
258 | /* | |
259 | ** NOTE: combiners are in sRef | |
260 | */ | |
261 | ||
262 | # else | |
263 | # error "Multiple include" | |
264 | # endif |