]> 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
Fixed problem with print format for +showalluses.
[splint.git] / src / Headers / sRef.h
CommitLineData
885824d3 1/*
28bf4b0b 2** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
885824d3 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,
28bf4b0b 25 SR_SYSTEM,
26 SR_GLOBALMARKER
885824d3 27} speckind;
28
29typedef enum {
30 SK_PARAM,
31 SK_ARRAYFETCH,
32 SK_FIELD,
33 SK_PTR,
34 SK_ADR,
35 SK_CONST,
36 SK_CVAR,
37 SK_UNCONSTRAINED,
38 SK_OBJECT,
39 SK_CONJ,
40 SK_EXTERNAL,
41 SK_DERIVED,
42 SK_NEW,
43 SK_TYPE,
44 SK_RESULT,
45 SK_SPECIAL,
46 SK_UNKNOWN
47} skind;
48
28bf4b0b 49typedef struct
885824d3 50{
51 int lexlevel;
52 usymId index;
53} *cref;
54
28bf4b0b 55typedef struct
885824d3 56{
57 /*@exposed@*/ /*@notnull@*/ sRef arr;
58 bool indknown;
59 int ind;
60} *ainfo;
61
28bf4b0b 62typedef struct
885824d3 63{
64 /*@exposed@*/ /*@notnull@*/ sRef rec;
65 /*@observer@*/ cstring field;
66} *fldinfo ;
67
28bf4b0b 68typedef struct
885824d3 69{
70 /*@exposed@*/ /*@notnull@*/ sRef a;
71 /*@exposed@*/ /*@notnull@*/ sRef b;
72} *cjinfo ;
73
28bf4b0b 74typedef union
885824d3 75{
76 /*@only@*/ cref cvar;
77 int paramno;
78 /*@only@*/ ainfo arrayfetch;
28bf4b0b 79 /*@only@*/ fldinfo field;
885824d3 80 ctype object;
81 /*@observer@*/ cstring fname; /* unconstrained, new */
b9904f57 82 /*@exposed@*/ /*@notnull@*/ sRef ref;
885824d3 83 /*@only@*/ cjinfo conj;
84 speckind spec;
85} *sinfo;
86
28bf4b0b 87struct s_sRef
885824d3 88{
89 /* does it need to be inside parens (macros) */
28bf4b0b 90 bool safe;
885824d3 91
92 /* has it been modified */
28bf4b0b 93 bool modified; /* BOOLBITS; */
94
95 /* for debugging: make this sRef as immutable. */
96 bool immut; /* BOOLBITS; */
885824d3 97
98 skind kind;
99 ctype type;
100
b9904f57 101 multiVal val; /* Some sRef's have known values */
102
885824d3 103 sstate defstate;
104 nstate nullstate;
105
1ac6313d 106 /* start modifications: We keep a track of the buf state(nullterm info)*/
28bf4b0b 107 struct s_bbufinfo bufinfo;
1ac6313d 108 /* end modifications */
109
885824d3 110 alkind aliaskind;
111 alkind oaliaskind;
112
113 exkind expkind; /* exposed, observer, normal */
114 exkind oexpkind;
115
116 /* where it becomes observer/exposed */
28bf4b0b 117 /*@null@*/ /*@only@*/ stateInfo expinfo;
885824d3 118
119 /* where it changed alias kind */
28bf4b0b 120 /*@null@*/ /*@only@*/ stateInfo aliasinfo;
885824d3 121
122 /* where it is defined/allocated */
28bf4b0b 123 /*@null@*/ /*@only@*/ stateInfo definfo;
885824d3 124
28bf4b0b 125 /* where it is null */
126 /*@null@*/ /*@only@*/ stateInfo nullinfo;
885824d3 127
128 /*@only@*/ /*@relnull@*/ sinfo info;
129
130 /* stores fields for structs, elements for arrays, derefs for pointers */
131 /*@only@*/ sRefSet deriv;
28bf4b0b 132
133 /* sRef's include a lookup table of state variables. */
134 /*@only@*/ valueTable state;
885824d3 135} ;
136
137extern bool sRef_perhapsNull (sRef p_s);
138extern bool sRef_possiblyNull (sRef p_s);
139extern bool sRef_definitelyNull (sRef p_s);
140
28bf4b0b 141extern bool sRef_definitelyNullContext (sRef p_s);
142extern bool sRef_definitelyNullAltContext (sRef p_s);
143
885824d3 144extern void sRef_setNullError (sRef p_s);
145extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc);
146extern void sRef_setNotNull (sRef p_s, fileloc p_loc);
147extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc);
148extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc);
149extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
150extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
151
0e41eb0e 152extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
153extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
6483a926 154extern /*@falsewhennull@*/ bool sRef_isReasonable (sRef p_s) /*@*/ ;
885824d3 155
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)
160
161extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ;
162extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
163extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ;
164extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
165
885824d3 166extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
167
0e41eb0e 168extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
169extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
170extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
171extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
172extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 173
174extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
175# define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
176
177# define sRef_isKnown(s) (sRef_isValid(s) && (s)->kind != SK_UNKNOWN)
178
179extern 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)
393e573f 182
183extern bool sRef_isSomewhatMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
184# define sRef_isSomewhatMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \
185 && (s)->kind != SK_TYPE)
885824d3 186extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
187# define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW)
188
189extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ;
190# define sRef_isType(s) (sRef_isValid(s) && (s)->kind == SK_TYPE)
191
192extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ;
193# define sRef_isSafe(s) (sRef_isValid(s) && (s)->safe)
194
195extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ;
196# define sRef_isUnsafe(s) (sRef_isValid(s) && !(s)->safe)
197
198extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ;
199# define sRef_clearAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR)
200
201extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ;
202# define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN)
203
204extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 205
206extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
207# define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
208
0e41eb0e 209extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 210# define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ)
211
212extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
213extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f);
214
215extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ;
216extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ;
217extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
218
219extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ;
220extern void sRef_clearDerived (sRef p_s);
221extern void sRef_clearDerivedComplete (sRef p_s);
222extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s);
223
28bf4b0b 224extern /*@observer@*/ sRefSet sRef_derivedFields (/*@temp@*/ sRef p_rec) /*@*/ ;
885824d3 225extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ;
226extern bool sRef_isDirectParam (sRef p_s) /*@*/ ;
227extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr);
228extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ;
229
230extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc);
231extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ;
232
233extern void sRef_destroyMod (void) /*@modifies internalState@*/ ;
234
235extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s);
236
237extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
238
239extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
240
0e41eb0e 241extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 242# define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
243
244extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
245
246extern bool sRef_isSystemState (sRef p_s) /*@*/ ;
28bf4b0b 247extern bool sRef_isGlobalMarker (sRef p_s) /*@*/ ;
885824d3 248extern bool sRef_isInternalState (sRef p_s) /*@*/ ;
249extern bool sRef_isResult (sRef p_s) /*@*/ ;
250extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ;
251extern bool sRef_isSpecState (sRef p_s) /*@*/ ;
252extern bool sRef_isNothing (sRef p_s) /*@*/ ;
253
28bf4b0b 254extern bool sRef_isFileOrGlobalScope (sRef p_s) /*@*/ ;
885824d3 255extern bool sRef_isReference (sRef p_s) /*@*/ ;
256
257extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ;
258extern ctype sRef_getType (sRef p_s) /*@*/ ;
259
28bf4b0b 260extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ;
261
0e41eb0e 262extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
263extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
264extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
265extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ;
266extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
267extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
268extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
885824d3 269
270extern void sRef_setType (sRef p_s, ctype p_t);
271extern void sRef_setTypeFull (sRef p_s, ctype p_t);
272extern void sRef_mergeNullState (sRef p_s, nstate p_n);
28bf4b0b 273extern void sRef_setLastReference (/*@temp@*/ sRef p_s, /*@exposed@*/ sRef p_ref, fileloc p_loc);
885824d3 274extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
275extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
276extern bool sRef_isIReference (sRef p_s) /*@*/ ;
277extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ;
278extern bool sRef_isModified (sRef p_s) /*@*/ ;
279
280extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ;
281extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ;
282extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ;
28bf4b0b 283extern bool sRef_sameObject (sRef p_s1, sRef p_s2) /*@*/ ;
885824d3 284extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ;
285extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ;
286extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ;
287extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ;
288extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ;
289extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ;
290extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ;
291extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ;
292extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
293extern int sRef_getIndex (sRef p_arr) /*@*/ ;
294extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s);
2e127cb8 295
296/* Use this one to clear after error */
297extern void sRef_setDefinedCompleteDirect (sRef p_s, fileloc p_loc) ;
298
299extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc) ;
300extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc) ;
885824d3 301extern int sRef_getParam (sRef p_s) /*@*/ ;
302extern int sRef_lexLevel (sRef p_s) /*@*/ ;
303extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind);
28bf4b0b 304
885824d3 305extern /*@exposed@*/ sRef
3120b462 306 sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base)
885824d3 307 /*@modifies p_s, p_base@*/ ;
308
80489f0a 309extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_warningstream@*/ ;
885824d3 310
28bf4b0b 311extern void sRef_enterFunctionScope (void) /*@modifies internalState@*/ ;
312extern void sRef_setGlobalScope (void) /*@modifies internalState@*/ ;
313extern bool sRef_inGlobalScope (void) /*@*/ ;
314extern void sRef_exitFunctionScope (void) /*@modifies internalState@*/ ;
315extern void sRef_clearGlobalScopeSafe (void) /*@modifies internalState@*/ ;
316extern void sRef_setGlobalScopeSafe (void) /*@modifies internalState@*/ ;
885824d3 317
318extern /*@notnull@*/ /*@exposed@*/ sRef
319 sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr);
320extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
321extern /*@exposed@*/ sRef
28bf4b0b 322 sRef_buildField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f)
885824d3 323 /*@modifies p_rec@*/ ;
324extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t)
325 /*@modifies p_t@*/ ;
326
327extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t);
328extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ;
329
0e41eb0e 330extern /*@falsewhennull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
885824d3 331
332extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ;
333
28bf4b0b 334extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (/*@exposed@*/ sRef p_arr) /*@*/ ;
885824d3 335extern /*@notnull@*/ /*@exposed@*/ sRef
28bf4b0b 336 sRef_makeArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
885824d3 337extern /*@notnull@*/ /*@dependent@*/ sRef
338 sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
339extern /*@notnull@*/ /*@dependent@*/ sRef
6970c11b 340 sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo);
885824d3 341extern /*@notnull@*/ /*@dependent@*/ sRef
342 sRef_makeConst (ctype p_ct);
343extern /*@exposed@*/ sRef
344 sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
345extern /*@notnull@*/ /*@dependent@*/ sRef
6970c11b 346 sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo);
885824d3 347extern /*@exposed@*/ sRef
28bf4b0b 348 sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
885824d3 349extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
350extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef
351 sRef_makeObject (ctype p_o) /*@*/ ;
352extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
6970c11b 353extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ;
28bf4b0b 354extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ;
885824d3 355extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
356extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;
885824d3 357
28bf4b0b 358extern /*@dependent@*/ sRef sRef_makeUnknown (void) /*@*/ ;
359extern /*@dependent@*/ sRef sRef_makeNothing (void) /*@*/ ;
360extern /*@dependent@*/ sRef sRef_makeInternalState (void) /*@*/ ;
361extern /*@dependent@*/ sRef sRef_makeSpecState (void) /*@*/ ;
362extern /*@dependent@*/ sRef sRef_makeGlobalMarker (void) /*@*/ ;
363extern /*@dependent@*/ sRef sRef_makeSystemState (void) /*@*/ ;
885824d3 364
b072092f 365extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (ctype) /*@*/ ;
885824d3 366extern /*@exposed@*/ sRef
367 sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue)
368 /*@modifies p_s@*/;
369
370extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/;
371
28bf4b0b 372extern /*@notnull@*/ /*@dependent@*/ sRef
373 sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name) ;
885824d3 374
375extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ;
376extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s);
377
378extern /*@exposed@*/ sRef
379 sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args)
380 /*@modifies p_s@*/ ;
381
ef2aa32a 382 /*
383 drl7x
384 added function
385 12/24/2000
386 */
4ab867d6 387
28bf4b0b 388/*@only@*/ constraintExpr sRef_fixConstraintParam (/*@observer@*/ sRef p_s, /*@observer@*/ /*@temp@*/ exprNodeList p_args);
ef2aa32a 389
885824d3 390extern bool sRef_isUnionField (sRef p_s);
391extern void sRef_setModified (sRef p_s);
392
393extern void sRef_resetState (sRef p_s);
394extern void sRef_resetStateComplete (sRef p_s);
395
396extern void sRef_storeState (sRef p_s);
397extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ;
398extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ;
399
400extern /*@observer@*/ uentry sRef_getUentry (sRef p_s);
401
402extern cstring sRef_dump (sRef p_s) /*@*/ ;
403extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ;
404extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ;
405extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ;
406
407extern /*@only@*/ sRef sRef_saveCopy (sRef p_s);
408extern /*@dependent@*/ sRef sRef_copy (sRef p_s);
409
410extern cstring sRef_unparseState (sRef p_s) /*@*/ ;
411extern ynm sRef_isWriteable (sRef p_s) /*@*/ ;
3e3ec469 412extern ynm sRef_isValidLvalue (sRef p_s) /*@*/ ;
885824d3 413extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ;
414extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ;
80489f0a 415extern void sRef_showExpInfo (sRef p_s) /*@modifies g_warningstream*/ ;
885824d3 416extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
417extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
418extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
419extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
420extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
421extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
422extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
423extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
424extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
80489f0a 425extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
426extern void sRef_showMetaStateInfo (sRef p_s, cstring p_key) /*@modifies g_warningstream@*/ ;
427extern void sRef_showNullInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
428extern void sRef_showStateInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
885824d3 429extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ;
430extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
431extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
432extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
433extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
434extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ;
0e41eb0e 435extern /*@falsewhennull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
436extern /*@falsewhennull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
885824d3 437
438extern int sRef_getScope (sRef p_s) /*@*/ ;
439extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ;
440
441/* must be real function (passed as function param) */
0e41eb0e 442extern /*@falsewhennull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
443extern /*@falsewhennull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
885824d3 444extern bool sRef_isStateLive (sRef p_s) /*@*/ ;
0e41eb0e 445extern /*@falsewhennull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
446extern /*@nullwhentrue@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
885824d3 447extern bool sRef_isUnuseable (sRef p_s) /*@*/ ;
448
449extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t)
450 /*@modifies p_t@*/ ;
451
452extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t)
453 /*@modifies p_t@*/ ;
454
455extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ;
456
0e41eb0e 457extern /*@falsewhennull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
885824d3 458
459extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ;
460# define sRef_isUndefGlob(s) \
461 ((sRef_isValid(s)) \
462 && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED))
463
464extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ;
465# define sRef_isKilledGlob(s) \
466 ((sRef_isValid(s)) \
467 && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED))
468
469extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ;
470# define sRef_isRelDef(s) \
471 ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF))
472
473extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ;
474# define sRef_isPartial(s) \
475 ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL))
476
477extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
478# define sRef_isStateSpecial(s) \
479 ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL))
480
28bf4b0b 481extern bool sRef_makeStateSpecial (sRef p_s)
482 /*@modifies p_s@*/
483 /* returns false is sRef already has an inconsistend defstate */ ;
484
885824d3 485extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ;
486# define sRef_isStateDefined(s) \
487 ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \
488 || (s)->defstate == SS_RELDEF))
489
490extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ;
491# define sRef_isAnyDefined(s) ((sRef_isValid(s)) && \
492 (((s)->defstate == SS_DEFINED) \
493 || ((s)->defstate == SS_RELDEF) \
494 || ((s)->defstate == SS_PARTIAL)))
495
0e41eb0e 496extern /*@falsewhennull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 497# define sRef_isPdefined(s) \
498 ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED))
499
500extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ;
501
502extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ;
503# define sRef_isStateUnknown(s) \
504 ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN))
505
0e41eb0e 506extern /*@falsewhennull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 507# define sRef_isRefCounted(s) \
508 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED))
509
0e41eb0e 510extern /*@falsewhennull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 511# define sRef_isNewRef(s) \
512 ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF))
513
0e41eb0e 514extern /*@falsewhennull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
885824d3 515# define sRef_isKillRef(s) \
516 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF))
517
518extern bool sRef_isOnly (sRef p_s) /*@*/ ;
519extern bool sRef_isDependent (sRef p_s) /*@*/ ;
520extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ;
521extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ;
522
523extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ;
524# define sRef_isKept(s) \
525 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT))
526
527extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ;
528
529extern bool sRef_isStack (sRef p_s) /*@*/ ;
530extern bool sRef_isLocalState (sRef p_s) /*@*/ ;
531extern bool sRef_isUnique (sRef p_s) /*@*/ ;
532extern bool sRef_isShared (sRef p_s) /*@*/ ;
533extern bool sRef_isExposed (sRef p_s) /*@*/ ;
534extern bool sRef_isObserver (sRef p_s) /*@*/ ;
535extern bool sRef_isFresh (sRef p_s) /*@*/ ;
536
537extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ;
538# define sRef_isRefsField(s) \
539 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS))
540
541extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ;
542extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ;
543
544extern exkind sRef_getExKind (sRef p_s) /*@*/ ;
545extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ;
546extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ;
547extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/;
548
549extern bool sRef_isAnyParam (sRef p_s) /*@*/ ;
28bf4b0b 550extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@temp@*/ sRef p_s) /*@*/ ;
885824d3 551extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ;
552
28bf4b0b 553extern /*@exposed@*/ sRef sRef_constructPointer (/*@exposed@*/ sRef p_t) /*@modifies p_t*/ ;
885824d3 554extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ;
555extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ;
556extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ;
557extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ;
558extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ;
559extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
560extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ;
561extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ;
562extern bool sRef_isExternal (sRef p_s) /*@*/ ;
563extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ;
564extern cstring sRef_unparseFull (sRef p_s) /*@*/ ;
565extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ;
566extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
567 /*@modifies p_res, p_other@*/ ;
568extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
569 /*@modifies p_res, p_other@*/ ;
570extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other)
571 /*@modifies p_res@*/ ;
28bf4b0b 572extern void sRef_mergeStateQuietReverse (/*@dependent@*/ sRef p_res, /*@dependent@*/ sRef p_other)
885824d3 573 /*@modifies p_res@*/ ;
574extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue)
575 /*@modifies p_s@*/ ;
576extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ;
577extern bool sRef_modInFunction (void) /*@*/ ;
578extern void sRef_clearAliasState (sRef p_s, fileloc p_loc)
579 /*@modifies p_s@*/ ;
580extern void sRef_setPartial (sRef p_s, fileloc p_loc)
581 /*@modifies p_s@*/ ;
582extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns)
583 /*@modifies p_set@*/ ;
584
585extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ;
586
28bf4b0b 587extern /*@dependent@*/ sRef sRef_makeDerived (/*@exposed@*/ sRef p_t);
885824d3 588
589extern sstate sRef_getDefState (sRef p_s) /*@*/ ;
590extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc);
591extern void sRef_showRefLost (sRef p_s);
592extern void sRef_showRefKilled (sRef p_s);
593extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s);
594
28bf4b0b 595extern void sRef_reflectAnnotation (sRef p_s, annotationInfo p_a, fileloc p_loc);
596extern /*@observer@*/ valueTable sRef_getValueTable (sRef p_s) /*@*/ ;
597
885824d3 598extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode),
599 /*@null@*/ bool (p_checkAliases) (sRef),
600 sRef p_s, exprNode p_e, exprNode p_err);
601extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s);
602
603extern void sRef_showStateInconsistent (sRef p_s);
604
605extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc);
606
607extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc);
608
609extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ;
610
611extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ;
612extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ;
613
614extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ;
615
616extern bool sRef_hasName (sRef p_s) /*@*/ ;
885824d3 617extern void sRef_free (/*@only@*/ sRef p_s);
885824d3 618extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
619
1ac6313d 620/* start modifications */
621/* functions for making modification to null-term info */
28bf4b0b 622extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct s_bbufinfo p_b, fileloc p_loc);
623extern struct s_bbufinfo sRef_getNullTerminatedState(sRef p_s);
1ac6313d 624extern void sRef_setNullTerminatedState (sRef p_s);
625extern void sRef_setPossiblyNullTerminatedState (sRef p_s);
626extern void sRef_setNotNullTerminatedState (sRef p_s);
4cccc6ad 627extern void sRef_setSize(sRef p_s, int p_size);
628extern void sRef_setLen(sRef p_s, int p_len);
1ac6313d 629
630extern int sRef_getSize(sRef p_s);
84c9ffbf 631
632/*@-nullderef@*/
633
1ac6313d 634#define sRef_getSize(p_s) \
ef2aa32a 635 ((p_s)->bufinfo.size)
1ac6313d 636
637extern int sRef_getLen(sRef p_s);
638#define sRef_getLen(p_s) \
ef2aa32a 639 ((p_s)->bufinfo.len)
1ac6313d 640
28bf4b0b 641extern bool sRef_hasBufStateInfo(sRef p_s);
1ac6313d 642# define sRef_hasBufStateInfo(p_s) \
643 (sRef_isValid(p_s))
644
84c9ffbf 645extern bool sRef_isNullTerminated(/*@sef@*/sRef p_s);
1ac6313d 646# define sRef_isNullTerminated(p_s) \
84c9ffbf 647 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
1ac6313d 648 == BB_NULLTERMINATED) : FALSE)
649
84c9ffbf 650extern bool sRef_isPossiblyNullTerminated(/*@sef@*/sRef p_s);
1ac6313d 651# define sRef_isPossiblyNullTerminated(p_s) \
bb7c2085 652 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
1ac6313d 653 == BB_POSSIBLYNULLTERMINATED) : FALSE)
654
84c9ffbf 655extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s);
1ac6313d 656# define sRef_isNotNullTerminated(p_s) \
84c9ffbf 657 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
1ac6313d 658 == BB_NOTNULLTERMINATED) : FALSE)
34f0c5e7 659
84c9ffbf 660/*@=nullderef@*/
661
662
34f0c5e7 663 /*drl7x 11/28/00*/
37ae0b5e 664extern bool sRef_isFixedArray (sRef p_s) /*@*/;
665extern size_t sRef_getArraySize (sRef p_s) /*@*/;
34f0c5e7 666
4cccc6ad 667extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s);
28bf4b0b 668extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ;
669
1ac6313d 670/* end modifications */
671
28bf4b0b 672extern void sRef_setMetaStateValueComplete (sRef p_s, cstring p_key, int p_value, fileloc p_loc)
673 /*@modifies p_s@*/ ;
674
675extern void sRef_setMetaStateValue (sRef p_s, cstring p_key, int p_value, fileloc p_loc)
676 /*@modifies p_s@*/ ;
677
678extern /*@observer@*/ stateValue sRef_getMetaStateValue (sRef p_s, cstring p_key) /*@*/ ;
679
680extern bool sRef_checkMetaStateValue (sRef p_s, cstring p_key, int p_value)
681 /*@modifies p_s@*/ ;
682
b9904f57 683extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@*/ ;
684extern bool sRef_hasValue (sRef p_s) /*@*/ ;
685extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ;
686
27c9e640 687extern /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ;
2934b455 688
1d239d69 689extern void
690sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc)
691 /*@modifies p_s@*/ ;
692
693extern void
694sRef_aliasSetCompleteParam (void (p_predf) (sRef, int, fileloc), sRef p_s,
695 int p_kind, fileloc p_loc)
696 /*@modifies p_s@*/ ;
697
68de3f33 698extern void
699sRef_aliasSetCompleteAlkParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s,
700 alkind p_kind, fileloc p_loc)
701 /*@modifies p_s@*/ ;
702
6483a926 703# ifdef DEBUGSPLINT
02b84d4b 704extern void sRef_checkCompletelyReasonable (sRef p_s) /*@modifies g_errorstream@*/ ;
6483a926 705# endif
706
885824d3 707# else
708# error "Multiple include"
709# endif
710
711
712
713
714
715
716
717
718
719
720
721
722
git-cvsimport mirror of splint
This page took 0.619431 seconds and 5 git commands to generate.