]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
28bf4b0b | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
6 | ** This program is free software; you can redistribute it and/or modify it | |
7 | ** under the terms of the GNU General Public License as published by the | |
8 | ** Free Software Foundation; either version 2 of the License, or (at your | |
9 | ** option) any later version. | |
10 | ** | |
11 | ** This program is distributed in the hope that it will be useful, but | |
12 | ** WITHOUT ANY WARRANTY; without even the implied warranty of | |
13 | ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU | |
14 | ** General Public License for more details. | |
15 | ** | |
16 | ** The GNU General Public License is available from http://www.gnu.org/ or | |
17 | ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, | |
18 | ** MA 02111-1307, USA. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
28bf4b0b | 23 | */ |
24 | /* | |
25 | ** stateClauseList.c | |
26 | */ | |
27 | ||
1b8ae690 | 28 | # include "splintMacros.nf" |
28bf4b0b | 29 | # include "basic.h" |
30 | ||
31 | static /*@notnull@*/ stateClauseList stateClauseList_new (void) | |
32 | { | |
33 | stateClauseList s = (stateClauseList) dmalloc (sizeof (*s)); | |
34 | ||
35 | s->nelements = 0; | |
36 | s->nspace = stateClauseListBASESIZE; | |
37 | s->elements = (stateClause *) | |
38 | dmalloc (sizeof (*s->elements) * stateClauseListBASESIZE); | |
39 | ||
40 | return (s); | |
41 | } | |
42 | ||
43 | static void | |
44 | stateClauseList_grow (stateClauseList s) | |
45 | { | |
46 | int i; | |
47 | stateClause *newelements; | |
48 | ||
49 | llassert (stateClauseList_isDefined (s)); | |
50 | ||
51 | s->nspace += stateClauseListBASESIZE; | |
52 | ||
53 | newelements = (stateClause *) | |
54 | dmalloc (sizeof (*newelements) * (s->nelements + s->nspace)); | |
55 | ||
56 | for (i = 0; i < s->nelements; i++) | |
57 | { | |
58 | newelements[i] = s->elements[i]; | |
59 | } | |
60 | ||
61 | sfree (s->elements); | |
62 | s->elements = newelements; | |
63 | } | |
64 | ||
65 | stateClauseList stateClauseList_add (stateClauseList s, stateClause el) | |
66 | { | |
67 | DPRINTF (("Adding: %s", stateClause_unparse (el))); | |
68 | ||
69 | if (stateClauseList_isUndefined (s)) | |
70 | { | |
71 | s = stateClauseList_new (); | |
72 | } | |
73 | else | |
74 | { | |
75 | stateClauseList_elements (s, cl) | |
76 | { | |
77 | if (stateClause_sameKind (cl, el)) | |
78 | { | |
79 | voptgenerror | |
80 | (FLG_SYNTAX, | |
81 | message ("Multiple %q clauses for one function (ignoring second)", | |
82 | stateClause_unparseKind (cl)), | |
83 | g_currentloc); | |
84 | ||
85 | stateClause_free (el); | |
86 | return s; | |
87 | } | |
88 | } end_stateClauseList_elements ; | |
89 | } | |
90 | ||
91 | if (s->nspace <= 0) | |
92 | { | |
93 | stateClauseList_grow (s); | |
94 | } | |
95 | ||
96 | s->nspace--; | |
97 | s->elements[s->nelements] = el; | |
98 | s->nelements++; | |
99 | ||
100 | return s; | |
101 | } | |
102 | ||
103 | cstring stateClauseList_unparse (stateClauseList s) | |
104 | { | |
105 | cstring st = cstring_undefined; | |
106 | int i; | |
107 | ||
108 | if (stateClauseList_isDefined (s)) | |
109 | { | |
110 | for (i = 0; i < stateClauseList_size (s); i++) | |
111 | { | |
112 | if (i == 0) | |
113 | { | |
114 | st = message ("%q;", stateClause_unparse (s->elements[i])); | |
115 | } | |
116 | else | |
117 | st = message ("%q %q;", st, stateClause_unparse (s->elements[i])); | |
118 | } | |
119 | } | |
120 | ||
121 | return (st); | |
122 | } | |
123 | ||
124 | stateClauseList stateClauseList_copy (stateClauseList s) | |
125 | { | |
126 | if (stateClauseList_isDefined (s)) | |
127 | { | |
128 | stateClauseList t = (stateClauseList) dmalloc (sizeof (*t)); | |
129 | int i; | |
130 | ||
131 | t->nelements = s->nelements; | |
132 | t->nspace = 0; | |
133 | ||
134 | if (s->nelements > 0) | |
135 | { | |
136 | t->elements = (stateClause *) dmalloc (sizeof (*t->elements) * t->nelements); | |
137 | for (i = 0; i < s->nelements; i++) | |
138 | { | |
139 | t->elements[i] = stateClause_copy (s->elements[i]); | |
140 | } | |
141 | } | |
142 | else | |
143 | { | |
144 | t->elements = NULL; | |
145 | } | |
146 | ||
147 | return t; | |
148 | } | |
149 | else | |
150 | { | |
151 | return stateClauseList_undefined; | |
152 | } | |
153 | } | |
154 | ||
155 | void | |
156 | stateClauseList_free (stateClauseList s) | |
157 | { | |
158 | if (!stateClauseList_isUndefined (s)) | |
159 | { | |
160 | int i; | |
161 | ||
162 | for (i = 0; i < s->nelements; i++) | |
163 | { | |
164 | stateClause_free (s->elements[i]); | |
165 | } | |
166 | ||
167 | sfree (s->elements); | |
168 | sfree (s); | |
169 | } | |
170 | } | |
171 | ||
172 | cstring stateClauseList_dump (stateClauseList s) | |
173 | { | |
174 | cstring st = cstring_undefined; | |
175 | ||
176 | if (stateClauseList_isUndefined (s)) return st; | |
177 | ||
178 | stateClauseList_elements (s, current) | |
179 | { | |
180 | st = message ("%q%q$", st, stateClause_dump (current)); | |
181 | } end_stateClauseList_elements; | |
182 | ||
183 | return st; | |
184 | } | |
185 | ||
186 | stateClauseList stateClauseList_undump (char **s) | |
187 | { | |
188 | char c; | |
189 | stateClauseList pn = stateClauseList_new (); | |
190 | int paramno = 0; | |
191 | ||
192 | c = **s; | |
193 | ||
194 | while (c != '#' && c != '@') | |
195 | { | |
196 | stateClause sc = stateClause_undump (s); | |
197 | ||
198 | pn = stateClauseList_add (pn, sc); | |
199 | reader_checkChar (s, '$'); | |
200 | c = **s; | |
201 | paramno++; | |
202 | } | |
203 | ||
204 | return pn; | |
205 | } | |
206 | ||
207 | int stateClauseList_compare (stateClauseList s1, stateClauseList s2) | |
208 | { | |
209 | if (stateClauseList_isUndefined (s1) | |
210 | && stateClauseList_isUndefined (s2)) | |
211 | { | |
212 | return 0; | |
213 | } | |
214 | else | |
215 | { | |
b7e84605 | 216 | if (s1 - s2 > 0) /* evans 2001-08-21: was (int) s1 > (int) s2) */ |
28bf4b0b | 217 | { |
218 | return 1; | |
219 | } | |
220 | else | |
221 | { | |
222 | return -1; | |
223 | } | |
224 | } | |
225 | } | |
226 | ||
227 | static /*@exposed@*/ sRefSet | |
228 | stateClauseList_getClause (stateClauseList s, stateClause k) | |
229 | { | |
230 | stateClauseList_elements (s, el) | |
231 | { | |
232 | if (stateClause_matchKind (el, k)) | |
233 | { | |
234 | return stateClause_getRefs (el); | |
235 | } | |
236 | } end_stateClauseList_elements ; | |
237 | ||
238 | return sRefSet_undefined; | |
239 | } | |
240 | ||
241 | void stateClauseList_checkAll (uentry ue) | |
242 | { | |
243 | stateClauseList clauses = uentry_getStateClauseList (ue); | |
244 | sRef res = uentry_getSref (ue); | |
245 | bool specialResult = FALSE; | |
246 | ||
247 | DPRINTF (("Check state clauses: %s", uentry_unparseFull (ue))); | |
248 | ||
249 | stateClauseList_elements (clauses, cl) | |
250 | { | |
251 | bool isPre = stateClause_isBeforeOnly (cl); | |
252 | ||
253 | if (stateClause_isGlobal (cl)) | |
254 | { | |
b73d1009 | 255 | ; |
28bf4b0b | 256 | } |
257 | else | |
258 | { | |
259 | sRefSet refs = stateClause_getRefs (cl); | |
260 | ||
261 | sRefSet_allElements (refs, el) | |
262 | { | |
263 | sRef rb = sRef_getRootBase (el); | |
264 | ||
265 | DPRINTF (("Check: %s", sRef_unparse (el))); | |
b7e84605 | 266 | |
267 | if (sRef_isResult (rb)) | |
268 | { | |
269 | /* | |
270 | ** The result type is now know, need to set it: | |
271 | */ | |
272 | ||
273 | if (ctype_isUnknown (sRef_getType (rb))) | |
274 | { | |
275 | ctype utype = uentry_getType (ue); | |
276 | llassert (ctype_isFunction (utype)); | |
277 | ||
278 | sRef_setTypeFull (rb, ctype_getReturnType (utype)); | |
279 | DPRINTF (("el: %s", sRef_unparseFull (el))); | |
280 | } | |
281 | } | |
28bf4b0b | 282 | |
283 | if (stateClause_setsMetaState (cl)) | |
284 | { | |
285 | qual q = stateClause_getMetaQual (cl); | |
286 | annotationInfo qa = qual_getAnnotationInfo (q); | |
287 | ||
288 | if (!annotationInfo_matchesContextRef (qa, el)) | |
289 | { | |
290 | if (optgenerror | |
291 | (FLG_ANNOTATIONERROR, | |
0bf5022d | 292 | message ("Attribute annotation %s used on inappropriate reference %q in %q clause of %q: %q", |
28bf4b0b | 293 | qual_unparse (q), |
294 | sRef_unparse (el), | |
295 | stateClause_unparseKind (cl), | |
296 | uentry_getName (ue), | |
297 | stateClause_unparse (cl)), | |
298 | uentry_whereLast (ue))) | |
299 | { | |
300 | /*@i! annotationInfo_showContextError (ainfo, ue); */ | |
301 | } | |
302 | } | |
303 | } | |
304 | ||
305 | if (sRef_isResult (rb)) | |
306 | { | |
307 | if (isPre) | |
308 | { | |
309 | voptgenerror | |
310 | (FLG_INCONDEFS, | |
311 | message ("Function result is used in %q clause of %q " | |
312 | "(%q applies to the state before function is " | |
313 | "called, so should not use result): %q", | |
314 | stateClause_unparseKind (cl), | |
315 | uentry_getName (ue), | |
316 | stateClause_unparseKind (cl), | |
317 | sRef_unparse (el)), | |
318 | uentry_whereLast (ue)); | |
319 | } | |
320 | else | |
321 | { | |
322 | if (!sRef_isStateSpecial (res)) | |
323 | { | |
ccf0a4a8 | 324 | DPRINTF (("Here we are: %s", sRef_unparseFull (res))); |
325 | ||
28bf4b0b | 326 | if (!specialResult) |
327 | { | |
328 | sstate pstate = sRef_getDefState (res); | |
329 | ||
330 | if (!sRef_makeStateSpecial (res)) | |
331 | { | |
ccf0a4a8 | 332 | if (optgenerror |
333 | (FLG_INCONDEFS, | |
334 | message ("Function result is used in %q clause of %q " | |
335 | "but was previously annotated with %s: %q", | |
336 | stateClause_unparseKind (cl), | |
337 | uentry_getName (ue), | |
338 | sstate_unparse (pstate), | |
339 | sRef_unparse (el)), | |
340 | uentry_whereLast (ue))) | |
341 | { | |
342 | specialResult = TRUE; | |
343 | } | |
344 | } | |
28bf4b0b | 345 | } |
346 | } | |
347 | ||
ccf0a4a8 | 348 | DPRINTF (("Fixing result type! %s", sRef_unparseFull (el))); |
28bf4b0b | 349 | (void) sRef_fixResultType (el, sRef_getType (res), ue); |
350 | } | |
351 | } | |
352 | else if (sRef_isParam (rb)) | |
353 | { | |
354 | DPRINTF (("Make special: %s", sRef_unparseFull (rb))); | |
355 | ||
356 | if (!sRef_makeStateSpecial (rb)) | |
357 | { | |
358 | if (fileloc_isXHFile (uentry_whereLast (ue))) | |
359 | { | |
360 | ; /* Okay to override in .xh files */ | |
361 | } | |
3e3ec469 | 362 | else if (stateClause_isQual (cl)) |
363 | { | |
364 | ; /* qual clauses don't interfere with definition state */ | |
365 | } | |
28bf4b0b | 366 | else |
367 | { | |
368 | voptgenerror | |
369 | (FLG_INCONDEFS, | |
370 | message ("Reference %q used in %q clause of %q, " | |
371 | "but was previously annotated with %s: %q", | |
372 | sRef_unparse (rb), | |
373 | stateClause_unparseKind (cl), | |
374 | uentry_getName (ue), | |
375 | sstate_unparse (sRef_getDefState (res)), | |
376 | sRef_unparse (el)), | |
377 | uentry_whereLast (ue)); | |
378 | } | |
379 | } | |
380 | ||
381 | DPRINTF (("Made special: %s", sRef_unparseFull (rb))); | |
382 | } | |
383 | else if (sRef_isInvalid (rb)) | |
384 | { | |
385 | /*@innercontinue@*/ continue; | |
386 | } | |
387 | else | |
388 | { | |
389 | BADBRANCHCONT; | |
390 | /*@innercontinue@*/ continue; | |
391 | } | |
392 | ||
393 | if (stateClause_isMemoryAllocation (cl)) | |
394 | { | |
395 | if (!ctype_isVisiblySharable (sRef_getType (el))) | |
396 | { | |
397 | voptgenerror | |
398 | (FLG_ANNOTATIONERROR, | |
b73d1009 | 399 | /*@-sefparams@*/ /* This is okay because its fresh storage. */ |
28bf4b0b | 400 | message |
401 | ("%q clauses includes %q of " | |
402 | "non-dynamically allocated type %s", | |
403 | cstring_capitalizeFree (stateClause_unparseKind (cl)), | |
404 | sRef_unparse (el), | |
405 | ctype_unparse (sRef_getType (el))), | |
406 | uentry_whereLast (ue)); | |
407 | /*@=sefparams@*/ | |
408 | } | |
409 | } | |
410 | ||
411 | } end_sRefSet_allElements ; | |
412 | } | |
413 | } end_stateClauseList_elements ; | |
414 | } | |
415 | ||
416 | void stateClauseList_checkEqual (uentry old, uentry unew) | |
417 | { | |
418 | stateClauseList oldClauses = uentry_getStateClauseList (old); | |
419 | stateClauseList newClauses = uentry_getStateClauseList (unew); | |
420 | ||
421 | if (stateClauseList_isDefined (newClauses)) | |
422 | { | |
423 | stateClauseList_elements (newClauses, cl) | |
424 | { | |
425 | if (stateClause_isGlobal (cl)) | |
426 | { | |
427 | ; | |
428 | } | |
429 | else | |
430 | { | |
431 | sRefSet sc = stateClauseList_getClause (oldClauses, cl); | |
432 | ||
433 | if (!sRefSet_equal (sc, stateClause_getRefs (cl))) | |
434 | { | |
435 | if (optgenerror | |
436 | (FLG_INCONDEFS, | |
437 | message ("Function %q %rdeclared with inconsistent %q clause: %q", | |
438 | uentry_getName (old), | |
439 | uentry_isDeclared (old), | |
440 | stateClause_unparseKind (cl), | |
441 | sRefSet_unparsePlain (stateClause_getRefs (cl))), | |
442 | g_currentloc)) | |
443 | { | |
444 | uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc)); | |
445 | } | |
446 | } | |
447 | } | |
448 | } end_stateClauseList_elements ; | |
449 | ||
450 | stateClauseList_elements (oldClauses, cl) | |
451 | { | |
452 | if (stateClause_isGlobal (cl)) | |
453 | { | |
b73d1009 | 454 | ; /* Don't handle globals for now */ |
28bf4b0b | 455 | } |
456 | else | |
457 | { | |
458 | sRefSet sc = stateClauseList_getClause (newClauses, cl); | |
459 | ||
460 | if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (stateClause_getRefs (cl))) | |
461 | { | |
462 | if (optgenerror | |
463 | (FLG_INCONDEFS, | |
464 | message ("Function %q %rdeclared without %q clause (either " | |
465 | "use no special clauses in redeclaration, or " | |
466 | "they must match exactly: %q", | |
467 | uentry_getName (old), | |
468 | uentry_isDeclared (old), | |
469 | stateClause_unparseKind (cl), | |
470 | sRefSet_unparsePlain (stateClause_getRefs (cl))), | |
471 | g_currentloc)) | |
472 | { | |
473 | uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc)); | |
474 | } | |
475 | } | |
476 | } | |
477 | } end_stateClauseList_elements ; | |
478 | } | |
479 | } | |
480 | ||
481 | ||
482 |