]> 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
Initial revision
[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
107 alkind aliaskind;
108 alkind oaliaskind;
109
110 exkind expkind; /* exposed, observer, normal */
111 exkind oexpkind;
112
113 /* where it becomes observer/exposed */
114 /*@null@*/ /*@only@*/ alinfo expinfo;
115
116 /* where it changed alias kind */
117 /*@null@*/ /*@only@*/ alinfo aliasinfo;
118
119 /* where it is defined/allocated */
120 /*@null@*/ /*@only@*/ alinfo definfo;
121
122 /* where it changes null state */
123 /*@null@*/ /*@only@*/ alinfo nullinfo;
124
125 /*@only@*/ /*@relnull@*/ sinfo info;
126
127 /* stores fields for structs, elements for arrays, derefs for pointers */
128 /*@only@*/ sRefSet deriv;
129} ;
130
131extern bool sRef_perhapsNull (sRef p_s);
132extern bool sRef_possiblyNull (sRef p_s);
133extern bool sRef_definitelyNull (sRef p_s);
134
135extern void sRef_setNullError (sRef p_s);
136extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc);
137extern void sRef_setNotNull (sRef p_s, fileloc p_loc);
138extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc);
139extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc);
140extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
141extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
142
143extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
144extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
145
146/*@constant null sRef sRef_undefined; @*/
147# define sRef_undefined ((sRef) NULL)
148# define sRef_isInvalid(s) ((s) == NULL)
149# define sRef_isValid(s) ((s) != NULL)
150
151extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ;
152extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
153extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ;
154extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
155
156# define sRef_getNullState(s) (sRef_isValid(s) ? (s)->nullstate : NS_UNKNOWN)
157extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
158
159extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
160extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
161extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
162extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
163extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
164
165extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
166# define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
167
168# define sRef_isKnown(s) (sRef_isValid(s) && (s)->kind != SK_UNKNOWN)
169
170extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
171# define sRef_isMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \
172 && (s)->kind != SK_NEW && (s)->kind != SK_TYPE)
173extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
174# define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW)
175
176extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ;
177# define sRef_isType(s) (sRef_isValid(s) && (s)->kind == SK_TYPE)
178
179extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ;
180# define sRef_isSafe(s) (sRef_isValid(s) && (s)->safe)
181
182extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ;
183# define sRef_isUnsafe(s) (sRef_isValid(s) && !(s)->safe)
184
185extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ;
186# define sRef_clearAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR)
187
188extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ;
189# define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN)
190
191extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
192# define sRef_getAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind : AK_ERROR)
193
194extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
195# define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
196
197extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
198# define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ)
199
200extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
201extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f);
202
203extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ;
204extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ;
205extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
206
207extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ;
208extern void sRef_clearDerived (sRef p_s);
209extern void sRef_clearDerivedComplete (sRef p_s);
210extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s);
211
212extern /*@observer@*/ sRefSet sRef_derivedFields (/*@dependent@*/ sRef p_rec) /*@*/ ;
213extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ;
214extern bool sRef_isDirectParam (sRef p_s) /*@*/ ;
215extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr);
216extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ;
217
218extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc);
219extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ;
220
221extern void sRef_destroyMod (void) /*@modifies internalState@*/ ;
222
223extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s);
224
225extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
226
227extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
228
229extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
230# define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
231
232extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
233
234extern bool sRef_isSystemState (sRef p_s) /*@*/ ;
235extern bool sRef_isInternalState (sRef p_s) /*@*/ ;
236extern bool sRef_isResult (sRef p_s) /*@*/ ;
237extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ;
238extern bool sRef_isSpecState (sRef p_s) /*@*/ ;
239extern bool sRef_isNothing (sRef p_s) /*@*/ ;
240
241extern bool sRef_isGlobal (sRef p_s) /*@*/ ;
242extern bool sRef_isReference (sRef p_s) /*@*/ ;
243
244extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ;
245extern ctype sRef_getType (sRef p_s) /*@*/ ;
246
247extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
248extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
249extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
250extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ;
251extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
252extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
253extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
254
255extern void sRef_setType (sRef p_s, ctype p_t);
256extern void sRef_setTypeFull (sRef p_s, ctype p_t);
257extern void sRef_mergeNullState (sRef p_s, nstate p_n);
258extern void sRef_setLastReference (sRef p_s, sRef p_ref, fileloc p_loc);
259extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
260extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
261extern bool sRef_isIReference (sRef p_s) /*@*/ ;
262extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ;
263extern bool sRef_isModified (sRef p_s) /*@*/ ;
264
265extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ;
266extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ;
267extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ;
268extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ;
269extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ;
270extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ;
271extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ;
272extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ;
273extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ;
274extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ;
275extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ;
276extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
277extern int sRef_getIndex (sRef p_arr) /*@*/ ;
278extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s);
279extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc);
280extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc);
281extern int sRef_getParam (sRef p_s) /*@*/ ;
282extern int sRef_lexLevel (sRef p_s) /*@*/ ;
283extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind);
284extern /*@exposed@*/ sRef
285 sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base)
286 /*@modifies p_s, p_base@*/ ;
287
288extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_msgstream@*/ ;
289
290extern void sRef_enterFunctionScope (void);
291extern void sRef_setGlobalScope (void);
292extern void sRef_exitFunctionScope (void);
293extern void sRef_clearGlobalScopeSafe (void);
294extern void sRef_setGlobalScopeSafe (void);
295
296extern /*@notnull@*/ /*@exposed@*/ sRef
297 sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr);
298extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
299extern /*@exposed@*/ sRef
300 sRef_buildField (sRef p_rec, /*@dependent@*/ cstring p_f)
301 /*@modifies p_rec@*/ ;
302extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t)
303 /*@modifies p_t@*/ ;
304
305extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t);
306extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ;
307
308extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
309
310extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ;
311
312extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (sRef p_arr) /*@*/ ;
313extern /*@notnull@*/ /*@exposed@*/ sRef
314 sRef_makeArrayFetchKnown (sRef p_arr, int p_i);
315extern /*@notnull@*/ /*@dependent@*/ sRef
316 sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
317extern /*@notnull@*/ /*@dependent@*/ sRef
318 sRef_makeCvar (int p_level, usymId p_index, ctype p_ct);
319extern /*@notnull@*/ /*@dependent@*/ sRef
320 sRef_makeConst (ctype p_ct);
321extern /*@exposed@*/ sRef
322 sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
323extern /*@notnull@*/ /*@dependent@*/ sRef
324 sRef_makeGlobal (usymId p_l, ctype p_ct);
325extern /*@exposed@*/ sRef
326 sRef_makeNCField (sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
327extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
328extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef
329 sRef_makeObject (ctype p_o) /*@*/ ;
330extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
331extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ;
332extern /*@exposed@*/ sRef sRef_makePointer (sRef p_s) /*@modifies p_s@*/ ;
333extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
334extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;
335extern sRef sRef_makeUnknown (void) /*@*/ ;
336
337extern sRef sRef_makeNothing (void) /*@*/ ;
338extern sRef sRef_makeInternalState (void) /*@*/ ;
339extern sRef sRef_makeSpecState (void) /*@*/ ;
340extern sRef sRef_makeSystemState (void) /*@*/ ;
341
342extern /*@notnull@*/ sRef sRef_makeResult (void) /*@*/ ;
343extern /*@exposed@*/ sRef
344 sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue)
345 /*@modifies p_s@*/;
346
347extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/;
348
349extern /*@notnull@*/ sRef
350 sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name);
351
352extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ;
353extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s);
354
355extern /*@exposed@*/ sRef
356 sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args)
357 /*@modifies p_s@*/ ;
358
359extern bool sRef_isUnionField (sRef p_s);
360extern void sRef_setModified (sRef p_s);
361
362extern void sRef_resetState (sRef p_s);
363extern void sRef_resetStateComplete (sRef p_s);
364
365extern void sRef_storeState (sRef p_s);
366extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ;
367extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ;
368
369extern /*@observer@*/ uentry sRef_getUentry (sRef p_s);
370
371extern cstring sRef_dump (sRef p_s) /*@*/ ;
372extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ;
373extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ;
374extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ;
375
376extern /*@only@*/ sRef sRef_saveCopy (sRef p_s);
377extern /*@dependent@*/ sRef sRef_copy (sRef p_s);
378
379extern cstring sRef_unparseState (sRef p_s) /*@*/ ;
380extern ynm sRef_isWriteable (sRef p_s) /*@*/ ;
381extern ynm sRef_isReadable (sRef p_s) /*@*/ ;
382extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ;
383extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ;
384extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ;
385extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
386extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
387extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
388extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
389extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
390extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
391extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
392extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
393extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
394extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
395extern void sRef_showNullInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
396extern void sRef_showStateInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
397extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ;
398extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
399extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
400extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
401extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
402extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ;
403extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
404extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
405
406extern int sRef_getScope (sRef p_s) /*@*/ ;
407extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ;
408
409/* must be real function (passed as function param) */
410extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
411extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
412extern bool sRef_isStateLive (sRef p_s) /*@*/ ;
413extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
414extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
415extern bool sRef_isUnuseable (sRef p_s) /*@*/ ;
416
417extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t)
418 /*@modifies p_t@*/ ;
419
420extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t)
421 /*@modifies p_t@*/ ;
422
423extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ;
424
425extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
426
427extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ;
428# define sRef_isUndefGlob(s) \
429 ((sRef_isValid(s)) \
430 && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED))
431
432extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ;
433# define sRef_isKilledGlob(s) \
434 ((sRef_isValid(s)) \
435 && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED))
436
437extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ;
438# define sRef_isRelDef(s) \
439 ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF))
440
441extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ;
442# define sRef_isPartial(s) \
443 ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL))
444
445extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
446# define sRef_isStateSpecial(s) \
447 ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL))
448
449extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ;
450# define sRef_isStateDefined(s) \
451 ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \
452 || (s)->defstate == SS_RELDEF))
453
454extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ;
455# define sRef_isAnyDefined(s) ((sRef_isValid(s)) && \
456 (((s)->defstate == SS_DEFINED) \
457 || ((s)->defstate == SS_RELDEF) \
458 || ((s)->defstate == SS_PARTIAL)))
459
460extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
461# define sRef_isPdefined(s) \
462 ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED))
463
464extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ;
465
466extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ;
467# define sRef_isStateUnknown(s) \
468 ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN))
469
470extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
471# define sRef_isRefCounted(s) \
472 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED))
473
474extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
475# define sRef_isNewRef(s) \
476 ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF))
477
478extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
479# define sRef_isKillRef(s) \
480 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF))
481
482extern bool sRef_isOnly (sRef p_s) /*@*/ ;
483extern bool sRef_isDependent (sRef p_s) /*@*/ ;
484extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ;
485extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ;
486
487extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ;
488# define sRef_isKept(s) \
489 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT))
490
491extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ;
492
493extern bool sRef_isStack (sRef p_s) /*@*/ ;
494extern bool sRef_isLocalState (sRef p_s) /*@*/ ;
495extern bool sRef_isUnique (sRef p_s) /*@*/ ;
496extern bool sRef_isShared (sRef p_s) /*@*/ ;
497extern bool sRef_isExposed (sRef p_s) /*@*/ ;
498extern bool sRef_isObserver (sRef p_s) /*@*/ ;
499extern bool sRef_isFresh (sRef p_s) /*@*/ ;
500
501extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ;
502# define sRef_isRefsField(s) \
503 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS))
504
505extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ;
506extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ;
507
508extern exkind sRef_getExKind (sRef p_s) /*@*/ ;
509extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ;
510extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ;
511extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/;
512
513extern bool sRef_isAnyParam (sRef p_s) /*@*/ ;
514extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@exposed@*/ sRef p_s) /*@*/ ;
515extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ;
516
517extern /*@exposed@*/ sRef sRef_constructPointer (sRef p_t) /*@modifies p_t*/ ;
518extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ;
519extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ;
520extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ;
521extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ;
522extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ;
523extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
524extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ;
525extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ;
526extern bool sRef_isExternal (sRef p_s) /*@*/ ;
527extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ;
528extern cstring sRef_unparseFull (sRef p_s) /*@*/ ;
529extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ;
530extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
531 /*@modifies p_res, p_other@*/ ;
532extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
533 /*@modifies p_res, p_other@*/ ;
534extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other)
535 /*@modifies p_res@*/ ;
536extern void sRef_mergeStateQuietReverse (sRef p_res, sRef p_other)
537 /*@modifies p_res@*/ ;
538extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue)
539 /*@modifies p_s@*/ ;
540extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ;
541extern bool sRef_modInFunction (void) /*@*/ ;
542extern void sRef_clearAliasState (sRef p_s, fileloc p_loc)
543 /*@modifies p_s@*/ ;
544extern void sRef_setPartial (sRef p_s, fileloc p_loc)
545 /*@modifies p_s@*/ ;
546extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns)
547 /*@modifies p_set@*/ ;
548
549extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ;
550
551extern sRef sRef_makeDerived (/*@exposed@*/ sRef p_t);
552
553extern sstate sRef_getDefState (sRef p_s) /*@*/ ;
554extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc);
555extern void sRef_showRefLost (sRef p_s);
556extern void sRef_showRefKilled (sRef p_s);
557extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s);
558
559extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode),
560 /*@null@*/ bool (p_checkAliases) (sRef),
561 sRef p_s, exprNode p_e, exprNode p_err);
562extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s);
563
564extern void sRef_showStateInconsistent (sRef p_s);
565
566extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc);
567
568extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc);
569
570extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ;
571
572extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ;
573extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ;
574
575extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ;
576
577extern bool sRef_hasName (sRef p_s) /*@*/ ;
578
579extern void sRef_free (/*@only@*/ sRef p_s);
580
581extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
582
583# else
584# error "Multiple include"
585# endif
586
587
588
589
590
591
592
593
594
595
596
597
598
git-cvsimport mirror of splint
This page took 0.120642 seconds and 5 git commands to generate.