X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/11db3170da99e22aa0acea76debd6c7b590a629c..6d43e86c47a9417dc3d577244ab526c126d4b4e4:/src/stateInfo.c diff --git a/src/stateInfo.c b/src/stateInfo.c index d4197ad..cf5246a 100644 --- a/src/stateInfo.c +++ b/src/stateInfo.c @@ -1,6 +1,6 @@ /* ** Splint - annotation-assisted static program checker -** Copyright (C) 1994-2001 University of Virginia, +** Copyright (C) 1994-2003 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -17,14 +17,25 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org ** For more information: http://www.splint.org */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" +# ifdef WIN32 +/* +** Make Microsoft VC++ happy: its control checking produces too +** many spurious warnings. +*/ + +# pragma warning (disable:4715) +# endif + +static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ; + void stateInfo_free (/*@only@*/ stateInfo a) { if (a != NULL) @@ -43,7 +54,8 @@ void stateInfo_free (/*@only@*/ stateInfo a) { if (old == NULL) { - old = stateInfo_copy (newinfo); + DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo))); + return stateInfo_copy (newinfo); } else if (newinfo == NULL) { @@ -52,45 +64,142 @@ void stateInfo_free (/*@only@*/ stateInfo a) } else { - old->loc = fileloc_update (old->loc, newinfo->loc); - old->ref = newinfo->ref; - old->ue = newinfo->ue; + if (fileloc_equal (old->loc, newinfo->loc) + && old->action == newinfo->action + /*@-abstractcompare@*/ && old->ref == newinfo->ref /*@=abstractcompare@*/) + { + /* + ** Duplicate (change through alias most likely) + ** don't add this info + */ + + return old; + } + else + { + stateInfo snew = stateInfo_makeRefLoc (newinfo->ref, + newinfo->loc, newinfo->action); + llassert (snew->previous == NULL); + snew->previous = old; + DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); + return snew; + } } - - return old; } -/*@only@*/ stateInfo stateInfo_updateLoc (/*@only@*/ stateInfo old, fileloc loc) +static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo stinfo) + /* Sorts in reverse location order */ { - if (old == NULL) + DPRINTF (("Sorting: %s", stateInfo_unparse (stinfo))); + + if (stinfo == NULL || stinfo->previous == NULL) { - old = stateInfo_makeLoc (loc); + return stinfo; } else { - old->loc = fileloc_update (old->loc, loc); - old->ue = uentry_undefined; - old->ref = sRef_undefined; - } + stateInfo snext = stateInfo_sort (stinfo->previous); + stateInfo sfirst = snext; + + DPRINTF (("stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); + llassert (snext != NULL); - return old; + if (!fileloc_lessthan (stinfo->loc, snext->loc)) + { + /*@i2@*/ stinfo->previous = sfirst; /* spurious? */ + DPRINTF (("Sorted ==> %s", stateInfo_unparse (stinfo))); + /*@i2@*/ return stinfo; /* spurious? */ + } + else + { + while (snext != NULL && fileloc_lessthan (stinfo->loc, snext->loc)) + { + /* + ** swap the order + */ + fileloc tloc = snext->loc; + stateAction taction = snext->action; + sRef tref = snext->ref; + + DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); + + snext->loc = stinfo->loc; + snext->action = stinfo->action; + /*@-modobserver@*/ + snext->ref = stinfo->ref; /* Doesn't actually modifie sfirst */ + /*@=modobserver@*/ + + stinfo->loc = tloc; + stinfo->action = taction; + stinfo->ref = tref; + /*@-mustfreeonly@*/ + stinfo->previous = snext->previous; + /*@=mustfreeonly@*/ + snext = snext->previous; + DPRINTF (("in while: stinfo/sext: %s // %s", stateInfo_unparse (stinfo), stateInfo_unparse (snext))); + } + + DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst))); + /*@-compmempass@*/ + return sfirst; + /*@=compmempass@*/ + } + } } /*@only@*/ stateInfo - stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref, fileloc loc) +stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc) { - if (old == NULL) + if (fileloc_isUndefined (loc)) { + loc = fileloc_copy (g_currentloc); + } + + if (old != NULL && fileloc_equal (old->loc, loc) && old->action == action) { - old = stateInfo_makeRefLoc (ref, loc); + /* + ** Duplicate (change through alias most likely) + ** don't add this info + */ + + return old; } else { - old->loc = fileloc_update (old->loc, loc); - old->ue = uentry_undefined; - old->ref = ref; + stateInfo snew = stateInfo_makeLoc (loc, action); + llassert (snew->previous == NULL); + snew->previous = old; + DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); + return snew; } +} - return old; +/*@only@*/ stateInfo +stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref, + stateAction action, fileloc loc) +{ + if (fileloc_isUndefined (loc)) { + loc = fileloc_copy (g_currentloc); + } + + if (old != NULL && fileloc_equal (old->loc, loc) + && old->action == action + /*@-abstractcompare*/ && old->ref == ref /*@=abstractcompare@*/) + { + /* + ** Duplicate (change through alias most likely) + ** don't add this info + */ + + return old; + } + else + { + stateInfo snew = stateInfo_makeRefLoc (ref, loc, action); + llassert (snew->previous == NULL); + snew->previous = old; + DPRINTF (("Update state ==> %s", stateInfo_unparse (snew))); + return snew; + } } /*@only@*/ stateInfo stateInfo_copy (stateInfo a) @@ -104,8 +213,9 @@ void stateInfo_free (/*@only@*/ stateInfo a) stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/ - ret->ue = a->ue; ret->ref = a->ref; + ret->action = a->action; + ret->previous = stateInfo_copy (a->previous); return ret; } @@ -114,50 +224,267 @@ void stateInfo_free (/*@only@*/ stateInfo a) /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) { - return stateInfo_makeLoc (g_currentloc); + return stateInfo_makeLoc (g_currentloc, SA_DECLARED); } /*@only@*/ /*@notnull@*/ stateInfo -stateInfo_makeLoc (fileloc loc) +stateInfo_makeLoc (fileloc loc, stateAction action) { stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); - ret->loc = fileloc_copy (loc); /* don't need to copy! */ - ret->ue = uentry_undefined; + if (fileloc_isUndefined (loc)) { + ret->loc = fileloc_copy (g_currentloc); + } else { + ret->loc = fileloc_copy (loc); + } + ret->ref = sRef_undefined; - + ret->action = action; + ret->previous = stateInfo_undefined; + + DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret))); return ret; } -/*@only@*/ stateInfo -stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc) +/*@only@*/ /*@notnull@*/ stateInfo +stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action) + /*@post:isnull result->previous@*/ { stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); - ret->loc = fileloc_copy (loc); + if (fileloc_isUndefined (loc)) { + ret->loc = fileloc_copy (g_currentloc); + } else { + ret->loc = fileloc_copy (loc); + } + ret->ref = ref; - ret->ue = uentry_undefined; - + ret->action = action; + ret->previous = stateInfo_undefined; + return ret; } /*@only@*/ cstring stateInfo_unparse (stateInfo s) { - if (stateInfo_isDefined (s) && - fileloc_isDefined (s->loc)) { - return fileloc_unparse (s->loc); - } else { - return cstring_makeLiteral (""); + cstring res = cstring_makeLiteral (""); + + while (stateInfo_isDefined (s)) { + res = message ("%q%q: ", res, fileloc_unparse (s->loc)); + if (sRef_isValid (s->ref)) { + res = message ("%q through alias %q ", res, sRef_unparse (s->ref)); } + + res = message ("%q%s; ", res, stateAction_unparse (s->action)); + s = s->previous; + } + + return res; } fileloc stateInfo_getLoc (stateInfo info) { - if (stateInfo_isDefined (info)) { + if (stateInfo_isDefined (info)) + { return info->loc; + } + + return fileloc_undefined; +} + +stateAction stateAction_fromNState (nstate ns) +{ + switch (ns) + { + case NS_ERROR: + case NS_UNKNOWN: + return SA_UNKNOWN; + case NS_NOTNULL: + case NS_MNOTNULL: + return SA_BECOMESNONNULL; + case NS_RELNULL: + case NS_CONSTNULL: + return SA_DECLARED; + case NS_POSNULL: + return SA_BECOMESPOSSIBLYNULL; + case NS_DEFNULL: + return SA_BECOMESNULL; + case NS_ABSNULL: + return SA_BECOMESPOSSIBLYNULL; } +} - return fileloc_undefined; +stateAction stateAction_fromExkind (exkind ex) +{ + switch (ex) + { + case XO_UNKNOWN: + case XO_NORMAL: + return SA_UNKNOWN; + case XO_EXPOSED: + return SA_EXPOSED; + case XO_OBSERVER: + return SA_OBSERVER; + } + + BADBRANCH; + /*@notreached@*/ return SA_UNKNOWN; +} + +stateAction stateAction_fromAlkind (alkind ak) +{ + switch (ak) + { + case AK_UNKNOWN: + case AK_ERROR: + return SA_UNKNOWN; + case AK_ONLY: + return SA_ONLY; + case AK_IMPONLY: + return SA_IMPONLY; + case AK_KEEP: + return SA_KEEP; + case AK_KEPT: + return SA_KEPT; + case AK_TEMP: + return SA_TEMP; + case AK_IMPTEMP: + return SA_IMPTEMP; + case AK_SHARED: + return SA_SHARED; + case AK_UNIQUE: + case AK_RETURNED: + return SA_DECLARED; + case AK_FRESH: + return SA_FRESH; + case AK_STACK: + return SA_XSTACK; + case AK_REFCOUNTED: + return SA_REFCOUNTED; + case AK_REFS: + return SA_REFS; + case AK_KILLREF: + return SA_KILLREF; + case AK_NEWREF: + return SA_NEWREF; + case AK_OWNED: + return SA_OWNED; + case AK_DEPENDENT: + return SA_DEPENDENT; + case AK_IMPDEPENDENT: + return SA_IMPDEPENDENT; + case AK_STATIC: + return SA_STATIC; + case AK_LOCAL: + return SA_LOCAL; + } + + BADBRANCH; + /*@notreached@*/ return SA_UNKNOWN; +} + +stateAction stateAction_fromSState (sstate ss) +{ + switch (ss) + { + case SS_UNKNOWN: return SA_DECLARED; + case SS_UNUSEABLE: return SA_KILLED; + case SS_UNDEFINED: return SA_UNDEFINED; + case SS_MUNDEFINED: return SA_MUNDEFINED; + case SS_ALLOCATED: return SA_ALLOCATED; + case SS_PDEFINED: return SA_PDEFINED; + case SS_DEFINED: return SA_DEFINED; + case SS_PARTIAL: return SA_PDEFINED; + case SS_DEAD: return SA_RELEASED; + case SS_HOFFA: return SA_PKILLED; + case SS_SPECIAL: return SA_DECLARED; + case SS_RELDEF: return SA_DECLARED; + case SS_FIXED: + case SS_UNDEFGLOB: + case SS_KILLED: + case SS_UNDEFKILLED: + case SS_LAST: + llbug (message ("Unexpected sstate: %s", sstate_unparse (ss))); + /*@notreached@*/ return SA_UNKNOWN; + } } +static /*@observer@*/ cstring stateAction_unparse (stateAction sa) +{ + switch (sa) + { + case SA_UNKNOWN: return cstring_makeLiteralTemp ("changed "); + case SA_CHANGED: return cstring_makeLiteralTemp ("changed"); + + case SA_CREATED: return cstring_makeLiteralTemp ("created"); + case SA_DECLARED: return cstring_makeLiteralTemp ("declared"); + case SA_DEFINED: return cstring_makeLiteralTemp ("defined"); + case SA_PDEFINED: return cstring_makeLiteralTemp ("partially defined"); + case SA_RELEASED: return cstring_makeLiteralTemp ("released"); + case SA_ALLOCATED: return cstring_makeLiteralTemp ("allocated"); + case SA_KILLED: return cstring_makeLiteralTemp ("released"); + case SA_PKILLED: return cstring_makeLiteralTemp ("possibly released"); + case SA_MERGED: return cstring_makeLiteralTemp ("merged"); + case SA_UNDEFINED: return cstring_makeLiteralTemp ("becomes undefined"); + case SA_MUNDEFINED: return cstring_makeLiteralTemp ("possibly undefined"); + + case SA_SHARED: return cstring_makeLiteralTemp ("becomes shared"); + case SA_ONLY: return cstring_makeLiteralTemp ("becomes only"); + case SA_IMPONLY: return cstring_makeLiteralTemp ("becomes implicitly only"); + case SA_OWNED: return cstring_makeLiteralTemp ("becomes owned"); + case SA_DEPENDENT: return cstring_makeLiteralTemp ("becomes dependent"); + case SA_IMPDEPENDENT: return cstring_makeLiteralTemp ("becomes implicitly dependent"); + case SA_KEPT: return cstring_makeLiteralTemp ("becomes kept"); + case SA_KEEP: return cstring_makeLiteralTemp ("becomes keep"); + case SA_FRESH: return cstring_makeLiteralTemp ("becomes fresh"); + case SA_TEMP: return cstring_makeLiteralTemp ("becomes temp"); + case SA_IMPTEMP: return cstring_makeLiteralTemp ("becomes implicitly temp"); + case SA_XSTACK: return cstring_makeLiteralTemp ("becomes stack-allocated storage"); + case SA_STATIC: return cstring_makeLiteralTemp ("becomes static"); + case SA_LOCAL: return cstring_makeLiteralTemp ("becomes local"); + + case SA_REFCOUNTED: return cstring_makeLiteralTemp ("becomes refcounted"); + case SA_REFS: return cstring_makeLiteralTemp ("becomes refs"); + case SA_NEWREF: return cstring_makeLiteralTemp ("becomes newref"); + case SA_KILLREF: return cstring_makeLiteralTemp ("becomes killref"); + + case SA_OBSERVER: return cstring_makeLiteralTemp ("becomes observer"); + case SA_EXPOSED: return cstring_makeLiteralTemp ("becomes exposed"); + + case SA_BECOMESNULL: return cstring_makeLiteralTemp ("becomes null"); + case SA_BECOMESNONNULL: return cstring_makeLiteralTemp ("becomes non-null"); + case SA_BECOMESPOSSIBLYNULL: return cstring_makeLiteralTemp ("becomes possibly null"); + } + + DPRINTF (("Bad state action: %d", sa)); + BADBRANCH; +} + +void stateInfo_display (stateInfo s, cstring sname) +{ + bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc); + + s = stateInfo_sort (s); + + while (stateInfo_isDefined (s)) + { + cstring msg = message ("%s%s", sname, stateAction_unparse (s->action)); + + if (sRef_isValid (s->ref)) { + msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref)); + } + + llgenindentmsg (msg, s->loc); + + if (!showdeep) { + break; + } + + s = s->previous; + } + + cstring_free (sname); +} + +