2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
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
25 # include "splintMacros.nf"
30 ** Make Microsoft VC++ happy: its control checking produces too
31 ** many spurious warnings.
34 # pragma warning (disable:4715)
37 static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ;
39 void stateInfo_free (/*@only@*/ stateInfo a)
43 fileloc_free (a->loc);
48 /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo old, stateInfo newinfo)
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
57 DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo)));
58 return stateInfo_copy (newinfo);
60 else if (newinfo == NULL)
67 if (fileloc_equal (old->loc, newinfo->loc)
68 && old->action == newinfo->action
69 /*@-abstractcompare@*/ && old->ref == newinfo->ref /*@=abstractcompare@*/)
72 ** Duplicate (change through alias most likely)
73 ** don't add this info
80 stateInfo snew = stateInfo_makeRefLoc (newinfo->ref,
81 newinfo->loc, newinfo->action);
82 llassert (snew->previous == NULL);
84 DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
90 static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo stinfo)
91 /* Sorts in reverse location order */
93 DPRINTF (("Sorting: %s", stateInfo_unparse (stinfo)));
95 if (stinfo == NULL || stinfo->previous == NULL)
101 stateInfo snext = stateInfo_sort (stinfo->previous);
102 stateInfo sfirst = snext;
104 DPRINTF (("stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
105 llassert (snext != NULL);
107 if (!fileloc_lessthan (stinfo->loc, snext->loc))
109 /*@i2@*/ stinfo->previous = sfirst; /* spurious? */
110 DPRINTF (("Sorted ==> %s", stateInfo_unparse (stinfo)));
111 /*@i2@*/ return stinfo; /* spurious? */
115 while (snext != NULL && fileloc_lessthan (stinfo->loc, snext->loc))
120 fileloc tloc = snext->loc;
121 stateAction taction = snext->action;
122 sRef tref = snext->ref;
124 DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
126 snext->loc = stinfo->loc;
127 snext->action = stinfo->action;
129 snext->ref = stinfo->ref; /* Doesn't actually modifie sfirst */
133 stinfo->action = taction;
136 stinfo->previous = snext->previous;
138 snext = snext->previous;
139 DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext)));
142 DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
151 stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc)
153 if (fileloc_isUndefined (loc)) {
154 loc = fileloc_copy (g_currentloc);
157 if (old != NULL && fileloc_equal (old->loc, loc) && old->action == action)
160 ** Duplicate (change through alias most likely)
161 ** don't add this info
168 stateInfo snew = stateInfo_makeLoc (loc, action);
169 llassert (snew->previous == NULL);
170 snew->previous = old;
171 DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
177 stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref,
178 stateAction action, fileloc loc)
180 if (fileloc_isUndefined (loc)) {
181 loc = fileloc_copy (g_currentloc);
184 if (old != NULL && fileloc_equal (old->loc, loc)
185 && old->action == action
186 /*@-abstractcompare*/ && old->ref == ref /*@=abstractcompare@*/)
189 ** Duplicate (change through alias most likely)
190 ** don't add this info
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)));
205 /*@only@*/ stateInfo stateInfo_copy (stateInfo a)
213 stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
215 ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
217 ret->action = a->action;
218 ret->previous = stateInfo_copy (a->previous);
224 /*@only@*/ /*@notnull@*/ stateInfo
225 stateInfo_currentLoc (void)
227 return stateInfo_makeLoc (g_currentloc, SA_DECLARED);
230 /*@only@*/ /*@notnull@*/ stateInfo
231 stateInfo_makeLoc (fileloc loc, stateAction action)
233 stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
235 if (fileloc_isUndefined (loc)) {
236 ret->loc = fileloc_copy (g_currentloc);
238 ret->loc = fileloc_copy (loc);
241 ret->ref = sRef_undefined;
242 ret->action = action;
243 ret->previous = stateInfo_undefined;
245 DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret)));
249 /*@only@*/ /*@notnull@*/ stateInfo
250 stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action)
251 /*@post:isnull result->previous@*/
253 stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
255 if (fileloc_isUndefined (loc)) {
256 ret->loc = fileloc_copy (g_currentloc);
258 ret->loc = fileloc_copy (loc);
262 ret->action = action;
263 ret->previous = stateInfo_undefined;
269 stateInfo_unparse (stateInfo s)
271 cstring res = cstring_makeLiteral ("");
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));
279 res = message ("%q%s; ", res, stateAction_unparse (s->action));
286 fileloc stateInfo_getLoc (stateInfo info)
288 if (stateInfo_isDefined (info))
293 return fileloc_undefined;
296 stateAction stateAction_fromNState (nstate ns)
305 return SA_BECOMESNONNULL;
310 return SA_BECOMESPOSSIBLYNULL;
312 return SA_BECOMESNULL;
314 return SA_BECOMESPOSSIBLYNULL;
318 stateAction stateAction_fromExkind (exkind ex)
332 /*@notreached@*/ return SA_UNKNOWN;
335 stateAction stateAction_fromAlkind (alkind ak)
364 return SA_REFCOUNTED;
375 case AK_IMPDEPENDENT:
376 return SA_IMPDEPENDENT;
384 /*@notreached@*/ return SA_UNKNOWN;
387 stateAction stateAction_fromSState (sstate ss)
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;
408 llbug (message ("Unexpected sstate: %s", sstate_unparse (ss)));
409 /*@notreached@*/ return SA_UNKNOWN;
413 static /*@observer@*/ cstring stateAction_unparse (stateAction sa)
417 case SA_UNKNOWN: return cstring_makeLiteralTemp ("changed <unknown modification>");
418 case SA_CHANGED: return cstring_makeLiteralTemp ("changed");
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");
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");
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");
452 case SA_OBSERVER: return cstring_makeLiteralTemp ("becomes observer");
453 case SA_EXPOSED: return cstring_makeLiteralTemp ("becomes exposed");
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");
460 DPRINTF (("Bad state action: %d", sa));
464 void stateInfo_display (stateInfo s, cstring sname)
466 bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc);
468 s = stateInfo_sort (s);
470 while (stateInfo_isDefined (s))
472 cstring msg = message ("%s%s", sname, stateAction_unparse (s->action));
474 if (sRef_isValid (s->ref)) {
475 msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref));
478 llgenindentmsg (msg, s->loc);
487 cstring_free (sname);