/*
** 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
case SK_PARAM:
llassert (s->info->paramno >= -1);
- llassert (s->info->paramno <= 50); /*@i32 bogus...*/
+ llassert (s->info->paramno <= 999); /* sanity check */
break;
case SK_ARRAYFETCH:
/* start modifications */
s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
- s->bufinfo.size = -1; /*@i24 unknown@*/
- s->bufinfo.len = -1; /*@i24 unknown@*/
+ s->bufinfo.size = -1;
+ s->bufinfo.len = -1;
/* end modifications */
s->aliaskind = AK_UNKNOWN;
}
}
-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)));
switch (base->kind)
{
case SK_PARAM:
- res = usymtab_getRefQuiet (paramsScope, base->info->paramno);
+ res = usymtab_getRefQuiet (paramsScope, usymId_fromInt (base->info->paramno));
break;
case SK_CVAR:
switch (s->kind)
{
case SK_PARAM:
- return (usymtab_getRefQuiet (paramsScope, s->info->paramno));
+ return (usymtab_getRefQuiet (paramsScope, usymId_fromInt (s->info->paramno)));
case SK_CVAR:
return (usymtab_getRefQuiet (s->info->cvar->lexlevel, s->info->cvar->index));
case SK_CONJ:
return sRef_getUentry (s->info->conj->b);
}
}
+ case SK_FIELD: /* evans 2002-07-17: added case for SK_FIELD */
case SK_UNKNOWN:
case SK_SPECIAL:
return uentry_undefined;
{
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;
}
return ce;
}
case SK_PARAM:
- llassert(exprNodeList_size (args) > s->info->paramno);
- {
- exprNode e = exprNodeList_nth (args, s->info->paramno);
-
- llassert( !(exprNode_isError (e)) );
- ce = constraintExpr_makeExprNode (e);
- return ce;
- }
+ {
+ exprNode e;
+ llassert (exprNodeList_size (args) > s->info->paramno);
+ e = exprNodeList_nth (args, s->info->paramno);
+
+ llassert (!(exprNode_isError (e)));
+ ce = constraintExpr_makeExprNode (e);
+ return ce;
+ }
default:
{
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_UNCONSTRAINED;
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->fname = fname;
+ s->info->fname = cstring_copy (fname); /* evans 2002-07-12: this was exposed, causing memory errors */
return (s);
}
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;
}
}
sRef
sRef_makeObject (ctype o)
{
- sRef s = sRef_newRef (); /*@i423 same line is bad...@*/
+ sRef s = sRef_newRef ();
s->kind = SK_OBJECT;
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->kind = SK_EXTERNAL;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->type = t->type;
- s->info->ref = t; /* sRef_copy (t); */ /*@i32 was exposed@*/
+ s->info->ref = t;
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->kind = SK_DERIVED;
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->ref = t; /* sRef_copy (t); */ /*@i32@*/
+ s->info->ref = t;
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);
}
** Merge value table states
*/
-
- /*@i3245@*/
# if 0
/*
** This doesn't do anything. And its broken too...
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);
s->kind = SK_CONJ;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->conj = (cjinfo) dmalloc (sizeof (*s->info->conj));
- s->info->conj->a = a; /* sRef_copy (a) */ /*@i32*/ ;
- s->info->conj->b = b; /* sRef_copy (b);*/ /*@i32@*/ ;
+ s->info->conj->a = a;
+ s->info->conj->b = b;
if (ctype_equal (a->type, b->type)) s->type = a->type;
else s->type = ctype_makeConj (a->type, b->type);
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;
}
return ((s->kind == SK_CVAR) &&
(s->info->cvar->lexlevel == functionScope) &&
(context_inFunction () &&
- (s->info->cvar->index <= uentryList_size (context_getParams ()))));
+ (s->info->cvar->index <= usymId_fromInt (uentryList_size (context_getParams ())))));
}
bool sRef_isPointer (sRef s)
DPRINTF (("Free sref: [%p]", s));
sRef_checkValid (s);
+
+ multiVal_free (s->val); /* evans 2002-07-12 */
stateInfo_free (s->expinfo);
stateInfo_free (s->aliasinfo);
sRefSet_free (s->deriv);
s->deriv = sRefSet_undefined;
- /*@i43@*/ /* valueTable_free (s->state); */
+ valueTable_free (s->state);
sinfo_free (s);
s->definfo = stateInfo_undefined;
s->nullinfo = stateInfo_undefined;
- /*@i32@*/ sfree (s);
+ sfree (s);
}
}
s->kind = SK_FIELD;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->field = (fldinfo) dmalloc (sizeof (*s->info->field));
- s->info->field->rec = rec; /* sRef_copy (rec); */ /*@i32@*/
+ s->info->field->rec = rec;
s->info->field->field = f; /* doesn't copy f */
if (ctype_isKnown (ct) && ctype_isSU (ct))
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
s->info->arrayfetch = (ainfo) dmalloc (sizeof (*s->info->arrayfetch));
s->info->arrayfetch->indknown = FALSE;
s->info->arrayfetch->ind = 0;
- s->info->arrayfetch->arr = arr; /* sRef_copy (arr); */ /*@i32@*/
+ s->info->arrayfetch->arr = arr;
sRef_setArrayFetchState (s, arr);
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;
}
s->kind = SK_ARRAYFETCH;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->arrayfetch = (ainfo) dmalloc (sizeof (*s->info->arrayfetch));
- s->info->arrayfetch->arr = arr; /* sRef_copy (arr); */ /*@i32@*/
+ s->info->arrayfetch->arr = arr;
s->info->arrayfetch->indknown = TRUE;
s->info->arrayfetch->ind = i;
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;
s->kind = SK_PTR;
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->ref = t; /* sRef_copy (t); */ /*@i32*/
+ s->info->ref = t;
if (ctype_isRealAP (rt))
{
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;
}
s1->nullstate = s2->nullstate;
s1->nullinfo = stateInfo_update (s1->nullinfo, s2->nullinfo);
- /*@-mustfree@*/
- /*@i834 don't free it: valueTable_free (s1->state); */
- /*@i32@*/ s1->state = valueTable_copy (s2->state);
- /*@=mustfree@*/
+ valueTable_free (s1->state);
+ s1->state = valueTable_copy (s2->state);
s1->safe = s2->safe;
}
}
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;
/* start modification */
s->bufinfo.bufstate = BB_NULLTERMINATED;
/* end modification */
- if (ctype_isUA (ct))
+
+ /* evans 2002-04-22: added isManifestBool to avoid errors for -boolfalse initializations */
+ if (!ctype_isManifestBool (ct) && ctype_isUA (ct))
{
typeId uid = ctype_typeId (ct);
uentry te = usymtab_getTypeEntrySafe (uid);
}
}
-
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));
return s;
}
void
sRef_showRefKilled (sRef s)
{
- if (sRef_hasStateInfoLoc (s))
+ if (sRef_isValid (s))
{
- llgenindentmsg (message ("Storage %q released",
- sRef_unparse (s)), sRef_getStateInfoLoc (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 (n != old && n != NS_UNKNOWN)
{
- sRef_setNullState (s, n, g_currentloc);
+ sRef_setNullState (s, n, g_currentloc);
}
}
else
sRef_possiblyNull (sRef s)
{
if (sRef_isReasonable (s))
- {
- if (sRef_getNullState (s) == NS_ABSNULL)
+ {
+ if (sRef_getNullState (s) == NS_ABSNULL)
{
ctype rct = ctype_realType (s->type);
-
+
if (ctype_isAbstract (rct))
{
return FALSE;
return nstate_possiblyNull (sRef_getNullState (s));
}
}
-
+
return FALSE;
}
{
res->aliaskind = AK_KEPT;
}
+ else if ((ares == AK_OWNED && aother == AK_ONLY)
+ || (aother == AK_OWNED && ares == AK_ONLY))
+ {
+ res->aliaskind = AK_OWNED;
+
+ if (aother == AK_OWNED)
+ {
+ res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
+ }
+ }
else
{
hasError = TRUE;
ret->arrayfetch = (ainfo) dmalloc (sizeof (*ret->arrayfetch));
ret->arrayfetch->indknown = s->info->arrayfetch->indknown;
ret->arrayfetch->ind = s->info->arrayfetch->ind;
- ret->arrayfetch->arr = s->info->arrayfetch->arr; /* sRef_copy (s->info->arrayfetch->arr); */ /*@i32@*/
+ ret->arrayfetch->arr = s->info->arrayfetch->arr;
break;
case SK_FIELD:
ret = (sinfo) dmalloc (sizeof (*ret));
ret->field = (fldinfo) dmalloc (sizeof (*ret->field));
- ret->field->rec = s->info->field->rec; /* sRef_copy (s->info->field->rec); */ /*@i32@*/
+ ret->field->rec = s->info->field->rec;
ret->field->field = s->info->field->field;
break;
ret = (sinfo) dmalloc (sizeof (*ret));
ret->spec = s->info->spec;
break;
+
case SK_UNCONSTRAINED:
case SK_NEW:
ret = (sinfo) dmalloc (sizeof (*ret));
ret->fname = s->info->fname;
break;
+
case SK_RESULT:
case SK_CONST:
case SK_TYPE:
case SK_PTR:
case SK_ADR:
case SK_DERIVED:
- case SK_EXTERNAL: /*@i32 is copy now! */
+ case SK_EXTERNAL: /* is copy now! */
break;
case SK_CONJ:
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)));
** Default defined state can be made special.
*/
- llassert (sRef_isReasonable (s)); /*@i523 why doesn't null-checking work!??? */
+ llassert (sRef_isReasonable (s));
if (s->defstate == SS_UNKNOWN || s->defstate == SS_DEFINED || s->defstate == SS_SPECIAL)
{
return ( ctype_isFixedArray (c) );
}
-long int sRef_getArraySize (sRef p_s) /*@*/ {
+size_t sRef_getArraySize (sRef p_s) /*@*/
+{
ctype c;
llassert (sRef_isFixedArray(p_s) );
DPRINTF (( message ("sRef_getArraySize getting array size for %s", sRef_unparse(p_s) ) ));
c = sRef_getType (p_s);
-
- return (ctype_getArraySize (c) );
+ return (ctype_getArraySize (c));
}
void sRef_setValue (sRef s, multiVal val)
{
- llassert (sRef_isReasonable (s));
+ if (!sRef_isReasonable (s))
+ {
+ llcontbuglit ("Unreasonable sRef");
+ llcontbug (message ("sRef: %s", sRef_unparse (s)));
+ return;
+ }
+
multiVal_free (s->val);
s->val = val;
}
andersk / splint.git / blobdiff