static void uentry_checkIterArgs (uentry p_ue);
static cstring uentry_dumpAux (uentry p_v, bool p_isParam);
-static void uentry_showWhereLastKind (uentry p_spec) /*@modifies g_msgstream@*/ ;
+static void uentry_showWhereLastKind (uentry p_spec) /*@modifies g_warningstream@*/ ;
static void uentry_combineModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr)
/*@modifies p_ue@*/ ;
bool p_mustConform, bool p_completeConform)
/*@modifies p_old, p_unew@*/;
-# ifndef NOLCL
static void uentry_setHasMods (uentry p_ue) /*@modifies p_ue@*/;
static void uentry_setHasGlobs (uentry p_ue) /*@modifies p_ue@*/;
-# endif
static void uentry_reallyFree (/*@notnull@*/ /*@only@*/ uentry p_e);
paramTypeError (/*@notnull@*/ uentry p_old, /*@notnull@*/ uentry p_oldCurrent,
ctype p_oldType, /*@notnull@*/ uentry p_unew,
/*@notnull@*/ uentry p_newCurrent,
- ctype p_newType, int p_paramno) /*@modifies g_msgstream@*/ ;
+ ctype p_newType, int p_paramno) /*@modifies g_warningstream@*/ ;
static /*@only@*/ /*@notnull@*/ uentry
uentry_makeVariableAux (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
return ue;
}
-# ifndef NOLCL
/*@notnull@*/ uentry uentry_makeSpecEnumConstant (cstring n, ctype t, fileloc loc)
{
uentry ue = uentry_makeConstant (n, t, loc);
ue->ukind = KENUMCONST;
return ue;
}
-# endif
/*@notnull@*/ uentry uentry_makeVariableLoc (cstring n, ctype t)
{
return uentry_makeVariable (n, t, setLocation (), FALSE);
}
-# ifndef NOLCL
+bool uentry_isUnnamedVariable (uentry ue)
+{
+ return uentry_isVariable (ue) && cstring_isUndefined (ue->uname);
+}
+
/*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype t)
{
return uentry_makeVariable (cstring_undefined, t, setLocation (), FALSE);
}
-# endif
/*@notnull@*/ uentry uentry_makeIdDatatype (idDecl id)
{
if (uentry_isRealFunction (ue))
{
uentryList params = uentry_getParams (ue);
+ int paramno = 0;
uentryList_elements (params, current)
{
+ paramno++;
+
if (uentry_isValid (current))
{
ctype ct = current->utype;
}
else
{
- voptgenerror
- (FLG_FIXEDFORMALARRAY,
- message ("Function parameter %q declared as "
- "manifest array (size constant is meaningless)",
- uentry_getName (current)),
- uentry_whereDeclared (current));
+ if (uentry_hasName (current))
+ {
+ voptgenerror
+ (FLG_FIXEDFORMALARRAY,
+ message ("Function parameter %q declared as "
+ "manifest array (size constant is meaningless)",
+ uentry_getName (current)),
+ uentry_whereDeclared (current));
+ }
+ else
+ {
+ voptgenerror
+ (FLG_FIXEDFORMALARRAY,
+ message ("Unnamed function parameter %d declared as "
+ "manifest array (size constant is meaningless)",
+ paramno),
+ uentry_whereDeclared (current));
+ }
}
}
else
{
if (ctype_isArray (ct))
{
- voptgenerror
- (FLG_FORMALARRAY,
- message ("Function parameter %q declared as "
- "array (treated as pointer)",
- uentry_getName (current)),
- uentry_whereDeclared (current));
+ if (uentry_hasName (current))
+ {
+ voptgenerror
+ (FLG_FORMALARRAY,
+ message ("Function parameter %q declared as "
+ "array (treated as pointer)",
+ uentry_getName (current)),
+ uentry_whereDeclared (current));
+ }
+ else
+ {
+ voptgenerror
+ (FLG_FORMALARRAY,
+ message ("Unnamed function parameter %d declared as "
+ "array (treated as pointer)",
+ paramno),
+ uentry_whereDeclared (current));
+ }
}
}
return (e);
}
-# ifndef NOLCL
void
uentry_setRefCounted (uentry e)
{
sRef_storeState (e->sref);
}
}
-# endif
void
uentry_setStatic (uentry c)
else if (qual_isUnused (qel))
{
uentry_setUsed (ue, fileloc_undefined);
+ DPRINTF (("Used: %s", uentry_unparseFull (ue)));
}
else if (qual_isExternal (qel))
{
{
fileloc loc = setLocation ();
uentry ue = uentry_makeVariable (idDecl_observeId (t), ct, loc, FALSE);
-
+
uentry_reflectQualifiers (ue, idDecl_getQuals (t));
if (!uentry_isExtern (ue))
}
}
-# ifndef NOLCL
/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t, fileloc loc)
{
return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), fileloc_copy (loc), SS_DEFINED));
}
-# endif
/*
** constants
/*@notnull@*/ uentry uentry_makeConstant (cstring n, ctype t, fileloc f)
{
- return (uentry_makeConstantAux (n, t, f, FALSE, FALSE, multiVal_unknown ()));
+ uentry ue = uentry_makeConstantAux (n, t, f, FALSE, FALSE, multiVal_unknown ());
+ return ue;
}
/*@notnull@*/ uentry uentry_makeConstantValue (cstring n, ctype t, fileloc f, bool priv, multiVal val)
{
- return (uentry_makeConstantAux (n, t, f, priv, FALSE, val));
+ uentry ue = uentry_makeConstantAux (n, t, f, priv, FALSE, val);
+ return ue;
}
/*@notnull@*/ uentry uentry_makeMacroConstant (cstring n, ctype t, fileloc f)
{
- return (uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ()));
+ uentry ue = uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ());
+ return ue;
}
/*@notnull@*/ uentry uentry_makeIdConstant (idDecl t)
}
void
-uentry_setGlobals (uentry ue, /*@owned@*/ globSet globs)
+uentry_setGlobals (uentry ue, /*@only@*/ globSet globs)
{
llassert (uentry_isValid (ue));
+ globSet_markImmutable (globs);
+
if (uentry_isIter (ue))
{
- llassert (globSet_isUndefined (ue->info->iter->globs));
- ue->info->iter->globs = globs;
+ ue->info->iter->globs = globSet_unionFree (ue->info->iter->globs, globs);
}
else
{
uentry_convertVarFunction (ue);
-
llassert (uentry_isFunction (ue));
- llassert (!ue->info->fcn->hasGlobs
- && globSet_isUndefined (ue->info->fcn->globs));
-
- ue->info->fcn->hasGlobs = TRUE;
- globSet_markImmutable (globs);
- /*@-mustfree@*/ ue->info->fcn->globs = globs;
- /*@=mustfree@*/
- }
- /*@i23*/
- /* ??? - evans 2001-09-09 not sure what's going on here...?
- if (globSet_hasStatic (globs))
- {
- context_recordFileGlobals (globs);
+ ue->info->fcn->hasGlobs = TRUE;
+ ue->info->fcn->globs = globSet_unionFree (ue->info->fcn->globs, globs);
}
- */
if (context_getFlag (FLG_GLOBALSIMPMODIFIESNOTHING))
{
FALSE, FALSE));
}
-# ifndef NOLCL
/*@notnull@*/ uentry
uentry_makePrivFunction2 (cstring n, ctype t,
typeIdSet access,
reflectImplicitFunctionQualifiers (ue, TRUE);
return (ue);
}
-# endif
uentry uentry_makeExpandedMacro (cstring s, fileloc f)
{
return FALSE;
}
-# ifndef NOLCL
/*@notnull@*/ uentry
uentry_makeTypeListFunction (cstring n, typeIdSet access, fileloc f)
{
reflectImplicitFunctionQualifiers (ue, TRUE);
return ue;
}
-# endif
/*
** datatypes
return (ret);
}
-# ifndef NOLCL
uentry
uentry_makeEnumTag (cstring n, ctype t, fileloc loc)
{
cstring_free (ename);
return ret;
}
-# endif
uentry
uentry_makeUnionTagLoc (cstring n, ctype t)
return (e);
}
-# ifndef NOLCL
static void uentry_setHasGlobs (uentry ue)
{
llassert (uentry_isFunction (ue));
ue->info->fcn->hasMods = TRUE;
}
-# endif
bool uentry_hasGlobs (uentry ue)
{
}
else if (uentry_isConstant (v))
{
- res = message ("%q = %q",
- res, multiVal_unparse (uentry_getConstantValue (v)));
+ res = message ("%q = %q / %q",
+ res, multiVal_unparse (uentry_getConstantValue (v)),
+ sRef_unparseFull (v->sref));
}
else
{
return globSet_undefined;
}
- if (l->ukind != KFCN)
+ if (uentry_isFunction (l))
+ {
+ return l->info->fcn->globs;
+ }
+ else if (uentry_isIter (l))
+ {
+ return l->info->iter->globs;
+ }
+ else if (uentry_isEndIter (l))
+ {
+ return globSet_undefined;
+ }
+ else
{
- if (l->ukind != KITER && l->ukind != KENDITER)
+ if (l->ukind == KVAR)
{
- if (l->ukind == KVAR)
- {
- llbug (message ("Bad call to uentry_getGlobs (var): %q (%s)",
+ llcontbug (message ("Bad call to uentry_getGlobs (var): %q (%s)",
uentry_unparse (l),
ekind_unparse (l->ukind)));
- }
- else
- {
- llbug (message ("Bad call to uentry_getGlobs: %q (%s)",
+ }
+ else
+ {
+ llcontbug (message ("Bad call to uentry_getGlobs: %q (%s)",
uentry_unparse (l),
ekind_unparse (l->ukind)));
- }
}
+
return globSet_undefined;
}
-
- return l->info->fcn->globs;
}
/*@observer@*/ sRefSet
return sRefSet_undefined;
}
- return l->info->fcn->mods;
+ if (uentry_isFunction (l))
+ {
+ return l->info->fcn->mods;
+ }
+ else if (uentry_isIter (l))
+ {
+ return l->info->iter->mods;
+ }
+ else if (uentry_isEndIter (l))
+ {
+ return sRefSet_undefined;
+ }
+ else
+ {
+ BADBRANCH;
+ }
}
ekind
nuentries--;
sfree (e);
- }
+}
extern void uentry_markOwned (/*@owned@*/ uentry u)
{
llassert (uentry_isValid (old));
llassert (uentry_isValid (unew));
- if (uentry_isEitherConstant (unew)
+ if ((uentry_isEitherConstant (unew) || uentry_isDatatype (unew))
&& (fileloc_isPreproc (uentry_whereDeclared (old))
|| ctype_isUnknown (old->utype))
&& !uentry_isSpecified (old))
if (optgenerror
(FLG_MATCHFIELDS,
message ("Enum %q declared with members { %q } but "
- "specified with members { %q }",
+ "%s with members { %q }",
uentry_getName (old),
enumNameList_unparse (enew),
+ uentry_specOrDefName (old),
enumNameList_unparse (eold)),
uentry_whereDeclared (unew)))
{
unew->info = uinfo_copy (old->info, old->ukind);
}
-
-uentry
-uentry_copy (uentry e)
+static uentry
+uentry_copyAux (uentry e, bool saveCopy)
{
+
if (uentry_isValid (e))
{
uentry enew = uentry_alloc ();
enew->whereDefined = fileloc_copy (e->whereDefined);
enew->whereDeclared = fileloc_copy (e->whereDeclared);
- enew->sref = sRef_saveCopy (e->sref); /* Memory leak! */
+ if (saveCopy)
+ {
+ enew->sref = sRef_saveCopy (e->sref); /* Memory leak! */
+ }
+ else
+ {
+ enew->sref = sRef_copy (e->sref);
+ }
+
enew->used = e->used;
enew->lset = FALSE;
enew->isPrivate = e->isPrivate;
}
}
+uentry
+uentry_copy (uentry e)
+{
+ return uentry_copyAux (e, TRUE);
+}
+
+uentry
+uentry_copyNoSave (uentry e)
+{
+ return uentry_copyAux (e, FALSE);
+}
+
void
uentry_setState (uentry res, uentry other)
{
*/
static void
- branchStateError (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other,
- bool flip, clause cl, fileloc loc)
+branchStateError (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other,
+ bool flip, clause cl, fileloc loc)
{
if (optgenerror
(FLG_BRANCHSTATE,
if (sRef_isDead (res->sref))
{
sRef_showStateInfo (res->sref);
+ sRef_showStateInfo (other->sref);
}
else if (sRef_isKept (res->sref))
{
sRef_showAliasInfo (res->sref);
+ sRef_showAliasInfo (other->sref);
}
else /* dependent */
{
}
# endif
-/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
+/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args, fileloc loc)
{
llassert (uentry_isRealFunction (u));
sRef res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
DPRINTF (("Returned: %s", sRef_unparseFull (res)));
- sRef_setAllocated (res, g_currentloc);
+ sRef_setAllocated (res, loc);
DPRINTF (("ensures clause: %s / %s", uentry_unparse (u),
stateClauseList_unparse (clauses)));
if (modf != NULL)
{
sRef sr = sRef_fixBase (el, res);
- modf (sr, g_currentloc);
+ modf (sr, loc);
}
}
else
usymtab_addForceMustAlias (tcref, tref); /* evans 2001-05-27 */
+ if (sRef_isNew (tcref))
+ {
+ /* tcref->kind = SK_OBJECT; */ /*!! Not new anymore */
+ }
+
if (sRef_isDead (tcref))
{
- sRef_setDefined (tcref, g_currentloc);
- sRef_setOnly (tcref, g_currentloc);
+ sRef_setDefined (tcref, loc);
+ sRef_setOnly (tcref, loc);
}
if (sRef_isRefCounted (tcref))
{
/* could be a new ref now (but only if its returned) */
- sRef_setAliasKindComplete (tcref, AK_ERROR, g_currentloc);
+ sRef_setAliasKindComplete (tcref, AK_ERROR, loc);
}
sRef_makeSafe (tcref);
+ DPRINTF (("Returns tcref / %s", sRef_unparseFull (tcref)));
prefs = sRefSet_insert (prefs, tcref);
}
}
if (nstate_isKnown (n))
{
- sRef_setNullState (res, n, g_currentloc);
+ sRef_setNullState (res, n, loc);
}
}
else
if (sRef_isRefCounted (res))
{
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+ sRef_setAliasKind (res, AK_NEWREF, loc);
}
}
if (ctype_isAbstract (ct))
{
- sRef_setNotNull (res, g_currentloc);
+ sRef_setNotNull (res, loc);
}
else
{
}
else
{
- sRef_setNotNull (res, g_currentloc);
+ sRef_setNotNull (res, loc);
}
}
}
if (sRef_isRefCounted (res))
{
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+ sRef_setAliasKind (res, AK_NEWREF, loc);
}
else if (sRef_isKillRef (res))
{
- sRef_setAliasKind (res, AK_REFCOUNTED, g_currentloc);
+ sRef_setAliasKind (res, AK_REFCOUNTED, loc);
}
else
{
{
sRef_setAliasKind (res,
alkind_fixImplicit (ak),
- g_currentloc);
+ loc);
}
sRefSet_free (prefs);
-
+
+ /*
+ if (sRef_isOnly (res))
+ {
+ sRef_setFresh (res, loc);
+ }
+ */
+
DPRINTF (("Returns ref: %s", sRef_unparseFull (res)));
return res;
}
llassert (uentry_isValid (e) && uentry_isFunction (e));
return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
}
+
+# ifdef DEBUGSPLINT
+
+/*
+** For debugging only
+*/
+
+void uentry_checkValid (uentry ue)
+{
+ if (uentry_isValid (ue))
+ {
+ sRef_checkCompletelyReasonable (ue->sref);
+ }
+}
+
+# endif
andersk / splint.git / blobdiff