/*
** 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
static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef p_s) /*@*/ ;
static void sRef_setPartsFromUentry (sRef p_s, uentry p_ue)
/*@modifies p_s@*/ ;
-static bool checkDeadState (/*@notnull@*/ sRef p_el, bool p_tbranch, fileloc p_loc);
+static bool checkDeadState (/*@notnull@*/ sRef p_el, /*@null@*/ sRef p_e2,
+ bool p_tbranch, fileloc p_loc);
static /*@dependent@*/ sRef sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef p_t) /*@*/ ;
static void
}
}
-static bool
- sRef_hasAliasInfoLoc (sRef s)
+bool sRef_hasAliasInfoLoc (sRef s)
{
return (sRef_isReasonable (s) && (s->aliasinfo != NULL)
&& (fileloc_isDefined (s->aliasinfo->loc)));
}
-static /*@falsewhennull@*/ bool
-sRef_hasStateInfoLoc (sRef s)
+/*@falsewhennull@*/ bool sRef_hasStateInfoLoc (sRef s)
{
return (sRef_isReasonable (s) && (s->definfo != NULL)
&& (fileloc_isDefined (s->definfo->loc)));
}
-static /*@falsewhennull@*/ bool
-sRef_hasExpInfoLoc (sRef s)
+/*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef s)
{
return (sRef_isReasonable (s)
&& (s->expinfo != NULL) && (fileloc_isDefined (s->expinfo->loc)));
{
case SK_RESULT:
{
- /* s = sRef_saveCopy(s); */ /*@i523@*/
ce = constraintExpr_makeTermsRef (s);
return ce;
}
{
sRef temp;
temp = (sRef_makePointer (sRef_fixBaseParam (s->info->ref, args)));
- /* temp = sRef_saveCopy(temp); */ /*@i523@*/
ce = constraintExpr_makeTermsRef (temp);
return ce;
}
switch (p)
{
case 'g':
- return (sRef_makeGlobal (usymId_fromInt (reader_getInt (c)), ctype_unknown, stateInfo_currentLoc ()));
+ return (sRef_makeGlobal (usymId_fromInt (reader_getInt (c)),
+ ctype_unknown, stateInfo_currentLoc ()));
case 'p':
- return (sRef_makeParam (reader_getInt (c), ctype_unknown, stateInfo_makeLoc (g_currentloc)));
+ return (sRef_makeParam (reader_getInt (c), ctype_unknown,
+ stateInfo_makeLoc (g_currentloc, SA_DECLARED)));
case 'r':
return (sRef_makeResult (ctype_undump (c)));
case 'a':
s->kind = SK_ADR;
s->type = ctype_makePointer (t->type);
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->ref = t; /* sRef_copy (t); */ /*@i32@*/
+ s->info->ref = t;
if (t->defstate == SS_UNDEFINED)
/* no! it is allocated even still: && !ctype_isPointer (t->type)) */
}
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s,
+ stateInfo_makeLoc (g_currentloc, SA_CREATED));
return s;
}
}
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->object = o;
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
return s;
}
s->type = t->type;
s->info->ref = t; /* sRef_copy (t); */ /*@i32 was exposed@*/
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_DECLARED));
return s;
}
s->type = t->type;
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
return s;
}
else
if (other->defstate != SS_UNKNOWN)
{
res->defstate = other->defstate;
+ res->definfo = stateInfo_update (res->definfo, other->definfo);
}
}
}
else
{
- if (sRef_getNullState (other) != NS_UNKNOWN && sRef_getNullState (other) != sRef_getNullState (res))
+ if (sRef_getNullState (other) != NS_UNKNOWN
+ && sRef_getNullState (other) != sRef_getNullState (res))
{
changed = TRUE;
sRef_updateNullState (res, other);
res->defstate = SS_DEAD;
}
+ res->definfo = stateInfo_update (res->definfo, other->definfo);
sRef_clearDerived (other);
sRef_clearDerived (res);
}
el->defstate == SS_PDEFINED)
{
el->defstate = SS_ALLOCATED;
+ el->definfo = stateInfo_update (el->definfo, e2->definfo);
sRef_clearDerived (el);
}
else if ((el->defstate == SS_DEAD || sRef_isKept (el)) &&
(e2->defstate == SS_DEFINED && !sRef_isKept (e2)))
{
-
- if (checkDeadState (el, TRUE, loc))
+ DPRINTF (("Checking dead: %s / %s", sRef_unparseFull (el),
+ sRef_unparseFull (e2)));
+
+ if (checkDeadState (el, e2, TRUE, loc))
{
if (sRef_isThroughArrayFetch (el))
{
else if ((e2->defstate == SS_DEAD || sRef_isKept (e2)) &&
(el->defstate == SS_DEFINED && !sRef_isKept (el)))
{
-
- if (checkDeadState (e2, FALSE, loc))
+ DPRINTF (("Checking dead: %s / %s", sRef_unparseFull (el),
+ sRef_unparseFull (e2)));
+
+ if (checkDeadState (e2, el, FALSE, loc))
{
if (sRef_isThroughArrayFetch (el))
{
{
DPRINTF (("set pdefined: %s", sRef_unparseFull (el)));
el->defstate = SS_PDEFINED;
+ el->definfo = stateInfo_update (el->definfo, e2->definfo);
}
else if (e2->defstate == SS_DEFINED &&
el->defstate == SS_PDEFINED)
{
DPRINTF (("set pdefined: %s", sRef_unparseFull (e2)));
e2->defstate = SS_PDEFINED;
+ e2->definfo = stateInfo_update (e2->definfo, el->definfo);
}
else
{
}
else /* not defined */
{
- (void) checkDeadState (el, TRUE, loc);
+ DPRINTF (("Checking dead: %s", sRef_unparseFull (el)));
+ (void) checkDeadState (el, e2, TRUE, loc);
}
}
} end_sRefSet_allElements;
{
if (sRef_isReasonable (el))
{
- (void) checkDeadState (el, FALSE, loc);
+ DPRINTF (("Checking dead: %s", sRef_unparseFull (el)));
+ (void) checkDeadState (el, sRef_undefined, FALSE, loc);
}
} end_sRefSet_allElements;
** Returns TRUE is there is an error.
*/
-static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
+static bool checkDeadState (/*@notnull@*/ sRef el, sRef e2, bool tbranch, fileloc loc)
{
/*
** usymtab_isGuarded --- the utab should still be in the
if ((sRef_isDead (el) || sRef_isKept (el))
- && !sRef_isDeepUnionField (el) && !sRef_isThroughArrayFetch (el))
+ && !sRef_isDeepUnionField (el)
+ && !sRef_isThroughArrayFetch (el))
{
if (!tbranch)
sRef_showStateInfo (el);
}
+ if (sRef_isValid (e2))
+ {
+ if (sRef_isKept (e2))
+ {
+ sRef_showAliasInfo (e2);
+ }
+ else
+ {
+ sRef_showStateInfo (e2);
+ }
+ }
+
/* prevent further errors */
el->defstate = SS_UNKNOWN;
- sRef_setAliasKind (el, AK_ERROR, fileloc_undefined);
-
+ sRef_setAliasKind (el, AK_ERROR, fileloc_undefined);
return FALSE;
}
}
static void
checkDerivDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
{
-
- if (checkDeadState (el, tbranch, loc))
+ if (checkDeadState (el, sRef_undefined, tbranch, loc))
{
sRefSet_allElements (el->deriv, t)
{
if (sRef_isReasonable (t))
{
- checkDerivDeadState (t, tbranch, loc);
+ checkDerivDeadState (t, tbranch, loc);
}
} end_sRefSet_allElements;
}
{
if (!opt)
{
- checkDerivDeadState (el, (cl == FALSECLAUSE), loc);
+ checkDerivDeadState (el, (cl == FALSECLAUSE), loc);
}
ret = sRefSet_insert (ret, el);
if (a->defstate == b->defstate)
{
s->defstate = a->defstate;
+ s->definfo = stateInfo_update (s->definfo, a->definfo);
+ s->definfo = stateInfo_update (s->definfo, b->definfo);
}
else
{
s->aliaskind = alkind_resolve (a->aliaskind, b->aliaskind);
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_MERGED));
return s;
}
else
s->aliaskind = AK_UNKNOWN;
sRef_setNullStateN (s, NS_UNKNOWN);
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_DECLARED));
DPRINTF (("Result: [%p] %s", s, sRef_unparseFull (s)));
return s;
{
if (sRef_isInvalid (s)) return (cstring_undefined);
- return (message ("[%p] %q - %q [%s] { %q } < %q >",
+ return (message ("[%p] %q - %q { %q } [%s] { %q } < %q >",
s,
sRef_unparseDebug (s),
sRef_unparseState (s),
+ stateInfo_unparse (s->definfo),
exkind_unparse (s->oexpkind),
sRefSet_unparseDebug (s->deriv),
valueTable_unparse (s->state)));
if ((kind != s->aliaskind && kind != s->oaliaskind)
&& fileloc_isDefined (loc))
{
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, stateAction_fromAlkind (kind), loc);
}
s->aliaskind = kind;
{
if (s->expkind != exp)
{
- s->expinfo = stateInfo_updateLoc (s->expinfo, loc);
+ s->expinfo = stateInfo_updateLoc (s->expinfo, stateAction_fromExkind (exp), loc);
}
s->expkind = exp;
if (sRef_isReasonable (s))
{
s->defstate = SS_UNDEFINED;
-
- if (fileloc_isDefined (loc))
- {
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
- }
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_UNDEFINED, loc);
sRef_clearDerived (s);
}
DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
- if (s->defstate != SS_DEFINED && fileloc_isDefined (loc))
- {
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
- }
-
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_DEFINED, loc);
s->defstate = SS_DEFINED;
DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
el->defstate = SS_DEFINED;
} end_sRefSet_elements ;
}
-
+
DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
}
return;
}
- if (s->defstate != SS_PDEFINED && fileloc_isDefined (loc))
- {
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
- }
-
- DPRINTF (("set pdefined: %s", sRef_unparseFull (s)));
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_PDEFINED, loc);
s->defstate = SS_PDEFINED;
/* e.g., if x is allocated, *x = 3 defines x */
{
sRef_checkMutable (s);
+ DPRINTF (("Set state: %s => %s", sRef_unparseFull (s), sstate_unparse (ss)));
+
if (sRef_isReasonable (s))
{
/* if (s->defstate == SS_RELDEF) return; */
if (s->defstate != ss && fileloc_isDefined (loc))
{
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
+ s->definfo = stateInfo_updateLoc (s->definfo,
+ stateAction_fromSState (ss), loc);
}
s->defstate = ss;
if (s->defstate == SS_DEAD || s->defstate == SS_UNDEFINED)
{
s->defstate = SS_ALLOCATED;
-
- if (fileloc_isDefined (loc))
- {
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
- }
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_ALLOCATED, loc);
}
}
}
{
if (s->aliaskind != AK_SHARED && fileloc_isDefined (loc))
{
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_SHARED, loc);
}
s->aliaskind = AK_SHARED;
if (sRef_isReasonable (s))
{
s->aliaskind = sRef_getAliasKind (ref);
- s->aliasinfo = stateInfo_updateRefLoc (s->aliasinfo, ref, loc);
+ s->aliasinfo = stateInfo_updateRefLoc (s->aliasinfo, ref, stateAction_fromAlkind (s->aliaskind), loc);
}
}
if (fileloc_isDefined (loc))
{
- s->nullinfo = stateInfo_updateLoc (s->nullinfo, loc);
+ s->nullinfo = stateInfo_updateLoc (s->nullinfo, stateAction_fromNState (ns), loc);
}
}
{
sRef_checkMutable (s);
s->aliaskind = AK_ONLY;
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_ONLY, loc);
}
}
sRef_checkMutable (s);
DPRINTF (("Setting dependent: %s", sRef_unparseFull (s)));
s->aliaskind = AK_DEPENDENT;
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_DEPENDENT, loc);
}
}
{
sRef_checkMutable (s);
s->aliaskind = AK_OWNED;
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_OWNED, loc);
}
}
sRef_checkMutable (s);
s->aliaskind = AK_KEPT;
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_KEPT, loc);
}
}
{
sRef_checkMutable (s);
s->aliaskind = AK_FRESH;
- s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
+ s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_CREATED, loc);
DPRINTF (("SetFresh: %s", sRef_unparseFull (s)));
}
}
s->aliaskind = s->oaliaskind;
s->defstate = SS_DEAD;
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
-
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_KILLED, loc);
+ DPRINTF (("State info: %s", stateInfo_unparse (s->definfo)));
sRef_clearDerived (s);
}
}
s->aliaskind = s->oaliaskind;
s->defstate = SS_HOFFA;
- s->definfo = stateInfo_updateLoc (s->definfo, loc);
+ s->definfo = stateInfo_updateLoc (s->definfo, SA_PKILLED, loc);
+ DPRINTF (("State info: %s / %s", sRef_unparse (s),
+ stateInfo_unparse (s->definfo)));
sRef_clearDerived (s);
}
t->deriv = sRefSet_newDeepCopy (s->deriv);
t->state = valueTable_copy (s->state);
-
+
DPRINTF (("Made copy: %s => %s", sRef_unparseFull (s), sRef_unparseFull (t)));
return t;
}
s->oaliaskind = s->aliaskind;
s->oexpkind = s->expkind;
-
+
DPRINTF (("sref: %s", sRef_unparseFull (s)));
}
else
if (ctype_isMutable (s->type))
{
- sRef_setExKind (s, sRef_getExKind (sp), fileloc_undefined);
-
+ s->expkind = sRef_getExKind (sp);
+ s->expinfo = stateInfo_copy (sp->expinfo);
+
s->aliaskind = sp->aliaskind;
+ s->aliasinfo = stateInfo_copy (sp->aliasinfo);
}
s->defstate = sp->defstate;
*/
}
- sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);
-
+ s->expkind = sRef_getExKind (arr);
+ s->expinfo = stateInfo_copy (arr->expinfo);
+
if (arr->aliaskind == AK_LOCAL || arr->aliaskind == AK_FRESH)
{
s->aliaskind = AK_LOCAL;
if (sRef_isObserver (arr))
{
s->expkind = XO_OBSERVER;
+ s->expinfo = stateInfo_copy (arr->expinfo);
}
}
return res;
}
- sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);
+ s->expkind = sRef_getExKind (arr);
+ s->expinfo = stateInfo_copy (arr->expinfo);
+
return s;
}
else
if (valueTable_isUndefined (s->state))
{
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable
+ (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
}
return (s);
return res;
}
- sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);
+ s->expkind = sRef_getExKind (arr);
+ s->expinfo = stateInfo_copy (arr->expinfo);
+
llassert (s->info->arrayfetch->arr == arr);
return s;
}
sRef_addDeriv (arr, s);
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
return (s);
}
}
if (sRef_isReasonable (s))
{
-
- sRef_setExKind (s, sRef_getExKind (t), g_currentloc);
+ s->expkind = sRef_getExKind (t);
+ s->expinfo = stateInfo_copy (t->expinfo);
+
s->oaliaskind = s->aliaskind;
s->oexpkind = s->expkind;
if (t->defstate == SS_UNDEFINED)
{
s->defstate = SS_UNUSEABLE;
+ s->definfo = stateInfo_copy (t->definfo);
}
else if ((t->defstate == SS_ALLOCATED) && !ctype_isSU (st))
{
s->defstate = SS_UNDEFINED;
+ s->definfo = stateInfo_copy (t->definfo);
}
else
{
s->defstate = t->defstate;
+ s->definfo = stateInfo_copy (t->definfo);
}
if (t->aliaskind == AK_LOCAL || t->aliaskind == AK_FRESH)
s->aliaskind = AK_UNKNOWN;
}
- sRef_setExKind (s, sRef_getExKind (t), fileloc_undefined);
+ s->expkind = sRef_getExKind (t);
+ s->expinfo = stateInfo_copy (t->expinfo);
+
sRef_setTypeState (s);
s->oaliaskind = s->aliaskind;
if (valueTable_isUndefined (s->state))
{
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
}
+ DPRINTF (("pointer: %s", sRef_unparseFull (s)));
return s;
}
{
sRef res = sRef_buildPointer (s);
- DPRINTF (("Res: %s", sRef_unparse (res)));
+ DPRINTF (("Res: %s", sRef_unparseFull (res)));
return res;
}
s->oaliaskind = s->aliaskind;
s->oexpkind = s->expkind;
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
DPRINTF (("Create: %s", sRef_unparseFull (s)));
return s;
s->oexpkind = s->expkind;
llassert (valueTable_isUndefined (s->state));
- s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
+ s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
return s;
}
void
sRef_showRefKilled (sRef s)
{
- if (sRef_hasStateInfoLoc (s))
+ if (sRef_isValid (s))
{
- stateInfo_display (s->definfo, sRef_unparse (s));
+ DPRINTF (("Killed: %s", sRef_unparseFull (s)));
+ if (context_getLocIndentSpaces () == 0) {
+ stateInfo_display (s->definfo, message (" Storage %q", sRef_unparseOpt (s)));
+ } else {
+ stateInfo_display (s->definfo, message ("Storage %q", sRef_unparseOpt (s)));
+ }
}
}
void
sRef_showStateInfo (sRef s)
{
- if (sRef_hasStateInfoLoc (s))
- {
- if (s->defstate == SS_DEAD)
- {
- llgenindentmsg
- (message ("Storage %qis released", sRef_unparseOpt (s)),
- sRef_getStateInfoLoc (s));
- }
- else if (s->defstate == SS_ALLOCATED || s->defstate == SS_DEFINED)
- {
- llgenindentmsg
- (message ("Storage %qis %s", sRef_unparseOpt (s),
- sstate_unparse (s->defstate)),
- sRef_getStateInfoLoc (s));
- }
- else if (s->defstate == SS_UNUSEABLE)
- {
- llgenindentmsg
- (message ("Storage %qbecomes inconsistent (clauses merge with"
- "%qreleased on one branch)",
- sRef_unparseOpt (s),
- sRef_unparseOpt (s)),
- sRef_getStateInfoLoc (s));
- }
- else
- {
- llgenindentmsg (message ("Storage %qbecomes %s",
- sRef_unparseOpt (s),
- sstate_unparse (s->defstate)),
- sRef_getStateInfoLoc (s));
- }
+ if (sRef_isValid (s)) {
+ if (context_getLocIndentSpaces () == 0) {
+ stateInfo_display (s->definfo, message (" Storage %q", sRef_unparseOpt (s)));
+ } else {
+ stateInfo_display (s->definfo, message ("Storage %q", sRef_unparseOpt (s)));
}
+ }
}
void
sRef_showExpInfo (sRef s)
{
- if (sRef_hasExpInfoLoc (s))
- {
- llgenindentmsg (message ("Storage %qbecomes %s", sRef_unparseOpt (s),
- exkind_unparse (s->expkind)),
- sRef_getExpInfoLoc (s));
+ if (sRef_isValid (s)) {
+ if (context_getLocIndentSpaces () == 0) {
+ stateInfo_display (s->expinfo, message (" Storage %q", sRef_unparseOpt (s)));
+ } else {
+ stateInfo_display (s->expinfo, message ("Storage %q", sRef_unparseOpt (s)));
}
+ }
}
void
void
sRef_showAliasInfo (sRef s)
{
- if (sRef_hasAliasInfoLoc (s))
+ if (sRef_isValid (s))
{
if (sRef_isFresh (s))
{
- llgenindentmsg
- (message ("Fresh storage %qallocated", sRef_unparseOpt (s)),
- sRef_getAliasInfoLoc (s));
+ if (context_getLocIndentSpaces () == 0) {
+ stateInfo_display (s->aliasinfo, message (" Fresh storage %q", sRef_unparseOpt (s)));
+ } else {
+ stateInfo_display (s->aliasinfo, message ("Fresh storage %q", sRef_unparseOpt (s)));
+ }
}
- else
+ else
{
- if (!sRef_isRefCounted (s))
- {
- llgenindentmsg
- (message ("Storage %qbecomes %s",
- sRef_unparseOpt (s),
- alkind_unparse (sRef_getAliasKind (s))),
- sRef_getAliasInfoLoc (s));
- }
+ if (context_getLocIndentSpaces () == 0) {
+ stateInfo_display (s->aliasinfo, message (" Storage %q", sRef_unparseOpt (s)));
+ } else {
+ stateInfo_display (s->aliasinfo, message ("Storage %q", sRef_unparseOpt (s)));
+ }
}
}
}
if (!valueTable_isDefined (s->state))
{
s->state = valueTable_create (1);
- valueTable_insert (s->state,
- cstring_copy (metaStateInfo_getName (annotationInfo_getState (a))),
- stateValue_create (annotationInfo_getValue (a), stateInfo_makeLoc (loc)));
+ valueTable_insert
+ (s->state,
+ cstring_copy (metaStateInfo_getName (annotationInfo_getState (a))),
+ stateValue_create (annotationInfo_getValue (a),
+ stateInfo_makeLoc (loc, SA_DECLARED)));
}
else
{
valueTable_update
(s->state,
metaStateInfo_getName (annotationInfo_getState (a)),
- stateValue_create (annotationInfo_getValue (a), stateInfo_makeLoc (loc)));
- DPRINTF (("state info: %s", stateInfo_unparse (stateInfo_makeLoc (loc))));
+ stateValue_create (annotationInfo_getValue (a),
+ stateInfo_makeLoc (loc, SA_DECLARED)));
+
DPRINTF (("sref: %s", sRef_unparse (s)));
DPRINTF (("sref: %s", sRef_unparseFull (s)));
}
DPRINTF (("inserting state: %s: %s %d", sRef_unparse (s), key, value));
s->state = valueTable_create (1);
valueTable_insert (s->state, cstring_copy (key),
- stateValue_create (value, stateInfo_makeLoc (loc)));
+ stateValue_create (value,
+ stateInfo_makeLoc (loc, SA_CHANGED)));
}
else
{
if (valueTable_contains (s->state, key))
{
valueTable_update
- (s->state, key, stateValue_create (value, stateInfo_makeLoc (loc)));
+ (s->state, key, stateValue_create (value,
+ stateInfo_makeLoc (loc, SA_CHANGED)));
}
else
{
valueTable_insert
- (s->state, cstring_copy (key), stateValue_create (value, stateInfo_makeLoc (loc)));
+ (s->state, cstring_copy (key),
+ stateValue_create (value, stateInfo_makeLoc (loc, SA_CHANGED)));
}
DPRINTF (("After: %s", sRef_unparseFull (s)));
andersk / splint.git / blobdiff