]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
28bf4b0b | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
885824d3 | 3 | ** See ../LICENSE for license information. |
4 | */ | |
5 | # ifndef UENTRY_H | |
6 | # define UENTRY_H | |
7 | # define CENTRY_H | |
8 | ||
9 | /* | |
10 | ** universal symbol table entry | |
11 | ** (combines old llentry, centry, and ttentry) | |
12 | */ | |
13 | ||
14 | /* | |
15 | ** vkind --- need to fix value for consistency in dump files | |
16 | */ | |
17 | ||
28bf4b0b | 18 | typedef struct |
885824d3 | 19 | { |
b9904f57 | 20 | typeIdSet access; |
5e211f69 | 21 | bool macro; |
885824d3 | 22 | } *ucinfo; |
23 | ||
24 | typedef enum | |
25 | { | |
26 | VKSPEC = 0, VKNORMAL, | |
27 | VKPARAM, VKYIELDPARAM, VKREFYIELDPARAM, | |
28 | VKRETPARAM, VKREFPARAM, | |
29 | VKSEFPARAM, VKREFSEFPARAM, | |
30 | VKSEFRETPARAM, VKREFSEFRETPARAM, | |
31 | VKEXPMACRO | |
32 | } vkind; | |
33 | ||
34 | /*@constant vkind VKFIRST;@*/ | |
35 | # define VKFIRST VKSPEC | |
36 | ||
37 | /*@constant vkind VKLAST;@*/ | |
38 | # define VKLAST VKEXPMACRO | |
39 | ||
40 | typedef enum | |
41 | { | |
42 | CH_UNKNOWN, | |
43 | CH_UNCHECKED, | |
44 | CH_CHECKED, | |
45 | CH_CHECKMOD, | |
46 | CH_CHECKEDSTRICT | |
47 | } chkind; | |
48 | ||
1ac6313d | 49 | /* start modifications */ |
28bf4b0b | 50 | typedef enum { |
1ac6313d | 51 | BB_POSSIBLYNULLTERMINATED, /* buffer is possibly nullterm(can't decide statically) */ |
52 | BB_NULLTERMINATED, /*buffer is known to be nullterminated */ | |
53 | BB_NOTNULLTERMINATED /* buffer is known to be not nullterm */ | |
54 | } bbufstate; | |
55 | ||
abd7f895 | 56 | typedef /*@null@*/ struct s_bbufinfo { |
1ac6313d | 57 | bbufstate bufstate; /* state of the buffer */ |
58 | int size; /* size of the buffer allocated */ | |
59 | int len; /* len of the buffer VALID ONLY IF state is NULLTERM */ | |
60 | } *bbufinfo ; | |
61 | ||
28bf4b0b | 62 | typedef struct |
885824d3 | 63 | { |
64 | vkind kind; /* kind (parameter, specified) */ | |
65 | chkind checked; /* how is it checked */ | |
66 | sstate defstate; | |
67 | nstate nullstate; | |
1ac6313d | 68 | bbufinfo bufinfo; /* is valid only if the entry is a variable and (a pointer |
69 | or array) */ | |
885824d3 | 70 | } *uvinfo ; |
1ac6313d | 71 | /* end modifications */ |
885824d3 | 72 | |
28bf4b0b | 73 | typedef struct |
885824d3 | 74 | { |
75 | ynm abs; | |
76 | ynm mut; | |
77 | ctype type; | |
78 | } *udinfo ; | |
79 | ||
80 | /* information for specified functions */ | |
81 | ||
82 | typedef enum | |
83 | { | |
84 | SPC_NONE, | |
85 | SPC_PRINTFLIKE, | |
86 | SPC_SCANFLIKE, | |
87 | SPC_MESSAGELIKE, | |
88 | SPC_LAST | |
89 | } specCode; | |
90 | ||
28bf4b0b | 91 | typedef struct |
885824d3 | 92 | { |
93 | qual nullPred; | |
94 | specCode specialCode; | |
95 | exitkind exitCode; | |
96 | typeIdSet access; /* access types */ | |
97 | ||
98 | /*@owned@*/ globSet globs; /* globals list */ | |
99 | /*@owned@*/ sRefSet mods; /* modifies */ | |
100 | ||
28bf4b0b | 101 | stateClauseList specclauses; |
885824d3 | 102 | |
103 | /*@dependent@*/ uentryList defparams; | |
104 | bool hasGlobs BOOLBITS; | |
105 | bool hasMods BOOLBITS; | |
93307a76 | 106 | |
3814599d | 107 | functionConstraint preconditions; |
108 | functionConstraint postconditions; | |
93307a76 | 109 | |
885824d3 | 110 | } *ufinfo ; |
111 | ||
28bf4b0b | 112 | typedef struct |
885824d3 | 113 | { |
114 | typeIdSet access; | |
115 | /*@owned@*/ globSet globs; /* globals list */ | |
116 | /*@owned@*/ sRefSet mods; /* modifies */ | |
117 | } *uiinfo ; | |
118 | ||
28bf4b0b | 119 | typedef struct |
885824d3 | 120 | { |
121 | typeIdSet access; | |
122 | } *ueinfo ; | |
123 | ||
28bf4b0b | 124 | typedef union |
885824d3 | 125 | { |
126 | ucinfo uconst; | |
127 | uvinfo var; | |
128 | udinfo datatype; | |
129 | ufinfo fcn; | |
130 | uiinfo iter; | |
131 | ueinfo enditer; | |
132 | } *uinfo ; | |
133 | ||
28bf4b0b | 134 | struct s_uentry |
885824d3 | 135 | { |
136 | ekind ukind; | |
137 | cstring uname; | |
138 | ctype utype; | |
139 | ||
140 | fileloc whereSpecified; | |
141 | fileloc whereDefined; | |
142 | fileloc whereDeclared; | |
143 | ||
144 | /* meaning of sref is different for: | |
145 | ** variables current state | |
146 | ** functions state of return value | |
147 | ** types state of datatype | |
148 | */ | |
28bf4b0b | 149 | |
885824d3 | 150 | /*@exposed@*/ /*@null@*/ sRef sref; |
151 | ||
28bf4b0b | 152 | warnClause warn; |
153 | ||
885824d3 | 154 | /* Location list is complete only if showalluses is set. */ |
155 | filelocList uses; | |
156 | ||
157 | bool used BOOLBITS; | |
158 | bool lset BOOLBITS; /* set in local table */ | |
159 | bool isPrivate BOOLBITS; /* specification only */ | |
160 | bool hasNameError BOOLBITS; | |
161 | ||
162 | storageClassCode storageclass; | |
163 | /*@relnull@*/ uinfo info; /* null for KELIPSMARKER, KINVALID */ | |
495af944 | 164 | |
165 | qualList cQuals; /*drl 04-19-2002 stores c qualifiers. THis was neccessary to get the | |
166 | function to print out right as C quals are not stored anywhere else*/ | |
885824d3 | 167 | } ; |
168 | ||
169 | /* | |
170 | ** There is no uentry_isDefined to avoid confusion with | |
171 | ** uentry_isCodeDefined (which was previously called | |
b7e84605 | 172 | ** uentry_isDefined). |
885824d3 | 173 | */ |
174 | ||
0e41eb0e | 175 | extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) |
885824d3 | 176 | /*@*/ ; |
0e41eb0e | 177 | extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) |
885824d3 | 178 | /*@*/ ; |
0e41eb0e | 179 | extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) |
885824d3 | 180 | /*@*/ ; |
181 | ||
182 | /*@constant null uentry uentry_undefined; @*/ | |
183 | # define uentry_undefined ((uentry) NULL) | |
184 | ||
185 | # define uentry_isUndefined(e) ((e) == uentry_undefined) | |
186 | # define uentry_isValid(e) ((e) != uentry_undefined) | |
187 | # define uentry_isInvalid(e) ((e) == uentry_undefined) | |
188 | ||
189 | extern int uentry_compareStrict (uentry p_v1, uentry p_v2); | |
190 | ||
191 | /*@constant int PARAMUNKNOWN; @*/ | |
192 | # define PARAMUNKNOWN -1 | |
193 | ||
194 | extern bool uentry_isMaybeAbstract (uentry p_e) /*@*/ ; | |
195 | extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ; | |
196 | extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ; | |
197 | extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ; | |
198 | ||
0e41eb0e | 199 | extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e); |
885824d3 | 200 | # define uentry_isLset(e) \ |
201 | (uentry_isValid(e) && (e)->lset) | |
202 | ||
0e41eb0e | 203 | extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e); |
885824d3 | 204 | # define uentry_isUsed(e) (uentry_isValid(e) && (e)->used) |
205 | ||
0e41eb0e | 206 | extern /*@unused@*/ /*@falsewhennull@*/ bool |
885824d3 | 207 | uentry_isAbstractType (uentry p_e) /*@*/ ; |
208 | # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e)) | |
209 | ||
0e41eb0e | 210 | extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 211 | # define uentry_isConstant(e) \ |
212 | (uentry_isValid(e) && ekind_isConst ((e)->ukind)) | |
213 | ||
0e41eb0e | 214 | extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 215 | # define uentry_isEitherConstant(e) \ |
216 | (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind))) | |
217 | ||
0e41eb0e | 218 | extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 219 | # define uentry_isEnumConstant(e) \ |
220 | (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind)) | |
221 | ||
0e41eb0e | 222 | extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 223 | # define uentry_isExternal(c) \ |
224 | (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c))) | |
225 | ||
0e41eb0e | 226 | extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 227 | # define uentry_isExtern(c) \ |
228 | (uentry_isValid(c) && (c)->storageclass == SCEXTERN) | |
229 | ||
230 | extern bool uentry_isForward (uentry p_e) /*@*/ ; | |
231 | ||
0e41eb0e | 232 | extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 233 | # define uentry_isFunction(e) \ |
234 | (uentry_isValid(e) && ekind_isFunction ((e)->ukind)) | |
235 | ||
0e41eb0e | 236 | extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 237 | # define uentry_isPriv(e) \ |
238 | (uentry_isValid(e) && (e)->isPrivate) | |
239 | ||
0e41eb0e | 240 | extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ; |
241 | extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ; | |
885824d3 | 242 | |
0e41eb0e | 243 | extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ; |
885824d3 | 244 | # define uentry_isStatic(c) \ |
245 | (uentry_isValid(c) && (c)->storageclass == SCSTATIC) | |
246 | ||
247 | extern void uentry_setLset (/*@sef@*/ uentry p_e); | |
248 | # define uentry_setLset(e) \ | |
249 | (uentry_isValid(e) ? (e)->lset = TRUE : TRUE) | |
250 | ||
251 | extern bool uentry_isSpecialFunction (uentry p_ue) /*@*/ ; | |
252 | extern bool uentry_isMessageLike (uentry p_ue) /*@*/ ; | |
253 | extern bool uentry_isScanfLike (uentry p_ue) /*@*/ ; | |
254 | extern bool uentry_isPrintfLike (uentry p_ue) /*@*/ ; | |
255 | ||
256 | extern void uentry_setMessageLike (uentry p_ue) /*@modifies p_ue@*/ ; | |
257 | extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ; | |
258 | extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ; | |
259 | ||
80489f0a | 260 | extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ; |
885824d3 | 261 | |
262 | extern bool uentry_sameObject (uentry p_e1, uentry p_e2); | |
263 | # define uentry_sameObject(e1,e2) ((e1) == (e2)) | |
264 | ||
265 | extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ; | |
266 | ||
267 | extern void uentry_showWhereAny (uentry p_spec) | |
80489f0a | 268 | /*@modifies g_warningstream@*/ ; |
885824d3 | 269 | |
270 | extern void uentry_checkParams (uentry p_ue); | |
271 | extern void uentry_mergeUses (uentry p_res, uentry p_other); | |
272 | extern void uentry_setExtern (uentry p_c); | |
273 | extern void uentry_setUsed (uentry p_e, fileloc p_loc); | |
274 | extern void uentry_setDefState (uentry p_ue, sstate p_defstate); | |
275 | ||
276 | extern void uentry_setNotUsed (/*@sef@*/ uentry p_e); | |
277 | # define uentry_setNotUsed(e) \ | |
278 | (uentry_isValid (e) ? (e)->used = FALSE : FALSE) | |
279 | ||
280 | extern bool uentry_wasUsed (/*@sef@*/ uentry p_e); | |
281 | # define uentry_wasUsed(e) \ | |
282 | (uentry_isValid (e) ? (e)->used : TRUE) | |
283 | ||
284 | extern void uentry_mergeConstantValue (uentry p_ue, /*@only@*/ multiVal p_m); | |
285 | ||
286 | extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ; | |
287 | extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ; | |
288 | extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ; | |
289 | extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ; | |
0e41eb0e | 290 | extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ; |
291 | extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ; | |
292 | extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ; | |
293 | extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue) | |
885824d3 | 294 | /*@uses p_ue->ukind@*/ |
295 | /*@*/ ; | |
0e41eb0e | 296 | extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ; |
885824d3 | 297 | |
0e41eb0e | 298 | extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ; |
885824d3 | 299 | |
0e41eb0e | 300 | extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) |
885824d3 | 301 | /*@uses p_e->whereDeclared@*/ /*@*/ ; |
302 | ||
303 | extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ; | |
28bf4b0b | 304 | extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ; |
305 | ||
885824d3 | 306 | extern void uentry_showWhereDefined (uentry p_spec); |
0e41eb0e | 307 | extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ; |
308 | extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue) | |
885824d3 | 309 | /*@uses p_ue->ukind@*/ /*@*/ ; |
0e41eb0e | 310 | extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ; |
311 | extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ; | |
312 | extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ; | |
313 | extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ; | |
314 | extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ; | |
315 | extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ; | |
316 | extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) | |
885824d3 | 317 | /*@uses p_u->ukind, p_u->info@*/ |
318 | /*@*/ ; | |
319 | ||
0e41eb0e | 320 | extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ; |
321 | extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ; | |
885824d3 | 322 | |
0e41eb0e | 323 | extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) |
885824d3 | 324 | /*@uses p_ue->ukind@*/ /*@*/ ; |
0e41eb0e | 325 | extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue) |
885824d3 | 326 | /*@uses p_ue->ukind@*/ /*@*/ ; |
327 | ||
0e41eb0e | 328 | extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) |
885824d3 | 329 | /*@uses p_e->ukind@*/ |
330 | /*@*/ ; | |
331 | ||
0e41eb0e | 332 | extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) |
885824d3 | 333 | /*@uses p_e->ukind@*/ |
334 | /*@*/ ; | |
335 | ||
336 | extern cstring uentry_dump (uentry p_v) ; | |
337 | extern cstring uentry_dumpParam (uentry p_v); | |
28bf4b0b | 338 | |
339 | extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ; | |
340 | ||
885824d3 | 341 | extern cstring uentry_getName (/*@special@*/ uentry p_e) |
342 | /*@uses p_e->ukind, p_e->info, p_e->uname@*/ | |
343 | /*@*/ ; | |
344 | ||
345 | extern cstring uentry_unparse (uentry p_v) /*@*/ ; | |
346 | extern cstring uentry_unparseAbbrev (uentry p_v) /*@*/ ; | |
347 | extern cstring uentry_unparseFull (uentry p_v) /*@*/ ; | |
348 | extern void uentry_setMutable (uentry p_e) /*@modifies p_e@*/ ; | |
349 | extern ctype uentry_getAbstractType (uentry p_e) /*@*/ ; | |
350 | extern ctype uentry_getRealType (uentry p_e) /*@globals internalState@*/ ; | |
351 | extern ctype uentry_getType (uentry p_e) /*@*/ ; | |
352 | extern ekind uentry_getKind (uentry p_e) /*@*/ ; | |
353 | extern /*@observer@*/ fileloc uentry_whereDefined (uentry p_e) /*@*/ ; | |
354 | extern /*@observer@*/ fileloc uentry_whereSpecified (uentry p_e) /*@*/ ; | |
355 | extern int uentry_compare (uentry p_u1, uentry p_u2); | |
356 | extern /*@exposed@*/ sRef uentry_getSref (/*@temp@*/ uentry p_e) /*@*/ ; | |
357 | extern /*@observer@*/ sRefSet uentry_getMods (uentry p_l) /*@*/ ; | |
358 | extern typeIdSet uentry_accessType (uentry p_e) /*@*/ ; | |
359 | extern /*@observer@*/ fileloc uentry_whereEither (uentry p_e) /*@*/ ; | |
360 | extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s, | |
361 | /*@temp@*/ fileloc p_f) | |
362 | /*@*/ ; | |
363 | ||
80489f0a | 364 | extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ; |
885824d3 | 365 | |
28bf4b0b | 366 | extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ; |
885824d3 | 367 | |
368 | extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra) | |
80489f0a | 369 | /*@modifies g_warningstream@*/ ; |
885824d3 | 370 | |
371 | # ifndef NOLCL | |
372 | extern void uentry_setRefCounted (uentry p_e); | |
373 | ||
374 | extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t); | |
288cbc5c | 375 | extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/; |
885824d3 | 376 | |
377 | extern /*@notnull@*/ uentry | |
378 | uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access, | |
379 | /*@keep@*/ fileloc p_f); | |
380 | ||
381 | extern /*@notnull@*/ uentry | |
382 | uentry_makePrivFunction2 (cstring p_n, ctype p_t, | |
383 | typeIdSet p_access, | |
384 | /*@only@*/ globSet p_globs, | |
385 | /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f); | |
386 | ||
387 | extern /*@notnull@*/ uentry | |
388 | uentry_makeSpecEnumConstant (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_loc) /*@*/ ; | |
389 | ||
390 | extern /*@notnull@*/ uentry | |
391 | uentry_makeEnumTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc) /*@*/ ; | |
392 | ||
393 | extern /*@notnull@*/ uentry | |
394 | uentry_makeTypeListFunction (cstring p_n, typeIdSet p_access, /*@only@*/ fileloc p_f) | |
395 | /*@*/ ; | |
396 | ||
397 | extern /*@notnull@*/ uentry | |
398 | uentry_makeSpecFunction (cstring p_n, ctype p_t, | |
399 | typeIdSet p_access, /*@only@*/ globSet p_globs, | |
400 | /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f); | |
401 | # endif | |
402 | ||
403 | extern /*@notnull@*/ uentry | |
404 | uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ; | |
405 | ||
406 | extern /*@notnull@*/ uentry | |
407 | uentry_makeEnumInitializedConstant (cstring p_n, ctype p_t, exprNode p_expr) /*@*/ ; | |
408 | ||
409 | extern /*@notnull@*/ /*@only@*/ uentry | |
410 | uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f) | |
411 | /*@*/ ; | |
5e211f69 | 412 | |
413 | extern /*@only@*/ /*@notnull@*/ uentry | |
3e3ec469 | 414 | uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, |
415 | bool p_priv, /*@only@*/ multiVal p_val) | |
5e211f69 | 416 | /*@*/ ; |
417 | ||
418 | extern /*@notnull@*/ /*@only@*/ uentry | |
419 | uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f) | |
420 | /*@*/ ; | |
421 | ||
885824d3 | 422 | extern /*@notnull@*/ /*@only@*/ uentry |
28bf4b0b | 423 | uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abstract, |
885824d3 | 424 | /*@only@*/ fileloc p_f) /*@*/ ; |
425 | extern /*@notnull@*/ /*@only@*/ uentry | |
426 | uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, | |
28bf4b0b | 427 | ynm p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ; |
885824d3 | 428 | extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ; |
429 | ||
430 | extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ; | |
b072092f | 431 | extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ; |
885824d3 | 432 | |
433 | extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ; | |
434 | # define uentry_isElipsisMarker(u) \ | |
435 | (uentry_isValid(u) && ekind_isElipsis ((u)->ukind)) | |
436 | ||
437 | extern /*@notnull@*/ uentry | |
438 | uentry_makeEndIter (cstring p_n, /*@only@*/ fileloc p_f) /*@*/ ; | |
439 | extern /*@notnull@*/ uentry | |
440 | uentry_makeEnumTagLoc (cstring p_n, ctype p_t) /*@*/ ; | |
441 | extern /*@notnull@*/ uentry | |
442 | uentry_makeForwardFunction (cstring p_n, typeId p_access, /*@temp@*/ fileloc p_f) /*@*/ ; | |
443 | ||
444 | extern /*@notnull@*/ uentry | |
445 | uentry_makeFunction (cstring p_n, ctype p_t, | |
446 | typeId p_access, | |
447 | /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods, | |
28bf4b0b | 448 | /*@only@*/ warnClause p_warn, |
885824d3 | 449 | /*@only@*/ fileloc p_f); |
450 | ||
451 | extern /*@notnull@*/ uentry | |
452 | uentry_makeIter (cstring p_n, ctype p_ct, /*@only@*/ fileloc p_f) /*@*/ ; | |
453 | extern /*@notnull@*/ uentry | |
454 | uentry_makeParam (idDecl p_t, int p_i) /*@*/ ; | |
455 | ||
456 | extern /*@notnull@*/ uentry | |
457 | uentry_makeStructTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc); | |
458 | extern /*@notnull@*/ uentry | |
459 | uentry_makeStructTagLoc (cstring p_n, ctype p_t); | |
460 | extern /*@notnull@*/ uentry | |
461 | uentry_makeUnionTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc); | |
462 | extern /*@notnull@*/ uentry | |
463 | uentry_makeUnionTagLoc (cstring p_n, ctype p_t); | |
464 | extern /*@notnull@*/ uentry | |
465 | uentry_makeVariable (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, bool p_isPriv); | |
466 | extern /*@notnull@*/ /*@only@*/ uentry | |
467 | uentry_makeVariableLoc (cstring p_n, ctype p_t); | |
468 | ||
469 | # ifndef NOLCL | |
470 | extern /*@notnull@*/ /*@only@*/ | |
6970c11b | 471 | uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc); |
885824d3 | 472 | # endif |
473 | ||
474 | extern /*@notnull@*/ /*@only@*/ | |
6970c11b | 475 | uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc, |
476 | /*@exposed@*/ sRef p_s); | |
885824d3 | 477 | extern /*@notnull@*/ /*@only@*/ |
478 | uentry uentry_makeIdFunction (idDecl p_id); | |
479 | extern /*@notnull@*/ /*@only@*/ | |
480 | uentry uentry_makeIdDatatype (idDecl p_id); | |
481 | extern /*@notnull@*/ /*@only@*/ | |
28bf4b0b | 482 | uentry uentry_makeBoolDatatype (ynm p_abstract); |
885824d3 | 483 | extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew); |
484 | extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def); | |
485 | extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e); | |
486 | extern uentry uentry_undump (ekind p_kind, fileloc p_loc, char **p_s); | |
487 | extern /*@observer@*/ uentryList uentry_getParams (uentry p_l) /*@*/ ; | |
488 | extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn) | |
489 | /*@modifies p_ue@*/ ; | |
490 | extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ; | |
491 | extern qual uentry_nullPred (uentry p_u); | |
492 | extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e); | |
493 | extern void uentry_setDatatype (uentry p_e, usymId p_uid); | |
494 | ||
495 | extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f) | |
496 | /*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/ | |
497 | /*@modifies p_e@*/ ; | |
498 | ||
499 | extern void uentry_checkDecl (void); | |
500 | extern void uentry_clearDecl (void); | |
501 | extern void uentry_setDeclared (uentry p_e, fileloc p_f); | |
502 | extern void uentry_setDeclaredOnly (uentry p_e, /*@only@*/ fileloc p_f); | |
503 | extern void uentry_setDeclaredForceOnly (uentry p_e, /*@only@*/ fileloc p_f); | |
504 | extern void uentry_setFunctionDefined (uentry p_e, fileloc p_loc); | |
505 | extern void uentry_setName (uentry p_e, /*@only@*/ cstring p_n); | |
506 | extern void uentry_setParam (uentry p_e); | |
507 | extern void uentry_setSref (uentry p_e, /*@exposed@*/ sRef p_s); | |
508 | extern void uentry_setStatic (uentry p_c); | |
509 | ||
510 | extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr) | |
511 | /*@modifies p_ue, p_sr@*/; | |
512 | ||
28bf4b0b | 513 | extern bool uentry_hasWarning (uentry p_ue) /*@*/ ; |
514 | ||
515 | extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn) | |
516 | /*@modifies p_ue*/; | |
517 | ||
518 | extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses) | |
885824d3 | 519 | /*@modifies p_ue@*/ ; |
520 | ||
521 | extern void uentry_setType (uentry p_e, ctype p_t); | |
522 | ||
523 | extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue); | |
80489f0a | 524 | extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ; |
885824d3 | 525 | |
526 | extern void | |
527 | uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s) | |
80489f0a | 528 | /*@modifies g_warningstream@*/ ; |
885824d3 | 529 | |
80489f0a | 530 | extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ; |
531 | extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ; | |
532 | extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ; | |
885824d3 | 533 | |
534 | extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ; | |
535 | extern uentry uentry_copy (uentry p_e) /*@*/ ; | |
536 | extern void uentry_freeComplete (/*@only@*/ uentry p_e) ; | |
537 | extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/; | |
538 | extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ; | |
539 | ||
540 | extern void | |
541 | uentry_mergeState (uentry p_res, uentry p_other, fileloc p_loc, | |
542 | bool p_mustReturn, bool p_flip, bool p_opt, | |
543 | clause p_cl) /*@modifies p_res, p_other@*/ ; | |
544 | ||
545 | extern void uentry_setState (uentry p_res, uentry p_other) | |
546 | /*@modifies p_res, p_other@*/ ; | |
547 | ||
548 | extern void uentry_setRefParam (uentry p_e) /*@modifies p_e@*/ ; | |
549 | ||
550 | extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/; | |
551 | extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ; | |
28bf4b0b | 552 | extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/; |
553 | extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/; | |
885824d3 | 554 | extern bool uentry_isRefParam (uentry p_u) /*@*/ ; |
555 | extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ; | |
556 | extern bool uentry_hasMods (uentry p_ue) /*@*/ ; | |
557 | ||
28bf4b0b | 558 | extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ; |
ccf0a4a8 | 559 | extern bool uentry_hasConditions (uentry p_ue) /*@*/ ; |
560 | ||
885824d3 | 561 | extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ; |
562 | ||
563 | extern void uentry_checkYieldParam (uentry p_old, uentry p_unew); | |
564 | extern bool uentry_isOnly (uentry p_ue) /*@*/ ; | |
565 | extern bool uentry_isUnique (uentry p_ue) /*@*/ ; | |
566 | extern void uentry_reflectQualifiers (uentry p_ue, qualList p_q) /*@modifies p_ue@*/; | |
567 | extern bool uentry_isOut (uentry p_u) /*@*/ ; | |
568 | extern bool uentry_isPartial (uentry p_u) /*@*/ ; | |
569 | extern bool uentry_isStateSpecial (uentry p_u) /*@*/ ; | |
570 | extern bool uentry_possiblyNull (uentry p_u) /*@*/ ; | |
571 | extern ctype uentry_getForceRealType (uentry p_e) /*@globals internalState@*/ ; | |
572 | extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ; | |
573 | extern exkind uentry_getExpKind (uentry p_u) /*@*/ ; | |
574 | extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ; | |
575 | extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ; | |
b87215ab | 576 | extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ; |
885824d3 | 577 | extern bool uentry_isYield (uentry p_ue) /*@*/ ; |
578 | extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ; | |
579 | extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ; | |
580 | extern int uentry_xcomparealpha (uentry *p_p1, uentry *p_p2) /*@*/ ; | |
581 | extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ; | |
582 | extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ; | |
583 | extern void uentry_copyState (uentry p_res, uentry p_other); | |
584 | extern bool uentry_sameKind (uentry p_u1, uentry p_u2); | |
585 | extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args); | |
586 | extern bool uentry_isReturned (uentry p_u); | |
587 | extern bool uentry_isRefCountedDatatype (uentry p_e); | |
588 | extern sstate uentry_getDefState (uentry p_u); | |
589 | extern /*@unused@*/ void uentry_markFree (/*@owned@*/ uentry p_u); | |
590 | extern /*@dependent@*/ sRef uentry_getOrigSref (uentry p_e); | |
591 | extern void uentry_destroyMod (void) /*@modifies internalState@*/; | |
592 | extern void uentry_showDefSpecInfo (uentry p_ce, fileloc p_fwhere); | |
593 | extern void uentry_markOwned (/*@owned@*/ uentry p_u); | |
594 | ||
595 | extern /*@observer@*/ fileloc uentry_whereLast (uentry p_e) /*@*/ ; | |
596 | extern void uentry_setParamNo (uentry p_ue, int p_pno) /*@modifies p_ue@*/; | |
597 | ||
598 | extern /*@observer@*/ filelocList uentry_getUses (/*@sef@*/ uentry p_e) /*@*/ ; | |
599 | # define uentry_getUses(u) (uentry_isValid (u) ? (u)->uses : filelocList_undefined) | |
600 | ||
601 | extern bool uentry_isCheckedUnknown (uentry p_ue) /*@*/ ; | |
602 | extern bool uentry_isCheckedModify (uentry p_ue) /*@*/ ; | |
603 | extern bool uentry_isUnchecked (uentry p_ue) /*@*/ ; | |
604 | extern bool uentry_isChecked (uentry p_ue) /*@*/ ; | |
605 | extern bool uentry_isCheckMod (uentry p_ue) /*@*/ ; | |
606 | extern bool uentry_isCheckedStrict (uentry p_ue) /*@*/ ; | |
607 | extern void uentry_setUnchecked (uentry p_ue) /*@modifies p_ue@*/ ; | |
608 | extern void uentry_setChecked (uentry p_ue) /*@modifies p_ue@*/ ; | |
609 | extern void uentry_setCheckMod (uentry p_ue) /*@modifies p_ue@*/ ; | |
610 | extern void uentry_setCheckedStrict (uentry p_ue) /*@modifies p_ue@*/ ; | |
611 | ||
612 | extern bool uentry_hasAccessType (uentry p_e); | |
613 | ||
28bf4b0b | 614 | /*@constant cstring GLOBAL_MARKER_NAME@*/ |
615 | # define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#") | |
1ac6313d | 616 | |
1ac6313d | 617 | /* functions for making modification to null-term info */ |
b7b694d6 | 618 | extern void uentry_setNullTerminatedState (uentry p_e); |
619 | extern void uentry_setPossiblyNullTerminatedState (uentry p_e); | |
620 | extern void uentry_setSize(uentry p_e, int p_size); | |
621 | extern void uentry_setLen(uentry p_e, int p_len); | |
1ac6313d | 622 | |
4cccc6ad | 623 | /*@i66*/ |
624 | /*@-nullderef@*/ | |
1ac6313d | 625 | extern bool uentry_hasBufStateInfo (uentry p_ue); |
626 | # define uentry_hasBufStateInfo(p_ue) \ | |
627 | (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE) | |
628 | ||
84c9ffbf | 629 | /*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue); |
1ac6313d | 630 | # define uentry_isNullTerminated(p_ue) \ |
bb7c2085 | 631 | ( uentry_hasBufStateInfo((p_ue ) ) ? ((p_ue)->info->var->bufinfo->bufstate \ |
1ac6313d | 632 | == BB_NULLTERMINATED) : FALSE) |
633 | ||
84c9ffbf | 634 | /*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue); |
1ac6313d | 635 | # define uentry_isPossiblyNullTerminated(p_ue) \ |
bb7c2085 | 636 | ( uentry_hasBufStateInfo((p_ue)) ? ((p_ue)->info->var->bufinfo->bufstate \ |
1ac6313d | 637 | == BB_POSSIBLYNULLTERMINATED) : FALSE) |
638 | ||
84c9ffbf | 639 | /*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue); |
1ac6313d | 640 | # define uentry_isNotNullTerminated(p_ue) \ |
bb7c2085 | 641 | ( uentry_hasBufStateInfo((p_ue) ) ? ((p_ue)->info->var->bufinfo->bufstate \ |
1ac6313d | 642 | == BB_NOTNULLTERMINATED) : FALSE) |
4cccc6ad | 643 | /*@=nullderef@*/ |
1ac6313d | 644 | |
645 | /* end modifications */ | |
646 | ||
28bf4b0b | 647 | extern uentry uentry_makeGlobalMarker (void) ; |
648 | extern bool uentry_isGlobalMarker (uentry) /*@*/ ; | |
649 | ||
7ebcc5bb | 650 | extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc); |
28bf4b0b | 651 | |
885824d3 | 652 | # ifdef DOANNOTS |
5e211f69 | 653 | typedef enum |
654 | { | |
655 | AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR, | |
656 | AN_CONST, AN_LAST | |
657 | } ancontext; | |
885824d3 | 658 | |
659 | extern void initAnnots (); | |
660 | extern void printAnnots (void); | |
661 | extern void uentry_tallyAnnots (uentry u, ancontext kind); | |
662 | # endif /* DOANNOTS */ | |
663 | ||
ba45e1e4 | 664 | extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ; |
ccf0a4a8 | 665 | extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e); |
ba45e1e4 | 666 | |
4cccc6ad | 667 | /* start modifications */ |
b7b694d6 | 668 | |
93307a76 | 669 | /*drl7x*/ |
28bf4b0b | 670 | extern constraintList uentry_getFcnPreconditions (uentry p_ue); |
671 | extern constraintList uentry_getFcnPostconditions (uentry p_ue); | |
920a3797 | 672 | |
3814599d | 673 | extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions); |
674 | ||
675 | extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions); | |
b7b694d6 | 676 | /*end mods*/ |
4cccc6ad | 677 | |
495af944 | 678 | /*drl added function for cod generation */ |
679 | extern /*@only@*/ cstring uentry_unparseFunctionHeader (uentry p_v) /*@*/; | |
680 | ||
681 | /*end drl*/ | |
6483a926 | 682 | /* |
683 | ** For debugging only | |
684 | */ | |
685 | ||
686 | # ifdef DEBUGSPLINT | |
687 | extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ; | |
688 | # endif | |
689 | ||
885824d3 | 690 | # else |
691 | # error "Multiple include" | |
692 | # endif | |
693 | ||
694 | ||
695 |