/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 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
# 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)
{
if (old == NULL)
{
+ DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo)));
return stateInfo_copy (newinfo);
}
else if (newinfo == NULL)
}
else
{
- stateInfo snew = stateInfo_makeRefLoc (newinfo->ref, newinfo->loc);
- snew->previous = old;
- return snew;
+ 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;
+ }
}
}
-/*@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->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->ref = ref;
+ stateInfo snew = stateInfo_makeLoc (loc, action);
+ llassert (snew->previous == NULL);
+ snew->previous = old;
+ DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
+ return snew;
}
+}
+
+/*@only@*/ stateInfo
+stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref,
+ stateAction action, fileloc loc)
+{
+ if (fileloc_isUndefined (loc)) {
+ loc = fileloc_copy (g_currentloc);
+ }
- return old;
+ 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)
ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
ret->ref = a->ref;
+ ret->action = a->action;
ret->previous = stateInfo_copy (a->previous);
return ret;
/*@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! */
+ 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->action = action;
ret->previous = stateInfo_undefined;
return ret;
/*@only@*/ cstring
stateInfo_unparse (stateInfo s)
{
- if (stateInfo_isDefined (s) && fileloc_isDefined (s->loc))
- {
- if (stateInfo_isDefined (s->previous)) {
- return message ("%q; %q", fileloc_unparse (s->loc), stateInfo_unparse (s->previous));
- } else {
- return fileloc_unparse (s->loc);
- }
- }
- else
- {
- return cstring_makeLiteral ("<no info>");
- }
+ 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)
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;
+ }
+}
+
+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 <unknown modification>");
+ 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 ("Storage %s ", sname);
-
+ 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));
+ msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref));
}
-
- msg = message ("%qreleased", msg); /* For now, just used for release...need to make this work. */
+
llgenindentmsg (msg, s->loc);
+
+ if (!showdeep) {
+ break;
+ }
+
s = s->previous;
}
andersk / splint.git / blobdiff