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