]>
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 | ||
38 | typedef enum { | |
39 | SCNONE, | |
40 | SCEXTERN, | |
41 | SCSTATIC | |
42 | } storageClassCode ; | |
43 | ||
28bf4b0b | 44 | typedef enum { |
885824d3 | 45 | NS_ERROR = -1, /* error (suppress messages) */ |
46 | NS_UNKNOWN = 0, /* no annotation */ | |
47 | NS_NOTNULL, /* definitely not null */ | |
48 | NS_MNOTNULL, /* marked with notnull */ | |
49 | ||
50 | /* perhaps null */ | |
51 | NS_RELNULL, /* relaxed null --- okay null for set, not null for checking */ | |
52 | NS_CONSTNULL, /* null constant (for abstract types) */ | |
53 | ||
54 | /* don't change the order! */ /* possibly null */ | |
55 | NS_POSNULL, /* possibly null */ | |
56 | NS_DEFNULL, /* definitely null */ | |
57 | NS_ABSNULL /* null from abstract type definition (concrete type unknown) */ | |
58 | } nstate; | |
59 | ||
60 | extern bool nstate_isKnown (nstate p_n) /*@*/ ; | |
61 | # define nstate_isKnown(n) ((n) != NS_UNKNOWN) | |
62 | ||
28bf4b0b | 63 | extern bool nstate_isValid (/*@sef@*/ nstate p_n) /*@*/ ; |
64 | # define nstate_isValid(n) ((n) >= NS_ERROR && (n) <= NS_ABSNULL) | |
65 | ||
885824d3 | 66 | /* |
67 | ** aliasing states | |
68 | */ | |
69 | ||
70 | /* | |
71 | ** HEY STUPID! Don't switch around the order! | |
72 | ** | |
73 | ** These numbers are fixed into the library format. If the order | |
74 | ** changes, remember to remake all libraries! | |
75 | */ | |
76 | ||
77 | typedef enum { | |
78 | AK_UNKNOWN = 0, /* AK_UNKNOWN must be first */ | |
79 | AK_ERROR, | |
80 | AK_ONLY, | |
81 | AK_IMPONLY, | |
82 | AK_KEEP, | |
83 | AK_KEPT, | |
28bf4b0b | 84 | AK_TEMP, /* 6 */ |
885824d3 | 85 | AK_IMPTEMP, |
86 | AK_SHARED, | |
87 | AK_UNIQUE, | |
28bf4b0b | 88 | AK_RETURNED, /* 10 */ |
885824d3 | 89 | AK_FRESH, /* local only storage (may be shared) */ |
90 | AK_STACK, /* allocated on local stack */ | |
91 | AK_REFCOUNTED, | |
92 | AK_REFS, | |
93 | AK_KILLREF, | |
94 | AK_NEWREF, | |
95 | AK_OWNED, | |
28bf4b0b | 96 | AK_DEPENDENT, /* 18 */ |
885824d3 | 97 | AK_IMPDEPENDENT, |
98 | AK_STATIC, | |
99 | AK_LOCAL /* AK_LOCAL must be last */ | |
100 | } alkind; | |
101 | ||
102 | typedef enum { | |
103 | XO_UNKNOWN, | |
104 | XO_NORMAL, | |
105 | XO_EXPOSED, | |
106 | XO_OBSERVER | |
107 | } exkind; | |
108 | ||
109 | extern bool sstate_isKnown (sstate p_s) /*@*/ ; | |
110 | # define sstate_isKnown(s) ((s) != SS_UNKNOWN) | |
111 | ||
112 | extern bool sstate_isUnknown (sstate p_s) /*@*/ ; | |
113 | # define sstate_isUnknown(s) ((s) == SS_UNKNOWN) | |
114 | ||
115 | extern bool exkind_isUnknown (exkind p_e) /*@*/ ; | |
116 | # define exkind_isUnknown(e) ((e) == XO_UNKNOWN) | |
117 | ||
118 | extern bool exkind_isKnown (/*@sef@*/ exkind p_e) /*@*/ ; | |
119 | # define exkind_isKnown(e) ((e) != XO_UNKNOWN && (e) != XO_NORMAL) | |
120 | ||
28bf4b0b | 121 | extern bool alkind_isValid (/*@sef@*/ alkind p_a) /*@*/ ; |
122 | # define alkind_isValid(a) ((a) >= AK_UNKNOWN && (a) <= AK_LOCAL) | |
123 | ||
885824d3 | 124 | extern bool alkind_isImplicit (/*@sef@*/ alkind p_a) /*@*/ ; |
125 | extern bool alkind_isDependent (/*@sef@*/ alkind p_a) /*@*/ ; | |
126 | extern bool alkind_isOnly (/*@sef@*/ alkind p_a) /*@*/ ; | |
127 | extern bool alkind_isTemp (/*@sef@*/ alkind p_a) /*@*/ ; | |
128 | ||
129 | # define alkind_isImplicit(a) (((a) == AK_IMPONLY || (a) == AK_IMPDEPENDENT \ | |
130 | || (a) == AK_IMPTEMP)) | |
131 | # define alkind_isDependent(a) (((a) == AK_DEPENDENT || (a) == AK_IMPDEPENDENT)) | |
132 | # define alkind_isOnly(a) ((a) == AK_ONLY || (a) == AK_IMPONLY) | |
133 | # define alkind_isTemp(a) (((a) == AK_TEMP || (a) == AK_IMPTEMP)) | |
134 | ||
135 | extern bool alkind_equal (alkind p_a1, alkind p_a2) /*@*/ ; | |
136 | ||
137 | extern bool alkind_isOwned (alkind p_a) /*@*/ ; | |
138 | extern bool alkind_isStack (alkind p_a) /*@*/ ; | |
139 | extern bool alkind_isStatic (alkind p_a) /*@*/ ; | |
140 | extern bool alkind_isKeep (alkind p_a) /*@*/ ; | |
141 | extern bool alkind_isKept (alkind p_a) /*@*/ ; | |
142 | extern bool alkind_isUnique (alkind p_a) /*@*/ ; | |
143 | extern bool alkind_isError (alkind p_a) /*@*/ ; | |
144 | extern bool alkind_isFresh (alkind p_a) /*@*/ ; | |
145 | extern bool alkind_isShared (alkind p_a) /*@*/ ; | |
146 | extern bool alkind_isLocal (alkind p_a) /*@*/ ; | |
147 | extern bool alkind_isKnown (alkind p_a) /*@*/ ; | |
148 | extern bool alkind_isUnknown (alkind p_a) /*@*/ ; | |
149 | extern bool alkind_isRefCounted (alkind p_a) /*@*/ ; | |
150 | extern /*@unused@*/ bool alkind_isRefs (alkind p_a) /*@*/ ; | |
151 | extern bool alkind_isNewRef (alkind p_a) /*@*/ ; | |
152 | extern bool alkind_isKillRef (alkind p_a) /*@*/ ; | |
153 | ||
154 | # define alkind_isOwned(a) ((a) == AK_OWNED) | |
155 | # define alkind_isStack(a) ((a) == AK_STACK) | |
156 | # define alkind_isStatic(a) ((a) == AK_STATIC) | |
157 | # define alkind_isKeep(a) ((a) == AK_KEEP) | |
158 | # define alkind_isKept(a) ((a) == AK_KEPT) | |
159 | # define alkind_isUnique(a) ((a) == AK_UNIQUE) | |
160 | # define alkind_isError(a) ((a) == AK_ERROR) | |
161 | # define alkind_isFresh(a) ((a) == AK_FRESH) | |
162 | # define alkind_isShared(a) ((a) == AK_SHARED) | |
163 | # define alkind_isLocal(a) ((a) == AK_LOCAL) | |
164 | # define alkind_isKnown(a) ((a) != AK_UNKNOWN) | |
165 | # define alkind_isUnknown(a) ((a) == AK_UNKNOWN) | |
166 | # define alkind_isRefCounted(a) ((a) == AK_REFCOUNTED) | |
167 | # define alkind_isRefs(a) ((a) == AK_REFS) | |
168 | # define alkind_isNewRef(a) ((a) == AK_NEWREF) | |
169 | # define alkind_isKillRef(a) ((a) == AK_KILLREF) | |
170 | ||
171 | extern /*@observer@*/ cstring sstate_unparse (sstate p_s) /*@*/ ; | |
172 | ||
173 | extern alkind alkind_fromQual (qual p_q) /*@*/ ; | |
174 | extern alkind alkind_derive (alkind p_outer, alkind p_inner) /*@*/ ; | |
175 | extern /*@observer@*/ cstring alkind_unparse (alkind p_a) /*@*/ ; | |
176 | extern /*@observer@*/ cstring alkind_capName (alkind p_a) /*@*/ ; | |
177 | extern alkind alkind_fromInt (int p_n) /*@*/ ; | |
178 | extern nstate nstate_fromInt (int p_n) /*@*/ ; | |
179 | extern /*@observer@*/ cstring nstate_unparse (nstate p_n) /*@*/ ; | |
180 | extern int nstate_compare (nstate p_n1, nstate p_n2) /*@*/ ; | |
181 | extern bool nstate_possiblyNull (nstate p_n) /*@*/ ; | |
182 | extern bool nstate_perhapsNull (nstate p_n) /*@*/ ; | |
183 | extern sstate sstate_fromInt (int p_n) /*@*/ ; | |
184 | extern exkind exkind_fromInt (int p_n) /*@*/ ; | |
185 | extern exkind exkind_fromQual (qual p_q) /*@*/ ; | |
186 | extern /*@observer@*/ cstring exkind_unparse (exkind p_a) /*@*/ ; | |
187 | extern /*@observer@*/ cstring exkind_capName (exkind p_a) /*@*/ ; | |
188 | extern /*@observer@*/ cstring exkind_unparseError (exkind p_a) /*@*/ ; | |
189 | extern sstate sstate_fromQual (qual p_q) /*@*/ ; | |
190 | extern bool alkind_compatible (alkind p_a1, alkind p_a2) /*@*/ ; | |
191 | extern alkind alkind_fixImplicit (alkind p_a) /*@*/ ; | |
192 | ||
28bf4b0b | 193 | typedef enum |
885824d3 | 194 | { |
195 | XK_ERROR, | |
196 | XK_UNKNOWN, | |
197 | XK_NEVERESCAPE, | |
198 | XK_GOTO, | |
199 | XK_MAYGOTO, | |
200 | XK_MAYEXIT, | |
201 | XK_MUSTEXIT, | |
202 | XK_TRUEEXIT, | |
203 | XK_FALSEEXIT, | |
204 | XK_MUSTRETURN, | |
205 | XK_MAYRETURN, | |
206 | XK_MAYRETURNEXIT, | |
207 | XK_MUSTRETURNEXIT /* must return or exit */ | |
208 | } exitkind; | |
209 | ||
210 | /*@constant exitkind XK_LAST; @*/ | |
211 | # define XK_LAST XK_MUSTRETURNEXIT | |
212 | ||
213 | extern exitkind exitkind_fromQual (qual p_q) /*@*/ ; | |
214 | extern /*@unused@*/ bool exitkind_isMustExit (exitkind p_e) /*@*/ ; | |
215 | # define exitkind_isMustExit(e) ((e) == XK_MUSTEXIT) | |
216 | ||
217 | extern bool exitkind_equal (exitkind p_e1, exitkind p_e2) /*@*/ ; | |
218 | # define exitkind_equal(e1,e2) ((e1) == (e2)) | |
219 | ||
220 | extern bool exitkind_couldExit (exitkind p_e) /*@*/ ; | |
221 | extern bool exitkind_couldEscape (exitkind p_e) /*@*/ ; | |
222 | extern exitkind exitkind_fromInt (int p_x) /*@*/ ; | |
223 | extern /*@observer@*/ cstring exitkind_unparse (exitkind p_k) /*@*/ ; | |
224 | ||
225 | extern bool exitkind_isKnown (exitkind p_e) /*@*/ ; | |
226 | # define exitkind_isKnown(e) ((e) != XK_UNKNOWN) | |
227 | ||
228 | extern bool exitkind_isTrueExit (exitkind p_e) /*@*/ ; | |
229 | # define exitkind_isTrueExit(e) \ | |
230 | ((e) == XK_TRUEEXIT) | |
231 | ||
232 | extern bool exitkind_isConditionalExit (/*@sef@*/ exitkind p_e) /*@*/ ; | |
233 | # define exitkind_isConditionalExit(e) \ | |
234 | ((e) == XK_TRUEEXIT || (e) == XK_FALSEEXIT) | |
235 | ||
236 | extern bool exitkind_isError (/*@sef@*/ exitkind p_e) /*@*/ ; | |
237 | # define exitkind_isError(e) ((e) == XK_ERROR) | |
238 | ||
239 | extern bool exitkind_mustExit (/*@sef@*/ exitkind p_e) /*@*/ ; | |
240 | # define exitkind_mustExit(e) ((e) == XK_MUSTEXIT) | |
241 | ||
242 | extern bool exitkind_mustEscape (/*@sef@*/ exitkind p_e) /*@*/ ; | |
243 | # define exitkind_mustEscape(e) \ | |
244 | ((e) == XK_MUSTEXIT || (e) == XK_MUSTRETURN \ | |
245 | || (e) == XK_MUSTRETURNEXIT || (e) == XK_GOTO) | |
246 | ||
247 | extern exitkind exitkind_makeConditional (exitkind p_k) /*@*/ ; | |
248 | extern exitkind exitkind_combine (exitkind p_k1, exitkind p_k2) /*@*/ ; | |
249 | ||
250 | /* | |
251 | ** NOTE: combiners are in sRef | |
252 | */ | |
253 | ||
254 | # else | |
255 | # error "Multiple include" | |
256 | # endif |