1 /*
2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
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 **
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
23 */
24
25 # include "splintMacros.nf"
26 # include "basic.h"
27
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
37 static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ;
38
stateInfo_free(stateInfo a)39 void stateInfo_free (/*@only@*/ stateInfo a)
40 {
41 if (a != NULL)
42 {
43 fileloc_free (a->loc);
44 sfree (a);
45 }
46 }
47
stateInfo_update(stateInfo old,stateInfo newinfo)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 {
57 DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo)));
58 return stateInfo_copy (newinfo);
59 }
60 else if (newinfo == NULL)
61 {
62 stateInfo_free (old);
63 return NULL;
64 }
65 else
66 {
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 }
87 }
88 }
89
stateInfo_sort(stateInfo stinfo)90 static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo stinfo)
91 /* Sorts in reverse location order */
92 {
93 DPRINTF (("Sorting: %s", stateInfo_unparse (stinfo)));
94
95 if (stinfo == NULL || stinfo->previous == NULL)
96 {
97 return stinfo;
98 }
99 else
100 {
101 stateInfo snext = stateInfo_sort (stinfo->previous);
102 stateInfo sfirst = snext;
103
104 DPRINTF (("stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
105 llassert (snext != NULL);
106
107 if (!fileloc_lessthan (stinfo->loc, snext->loc))
108 {
109 /*@i2@*/ stinfo->previous = sfirst; /* spurious? */
110 DPRINTF (("Sorted ==> %s", stateInfo_unparse (stinfo)));
111 /*@i2@*/ return stinfo; /* spurious? */
112 }
113 else
114 {
115 while (snext != NULL && fileloc_lessthan (stinfo->loc, snext->loc))
116 {
117 /*
118 ** swap the order
119 */
120 fileloc tloc = snext->loc;
121 stateAction taction = snext->action;
122 sRef tref = snext->ref;
123
124 DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
125
126 snext->loc = stinfo->loc;
127 snext->action = stinfo->action;
128 /*@-modobserver@*/
129 snext->ref = stinfo->ref; /* Doesn't actually modifie sfirst */
130 /*@=modobserver@*/
131
132 stinfo->loc = tloc;
133 stinfo->action = taction;
134 stinfo->ref = tref;
135 /*@-mustfreeonly@*/
136 stinfo->previous = snext->previous;
137 /*@=mustfreeonly@*/
138 snext = snext->previous;
139 DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
140 }
141
142 DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
143 /*@-compmempass@*/
144 return sfirst;
145 /*@=compmempass@*/
146 }
147 }
148 }
149
150 /*@only@*/ stateInfo
stateInfo_updateLoc(stateInfo old,stateAction action,fileloc loc)151 stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc)
152 {
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)
158 {
159 /*
160 ** Duplicate (change through alias most likely)
161 ** don't add this info
162 */
163
164 return old;
165 }
166 else
167 {
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;
173 }
174 }
175
176 /*@only@*/ stateInfo
stateInfo_updateRefLoc(stateInfo old,sRef ref,stateAction action,fileloc loc)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 }
203 }
204
stateInfo_copy(stateInfo a)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! >*/
216 ret->ref = a->ref;
217 ret->action = a->action;
218 ret->previous = stateInfo_copy (a->previous);
219
220 return ret;
221 }
222 }
223
224 /*@only@*/ /*@notnull@*/ stateInfo
stateInfo_currentLoc(void)225 stateInfo_currentLoc (void)
226 {
227 return stateInfo_makeLoc (g_currentloc, SA_DECLARED);
228 }
229
230 /*@only@*/ /*@notnull@*/ stateInfo
stateInfo_makeLoc(fileloc loc,stateAction action)231 stateInfo_makeLoc (fileloc loc, stateAction action)
232 {
233 stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
234
235 if (fileloc_isUndefined (loc)) {
236 ret->loc = fileloc_copy (g_currentloc);
237 } else {
238 ret->loc = fileloc_copy (loc);
239 }
240
241 ret->ref = sRef_undefined;
242 ret->action = action;
243 ret->previous = stateInfo_undefined;
244
245 DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret)));
246 return ret;
247 }
248
249 /*@only@*/ /*@notnull@*/ stateInfo
stateInfo_makeRefLoc(sRef ref,fileloc loc,stateAction action)250 stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action)
251 /*@post:isnull result->previous@*/
252 {
253 stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
254
255 if (fileloc_isUndefined (loc)) {
256 ret->loc = fileloc_copy (g_currentloc);
257 } else {
258 ret->loc = fileloc_copy (loc);
259 }
260
261 ret->ref = ref;
262 ret->action = action;
263 ret->previous = stateInfo_undefined;
264
265 return ret;
266 }
267
268 /*@only@*/ cstring
stateInfo_unparse(stateInfo s)269 stateInfo_unparse (stateInfo s)
270 {
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;
284 }
285
stateInfo_getLoc(stateInfo info)286 fileloc stateInfo_getLoc (stateInfo info)
287 {
288 if (stateInfo_isDefined (info))
289 {
290 return info->loc;
291 }
292
293 return fileloc_undefined;
294 }
295
stateAction_fromNState(nstate ns)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
stateAction_fromExkind(exkind ex)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
stateAction_fromAlkind(alkind ak)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
stateAction_fromSState(sstate ss)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
stateAction_unparse(stateAction sa)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
stateInfo_display(stateInfo s,cstring sname)464 void stateInfo_display (stateInfo s, cstring sname)
465 {
466 bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc);
467
468 s = stateInfo_sort (s);
469
470 while (stateInfo_isDefined (s))
471 {
472 cstring msg = message ("%s%s", sname, stateAction_unparse (s->action));
473
474 if (sRef_isValid (s->ref)) {
475 msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref));
476 }
477
478 llgenindentmsg (msg, s->loc);
479
480 if (!showdeep) {
481 break;
482 }
483
484 s = s->previous;
485 }
486
487 cstring_free (sname);
488 }
489
490
491