]>
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 | ||
1b8ae690 | 25 | # include "splintMacros.nf" |
28bf4b0b | 26 | # include "basic.h" |
27 | ||
4caf866b | 28 | # ifdef WIN32 |
29 | /* | |
30 | ** Make Microsoft VC++ happy: its control checking produces too | |
31 | ** many spurious warnings. | |
32 | */ | |
33 | ||
34 | # pragma warning (disable:4715) | |
35 | # endif | |
36 | ||
16c024b5 | 37 | static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ; |
38 | ||
28bf4b0b | 39 | void stateInfo_free (/*@only@*/ stateInfo a) |
40 | { | |
41 | if (a != NULL) | |
42 | { | |
43 | fileloc_free (a->loc); | |
44 | sfree (a); | |
45 | } | |
46 | } | |
47 | ||
48 | /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo old, stateInfo newinfo) | |
49 | /* | |
50 | ** returns an stateInfo with the same value as new. May reuse the | |
51 | ** storage of old. (i.e., same effect as copy, but more | |
52 | ** efficient.) | |
53 | */ | |
54 | { | |
55 | if (old == NULL) | |
56 | { | |
16c024b5 | 57 | DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo))); |
6fcd0b1e | 58 | return stateInfo_copy (newinfo); |
28bf4b0b | 59 | } |
60 | else if (newinfo == NULL) | |
61 | { | |
62 | stateInfo_free (old); | |
63 | return NULL; | |
64 | } | |
65 | else | |
66 | { | |
16c024b5 | 67 | if (fileloc_equal (old->loc, newinfo->loc) |
68 | && old->action == newinfo->action | |
69 | /*@-abstractcompare@*/ && old->ref == newinfo->ref /*@=abstractcompare@*/) | |
70 | { | |
71 | /* | |
72 | ** Duplicate (change through alias most likely) | |
73 | ** don't add this info | |
74 | */ | |
75 | ||
76 | return old; | |
77 | } | |
78 | else | |
79 | { | |
80 | stateInfo snew = stateInfo_makeRefLoc (newinfo->ref, | |
81 | newinfo->loc, newinfo->action); | |
82 | llassert (snew->previous == NULL); | |
83 | snew->previous = old; | |
84 | DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); | |
85 | return snew; | |
86 | } | |
28bf4b0b | 87 | } |
28bf4b0b | 88 | } |
89 | ||
6d43e86c | 90 | static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo stinfo) |
16c024b5 | 91 | /* Sorts in reverse location order */ |
28bf4b0b | 92 | { |
6d43e86c | 93 | DPRINTF (("Sorting: %s", stateInfo_unparse (stinfo))); |
16c024b5 | 94 | |
6d43e86c | 95 | if (stinfo == NULL || stinfo->previous == NULL) |
28bf4b0b | 96 | { |
6d43e86c | 97 | return stinfo; |
28bf4b0b | 98 | } |
99 | else | |
100 | { | |
6d43e86c | 101 | stateInfo snext = stateInfo_sort (stinfo->previous); |
16c024b5 | 102 | stateInfo sfirst = snext; |
28bf4b0b | 103 | |
6d43e86c | 104 | DPRINTF (("stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); |
16c024b5 | 105 | llassert (snext != NULL); |
106 | ||
6d43e86c | 107 | if (!fileloc_lessthan (stinfo->loc, snext->loc)) |
16c024b5 | 108 | { |
6d43e86c | 109 | /*@i2@*/ stinfo->previous = sfirst; /* spurious? */ |
110 | DPRINTF (("Sorted ==> %s", stateInfo_unparse (stinfo))); | |
111 | /*@i2@*/ return stinfo; /* spurious? */ | |
16c024b5 | 112 | } |
113 | else | |
114 | { | |
6d43e86c | 115 | while (snext != NULL && fileloc_lessthan (stinfo->loc, snext->loc)) |
16c024b5 | 116 | { |
117 | /* | |
118 | ** swap the order | |
119 | */ | |
120 | fileloc tloc = snext->loc; | |
121 | stateAction taction = snext->action; | |
122 | sRef tref = snext->ref; | |
123 | ||
6d43e86c | 124 | DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); |
16c024b5 | 125 | |
6d43e86c | 126 | snext->loc = stinfo->loc; |
127 | snext->action = stinfo->action; | |
b73d1009 | 128 | /*@-modobserver@*/ |
6d43e86c | 129 | snext->ref = stinfo->ref; /* Doesn't actually modifie sfirst */ |
b73d1009 | 130 | /*@=modobserver@*/ |
16c024b5 | 131 | |
6d43e86c | 132 | stinfo->loc = tloc; |
133 | stinfo->action = taction; | |
134 | stinfo->ref = tref; | |
b73d1009 | 135 | /*@-mustfreeonly@*/ |
6d43e86c | 136 | stinfo->previous = snext->previous; |
b73d1009 | 137 | /*@=mustfreeonly@*/ |
16c024b5 | 138 | snext = snext->previous; |
6d43e86c | 139 | DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); |
16c024b5 | 140 | } |
141 | ||
142 | DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst))); | |
b73d1009 | 143 | /*@-compmempass@*/ |
144 | return sfirst; | |
145 | /*@=compmempass@*/ | |
16c024b5 | 146 | } |
147 | } | |
28bf4b0b | 148 | } |
149 | ||
150 | /*@only@*/ stateInfo | |
16c024b5 | 151 | stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc) |
28bf4b0b | 152 | { |
16c024b5 | 153 | if (fileloc_isUndefined (loc)) { |
154 | loc = fileloc_copy (g_currentloc); | |
155 | } | |
156 | ||
157 | if (old != NULL && fileloc_equal (old->loc, loc) && old->action == action) | |
28bf4b0b | 158 | { |
16c024b5 | 159 | /* |
160 | ** Duplicate (change through alias most likely) | |
161 | ** don't add this info | |
162 | */ | |
163 | ||
164 | return old; | |
28bf4b0b | 165 | } |
166 | else | |
167 | { | |
16c024b5 | 168 | stateInfo snew = stateInfo_makeLoc (loc, action); |
169 | llassert (snew->previous == NULL); | |
170 | snew->previous = old; | |
171 | DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); | |
172 | return snew; | |
28bf4b0b | 173 | } |
16c024b5 | 174 | } |
28bf4b0b | 175 | |
16c024b5 | 176 | /*@only@*/ stateInfo |
177 | stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref, | |
178 | stateAction action, fileloc loc) | |
179 | { | |
180 | if (fileloc_isUndefined (loc)) { | |
181 | loc = fileloc_copy (g_currentloc); | |
182 | } | |
183 | ||
184 | if (old != NULL && fileloc_equal (old->loc, loc) | |
185 | && old->action == action | |
186 | /*@-abstractcompare*/ && old->ref == ref /*@=abstractcompare@*/) | |
187 | { | |
188 | /* | |
189 | ** Duplicate (change through alias most likely) | |
190 | ** don't add this info | |
191 | */ | |
192 | ||
193 | return old; | |
194 | } | |
195 | else | |
196 | { | |
197 | stateInfo snew = stateInfo_makeRefLoc (ref, loc, action); | |
198 | llassert (snew->previous == NULL); | |
199 | snew->previous = old; | |
200 | DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); | |
201 | return snew; | |
202 | } | |
28bf4b0b | 203 | } |
204 | ||
205 | /*@only@*/ stateInfo stateInfo_copy (stateInfo a) | |
206 | { | |
207 | if (a == NULL) | |
208 | { | |
209 | return NULL; | |
210 | } | |
211 | else | |
212 | { | |
213 | stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); | |
214 | ||
215 | ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/ | |
28bf4b0b | 216 | ret->ref = a->ref; |
16c024b5 | 217 | ret->action = a->action; |
6fcd0b1e | 218 | ret->previous = stateInfo_copy (a->previous); |
28bf4b0b | 219 | |
220 | return ret; | |
221 | } | |
222 | } | |
223 | ||
6970c11b | 224 | /*@only@*/ /*@notnull@*/ stateInfo |
225 | stateInfo_currentLoc (void) | |
226 | { | |
16c024b5 | 227 | return stateInfo_makeLoc (g_currentloc, SA_DECLARED); |
6970c11b | 228 | } |
229 | ||
28bf4b0b | 230 | /*@only@*/ /*@notnull@*/ stateInfo |
16c024b5 | 231 | stateInfo_makeLoc (fileloc loc, stateAction action) |
28bf4b0b | 232 | { |
233 | stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); | |
234 | ||
16c024b5 | 235 | if (fileloc_isUndefined (loc)) { |
236 | ret->loc = fileloc_copy (g_currentloc); | |
237 | } else { | |
238 | ret->loc = fileloc_copy (loc); | |
239 | } | |
240 | ||
28bf4b0b | 241 | ret->ref = sRef_undefined; |
16c024b5 | 242 | ret->action = action; |
6fcd0b1e | 243 | ret->previous = stateInfo_undefined; |
244 | ||
16c024b5 | 245 | DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret))); |
28bf4b0b | 246 | return ret; |
247 | } | |
248 | ||
2f2892c2 | 249 | /*@only@*/ /*@notnull@*/ stateInfo |
16c024b5 | 250 | stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action) |
6fcd0b1e | 251 | /*@post:isnull result->previous@*/ |
28bf4b0b | 252 | { |
253 | stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); | |
254 | ||
16c024b5 | 255 | if (fileloc_isUndefined (loc)) { |
256 | ret->loc = fileloc_copy (g_currentloc); | |
257 | } else { | |
258 | ret->loc = fileloc_copy (loc); | |
259 | } | |
260 | ||
28bf4b0b | 261 | ret->ref = ref; |
16c024b5 | 262 | ret->action = action; |
6fcd0b1e | 263 | ret->previous = stateInfo_undefined; |
264 | ||
28bf4b0b | 265 | return ret; |
266 | } | |
267 | ||
268 | /*@only@*/ cstring | |
269 | stateInfo_unparse (stateInfo s) | |
270 | { | |
16c024b5 | 271 | cstring res = cstring_makeLiteral (""); |
272 | ||
273 | while (stateInfo_isDefined (s)) { | |
274 | res = message ("%q%q: ", res, fileloc_unparse (s->loc)); | |
275 | if (sRef_isValid (s->ref)) { | |
276 | res = message ("%q through alias %q ", res, sRef_unparse (s->ref)); | |
277 | } | |
278 | ||
279 | res = message ("%q%s; ", res, stateAction_unparse (s->action)); | |
280 | s = s->previous; | |
281 | } | |
282 | ||
283 | return res; | |
28bf4b0b | 284 | } |
285 | ||
286 | fileloc stateInfo_getLoc (stateInfo info) | |
287 | { | |
6fcd0b1e | 288 | if (stateInfo_isDefined (info)) |
289 | { | |
28bf4b0b | 290 | return info->loc; |
6fcd0b1e | 291 | } |
292 | ||
293 | return fileloc_undefined; | |
294 | } | |
295 | ||
16c024b5 | 296 | stateAction stateAction_fromNState (nstate ns) |
297 | { | |
298 | switch (ns) | |
299 | { | |
300 | case NS_ERROR: | |
301 | case NS_UNKNOWN: | |
302 | return SA_UNKNOWN; | |
303 | case NS_NOTNULL: | |
304 | case NS_MNOTNULL: | |
305 | return SA_BECOMESNONNULL; | |
306 | case NS_RELNULL: | |
307 | case NS_CONSTNULL: | |
308 | return SA_DECLARED; | |
309 | case NS_POSNULL: | |
310 | return SA_BECOMESPOSSIBLYNULL; | |
311 | case NS_DEFNULL: | |
312 | return SA_BECOMESNULL; | |
313 | case NS_ABSNULL: | |
314 | return SA_BECOMESPOSSIBLYNULL; | |
315 | } | |
316 | } | |
317 | ||
318 | stateAction stateAction_fromExkind (exkind ex) | |
319 | { | |
320 | switch (ex) | |
321 | { | |
322 | case XO_UNKNOWN: | |
323 | case XO_NORMAL: | |
324 | return SA_UNKNOWN; | |
325 | case XO_EXPOSED: | |
326 | return SA_EXPOSED; | |
327 | case XO_OBSERVER: | |
328 | return SA_OBSERVER; | |
329 | } | |
330 | ||
331 | BADBRANCH; | |
332 | /*@notreached@*/ return SA_UNKNOWN; | |
333 | } | |
334 | ||
335 | stateAction stateAction_fromAlkind (alkind ak) | |
336 | { | |
337 | switch (ak) | |
338 | { | |
339 | case AK_UNKNOWN: | |
340 | case AK_ERROR: | |
341 | return SA_UNKNOWN; | |
342 | case AK_ONLY: | |
343 | return SA_ONLY; | |
344 | case AK_IMPONLY: | |
345 | return SA_IMPONLY; | |
346 | case AK_KEEP: | |
347 | return SA_KEEP; | |
348 | case AK_KEPT: | |
349 | return SA_KEPT; | |
350 | case AK_TEMP: | |
351 | return SA_TEMP; | |
352 | case AK_IMPTEMP: | |
353 | return SA_IMPTEMP; | |
354 | case AK_SHARED: | |
355 | return SA_SHARED; | |
356 | case AK_UNIQUE: | |
357 | case AK_RETURNED: | |
358 | return SA_DECLARED; | |
359 | case AK_FRESH: | |
360 | return SA_FRESH; | |
361 | case AK_STACK: | |
362 | return SA_XSTACK; | |
363 | case AK_REFCOUNTED: | |
364 | return SA_REFCOUNTED; | |
365 | case AK_REFS: | |
366 | return SA_REFS; | |
367 | case AK_KILLREF: | |
368 | return SA_KILLREF; | |
369 | case AK_NEWREF: | |
370 | return SA_NEWREF; | |
371 | case AK_OWNED: | |
372 | return SA_OWNED; | |
373 | case AK_DEPENDENT: | |
374 | return SA_DEPENDENT; | |
375 | case AK_IMPDEPENDENT: | |
376 | return SA_IMPDEPENDENT; | |
377 | case AK_STATIC: | |
378 | return SA_STATIC; | |
379 | case AK_LOCAL: | |
380 | return SA_LOCAL; | |
381 | } | |
382 | ||
383 | BADBRANCH; | |
384 | /*@notreached@*/ return SA_UNKNOWN; | |
385 | } | |
386 | ||
387 | stateAction stateAction_fromSState (sstate ss) | |
388 | { | |
389 | switch (ss) | |
390 | { | |
391 | case SS_UNKNOWN: return SA_DECLARED; | |
392 | case SS_UNUSEABLE: return SA_KILLED; | |
393 | case SS_UNDEFINED: return SA_UNDEFINED; | |
394 | case SS_MUNDEFINED: return SA_MUNDEFINED; | |
395 | case SS_ALLOCATED: return SA_ALLOCATED; | |
396 | case SS_PDEFINED: return SA_PDEFINED; | |
397 | case SS_DEFINED: return SA_DEFINED; | |
398 | case SS_PARTIAL: return SA_PDEFINED; | |
399 | case SS_DEAD: return SA_RELEASED; | |
400 | case SS_HOFFA: return SA_PKILLED; | |
401 | case SS_SPECIAL: return SA_DECLARED; | |
402 | case SS_RELDEF: return SA_DECLARED; | |
403 | case SS_FIXED: | |
404 | case SS_UNDEFGLOB: | |
405 | case SS_KILLED: | |
406 | case SS_UNDEFKILLED: | |
407 | case SS_LAST: | |
408 | llbug (message ("Unexpected sstate: %s", sstate_unparse (ss))); | |
409 | /*@notreached@*/ return SA_UNKNOWN; | |
410 | } | |
411 | } | |
412 | ||
413 | static /*@observer@*/ cstring stateAction_unparse (stateAction sa) | |
414 | { | |
415 | switch (sa) | |
416 | { | |
417 | case SA_UNKNOWN: return cstring_makeLiteralTemp ("changed <unknown modification>"); | |
418 | case SA_CHANGED: return cstring_makeLiteralTemp ("changed"); | |
419 | ||
420 | case SA_CREATED: return cstring_makeLiteralTemp ("created"); | |
421 | case SA_DECLARED: return cstring_makeLiteralTemp ("declared"); | |
422 | case SA_DEFINED: return cstring_makeLiteralTemp ("defined"); | |
423 | case SA_PDEFINED: return cstring_makeLiteralTemp ("partially defined"); | |
424 | case SA_RELEASED: return cstring_makeLiteralTemp ("released"); | |
425 | case SA_ALLOCATED: return cstring_makeLiteralTemp ("allocated"); | |
426 | case SA_KILLED: return cstring_makeLiteralTemp ("released"); | |
427 | case SA_PKILLED: return cstring_makeLiteralTemp ("possibly released"); | |
428 | case SA_MERGED: return cstring_makeLiteralTemp ("merged"); | |
429 | case SA_UNDEFINED: return cstring_makeLiteralTemp ("becomes undefined"); | |
430 | case SA_MUNDEFINED: return cstring_makeLiteralTemp ("possibly undefined"); | |
431 | ||
432 | case SA_SHARED: return cstring_makeLiteralTemp ("becomes shared"); | |
433 | case SA_ONLY: return cstring_makeLiteralTemp ("becomes only"); | |
434 | case SA_IMPONLY: return cstring_makeLiteralTemp ("becomes implicitly only"); | |
435 | case SA_OWNED: return cstring_makeLiteralTemp ("becomes owned"); | |
436 | case SA_DEPENDENT: return cstring_makeLiteralTemp ("becomes dependent"); | |
437 | case SA_IMPDEPENDENT: return cstring_makeLiteralTemp ("becomes implicitly dependent"); | |
438 | case SA_KEPT: return cstring_makeLiteralTemp ("becomes kept"); | |
439 | case SA_KEEP: return cstring_makeLiteralTemp ("becomes keep"); | |
440 | case SA_FRESH: return cstring_makeLiteralTemp ("becomes fresh"); | |
441 | case SA_TEMP: return cstring_makeLiteralTemp ("becomes temp"); | |
442 | case SA_IMPTEMP: return cstring_makeLiteralTemp ("becomes implicitly temp"); | |
443 | case SA_XSTACK: return cstring_makeLiteralTemp ("becomes stack-allocated storage"); | |
444 | case SA_STATIC: return cstring_makeLiteralTemp ("becomes static"); | |
445 | case SA_LOCAL: return cstring_makeLiteralTemp ("becomes local"); | |
446 | ||
447 | case SA_REFCOUNTED: return cstring_makeLiteralTemp ("becomes refcounted"); | |
448 | case SA_REFS: return cstring_makeLiteralTemp ("becomes refs"); | |
449 | case SA_NEWREF: return cstring_makeLiteralTemp ("becomes newref"); | |
450 | case SA_KILLREF: return cstring_makeLiteralTemp ("becomes killref"); | |
451 | ||
452 | case SA_OBSERVER: return cstring_makeLiteralTemp ("becomes observer"); | |
453 | case SA_EXPOSED: return cstring_makeLiteralTemp ("becomes exposed"); | |
454 | ||
455 | case SA_BECOMESNULL: return cstring_makeLiteralTemp ("becomes null"); | |
456 | case SA_BECOMESNONNULL: return cstring_makeLiteralTemp ("becomes non-null"); | |
457 | case SA_BECOMESPOSSIBLYNULL: return cstring_makeLiteralTemp ("becomes possibly null"); | |
458 | } | |
459 | ||
460 | DPRINTF (("Bad state action: %d", sa)); | |
461 | BADBRANCH; | |
462 | } | |
463 | ||
6fcd0b1e | 464 | void stateInfo_display (stateInfo s, cstring sname) |
465 | { | |
16c024b5 | 466 | bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc); |
467 | ||
468 | s = stateInfo_sort (s); | |
469 | ||
6fcd0b1e | 470 | while (stateInfo_isDefined (s)) |
471 | { | |
16c024b5 | 472 | cstring msg = message ("%s%s", sname, stateAction_unparse (s->action)); |
473 | ||
6fcd0b1e | 474 | if (sRef_isValid (s->ref)) { |
16c024b5 | 475 | msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref)); |
6fcd0b1e | 476 | } |
16c024b5 | 477 | |
6fcd0b1e | 478 | llgenindentmsg (msg, s->loc); |
16c024b5 | 479 | |
480 | if (!showdeep) { | |
481 | break; | |
482 | } | |
483 | ||
6fcd0b1e | 484 | s = s->previous; |
28bf4b0b | 485 | } |
486 | ||
6fcd0b1e | 487 | cstring_free (sname); |
28bf4b0b | 488 | } |
489 | ||
6fcd0b1e | 490 |