]>
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 | /* | |
7 | ** storeRef.h | |
8 | */ | |
9 | ||
10 | # ifndef STOREREF_H | |
11 | # define STOREREF_H | |
12 | ||
13 | /* | |
14 | ** note: forwardTypes defines sRef | |
15 | */ | |
16 | ||
17 | /* | |
18 | ** kinds of storage references | |
19 | */ | |
20 | ||
21 | typedef enum { | |
22 | SR_NOTHING, | |
23 | SR_INTERNAL, | |
24 | SR_SPECSTATE, | |
25 | SR_SYSTEM | |
26 | } speckind; | |
27 | ||
28 | typedef enum { | |
29 | SK_PARAM, | |
30 | SK_ARRAYFETCH, | |
31 | SK_FIELD, | |
32 | SK_PTR, | |
33 | SK_ADR, | |
34 | SK_CONST, | |
35 | SK_CVAR, | |
36 | SK_UNCONSTRAINED, | |
37 | SK_OBJECT, | |
38 | SK_CONJ, | |
39 | SK_EXTERNAL, | |
40 | SK_DERIVED, | |
41 | SK_NEW, | |
42 | SK_TYPE, | |
43 | SK_RESULT, | |
44 | SK_SPECIAL, | |
45 | SK_UNKNOWN | |
46 | } skind; | |
47 | ||
48 | typedef struct _cref | |
49 | { | |
50 | int lexlevel; | |
51 | usymId index; | |
52 | } *cref; | |
53 | ||
54 | typedef struct _ainfo | |
55 | { | |
56 | /*@exposed@*/ /*@notnull@*/ sRef arr; | |
57 | bool indknown; | |
58 | int ind; | |
59 | } *ainfo; | |
60 | ||
61 | typedef struct _fldinfo | |
62 | { | |
63 | /*@exposed@*/ /*@notnull@*/ sRef rec; | |
64 | /*@observer@*/ cstring field; | |
65 | } *fldinfo ; | |
66 | ||
67 | typedef struct _cjinfo | |
68 | { | |
69 | /*@exposed@*/ /*@notnull@*/ sRef a; | |
70 | /*@exposed@*/ /*@notnull@*/ sRef b; | |
71 | } *cjinfo ; | |
72 | ||
73 | typedef union _sinfo | |
74 | { | |
75 | /*@only@*/ cref cvar; | |
76 | int paramno; | |
77 | /*@only@*/ ainfo arrayfetch; | |
78 | /*@only@*/ fldinfo field; | |
79 | ctype object; | |
80 | /*@observer@*/ cstring fname; /* unconstrained, new */ | |
81 | /*@exposed@*/ /*@notnull@*/ sRef ref; | |
82 | /*@only@*/ cjinfo conj; | |
83 | speckind spec; | |
84 | } *sinfo; | |
85 | ||
86 | typedef /*@null@*/ struct _alinfo | |
87 | { | |
88 | /*@only@*/ fileloc loc; | |
89 | /*@observer@*/ sRef ref; | |
90 | /*@observer@*/ uentry ue; | |
91 | } *alinfo; | |
92 | ||
93 | struct _sRef | |
94 | { | |
95 | /* does it need to be inside parens (macros) */ | |
96 | bool safe BOOLBITS; | |
97 | ||
98 | /* has it been modified */ | |
99 | bool modified BOOLBITS; | |
100 | ||
101 | skind kind; | |
102 | ctype type; | |
103 | ||
104 | sstate defstate; | |
105 | nstate nullstate; | |
106 | ||
1ac6313d | 107 | /* start modifications: We keep a track of the buf state(nullterm info)*/ |
108 | struct _bbufinfo bufinfo; | |
109 | /* end modifications */ | |
110 | ||
885824d3 | 111 | alkind aliaskind; |
112 | alkind oaliaskind; | |
113 | ||
114 | exkind expkind; /* exposed, observer, normal */ | |
115 | exkind oexpkind; | |
116 | ||
117 | /* where it becomes observer/exposed */ | |
118 | /*@null@*/ /*@only@*/ alinfo expinfo; | |
119 | ||
120 | /* where it changed alias kind */ | |
121 | /*@null@*/ /*@only@*/ alinfo aliasinfo; | |
122 | ||
123 | /* where it is defined/allocated */ | |
124 | /*@null@*/ /*@only@*/ alinfo definfo; | |
125 | ||
126 | /* where it changes null state */ | |
127 | /*@null@*/ /*@only@*/ alinfo nullinfo; | |
128 | ||
129 | /*@only@*/ /*@relnull@*/ sinfo info; | |
130 | ||
131 | /* stores fields for structs, elements for arrays, derefs for pointers */ | |
132 | /*@only@*/ sRefSet deriv; | |
133 | } ; | |
134 | ||
135 | extern bool sRef_perhapsNull (sRef p_s); | |
136 | extern bool sRef_possiblyNull (sRef p_s); | |
137 | extern bool sRef_definitelyNull (sRef p_s); | |
138 | ||
139 | extern void sRef_setNullError (sRef p_s); | |
140 | extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc); | |
141 | extern void sRef_setNotNull (sRef p_s, fileloc p_loc); | |
142 | extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc); | |
143 | extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc); | |
144 | extern void sRef_setPosNull (sRef p_s, fileloc p_loc); | |
145 | extern void sRef_setDefNull (sRef p_s, fileloc p_loc); | |
146 | ||
147 | extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; | |
148 | extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; | |
149 | ||
150 | /*@constant null sRef sRef_undefined; @*/ | |
151 | # define sRef_undefined ((sRef) NULL) | |
152 | # define sRef_isInvalid(s) ((s) == NULL) | |
153 | # define sRef_isValid(s) ((s) != NULL) | |
154 | ||
155 | extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ; | |
156 | extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ; | |
157 | extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ; | |
158 | extern bool sRef_isNotNull (sRef p_s) /*@*/ ; | |
159 | ||
160 | # define sRef_getNullState(s) (sRef_isValid(s) ? (s)->nullstate : NS_UNKNOWN) | |
161 | extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ; | |
162 | ||
163 | extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; | |
164 | extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; | |
165 | extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; | |
166 | extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; | |
167 | extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; | |
168 | ||
169 | extern bool sRef_hasLastReference (sRef p_s) /*@*/ ; | |
170 | # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s)) | |
171 | ||
172 | # define sRef_isKnown(s) (sRef_isValid(s) && (s)->kind != SK_UNKNOWN) | |
173 | ||
174 | extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ; | |
175 | # define sRef_isMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \ | |
176 | && (s)->kind != SK_NEW && (s)->kind != SK_TYPE) | |
177 | extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ; | |
178 | # define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW) | |
179 | ||
180 | extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ; | |
181 | # define sRef_isType(s) (sRef_isValid(s) && (s)->kind == SK_TYPE) | |
182 | ||
183 | extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ; | |
184 | # define sRef_isSafe(s) (sRef_isValid(s) && (s)->safe) | |
185 | ||
186 | extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ; | |
187 | # define sRef_isUnsafe(s) (sRef_isValid(s) && !(s)->safe) | |
188 | ||
189 | extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ; | |
190 | # define sRef_clearAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR) | |
191 | ||
192 | extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ; | |
193 | # define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN) | |
194 | ||
195 | extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; | |
196 | # define sRef_getAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind : AK_ERROR) | |
197 | ||
198 | extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; | |
199 | # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR) | |
200 | ||
201 | extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; | |
202 | # define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ) | |
203 | ||
204 | extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f); | |
205 | extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f); | |
206 | ||
207 | extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ; | |
208 | extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ; | |
209 | extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
210 | ||
211 | extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ; | |
212 | extern void sRef_clearDerived (sRef p_s); | |
213 | extern void sRef_clearDerivedComplete (sRef p_s); | |
214 | extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s); | |
215 | ||
216 | extern /*@observer@*/ sRefSet sRef_derivedFields (/*@dependent@*/ sRef p_rec) /*@*/ ; | |
217 | extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ; | |
218 | extern bool sRef_isDirectParam (sRef p_s) /*@*/ ; | |
219 | extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr); | |
220 | extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ; | |
221 | ||
222 | extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc); | |
223 | extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ; | |
224 | ||
225 | extern void sRef_destroyMod (void) /*@modifies internalState@*/ ; | |
226 | ||
227 | extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s); | |
228 | ||
229 | extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s); | |
230 | ||
231 | extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc); | |
232 | ||
233 | extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; | |
234 | # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL) | |
235 | ||
236 | extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ; | |
237 | ||
238 | extern bool sRef_isSystemState (sRef p_s) /*@*/ ; | |
239 | extern bool sRef_isInternalState (sRef p_s) /*@*/ ; | |
240 | extern bool sRef_isResult (sRef p_s) /*@*/ ; | |
241 | extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ; | |
242 | extern bool sRef_isSpecState (sRef p_s) /*@*/ ; | |
243 | extern bool sRef_isNothing (sRef p_s) /*@*/ ; | |
244 | ||
245 | extern bool sRef_isGlobal (sRef p_s) /*@*/ ; | |
246 | extern bool sRef_isReference (sRef p_s) /*@*/ ; | |
247 | ||
248 | extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ; | |
249 | extern ctype sRef_getType (sRef p_s) /*@*/ ; | |
250 | ||
251 | extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; | |
252 | extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; | |
253 | extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; | |
254 | extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; | |
255 | extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ; | |
256 | extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; | |
257 | extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; | |
258 | ||
259 | extern void sRef_setType (sRef p_s, ctype p_t); | |
260 | extern void sRef_setTypeFull (sRef p_s, ctype p_t); | |
261 | extern void sRef_mergeNullState (sRef p_s, nstate p_n); | |
262 | extern void sRef_setLastReference (sRef p_s, sRef p_ref, fileloc p_loc); | |
263 | extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; | |
264 | extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; | |
265 | extern bool sRef_isIReference (sRef p_s) /*@*/ ; | |
266 | extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ; | |
267 | extern bool sRef_isModified (sRef p_s) /*@*/ ; | |
268 | ||
269 | extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ; | |
270 | extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ; | |
271 | extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ; | |
272 | extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ; | |
273 | extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ; | |
274 | extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ; | |
275 | extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ; | |
276 | extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ; | |
277 | extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ; | |
278 | extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ; | |
279 | extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ; | |
280 | extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
281 | extern int sRef_getIndex (sRef p_arr) /*@*/ ; | |
282 | extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s); | |
283 | extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc); | |
284 | extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc); | |
285 | extern int sRef_getParam (sRef p_s) /*@*/ ; | |
286 | extern int sRef_lexLevel (sRef p_s) /*@*/ ; | |
287 | extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind); | |
288 | extern /*@exposed@*/ sRef | |
289 | sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base) | |
290 | /*@modifies p_s, p_base@*/ ; | |
291 | ||
292 | extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_msgstream@*/ ; | |
293 | ||
294 | extern void sRef_enterFunctionScope (void); | |
295 | extern void sRef_setGlobalScope (void); | |
296 | extern void sRef_exitFunctionScope (void); | |
297 | extern void sRef_clearGlobalScopeSafe (void); | |
298 | extern void sRef_setGlobalScopeSafe (void); | |
299 | ||
300 | extern /*@notnull@*/ /*@exposed@*/ sRef | |
301 | sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr); | |
302 | extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i); | |
303 | extern /*@exposed@*/ sRef | |
304 | sRef_buildField (sRef p_rec, /*@dependent@*/ cstring p_f) | |
305 | /*@modifies p_rec@*/ ; | |
306 | extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t) | |
307 | /*@modifies p_t@*/ ; | |
308 | ||
309 | extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t); | |
310 | extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ; | |
311 | ||
312 | extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; | |
313 | ||
314 | extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ; | |
315 | ||
316 | extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (sRef p_arr) /*@*/ ; | |
317 | extern /*@notnull@*/ /*@exposed@*/ sRef | |
318 | sRef_makeArrayFetchKnown (sRef p_arr, int p_i); | |
319 | extern /*@notnull@*/ /*@dependent@*/ sRef | |
320 | sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b); | |
321 | extern /*@notnull@*/ /*@dependent@*/ sRef | |
322 | sRef_makeCvar (int p_level, usymId p_index, ctype p_ct); | |
323 | extern /*@notnull@*/ /*@dependent@*/ sRef | |
324 | sRef_makeConst (ctype p_ct); | |
325 | extern /*@exposed@*/ sRef | |
326 | sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f); | |
327 | extern /*@notnull@*/ /*@dependent@*/ sRef | |
328 | sRef_makeGlobal (usymId p_l, ctype p_ct); | |
329 | extern /*@exposed@*/ sRef | |
330 | sRef_makeNCField (sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ; | |
331 | extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
332 | extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef | |
333 | sRef_makeObject (ctype p_o) /*@*/ ; | |
334 | extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ; | |
335 | extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ; | |
336 | extern /*@exposed@*/ sRef sRef_makePointer (sRef p_s) /*@modifies p_s@*/ ; | |
337 | extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ; | |
338 | extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ; | |
339 | extern sRef sRef_makeUnknown (void) /*@*/ ; | |
340 | ||
341 | extern sRef sRef_makeNothing (void) /*@*/ ; | |
342 | extern sRef sRef_makeInternalState (void) /*@*/ ; | |
343 | extern sRef sRef_makeSpecState (void) /*@*/ ; | |
344 | extern sRef sRef_makeSystemState (void) /*@*/ ; | |
345 | ||
346 | extern /*@notnull@*/ sRef sRef_makeResult (void) /*@*/ ; | |
347 | extern /*@exposed@*/ sRef | |
348 | sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue) | |
349 | /*@modifies p_s@*/; | |
350 | ||
351 | extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/; | |
352 | ||
353 | extern /*@notnull@*/ sRef | |
354 | sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name); | |
355 | ||
356 | extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ; | |
357 | extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s); | |
358 | ||
359 | extern /*@exposed@*/ sRef | |
360 | sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args) | |
361 | /*@modifies p_s@*/ ; | |
362 | ||
363 | extern bool sRef_isUnionField (sRef p_s); | |
364 | extern void sRef_setModified (sRef p_s); | |
365 | ||
366 | extern void sRef_resetState (sRef p_s); | |
367 | extern void sRef_resetStateComplete (sRef p_s); | |
368 | ||
369 | extern void sRef_storeState (sRef p_s); | |
370 | extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ; | |
371 | extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ; | |
372 | ||
373 | extern /*@observer@*/ uentry sRef_getUentry (sRef p_s); | |
374 | ||
375 | extern cstring sRef_dump (sRef p_s) /*@*/ ; | |
376 | extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ; | |
377 | extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ; | |
378 | extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ; | |
379 | ||
380 | extern /*@only@*/ sRef sRef_saveCopy (sRef p_s); | |
381 | extern /*@dependent@*/ sRef sRef_copy (sRef p_s); | |
382 | ||
383 | extern cstring sRef_unparseState (sRef p_s) /*@*/ ; | |
384 | extern ynm sRef_isWriteable (sRef p_s) /*@*/ ; | |
385 | extern ynm sRef_isReadable (sRef p_s) /*@*/ ; | |
386 | extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ; | |
387 | extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ; | |
388 | extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ; | |
389 | extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
390 | extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
391 | extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
392 | extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
393 | extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
394 | extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
395 | extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
396 | extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
397 | extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
398 | extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_msgstream@*/ ; | |
399 | extern void sRef_showNullInfo (sRef p_s) /*@modifies g_msgstream@*/ ; | |
400 | extern void sRef_showStateInfo (sRef p_s) /*@modifies g_msgstream@*/ ; | |
401 | extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ; | |
402 | extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
403 | extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
404 | extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
405 | extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
406 | extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ; | |
407 | extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; | |
408 | extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; | |
409 | ||
410 | extern int sRef_getScope (sRef p_s) /*@*/ ; | |
411 | extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ; | |
412 | ||
413 | /* must be real function (passed as function param) */ | |
414 | extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; | |
415 | extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; | |
416 | extern bool sRef_isStateLive (sRef p_s) /*@*/ ; | |
417 | extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; | |
418 | extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; | |
419 | extern bool sRef_isUnuseable (sRef p_s) /*@*/ ; | |
420 | ||
421 | extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t) | |
422 | /*@modifies p_t@*/ ; | |
423 | ||
424 | extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t) | |
425 | /*@modifies p_t@*/ ; | |
426 | ||
427 | extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ; | |
428 | ||
429 | extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; | |
430 | ||
431 | extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ; | |
432 | # define sRef_isUndefGlob(s) \ | |
433 | ((sRef_isValid(s)) \ | |
434 | && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED)) | |
435 | ||
436 | extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ; | |
437 | # define sRef_isKilledGlob(s) \ | |
438 | ((sRef_isValid(s)) \ | |
439 | && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED)) | |
440 | ||
441 | extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ; | |
442 | # define sRef_isRelDef(s) \ | |
443 | ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF)) | |
444 | ||
445 | extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ; | |
446 | # define sRef_isPartial(s) \ | |
447 | ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL)) | |
448 | ||
449 | extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ; | |
450 | # define sRef_isStateSpecial(s) \ | |
451 | ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL)) | |
452 | ||
453 | extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ; | |
454 | # define sRef_isStateDefined(s) \ | |
455 | ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \ | |
456 | || (s)->defstate == SS_RELDEF)) | |
457 | ||
458 | extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ; | |
459 | # define sRef_isAnyDefined(s) ((sRef_isValid(s)) && \ | |
460 | (((s)->defstate == SS_DEFINED) \ | |
461 | || ((s)->defstate == SS_RELDEF) \ | |
462 | || ((s)->defstate == SS_PARTIAL))) | |
463 | ||
464 | extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; | |
465 | # define sRef_isPdefined(s) \ | |
466 | ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED)) | |
467 | ||
468 | extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ; | |
469 | ||
470 | extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ; | |
471 | # define sRef_isStateUnknown(s) \ | |
472 | ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN)) | |
473 | ||
474 | extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; | |
475 | # define sRef_isRefCounted(s) \ | |
476 | ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED)) | |
477 | ||
478 | extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; | |
479 | # define sRef_isNewRef(s) \ | |
480 | ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF)) | |
481 | ||
482 | extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; | |
483 | # define sRef_isKillRef(s) \ | |
484 | ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF)) | |
485 | ||
486 | extern bool sRef_isOnly (sRef p_s) /*@*/ ; | |
487 | extern bool sRef_isDependent (sRef p_s) /*@*/ ; | |
488 | extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ; | |
489 | extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ; | |
490 | ||
491 | extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ; | |
492 | # define sRef_isKept(s) \ | |
493 | ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT)) | |
494 | ||
495 | extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ; | |
496 | ||
497 | extern bool sRef_isStack (sRef p_s) /*@*/ ; | |
498 | extern bool sRef_isLocalState (sRef p_s) /*@*/ ; | |
499 | extern bool sRef_isUnique (sRef p_s) /*@*/ ; | |
500 | extern bool sRef_isShared (sRef p_s) /*@*/ ; | |
501 | extern bool sRef_isExposed (sRef p_s) /*@*/ ; | |
502 | extern bool sRef_isObserver (sRef p_s) /*@*/ ; | |
503 | extern bool sRef_isFresh (sRef p_s) /*@*/ ; | |
504 | ||
505 | extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ; | |
506 | # define sRef_isRefsField(s) \ | |
507 | ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS)) | |
508 | ||
509 | extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ; | |
510 | extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ; | |
511 | ||
512 | extern exkind sRef_getExKind (sRef p_s) /*@*/ ; | |
513 | extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ; | |
514 | extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ; | |
515 | extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/; | |
516 | ||
517 | extern bool sRef_isAnyParam (sRef p_s) /*@*/ ; | |
518 | extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@exposed@*/ sRef p_s) /*@*/ ; | |
519 | extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ; | |
520 | ||
521 | extern /*@exposed@*/ sRef sRef_constructPointer (sRef p_t) /*@modifies p_t*/ ; | |
522 | extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ; | |
523 | extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ; | |
524 | extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ; | |
525 | extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ; | |
526 | extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ; | |
527 | extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ; | |
528 | extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ; | |
529 | extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ; | |
530 | extern bool sRef_isExternal (sRef p_s) /*@*/ ; | |
531 | extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ; | |
532 | extern cstring sRef_unparseFull (sRef p_s) /*@*/ ; | |
533 | extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ; | |
534 | extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc) | |
535 | /*@modifies p_res, p_other@*/ ; | |
536 | extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc) | |
537 | /*@modifies p_res, p_other@*/ ; | |
538 | extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other) | |
539 | /*@modifies p_res@*/ ; | |
540 | extern void sRef_mergeStateQuietReverse (sRef p_res, sRef p_other) | |
541 | /*@modifies p_res@*/ ; | |
542 | extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue) | |
543 | /*@modifies p_s@*/ ; | |
544 | extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ; | |
545 | extern bool sRef_modInFunction (void) /*@*/ ; | |
546 | extern void sRef_clearAliasState (sRef p_s, fileloc p_loc) | |
547 | /*@modifies p_s@*/ ; | |
548 | extern void sRef_setPartial (sRef p_s, fileloc p_loc) | |
549 | /*@modifies p_s@*/ ; | |
550 | extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns) | |
551 | /*@modifies p_set@*/ ; | |
552 | ||
553 | extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ; | |
554 | ||
555 | extern sRef sRef_makeDerived (/*@exposed@*/ sRef p_t); | |
556 | ||
557 | extern sstate sRef_getDefState (sRef p_s) /*@*/ ; | |
558 | extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc); | |
559 | extern void sRef_showRefLost (sRef p_s); | |
560 | extern void sRef_showRefKilled (sRef p_s); | |
561 | extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s); | |
562 | ||
563 | extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode), | |
564 | /*@null@*/ bool (p_checkAliases) (sRef), | |
565 | sRef p_s, exprNode p_e, exprNode p_err); | |
566 | extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s); | |
567 | ||
568 | extern void sRef_showStateInconsistent (sRef p_s); | |
569 | ||
570 | extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc); | |
571 | ||
572 | extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc); | |
573 | ||
574 | extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ; | |
575 | ||
576 | extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ; | |
577 | extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ; | |
578 | ||
579 | extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ; | |
580 | ||
581 | extern bool sRef_hasName (sRef p_s) /*@*/ ; | |
582 | ||
583 | extern void sRef_free (/*@only@*/ sRef p_s); | |
584 | ||
585 | extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; | |
586 | ||
1ac6313d | 587 | /* start modifications */ |
588 | /* functions for making modification to null-term info */ | |
589 | extern void sRef_setNullTerminatedStateInnerComplete(sRef s, struct _bbufinfo b, fileloc loc); | |
590 | extern struct _bbufinfo sRef_getNullTerminatedState(sRef s); | |
591 | extern void sRef_setNullTerminatedState (sRef p_s); | |
592 | extern void sRef_setPossiblyNullTerminatedState (sRef p_s); | |
593 | extern void sRef_setNotNullTerminatedState (sRef p_s); | |
594 | extern void sRef_setSize(sRef p_s, int size); | |
595 | extern void sRef_setLen(sRef p_s, int len); | |
596 | ||
597 | extern int sRef_getSize(sRef p_s); | |
598 | #define sRef_getSize(p_s) \ | |
599 | (p_s->bufinfo.size) | |
600 | ||
601 | extern int sRef_getLen(sRef p_s); | |
602 | #define sRef_getLen(p_s) \ | |
603 | (p_s->bufinfo.len) | |
604 | ||
605 | extern void sRef_hasBufStateInfo(sRef p_s); | |
606 | # define sRef_hasBufStateInfo(p_s) \ | |
607 | (sRef_isValid(p_s)) | |
608 | ||
609 | extern bool sRef_isNullTerminated(sRef p_s); | |
610 | # define sRef_isNullTerminated(p_s) \ | |
611 | ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ | |
612 | == BB_NULLTERMINATED) : FALSE) | |
613 | ||
614 | extern bool sRef_isPossiblyNullTerminated(sRef p_s); | |
615 | # define sRef_isPossiblyNullTerminated(p_s) \ | |
616 | ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ | |
617 | == BB_POSSIBLYNULLTERMINATED) : FALSE) | |
618 | ||
619 | extern bool sRef_isNotNullTerminated(sRef p_s); | |
620 | # define sRef_isNotNullTerminated(p_s) \ | |
621 | ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ | |
622 | == BB_NOTNULLTERMINATED) : FALSE) | |
623 | ||
624 | /* end modifications */ | |
625 | ||
885824d3 | 626 | # else |
627 | # error "Multiple include" | |
628 | # endif | |
629 | ||
630 | ||
631 | ||
632 | ||
633 | ||
634 | ||
635 | ||
636 | ||
637 | ||
638 | ||
639 | ||
640 | ||
641 |