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