2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
14 ** note: forwardTypes defines sRef
18 ** kinds of storage references
57 /*@exposed@*/ /*@notnull@*/ sRef arr;
64 /*@exposed@*/ /*@notnull@*/ sRef rec;
65 /*@observer@*/ cstring field;
70 /*@exposed@*/ /*@notnull@*/ sRef a;
71 /*@exposed@*/ /*@notnull@*/ sRef b;
78 /*@only@*/ ainfo arrayfetch;
79 /*@only@*/ fldinfo field;
81 /*@observer@*/ cstring fname; /* unconstrained, new */
82 /*@exposed@*/ /*@notnull@*/ sRef ref;
83 /*@only@*/ cjinfo conj;
89 /* does it need to be inside parens (macros) */
92 /* has it been modified */
93 bool modified; /* BOOLBITS; */
95 /* for debugging: make this sRef as immutable. */
96 bool immut; /* BOOLBITS; */
101 multiVal val; /* Some sRef's have known values */
106 /* start modifications: We keep a track of the buf state(nullterm info)*/
107 struct s_bbufinfo bufinfo;
108 /* end modifications */
113 exkind expkind; /* exposed, observer, normal */
116 /* where it becomes observer/exposed */
117 /*@null@*/ /*@only@*/ stateInfo expinfo;
119 /* where it changed alias kind */
120 /*@null@*/ /*@only@*/ stateInfo aliasinfo;
122 /* where it is defined/allocated */
123 /*@null@*/ /*@only@*/ stateInfo definfo;
125 /* where it is null */
126 /*@null@*/ /*@only@*/ stateInfo nullinfo;
128 /*@only@*/ /*@relnull@*/ sinfo info;
130 /* stores fields for structs, elements for arrays, derefs for pointers */
131 /*@only@*/ sRefSet deriv;
133 /* sRef's include a lookup table of state variables. */
134 /*@only@*/ valueTable state;
137 extern bool sRef_perhapsNull (sRef p_s);
138 extern bool sRef_possiblyNull (sRef p_s);
139 extern bool sRef_definitelyNull (sRef p_s);
141 extern bool sRef_definitelyNullContext (sRef p_s);
142 extern bool sRef_definitelyNullAltContext (sRef p_s);
144 extern void sRef_setNullError (sRef p_s);
145 extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc);
146 extern void sRef_setNotNull (sRef p_s, fileloc p_loc);
147 extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc);
148 extern void sRef_setNullStateN (sRef p_s, nstate p_n);
149 extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc);
150 extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
151 extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
153 extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
154 extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
156 /*@constant null sRef sRef_undefined; @*/
157 # define sRef_undefined ((sRef) NULL)
158 # define sRef_isInvalid(s) ((s) == NULL)
159 # define sRef_isValid(s) ((s) != NULL)
161 extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ;
162 extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
163 extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ;
164 extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
166 extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
168 extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
169 extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
170 extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
171 extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
172 extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
174 extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
175 # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
177 # define sRef_isKnown(s) (sRef_isValid(s) && (s)->kind != SK_UNKNOWN)
179 extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
180 # define sRef_isMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \
181 && (s)->kind != SK_NEW && (s)->kind != SK_TYPE)
182 extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
183 # define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW)
185 extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ;
186 # define sRef_isType(s) (sRef_isValid(s) && (s)->kind == SK_TYPE)
188 extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ;
189 # define sRef_isSafe(s) (sRef_isValid(s) && (s)->safe)
191 extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ;
192 # define sRef_isUnsafe(s) (sRef_isValid(s) && !(s)->safe)
194 extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ;
195 # define sRef_clearAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR)
197 extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ;
198 # define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN)
200 extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
202 extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
203 # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
205 extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
206 # define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ)
208 extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
209 extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f);
211 extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ;
212 extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ;
213 extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
215 extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ;
216 extern void sRef_clearDerived (sRef p_s);
217 extern void sRef_clearDerivedComplete (sRef p_s);
218 extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s);
220 extern /*@observer@*/ sRefSet sRef_derivedFields (/*@temp@*/ sRef p_rec) /*@*/ ;
221 extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ;
222 extern bool sRef_isDirectParam (sRef p_s) /*@*/ ;
223 extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr);
224 extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ;
226 extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc);
227 extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ;
229 extern void sRef_destroyMod (void) /*@modifies internalState@*/ ;
231 extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s);
233 extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
235 extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
237 extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
238 # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
240 extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
242 extern bool sRef_isSystemState (sRef p_s) /*@*/ ;
243 extern bool sRef_isGlobalMarker (sRef p_s) /*@*/ ;
244 extern bool sRef_isInternalState (sRef p_s) /*@*/ ;
245 extern bool sRef_isResult (sRef p_s) /*@*/ ;
246 extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ;
247 extern bool sRef_isSpecState (sRef p_s) /*@*/ ;
248 extern bool sRef_isNothing (sRef p_s) /*@*/ ;
250 extern bool sRef_isFileOrGlobalScope (sRef p_s) /*@*/ ;
251 extern bool sRef_isReference (sRef p_s) /*@*/ ;
253 extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ;
254 extern ctype sRef_getType (sRef p_s) /*@*/ ;
256 extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ;
258 extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
259 extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
260 extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
261 extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ;
262 extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
263 extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
264 extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
266 extern void sRef_setType (sRef p_s, ctype p_t);
267 extern void sRef_setTypeFull (sRef p_s, ctype p_t);
268 extern void sRef_mergeNullState (sRef p_s, nstate p_n);
269 extern void sRef_setLastReference (/*@temp@*/ sRef p_s, /*@exposed@*/ sRef p_ref, fileloc p_loc);
270 extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
271 extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
272 extern bool sRef_isIReference (sRef p_s) /*@*/ ;
273 extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ;
274 extern bool sRef_isModified (sRef p_s) /*@*/ ;
276 extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ;
277 extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ;
278 extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ;
279 extern bool sRef_sameObject (sRef p_s1, sRef p_s2) /*@*/ ;
280 extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ;
281 extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ;
282 extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ;
283 extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ;
284 extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ;
285 extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ;
286 extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ;
287 extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ;
288 extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
289 extern int sRef_getIndex (sRef p_arr) /*@*/ ;
290 extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s);
291 extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc);
292 extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc);
293 extern int sRef_getParam (sRef p_s) /*@*/ ;
294 extern int sRef_lexLevel (sRef p_s) /*@*/ ;
295 extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind);
297 extern /*@exposed@*/ sRef
298 sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base)
299 /*@modifies p_s, p_base@*/ ;
301 extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_msgstream@*/ ;
303 extern void sRef_enterFunctionScope (void) /*@modifies internalState@*/ ;
304 extern void sRef_setGlobalScope (void) /*@modifies internalState@*/ ;
305 extern bool sRef_inGlobalScope (void) /*@*/ ;
306 extern void sRef_exitFunctionScope (void) /*@modifies internalState@*/ ;
307 extern void sRef_clearGlobalScopeSafe (void) /*@modifies internalState@*/ ;
308 extern void sRef_setGlobalScopeSafe (void) /*@modifies internalState@*/ ;
310 extern /*@notnull@*/ /*@exposed@*/ sRef
311 sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr);
312 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
313 extern /*@exposed@*/ sRef
314 sRef_buildField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f)
315 /*@modifies p_rec@*/ ;
316 extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t)
319 extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t);
320 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ;
322 extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
324 extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ;
326 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (/*@exposed@*/ sRef p_arr) /*@*/ ;
327 extern /*@notnull@*/ /*@exposed@*/ sRef
328 sRef_makeArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
329 extern /*@notnull@*/ /*@dependent@*/ sRef
330 sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
331 extern /*@notnull@*/ /*@dependent@*/ sRef
332 sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo);
333 extern /*@notnull@*/ /*@dependent@*/ sRef
334 sRef_makeConst (ctype p_ct);
335 extern /*@exposed@*/ sRef
336 sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
337 extern /*@notnull@*/ /*@dependent@*/ sRef
338 sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo);
339 extern /*@exposed@*/ sRef
340 sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
341 extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
342 extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef
343 sRef_makeObject (ctype p_o) /*@*/ ;
344 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
345 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ;
346 extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ;
347 extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
348 extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;
350 extern /*@dependent@*/ sRef sRef_makeUnknown (void) /*@*/ ;
351 extern /*@dependent@*/ sRef sRef_makeNothing (void) /*@*/ ;
352 extern /*@dependent@*/ sRef sRef_makeInternalState (void) /*@*/ ;
353 extern /*@dependent@*/ sRef sRef_makeSpecState (void) /*@*/ ;
354 extern /*@dependent@*/ sRef sRef_makeGlobalMarker (void) /*@*/ ;
355 extern /*@dependent@*/ sRef sRef_makeSystemState (void) /*@*/ ;
357 extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (ctype) /*@*/ ;
358 extern /*@exposed@*/ sRef
359 sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue)
362 extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/;
364 extern /*@notnull@*/ /*@dependent@*/ sRef
365 sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name) ;
367 extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ;
368 extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s);
370 extern /*@exposed@*/ sRef
371 sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args)
380 /*@only@*/ constraintExpr sRef_fixConstraintParam (/*@observer@*/ sRef p_s, /*@observer@*/ /*@temp@*/ exprNodeList p_args);
382 extern bool sRef_isUnionField (sRef p_s);
383 extern void sRef_setModified (sRef p_s);
385 extern void sRef_resetState (sRef p_s);
386 extern void sRef_resetStateComplete (sRef p_s);
388 extern void sRef_storeState (sRef p_s);
389 extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ;
390 extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ;
392 extern /*@observer@*/ uentry sRef_getUentry (sRef p_s);
394 extern cstring sRef_dump (sRef p_s) /*@*/ ;
395 extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ;
396 extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ;
397 extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ;
399 extern /*@only@*/ sRef sRef_saveCopy (sRef p_s);
400 extern /*@dependent@*/ sRef sRef_copy (sRef p_s);
402 extern cstring sRef_unparseState (sRef p_s) /*@*/ ;
403 extern ynm sRef_isWriteable (sRef p_s) /*@*/ ;
404 extern ynm sRef_isReadable (sRef p_s) /*@*/ ;
405 extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ;
406 extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ;
407 extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ;
408 extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
409 extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
410 extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
411 extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
412 extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
413 extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
414 extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
415 extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
416 extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
417 extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
418 extern void sRef_showMetaStateInfo (sRef p_s, cstring p_key) /*@modifies g_msgstream@*/ ;
419 extern void sRef_showNullInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
420 extern void sRef_showStateInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
421 extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ;
422 extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
423 extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
424 extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
425 extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
426 extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ;
427 extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
428 extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
430 extern int sRef_getScope (sRef p_s) /*@*/ ;
431 extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ;
433 /* must be real function (passed as function param) */
434 extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
435 extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
436 extern bool sRef_isStateLive (sRef p_s) /*@*/ ;
437 extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
438 extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
439 extern bool sRef_isUnuseable (sRef p_s) /*@*/ ;
441 extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t)
444 extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t)
447 extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ;
449 extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
451 extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ;
452 # define sRef_isUndefGlob(s) \
454 && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED))
456 extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ;
457 # define sRef_isKilledGlob(s) \
459 && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED))
461 extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ;
462 # define sRef_isRelDef(s) \
463 ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF))
465 extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ;
466 # define sRef_isPartial(s) \
467 ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL))
469 extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
470 # define sRef_isStateSpecial(s) \
471 ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL))
473 extern bool sRef_makeStateSpecial (sRef p_s)
475 /* returns false is sRef already has an inconsistend defstate */ ;
477 extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ;
478 # define sRef_isStateDefined(s) \
479 ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \
480 || (s)->defstate == SS_RELDEF))
482 extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ;
483 # define sRef_isAnyDefined(s) ((sRef_isValid(s)) && \
484 (((s)->defstate == SS_DEFINED) \
485 || ((s)->defstate == SS_RELDEF) \
486 || ((s)->defstate == SS_PARTIAL)))
488 extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
489 # define sRef_isPdefined(s) \
490 ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED))
492 extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ;
494 extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ;
495 # define sRef_isStateUnknown(s) \
496 ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN))
498 extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
499 # define sRef_isRefCounted(s) \
500 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED))
502 extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
503 # define sRef_isNewRef(s) \
504 ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF))
506 extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
507 # define sRef_isKillRef(s) \
508 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF))
510 extern bool sRef_isOnly (sRef p_s) /*@*/ ;
511 extern bool sRef_isDependent (sRef p_s) /*@*/ ;
512 extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ;
513 extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ;
515 extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ;
516 # define sRef_isKept(s) \
517 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT))
519 extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ;
521 extern bool sRef_isStack (sRef p_s) /*@*/ ;
522 extern bool sRef_isLocalState (sRef p_s) /*@*/ ;
523 extern bool sRef_isUnique (sRef p_s) /*@*/ ;
524 extern bool sRef_isShared (sRef p_s) /*@*/ ;
525 extern bool sRef_isExposed (sRef p_s) /*@*/ ;
526 extern bool sRef_isObserver (sRef p_s) /*@*/ ;
527 extern bool sRef_isFresh (sRef p_s) /*@*/ ;
529 extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ;
530 # define sRef_isRefsField(s) \
531 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS))
533 extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ;
534 extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ;
536 extern exkind sRef_getExKind (sRef p_s) /*@*/ ;
537 extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ;
538 extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ;
539 extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/;
541 extern bool sRef_isAnyParam (sRef p_s) /*@*/ ;
542 extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@temp@*/ sRef p_s) /*@*/ ;
543 extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ;
545 extern /*@exposed@*/ sRef sRef_constructPointer (/*@exposed@*/ sRef p_t) /*@modifies p_t*/ ;
546 extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ;
547 extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ;
548 extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ;
549 extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ;
550 extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ;
551 extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
552 extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ;
553 extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ;
554 extern bool sRef_isExternal (sRef p_s) /*@*/ ;
555 extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ;
556 extern cstring sRef_unparseFull (sRef p_s) /*@*/ ;
557 extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ;
558 extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
559 /*@modifies p_res, p_other@*/ ;
560 extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
561 /*@modifies p_res, p_other@*/ ;
562 extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other)
563 /*@modifies p_res@*/ ;
564 extern void sRef_mergeStateQuietReverse (/*@dependent@*/ sRef p_res, /*@dependent@*/ sRef p_other)
565 /*@modifies p_res@*/ ;
566 extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue)
568 extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ;
569 extern bool sRef_modInFunction (void) /*@*/ ;
570 extern void sRef_clearAliasState (sRef p_s, fileloc p_loc)
572 extern void sRef_setPartial (sRef p_s, fileloc p_loc)
574 extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns)
575 /*@modifies p_set@*/ ;
577 extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ;
579 extern /*@dependent@*/ sRef sRef_makeDerived (/*@exposed@*/ sRef p_t);
581 extern sstate sRef_getDefState (sRef p_s) /*@*/ ;
582 extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc);
583 extern void sRef_showRefLost (sRef p_s);
584 extern void sRef_showRefKilled (sRef p_s);
585 extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s);
587 extern void sRef_reflectAnnotation (sRef p_s, annotationInfo p_a, fileloc p_loc);
588 extern /*@observer@*/ valueTable sRef_getValueTable (sRef p_s) /*@*/ ;
590 extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode),
591 /*@null@*/ bool (p_checkAliases) (sRef),
592 sRef p_s, exprNode p_e, exprNode p_err);
593 extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s);
595 extern void sRef_showStateInconsistent (sRef p_s);
597 extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc);
599 extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc);
601 extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ;
603 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ;
604 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ;
606 extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ;
608 extern bool sRef_hasName (sRef p_s) /*@*/ ;
609 extern void sRef_free (/*@only@*/ sRef p_s);
610 extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
612 /* start modifications */
613 /* functions for making modification to null-term info */
614 extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct s_bbufinfo p_b, fileloc p_loc);
615 extern struct s_bbufinfo sRef_getNullTerminatedState(sRef p_s);
616 extern void sRef_setNullTerminatedState (sRef p_s);
617 extern void sRef_setPossiblyNullTerminatedState (sRef p_s);
618 extern void sRef_setNotNullTerminatedState (sRef p_s);
619 extern void sRef_setSize(sRef p_s, int p_size);
620 extern void sRef_setLen(sRef p_s, int p_len);
622 extern int sRef_getSize(sRef p_s);
626 #define sRef_getSize(p_s) \
627 ((p_s)->bufinfo.size)
629 extern int sRef_getLen(sRef p_s);
630 #define sRef_getLen(p_s) \
633 extern bool sRef_hasBufStateInfo(sRef p_s);
634 # define sRef_hasBufStateInfo(p_s) \
637 extern bool sRef_isNullTerminated(/*@sef@*/sRef p_s);
638 # define sRef_isNullTerminated(p_s) \
639 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
640 == BB_NULLTERMINATED) : FALSE)
642 extern bool sRef_isPossiblyNullTerminated(/*@sef@*/sRef p_s);
643 # define sRef_isPossiblyNullTerminated(p_s) \
644 ( sRef_hasBufStateInfo((p_s)) ? ( (p_s)->bufinfo.bufstate \
645 == BB_POSSIBLYNULLTERMINATED) : FALSE)
647 extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s);
648 # define sRef_isNotNullTerminated(p_s) \
649 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
650 == BB_NOTNULLTERMINATED) : FALSE)
656 extern bool sRef_isFixedArray (sRef p_s) /*@*/;
658 extern long int sRef_getArraySize (sRef p_s) /*@*/;
660 extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s);
661 extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ;
663 /* end modifications */
665 extern void sRef_setMetaStateValueComplete (sRef p_s, cstring p_key, int p_value, fileloc p_loc)
668 extern void sRef_setMetaStateValue (sRef p_s, cstring p_key, int p_value, fileloc p_loc)
671 extern /*@observer@*/ stateValue sRef_getMetaStateValue (sRef p_s, cstring p_key) /*@*/ ;
673 extern bool sRef_checkMetaStateValue (sRef p_s, cstring p_key, int p_value)
676 extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@*/ ;
677 extern bool sRef_hasValue (sRef p_s) /*@*/ ;
678 extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ;
680 extern /*@mayexit@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ;
683 # error "Multiple include"