/*
** 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
** 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
*/
/*
** uentry.c
*/
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
# include "structNames.h"
# include "nameChecks.h"
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,
/*@exposed@*/ sRef p_s, bool p_priv, vkind p_kind);
+static /*@only@*/ /*@notnull@*/ uentry
+ uentry_makeConstantAux (cstring p_n, ctype p_t,
+ /*@keep@*/ fileloc p_f, bool p_priv, bool p_macro,
+ /*@only@*/ multiVal p_m) /*@*/ ;
+
static void uentry_convertVarFunction (uentry ue) /*@modifies ue@*/
{
if (uentry_isVariable (ue)
{
functionConstraint constraint;
- DPRINTF( (message ("called uentry_getFcnPostconditions on %s",
+ DPRINTF((message ("called uentry_getFcnPostconditions on %s",
uentry_unparse (ue) ) ) );
if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
{
- DPRINTF( (message ("called uentry_getFunctionConditions on nonfunction %s",
+ DPRINTF((message ("called uentry_getFunctionConditions on nonfunction %s",
uentry_unparse (ue) ) ) );
if (!uentry_isFunction (ue) )
{
if (!uentry_isFunction(ue))
{
- DPRINTF( (message ("called uentry_getFunctionConditions on non function %s",
+ DPRINTF((message ("called uentry_getFunctionConditions on non function %s",
uentry_unparse (ue) ) ) );
return constraintList_undefined;
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)
{
ctype ct = idDecl_getCtype (id);
uentry ue = uentry_makeDatatype (idDecl_observeId (id), ct,
- MAYBE, MAYBE, setLocation ());
+ MAYBE, qual_createUnknown (),
+ setLocation ());
uentry_reflectQualifiers (ue, idDecl_getQuals (id));
- if (!ynm_isOn (ue->info->datatype->abs))
+ if (!qual_isEitherAbstract (ue->info->datatype->abs))
{
if (ctype_isUnknown (ct))
{
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));
+ }
}
}
if (uentry_hasGlobs (ue))
{
- voptgenerror
+ vgenhinterror
(FLG_SYNTAX,
message
("Multiple globals clauses for %q: %q",
uentry_getName (ue),
globalsClause_unparse (glc)),
+ cstring_makeLiteral ("Only one globals clause may be used. The second globals clause is ignored."),
globalsClause_getLoc (glc));
- uentry_setGlobals (ue, globalsClause_takeGlobs (glc)); /*@i32@*/
+
+ /*
+ uentry_setGlobals (ue, globalsClause_takeGlobs (glc));
+ */
}
else
{
+ DPRINTF (("Taking globs: %s", globalsClause_unparse (glc)));
uentry_setGlobals (ue, globalsClause_takeGlobs (glc));
+ DPRINTF (("Taking globs after: %s", globalsClause_unparse (glc)));
}
}
else if (functionClause_isModifies (el))
return (e);
}
-# ifndef NOLCL
void
uentry_setRefCounted (uentry e)
{
sRef_storeState (e->sref);
}
}
-# endif
void
uentry_setStatic (uentry c)
if (uentry_isVariable (ue))
{
- /*@i634 ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
+
+ /*@i634 ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
sRef_setDefState (sr, ue->info->var->defstate, fileloc_undefined);
sRef_setNullState (sr, ue->info->var->nullstate, fileloc_undefined);
}
}
-static void uentry_addStateClause (uentry ue, stateClause sc)
+static void uentry_addStateClause (/*@notnull@*/ uentry ue, stateClause sc)
{
/*
** Okay to allow multiple clauses of the same kind.
void uentry_addWarning (uentry ue, /*@only@*/ warnClause warn)
{
+ llassert (uentry_isValid (ue));
llassert (warnClause_isUndefined (ue->warn));
ue->warn = warn;
}
if (functionConstraint_isDefined (ue->info->fcn->preconditions))
{
- /* drl 11-29-2001
+ /*drl oops this date is wronge...*/
+ /* drl 11-29-2002
I changed this so it didn't appear as a Splint bug
among other things this gets triggered when there is
a function with two requires clauses. Now Splint
}
else
{
- llfatalbug ( (message("uentry_setPreconditions called with invalid uentry") ));
+ llfatalbug ((message("uentry_setPreconditions called with invalid uentry") ));
}
}
}
else
{
- llfatalbug ( (message("uentry_setPostconditions called with invalid uentry") ));
+ llfatalbug ((message("uentry_setPostconditions called with invalid uentry") ));
}
}
uentry_setNullState (ue, NS_MNOTNULL);
}
else if (qual_isAbstract (qel)
+ || qual_isNumAbstract (qel)
|| qual_isConcrete (qel))
{
if (!uentry_isDatatype (ue))
}
else
{
- ue->info->datatype->abs = ynm_fromBool (qual_isAbstract (qel));
+ ue->info->datatype->abs = qel;
+ DPRINTF (("Setting abstract %s: %s",
+ uentry_unparse (ue), qual_unparse (qel)));
}
}
else if (qual_isMutable (qel))
else if (qual_isUnused (qel))
{
uentry_setUsed (ue, fileloc_undefined);
+ DPRINTF (("Used: %s", uentry_unparseFull (ue)));
}
else if (qual_isExternal (qel))
{
ctype ct = idDecl_getCtype (t);
ctype base = ct;
fileloc loc = setLocation ();
- sRef pref = sRef_makeParam (i, ct, stateInfo_makeLoc (loc));
+ sRef pref = sRef_makeParam (i, ct, stateInfo_makeLoc (loc, SA_CREATED));
uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, loc, pref);
DPRINTF (("Make param: %s", uentry_unparseFull (ue)));
{
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
*/
-/*@only@*/ /*@notnull@*/
+static /*@only@*/ /*@notnull@*/
uentry uentry_makeConstantAux (cstring n, ctype t,
- /*@keep@*/ fileloc f, bool priv,
+ /*@keep@*/ fileloc f, bool priv, bool macro,
/*@only@*/ multiVal m)
{
uentry e = uentry_alloc ();
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
e->info->uconst->access = typeIdSet_undefined;
+ e->info->uconst->macro = macro;
uentry_setSpecDef (e, f);
/*@notnull@*/ uentry uentry_makeConstant (cstring n, ctype t, fileloc f)
{
- return (uentry_makeConstantAux (n, t, f, 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)
+{
+ uentry ue = uentry_makeConstantAux (n, t, f, priv, FALSE, val);
+ return ue;
+}
+
+/*@notnull@*/ uentry uentry_makeMacroConstant (cstring n, ctype t, fileloc f)
+{
+ uentry ue = uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ());
+ return ue;
}
/*@notnull@*/ uentry uentry_makeIdConstant (idDecl t)
}
static /*@only@*/ /*@notnull@*/
- uentry uentry_makeVariableAux (cstring n, ctype t,
- fileloc f,
- /*@exposed@*/ sRef s,
- bool priv, vkind kind)
+uentry uentry_makeVariableAux (cstring n, ctype t,
+ fileloc f,
+ /*@exposed@*/ sRef s,
+ bool priv, vkind kind)
{
uentry e = uentry_alloc ();
ctype rt = t;
-
+
DPRINTF (("Make variable: %s %s %s", n, ctype_unparse (t), sRef_unparse (s)));
e->ukind = KVAR;
it allocates memory and sets the fields. We check if the type of the variable
is a pointer or array and allocate a `bbufinfo' struct accordingly */
- if( ctype_isArray (t) || ctype_isPointer(t)) {
- /*@i222@*/e->info->var->bufinfo = dmalloc( sizeof(*e->info->var->bufinfo) );
- e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
- /*@access sRef@*/ /*i@222*/
- /* It probably isn't necessary to violate the abstraction here
- I'll fix this later
- */
- s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
- /*@noaccess sRef@*/
- } else {
- e->info->var->bufinfo = NULL;
- }/* end else */
-/* end modification */
+ if (ctype_isArray (t) || ctype_isPointer(t))
+ {
+ /*@i222@*/ e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
+ e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
+ sRef_setNotNullTerminatedState (s);
+ }
+ else
+ {
+ e->info->var->bufinfo = NULL;
+ }/* end else */
+ /* end modification */
return (e);
}
}
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
/* is exported for use by usymtab_interface */
/*@notnull@*/ uentry
- uentry_makeDatatypeAux (cstring n, ctype t, ynm mut, ynm abstract,
+ uentry_makeDatatypeAux (cstring n, ctype t, ynm mut, qual abstract,
fileloc f, bool priv)
{
uentry e = uentry_alloc ();
uentry_setDefined (e, f);
}
- if (ynm_isOn (abstract) && !(uentry_isCodeDefined (e)))
+ if (qual_isAbstract (abstract) && !(uentry_isCodeDefined (e)))
{
sRef_setNullState (e->sref, NS_ABSNULL, uentry_whereDeclared (e));
}
}
/*@notnull@*/ uentry
- uentry_makeDatatype (cstring n, ctype t, ynm mut, ynm abstract, fileloc f)
+ uentry_makeDatatype (cstring n, ctype t, ynm mut, qual abstract, fileloc f)
{
return (uentry_makeDatatypeAux (n, t, mut, abstract, f, FALSE));
}
-/*@notnull@*/ uentry uentry_makeBoolDatatype (ynm abstract)
+/*@notnull@*/ uentry uentry_makeBoolDatatype (qual abstract)
{
uentry ret = uentry_makeDatatypeAux (context_getBoolName (),
ctype_bool, NO, abstract,
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->datatype = (udinfo) dmalloc (sizeof (*e->info->datatype));
- e->info->datatype->abs = NO;
+ e->info->datatype->abs = qual_createUnknown ();
e->info->datatype->mut = (kind == KENUMTAG) ? NO : MAYBE;
e->info->datatype->type = t;
e->warn = warnClause_undefined; /*@i452@*/
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)
{
case KINVALID:
case KELIPSMARKER:
- /* bug detected by lclint:
+ /* bug detected by splint:
** uentry.c:753,14: Return value type bool does not match declared type int: TRUE
*/
return 0;
u2->info->datatype->type));
COMPARERETURN (ynm_compare (u1->info->datatype->mut,
u2->info->datatype->mut));
- return (ynm_compare (u1->info->datatype->abs, u2->info->datatype->abs));
+ return (generic_compare (u1->info->datatype->abs, u2->info->datatype->abs));
}
BADEXIT;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
e->info->uconst->access = access;
-
+ e->info->uconst->macro = FALSE; /*@i523! fix this when macro info added to library */
uentry_setConstantValue (e, m);
sRef_storeState (e->sref);
}
static /*@only@*/ uentry
-uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, ynm abstract,
+uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, qual abstract,
ynm mut, ctype rtype, alkind ak, exkind exp,
sstate defstate, nstate isnull,
/*@only@*/ fileloc loc)
sRef_setDefState (e->sref, defstate, loc);
- if (ynm_isOn (abstract) && ctype_isUnknown (ct) && isnull == NS_UNKNOWN)
+ if (qual_isEitherAbstract (abstract) && ctype_isUnknown (ct) && isnull == NS_UNKNOWN)
{
isnull = NS_ABSNULL;
}
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)
{
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->datatype = (udinfo) dmalloc (sizeof (*e->info->datatype));
- e->info->datatype->abs = NO;
+ e->info->datatype->abs = qual_createUnknown ();
e->info->datatype->mut = MAYBE;
e->info->datatype->type = rtype;
break;
case KDATATYPE:
{
- ynm abstract;
+ qual abstract;
ynm mut;
ctype rtype;
sstate defstate;
alkind aliased;
exkind exp;
- advanceField (s); abstract = ynm_fromCodeChar (reader_loadChar (s));
+ advanceField (s); abstract = qual_abstractFromCodeChar (reader_loadChar (s));
advanceField (s); mut = ynm_fromCodeChar (reader_loadChar (s));
advanceField (s); defstate = sstate_fromInt (reader_getInt (s));
advanceField (s); isnull = nstate_fromInt (reader_getInt (s));
else
{
sdump = message ("%d@%d@%d@%d@%d",
- (int) dss,
+ (int) dss,
(int) nst,
(int) alk,
(int) exk,
ctype_unparse (v->utype), (int) v->utype));
*/
- return (message ("%q@%s@%s@%d@%d@%d@%d@%q#%s",
+ return (message ("%q@%c@%s@%d@%d@%d@%d@%q#%s",
ctype_dump (v->utype),
- ynm_unparseCode (v->info->datatype->abs),
+ qual_abstractCode (v->info->datatype->abs),
ynm_unparseCode (v->info->datatype->mut),
(int) sRef_getDefState (v->sref),
(int) sRef_getNullState (v->sref),
{
cstring res;
- res = message ("[%w] %s %s: %s [spec: %q; decl: %q; def: %q]",
- (unsigned long) v, ekind_unparse (v->ukind), v->uname,
+ res = message ("[%p] %s %s: %s [spec: %q; decl: %q; def: %q]",
+ v, ekind_unparse (v->ukind), v->uname,
ctype_unparse (v->utype),
fileloc_unparse (uentry_whereSpecified (v)),
fileloc_unparse (uentry_whereDeclared (v)),
(ctype_isDefined (v->info->datatype->type)
? v->info->datatype->type : ctype_unknown),
ynm_unparse (v->info->datatype->mut),
- ynm_unparse (v->info->datatype->abs),
+ qual_unparse (v->info->datatype->abs),
sRef_unparseState (v->sref));
}
else if (uentry_isFunction (v))
}
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
{
typeId oldid;
llassert (uentry_isDatatype (e)
- && (ynm_isMaybe (e->info->datatype->abs)));
+ && (qual_isUnknown (e->info->datatype->abs)));
oldid = ctype_typeId (e->info->datatype->type);
- e->info->datatype->abs = YES;
+ e->info->datatype->abs = qual_createAbstract ();
e->info->datatype->type = ctype_createAbstract (oldid);
}
uentry_setConcrete (uentry e)
{
llassert (uentry_isDatatype (e)
- && (ynm_isMaybe (e->info->datatype->abs)));
+ && (qual_isUnknown (e->info->datatype->abs)
+ || qual_isConcrete (e->info->datatype->abs)));
- e->info->datatype->abs = NO;
+ e->info->datatype->abs = qual_createConcrete ();
}
bool
uentry_isAbstractDatatype (uentry e)
{
return (uentry_isDatatype (e)
- && (ynm_isOn (e->info->datatype->abs)));
+ && (qual_isEitherAbstract (e->info->datatype->abs)));
}
bool
uentry_isMaybeAbstract (uentry e)
{
return (uentry_isDatatype (e)
- && (ynm_isMaybe (e->info->datatype->abs)));
+ && (!qual_isConcrete (e->info->datatype->abs)));
}
bool
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;
+ }
+# ifdef WIN32
+/* Make Microsoft VC++ happy */
+# pragma warning (disable:4715)
+# endif
}
+# ifdef WIN32
+# pragma warning (enable:4715)
+# endif
+
ekind
uentry_getKind (uentry e)
{
{
ctype ct = l->utype;
- llassert (ctype_isFunction (ct));
+ /*drl 12/10/2002 changed to fix bug involving multiple redefines of library functions in macros. Bug was reported by Malcolm Parsons
+
+ Old code was simplly llassert (ctype_isFunction (ct) );
+ */
+
+ llassert (ctype_isFunction (ct) || context_inMacro() );
+
return (ctype_argsFunction (ct));
}
BADDEFAULT;
if (uentry_isAbstractType (e))
{
- e->info->datatype->type = ctype_createAbstract (uid);
+ if (qual_isNumAbstract (e->info->datatype->abs))
+ {
+ e->info->datatype->type = ctype_createNumAbstract (uid);
+ }
+ else
+ {
+ llassert (qual_isAbstract (e->info->datatype->abs));
+ e->info->datatype->type = ctype_createAbstract (uid);
+ }
}
else
{
{
ucinfo ret = (ucinfo) dmalloc (sizeof (*ret));
ret->access = u->access;
+ ret->macro = u->macro;
return ret;
}
ret->defstate = u->defstate;
ret->checked = u->checked;
- /*@i523 ret->origsref = sRef_copy (u->origsref); */
/* drl added 07-02-001 */
/* copy null terminated information */
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)))
{
paramno++;
/*
- ** Forgot this! detected by lclint:
+ ** Forgot this! detected by splint:
** uentry.c:1257,15: Suspected infinite loop
*/
}
}
}
- if (unew->info->datatype->abs != MAYBE)
+ if (!qual_isUnknown (unew->info->datatype->abs))
{
- if (ynm_isOff (old->info->datatype->abs)
- && ynm_isOn (unew->info->datatype->abs))
+ if (qual_isConcrete (old->info->datatype->abs)
+ && qual_isEitherAbstract (unew->info->datatype->abs))
{
if (!ctype_isDirectBool (old->utype))
{
}
}
}
- else if (ynm_isOn (old->info->datatype->abs)
- && ynm_isOff (unew->info->datatype->abs))
+ else if (qual_isEitherAbstract (old->info->datatype->abs)
+ && qual_isConcrete (unew->info->datatype->abs))
{
if (!ctype_isDirectBool (old->utype))
{
}
else
{
- if (ynm_isOn (old->info->datatype->abs))
+ if (qual_isEitherAbstract (old->info->datatype->abs))
{
old->sref = unew->sref;
unew->info->datatype->mut = old->info->datatype->mut;
}
else
{
- if (ynm_isOn (old->info->datatype->abs))
+ if (qual_isEitherAbstract (old->info->datatype->abs))
{
if (ynm_isOn (old->info->datatype->mut) && ynm_isOff (unew->info->datatype->mut))
{
static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old)
{
- ekind okind = unew->ukind;
+ ekind okind;
llassert (uentry_isValid (unew));
llassert (uentry_isValid (old));
DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
-
+ okind = unew->ukind;
unew->ukind = old->ukind;
llassert (cstring_equal (unew->uname, old->uname));
unew->utype = old->utype;
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,
sRef_stateAltVerb (res->sref), clause_nameFlip (cl, !flip)),
loc))
{
+ DPRINTF (("Here: %s / %s", sRef_unparseFull (res->sref), sRef_unparseFull (other->sref)));
+
if (sRef_isDead (res->sref))
{
- sRef_showStateInfo (res->sref);
+ if (sRef_hasStateInfoLoc (res->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+ sRef_showStateInfo (res->sref);
+ }
+
+ if (sRef_hasStateInfoLoc (other->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+ sRef_showStateInfo (other->sref);
+ }
}
else if (sRef_isKept (res->sref))
{
- sRef_showAliasInfo (res->sref);
+ if (sRef_hasAliasInfoLoc (res->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+ sRef_showAliasInfo (res->sref);
+ }
+
+ if (sRef_hasAliasInfoLoc (other->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+ sRef_showAliasInfo (other->sref);
+ }
}
else /* dependent */
{
- sRef_showAliasInfo (res->sref);
- sRef_showAliasInfo (other->sref);
+ if (sRef_hasAliasInfoLoc (res->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+ sRef_showAliasInfo (res->sref);
+ }
+
+ if (sRef_hasAliasInfoLoc (other->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+ sRef_showAliasInfo (other->sref);
+ }
}
sRef_setAliasKind (res->sref, AK_ERROR, fileloc_undefined);
{
if (sRef_isDead (other->sref))
{
- sRef_showStateInfo (other->sref);
+ if (sRef_hasStateInfoLoc (other->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+ sRef_showStateInfo (other->sref);
+ }
+
+ if (sRef_hasStateInfoLoc (res->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+ sRef_showStateInfo (res->sref);
+ }
}
else /* kept */
{
- sRef_showAliasInfo (other->sref);
+ if (sRef_hasAliasInfoLoc (other->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+ sRef_showAliasInfo (other->sref);
+ }
+
+ if (sRef_hasAliasInfoLoc (res->sref)) {
+ llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+ sRef_showAliasInfo (res->sref);
+ }
}
sRef_setAliasKind (res->sref, AK_ERROR, fileloc_undefined);
}
static void
-uentry_mergeAliasStates (uentry res, uentry other, fileloc loc,
- bool mustReturn, bool flip, bool opt,
+uentry_mergeAliasStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other,
+ fileloc loc, bool mustReturn, bool flip, bool opt,
clause cl)
{
sRef rs = res->sref;
}
else
{
- branchStateError (res, other, flip, cl, loc);
+ branchStateError (res, other, !flip, cl, loc); /* evans 2002-12-15: changed flip to !flip */
}
}
}
}
static void
-uentry_mergeValueStates (uentry res, uentry other, fileloc loc, bool mustReturn, /*@unused@*/ bool flip)
+uentry_mergeValueStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other,
+ fileloc loc, bool mustReturn, /*@unused@*/ bool flip)
{
valueTable rvalues;
valueTable ovalues;
static void
-uentry_mergeSetStates (uentry res, uentry other, /*@unused@*/ fileloc loc,
+uentry_mergeSetStates (/*@notnull@*/ uentry res,
+ /*@notnull@*/ uentry other, /*@unused@*/ fileloc loc,
bool flip, clause cl)
{
if (cl == DOWHILECLAUSE)
uentry_mergeAliasStates (res, other, loc, mustReturn, flip, opt, cl);
uentry_mergeValueStates (res, other, loc, mustReturn, flip);
uentry_mergeSetStates (res, other, loc, flip, cl);
+
+ DPRINTF (("Merge ==> %s", uentry_unparseFull (res)));
}
void uentry_setUsed (uentry e, fileloc loc)
|| u->info->var->kind == VKSEFRETPARAM));
}
+/*@i52323@*/
+# if 0
/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
{
llassert (uentry_isRealFunction (u));
alkind ak;
sRefSet prefs = sRefSet_new ();
sRef res = sRef_undefined;
+ sRef tcref = sRef_undefined;
+ sRef tref = sRef_undefined;
int paramno = 0;
params = uentry_getParams (u);
-
+
+ /*
+ ** Setting up aliases has to happen *after* setting null state!
+ */
+
uentryList_elements (params, current)
{
if (uentry_isReturned (current))
if (exprNodeList_size (args) >= paramno)
{
exprNode ecur = exprNodeList_nth (args, paramno);
- sRef tref = exprNode_getSref (ecur);
+ tref = exprNode_getSref (ecur);
DPRINTF (("Returned reference: %s", sRef_unparseFull (tref)));
if (sRef_isValid (tref))
{
- sRef tcref = sRef_copy (tref);
+ tcref = sRef_copy (tref);
- usymtab_addForceMustAlias (tcref, tref); /* evans 2001-05-27 */
-
if (sRef_isDead (tcref))
{
sRef_setDefined (tcref, g_currentloc);
paramno++;
} end_uentryList_elements ;
-
+
if (sRefSet_size (prefs) > 0)
{
nstate n = sRef_getNullState (u->sref);
-
+
if (sRefSet_size (prefs) == 1)
{
- res = sRefSet_choose (prefs);
+ sRef rref = sRefSet_choose (prefs);
+ tref = rref;
+ res = sRef_makeType (sRef_getType (rref));
+ sRef_copyState (res, tref);
}
else
{
if (nstate_isKnown (n))
{
sRef_setNullState (res, n, g_currentloc);
+ DPRINTF (("Setting null: %s", sRef_unparseFull (res)));
}
}
else
}
else
{
+ DPRINTF (("Making new from %s -->", uentry_unparseFull (u)));
res = sRef_makeNew (ctype_unknown, u->sref, u->uname);
}
}
}
-
if (sRef_getNullState (res) == NS_ABSNULL)
{
ctype ct = ctype_realType (u->utype);
ak = sRef_getAliasKind (res);
+ if (alkind_isImplicit (ak))
+ {
+ sRef_setAliasKind (res, alkind_fixImplicit (ak), g_currentloc);
+ }
+
+# if 0
+ DPRINTF (("Aliasing: %s / %s", sRef_unparseFull (res), sRef_unparseFull (tref)));
+ usymtab_addReallyForceMustAlias (tref, res); /* evans 2001-05-27 */
+
+ /* evans 2002-03-03 - need to be symettric explicitly, since its not a local now */
+ usymtab_addReallyForceMustAlias (res, tref);
+# endif
+
+ sRefSet_free (prefs);
+
+ DPRINTF (("Returns ref: %s", sRef_unparseFull (res)));
+ return res;
+ }
+}
+# endif
+
+/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args, fileloc loc)
+{
+ llassert (uentry_isRealFunction (u));
+
+ if (ctype_isFunction (u->utype) && sRef_isStateSpecial (uentry_getSref (u)))
+ {
+ stateClauseList clauses = uentry_getStateClauseList (u);
+ sRef res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
+
+ DPRINTF (("Returned: %s", sRef_unparseFull (res)));
+ sRef_setAllocated (res, loc);
+
+ DPRINTF (("ensures clause: %s / %s", uentry_unparse (u),
+ stateClauseList_unparse (clauses)));
+
+ /*
+ ** This should be in exprNode_reflectEnsuresClause
+ */
+
+ stateClauseList_postElements (clauses, cl)
+ {
+ if (!stateClause_isGlobal (cl))
+ {
+ sRefSet refs = stateClause_getRefs (cl);
+ sRefMod modf = stateClause_getEffectFunction (cl);
+
+ sRefSet_elements (refs, el)
+ {
+ sRef base = sRef_getRootBase (el);
+
+ if (sRef_isResult (base))
+ {
+ if (modf != NULL)
+ {
+ sRef sr = sRef_fixBase (el, res);
+ modf (sr, loc);
+ }
+ }
+ else
+ {
+ ;
+ }
+ } end_sRefSet_elements ;
+ }
+ } end_stateClauseList_postElements ;
+
+ return res;
+ }
+ else
+ {
+ uentryList params;
+ alkind ak;
+ sRefSet prefs = sRefSet_new ();
+ sRef res = sRef_undefined;
+ int paramno = 0;
+
+ params = uentry_getParams (u);
+
+ uentryList_elements (params, current)
+ {
+ if (uentry_isReturned (current))
+ {
+ if (exprNodeList_size (args) >= paramno)
+ {
+ exprNode ecur = exprNodeList_nth (args, paramno);
+ sRef tref = exprNode_getSref (ecur);
+
+ DPRINTF (("Returned reference: %s", sRef_unparseFull (tref)));
+
+ if (sRef_isValid (tref))
+ {
+ sRef tcref = sRef_copy (tref);
+
+ 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, 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, loc);
+ }
+
+ sRef_makeSafe (tcref);
+ DPRINTF (("Returns tcref / %s", sRef_unparseFull (tcref)));
+ prefs = sRefSet_insert (prefs, tcref);
+ }
+ }
+ }
+
+ paramno++;
+ } end_uentryList_elements ;
+
+ if (sRefSet_size (prefs) > 0)
+ {
+ nstate n = sRef_getNullState (u->sref);
+
+ if (sRefSet_size (prefs) == 1)
+ {
+ res = sRefSet_choose (prefs);
+ }
+ else
+ {
+ /* should this ever happen? */ /*@i534 evans 2001-05-27 */
+ res = sRefSet_mergeIntoOne (prefs);
+ }
+
+ if (nstate_isKnown (n))
+ {
+ sRef_setNullState (res, n, loc);
+ }
+ }
+ else
+ {
+ if (ctype_isFunction (u->utype))
+ {
+ DPRINTF (("Making new from %s -->", uentry_unparseFull (u)));
+ res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
+ }
+ else
+ {
+ res = sRef_makeNew (ctype_unknown, u->sref, u->uname);
+ }
+
+ if (sRef_isRefCounted (res))
+ {
+ sRef_setAliasKind (res, AK_NEWREF, loc);
+ }
+ }
+
+
+ if (sRef_getNullState (res) == NS_ABSNULL)
+ {
+ ctype ct = ctype_realType (u->utype);
+
+ if (ctype_isAbstract (ct))
+ {
+ sRef_setNotNull (res, loc);
+ }
+ else
+ {
+ if (ctype_isUser (ct))
+ {
+ sRef_setStateFromUentry (res, usymtab_getTypeEntry (ctype_typeId (ct)));
+ }
+ else
+ {
+ sRef_setNotNull (res, loc);
+ }
+ }
+ }
+
+ if (sRef_isRefCounted (res))
+ {
+ sRef_setAliasKind (res, AK_NEWREF, loc);
+ }
+ else if (sRef_isKillRef (res))
+ {
+ sRef_setAliasKind (res, AK_REFCOUNTED, loc);
+ }
+ else
+ {
+ ;
+ }
+
+ ak = sRef_getAliasKind (res);
+
if (alkind_isImplicit (ak))
{
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;
}
fileloc_free (tloc);
uentry_setHasNameError (ue);
- if (context_getFlag (FLG_REPEATUNRECOG))
+ if (context_getFlag (FLG_REPEATUNRECOG) || (context_inOldStyleScope()))
{
uentry_markOwned (ue);
}
*/
-void uentry_setPossiblyNullTerminatedState (uentry p_e) {
- /*@access sRef@*/ /*i523 shouldn't do this! */
- if( uentry_isValid(p_e) ) {
- if( p_e->info != NULL) {
- if( p_e->info->var != NULL) {
- p_e->info->var->bufinfo->bufstate = BB_POSSIBLYNULLTERMINATED;
- p_e->sref->bufinfo.bufstate = BB_POSSIBLYNULLTERMINATED;
- return;
- }
- }
- }
- /*@noaccess sRef@*/
+void uentry_setPossiblyNullTerminatedState (uentry p_e)
+{
+ llassert (uentry_isValid (p_e));
- fprintf(stderr, "uentry:Error in setPossiblyNullTerminatedState\n");
+ if (p_e->info != NULL)
+ {
+ if (p_e->info->var != NULL)
+ {
+ llassert (p_e->info->var->bufinfo != NULL);
+ p_e->info->var->bufinfo->bufstate = BB_POSSIBLYNULLTERMINATED;
+ sRef_setPossiblyNullTerminatedState (p_e->sref);
+ }
+ }
}
/*
*/
void uentry_setNullTerminatedState (uentry p_e) {
- if( uentry_isValid(p_e) ) {
- if( p_e->info != NULL) {
- if( p_e->info->var != NULL) {
- p_e->info->var->bufinfo->bufstate = BB_NULLTERMINATED;
- /*@access sRef@*/ /*@i523 bad!*/
- p_e->sref->bufinfo.bufstate = BB_NULLTERMINATED;
- /*@noaccess sRef@*/
- return;
- }
- }
- }
+ llassert (uentry_isValid (p_e));
- fprintf(stderr, "uentry:Error in setNullTerminatedState\n");
+ if (p_e->info != NULL)
+ {
+ if (p_e->info->var != NULL)
+ {
+ llassert (p_e->info->var->bufinfo != NULL);
+ p_e->info->var->bufinfo->bufstate = BB_NULLTERMINATED;
+ sRef_setNullTerminatedState (p_e->sref);
+ }
+ }
}
/*
effects: sets the size of the buffer
*/
-void uentry_setSize (uentry p_e, int size) {
- if( uentry_isValid(p_e) ) {
- if( p_e->info != NULL) {
- if( p_e->info->var != NULL) {
- p_e->info->var->bufinfo->size = size;
- /*@access sRef@*/ /*@i523 bad!*/
- p_e->sref->bufinfo.size = size;
- /*@noaccess sRef@*/
- return;
- }
+void uentry_setSize (uentry p_e, int size)
+{
+ if (uentry_isValid (p_e))
+ {
+ if (p_e->info != NULL)
+ {
+ if (p_e->info->var != NULL)
+ {
+ llassert (p_e->info->var->bufinfo != NULL);
+ p_e->info->var->bufinfo->size = size;
+ sRef_setSize (p_e->sref, size);
+ }
+ }
}
- }
-
- fprintf(stderr, "uentry:Error in setSize\n");
}
-
/*
requires: p_e is defined, is a ptr/array variable
modifies: p_e
effects: sets the length of the buffer
*/
-void uentry_setLen (uentry p_e, int len) {
- if( uentry_isValid(p_e) ) {
- if( p_e->info != NULL) {
- if( p_e->info->var != NULL) {
- p_e->info->var->bufinfo->len = len;
- /*@access sRef@*/ /*@i523 bad!*/
- p_e->sref->bufinfo.len = len;
- /*@noaccess sRef@*/
- return;
- }
+void uentry_setLen (uentry p_e, int len)
+{
+ if (uentry_isValid (p_e))
+ {
+ if (p_e->info != NULL
+ && p_e->info->var != NULL)
+ {
+ llassert (p_e->info->var->bufinfo != NULL);
+ p_e->info->var->bufinfo->len = len;
+ sRef_setLen (p_e->sref, len);
+ }
}
- }
-
- fprintf(stderr, "uentry:Error in setLen\n");
}
/*@=type*/
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