/*
** 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 /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/
{
uentry ue = (uentry) dmalloc (sizeof (*ue));
- ue->warn = warnClause_undefined; /*@i32@*/
+ ue->warn = warnClause_undefined;
nuentries++;
totuentries++;
{
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 (ctype_isFixedArray (ct))
{
+ DPRINTF (("Array: %s / %s",
+ ctype_unparse (ct),
+ ctype_unparse (ctype_baseArrayPtr (ct))));
+
if (ctype_isArray (ctype_baseArrayPtr (ct))
&& !ctype_isFixedArray (ctype_baseArrayPtr (ct)))
{
}
else
{
- if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype)))
+ if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype))
+ || ctype_isNumAbstract (ctype_getReturnType (ue->utype)))
{
; /* Immutable objects are not shared. */
}
uentry e = uentry_alloc ();
ctype ret;
- llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
-
- DPRINTF (("Make function: %s", n));
+ llassert (warnClause_isUndefined (warn));
if (ctype_isFunction (t))
{
**
*/
- uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); /*@i32@*/
+ uentry_combineModifies (ue, modifiesClause_takeMods (mlc));
}
else
{
static /*@only@*/ /*@notnull@*/ uentry
uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s,
- /*@only@*/ fileloc loc, sstate defstate) /*@i32 exposed*/
+ /*@only@*/ fileloc loc, sstate defstate)
{
cstring pname = makeParam (n);
uentry e;
if (uentry_isVariable (ue))
{
-
- /*@i634 ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
+ /* removed this: no need to copy? 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);
}
{
/*
** Okay to allow multiple clauses of the same kind.
- */ /*@i834 is this true?@*/
+ */
ue->info->fcn->specclauses =
stateClauseList_add (ue->info->fcn->specclauses, sc);
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))
uentry_unparse (ue)),
uentry_whereLast (ue)))
{
- /*@i! annotationInfo_showContextError (ainfo, ue); */
+ /* annotationInfo_showContextError (ainfo, ue); */
}
}
}
/*@notnull@*/ uentry uentry_makeParam (idDecl t, int i)
{
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)));
+ DPRINTF (("Base: %s [%d]", ctype_unparse (ct), ctype_isFixedArray (ct)));
uentry_reflectQualifiers (ue, idDecl_getQuals (t));
uentry_implicitParamAnnots (ue);
- /* Parameter type [][] or [x][] is invalid */
+ if (ctype_isArray (ct))
+ {
+ /* Parameter type [][] or [x][] is invalid, but [][x] is okay */
+ ctype base = ctype_baseArrayPtr (ct);
- while (ctype_isFixedArray (base)) {
- base = ctype_baseArrayPtr (base);
- }
-
- if (ctype_isIncompleteArray (base)) {
- base = ctype_baseArrayPtr (base);
-
- if (ctype_isArray (base)) {
- if (!uentry_hasName (ue)) {
- (void) optgenerror (FLG_INCOMPLETETYPE,
- message ("Unnamed function parameter %d is incomplete type (inner array must have bounds): %s",
- i + 1,
- ctype_unparse (ct)),
- uentry_whereLast (ue));
- } else {
- (void) optgenerror (FLG_INCOMPLETETYPE,
- message ("Function parameter %q is incomplete type (inner array must have bounds): %s",
- uentry_getName (ue),
- ctype_unparse (ct)),
- uentry_whereLast (ue));
- }
+ DPRINTF (("Check array: %s / Base: %s", ctype_unparse (ct),
+ ctype_unparse (base)));
+
+ if (ctype_isIncompleteArray (base))
+ {
+ if (!uentry_hasName (ue))
+ {
+ voptgenerror
+ (FLG_INCOMPLETETYPE,
+ message ("Unnamed function parameter %d is incomplete type "
+ "(inner array must have bounds): %s",
+ i + 1,
+ ctype_unparse (ct)),
+ uentry_whereLast (ue));
+ }
+ else
+ {
+ voptgenerror
+ (FLG_INCOMPLETETYPE,
+ message ("Function parameter %q is incomplete type "
+ "(inner array must have bounds): %s",
+ uentry_getName (ue),
+ ctype_unparse (ct)),
+ uentry_whereLast (ue));
+ }
+ }
}
- }
-
+
DPRINTF (("Param: %s", uentry_unparseFull (ue)));
return ue;
}
e->utype = t;
e->storageclass = SCNONE;
- e->warn = warnClause_undefined; /*@i32 warnings for constants? */
+ e->warn = warnClause_undefined; /* Don't support warnings for constants */
e->sref = sRef_makeConst (t);
e->storageclass = SCNONE;
- e->warn = warnClause_undefined; /*@i32 warnings for variable @*/
+ e->warn = warnClause_undefined; /* Don't support warnings for variables yet @*/
e->sref = s;
e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
e->info->var->kind = kind;
- /*@i523 e->info->var->origsref = sRef_saveCopy (e->sref); */
+ /* removed: e->info->var->origsref = sRef_saveCopy (e->sref); */
e->info->var->checked = CH_UNKNOWN;
DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref)));
sRef_setStateFromType (e->sref, rt);
}
- DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref)));
e->info->var->defstate = sRef_getDefState (e->sref);
e->info->var->nullstate = sRef_getNullState (e->sref);
if (ctype_isArray (t) || ctype_isPointer(t))
{
- /*@i222@*/ e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
+ e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
sRef_setNotNullTerminatedState (s);
}
}/* end else */
/* end modification */
+ DPRINTF (("New variable: %s", sRef_unparseFull (e->sref)));
+
return (e);
}
/*@only@*/ warnClause warn,
fileloc f)
{
- llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
+ llassert (warnClause_isUndefined (warn));
return (uentry_makeFunctionAux (n, t,
((typeId_isInvalid (access)) ? typeIdSet_emptySet ()
: typeIdSet_single (access)),
/* 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_setSpecDef (e, f);
- e->warn = warnClause_undefined; /*@i634@*/
+ e->warn = warnClause_undefined;
e->uses = filelocList_new ();
e->isPrivate = priv;
e->hasNameError = FALSE;
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,
uentry_setSpecDef (e, f);
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->uses = filelocList_new ();
e->isPrivate = FALSE;
e->hasNameError = FALSE;
e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
e->info->enditer->access = access;
+ e->warn = warnClause_undefined;
- e->warn = warnClause_undefined; /*@i452@*/
return (e);
}
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@*/
+ e->warn = warnClause_undefined;
if (uentry_isDeclared (e))
{
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->used = FALSE;
e->lset = FALSE;
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
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 */
+ e->info->uconst->macro = FALSE; /* fix this when macro info added to library */
uentry_setConstantValue (e, m);
sRef_storeState (e->sref);
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
}
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;
}
e->isPrivate = FALSE;
e->hasNameError = FALSE;
-
- e->warn = warnClause_undefined; /*@i452@*/
-
+ e->warn = warnClause_undefined;
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
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;
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->iter = (uiinfo) dmalloc (sizeof (*e->info->iter));
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
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))
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
uentry_isMutableDatatype (uentry e)
{
- bool res = uentry_isDatatype (e)
- && (ynm_toBoolRelaxed (e->info->datatype->mut));
-
- return res;
+ if (uentry_isDatatype (e))
+ {
+ if (ctype_isNumAbstract (e->info->datatype->type))
+ {
+ return FALSE;
+ }
+ else
+ {
+ return ynm_toBoolRelaxed (e->info->datatype->mut);
+ }
+ }
+
+ return FALSE;
}
bool
}
}
+# ifdef WIN32
+/* Make Microsoft VC++ happy */
+# pragma warning (disable : 4715)
+# endif
+
/*@observer@*/ sRefSet
uentry_getMods (uentry l)
{
uentry_getKind (uentry e)
{
llassert (uentry_isValid (e));
-
return (e->ukind);
}
sRef uentry_getOrigSref (uentry e)
{
- /*@i523*/ /* evans 2001-09-09 - need to fix this
+ /* evans 2003-04-12 - removed for now */
+ /* evans 2001-09-09 - need to fix this
if (uentry_isValid (e))
{
if (uentry_isVariable (e))
ctype uentry_getRealType (uentry e)
{
ctype ct;
- typeId uid = USYMIDINVALID;
+ typeId uid = typeId_invalid;
if (uentry_isInvalid (e))
{
return ctype_unknown;
}
-
- llassertprint (uentry_isDatatype (e), ("not datatype: %s", uentry_unparse (e)));
+
+ if (!uentry_isDatatype (e))
+ {
+ /* This shouldn't happen, except when types are redeclared in strange ways */
+ return ctype_unknown;
+ }
if (uentry_isAnyTag (e))
{
if (ctype_isUA (ct))
{
- usymId iid = ctype_typeId (ct);
+ typeId iid = ctype_typeId (ct);
- if (usymId_equal (iid, uid))
+ if (typeId_equal (iid, uid))
{
llcontbug (message ("uentry_getRealType: recursive type! %s",
ctype_unparse (ct)));
ctype uentry_getForceRealType (uentry e)
{
ctype ct;
- typeId uid = USYMIDINVALID;
+ typeId uid = typeId_invalid;
if (uentry_isInvalid (e))
{
if (ctype_isUA (ct))
{
- usymId iid = ctype_typeId (ct);
+ typeId iid = ctype_typeId (ct);
- if (usymId_equal (iid, uid))
+ if (typeId_equal (iid, uid))
{
llcontbug (message ("uentry_getRealType: recursive type! %s",
ctype_unparse (ct)));
}
void
-uentry_setDatatype (uentry e, usymId uid)
+uentry_setDatatype (uentry e, typeId uid)
{
llassert (uentry_isDatatype (e));
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
{
ret->defstate = u->defstate;
ret->checked = u->checked;
- /*@i523 ret->origsref = sRef_copy (u->origsref); */
/* drl added 07-02-001 */
/* copy null terminated information */
}
}
+static void uentry_convertIntoFunction (/*@notnull@*/ uentry old)
+{
+ /*
+ ** Convert old into a function
+ */
+
+ old->ukind = KFCN;
+ old->utype = ctype_unknown;
+ old->info->fcn = (ufinfo) dmalloc (sizeof (*old->info->fcn));
+ old->info->fcn->hasMods = FALSE;
+ old->info->fcn->hasGlobs = FALSE;
+ old->info->fcn->exitCode = XK_UNKNOWN;
+ old->info->fcn->nullPred = qual_createUnknown ();
+ old->info->fcn->specialCode = SPC_NONE;
+ old->info->fcn->access = typeIdSet_undefined;
+ old->info->fcn->globs = globSet_undefined;
+ old->info->fcn->defparams = uentryList_undefined;
+ old->info->fcn->mods = sRefSet_undefined;
+ old->info->fcn->specclauses = NULL;
+ old->info->fcn->preconditions = NULL;
+ old->info->fcn->postconditions = NULL;
+}
+
static void
checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
/*@notnull@*/ uentry unew,
if (ctype_isKnown (oldType))
{
- llassert (ctype_isFunction (oldType));
- oldRetType = ctype_getReturnType (oldType);
+ if (ctype_isFunction (oldType))
+ {
+ oldRetType = ctype_getReturnType (oldType);
+ }
+ else
+ {
+ if (optgenerror
+ (FLG_INCONDEFS,
+ message ("%s %q declared as function, but previously declared as %s",
+ ekind_capName (unew->ukind),
+ uentry_getName (unew),
+ ekind_unparseLong (old->ukind)),
+ uentry_whereDeclared (unew)))
+ {
+ uentry_showWhereLast (old);
+ }
+
+ uentry_convertIntoFunction (old);
+ return;
+ }
}
if (ctype_isKnown (newType))
}
*/
- /*@i23 need checking @*/
-
+ /* need to add some checking @*/
old->info->fcn->specclauses = unew->info->fcn->specclauses;
}
else
{
- /*@i43 should be able to append? @*/
+ /* should be able to append? */
stateClauseList_checkEqual (old, unew);
stateClauseList_free (unew->info->fcn->specclauses);
/*@-branchstate@*/
}
}
- /*@=branchstate@*/ /*@i23 shouldn't need this@*/
+ /*@=branchstate@*/ /* shouldn't need this */
if (fileloc_isUndefined (old->whereDeclared))
{
{
/* no change */
}
-/*@i523 @*/ }
+ /*@-compmempass@*/
+} /*@=compmempass@*/ /* I think this is a spurious warning */
void
uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m)
}
}
- 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))
{
llassert (uentry_isFunction (spec));
}
- DPRINTF (("Merge entries: %s / %s",
- uentry_unparseFull (spec),
+ DPRINTF (("Merge entries: %s / %s", uentry_unparseFull (spec),
uentry_unparseFull (def)));
uentry_mergeConstraints (spec, def);
uentry_convertVarFunction (old);
}
- llassert (uentry_isFunction (old));
+ if (!uentry_isFunction (old))
+ {
+ if (optgenerror
+ (FLG_INCONDEFS,
+ message ("%s %q declared as function, but previously declared as %s",
+ ekind_capName (unew->ukind),
+ uentry_getName (unew),
+ ekind_unparseLong (old->ukind)),
+ uentry_whereDeclared (unew)))
+ {
+ uentry_showWhereLast (old);
+ }
+
+ uentry_convertIntoFunction (old);
+ return;
+ }
}
DPRINTF (("uentry merge: %s / %s",
}
else
{
- fileloc_free (unew->whereSpecified); /*@i523 why no error without this? */
+ fileloc_free (unew->whereSpecified);
unew->whereSpecified = fileloc_copy (old->whereSpecified);
}
}
else
{
- fileloc_free (unew->whereDefined); /*@i523 why no error without this? */
+ fileloc_free (unew->whereDefined);
unew->whereDefined = fileloc_copy (old->whereDefined);
}
}
else
{
- fileloc_free (unew->whereDeclared); /*@i523 why no error without this? */
+ fileloc_free (unew->whereDeclared);
unew->whereDeclared = fileloc_copy (old->whereDeclared);
}
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);
- sRef_showStateInfo (other->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);
- 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);
+ }
}
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);
}
else
{
- branchStateError (res, other, flip, cl, loc);
+ branchStateError (res, other, !flip, cl, loc); /* evans 2002-12-15: changed flip to !flip */
}
}
}
** Copy values from other
*/
- /*@i$@#@*/
- DPRINTF (("Has value table: %s", sRef_unparseFull (other->sref)));
- DPRINTF (("No value table: %s", sRef_unparseFull (res->sref)));
- ;
+ /* ??? */
}
else
{
if (nval == stateValue_error)
{
- /*@i32 print extra info for assignments@*/
-
if (uentry_isGlobalMarker (res))
{
if (optgenerror
if (uentry_isValid (e))
{
- int dp;
-
if (warnClause_isDefined (e->warn))
{
flagSpec flg = warnClause_getFlag (e->warn);
}
}
- if ((dp = uentry_directParamNo (e)) >= 0)
+ if (usymId_isValid (usymtab_directParamNo (e)))
{
- uentry_setUsed (usymtab_getParam (dp), loc);
+ uentry_setUsed (usymtab_getParam (usymId_toInt (usymtab_directParamNo (e))), loc);
}
e->used = TRUE;
|| u->info->var->kind == VKSEFRETPARAM));
}
-/*@i52323@*/
-# if 0
-/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
-{
- 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, g_currentloc);
-
- 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, g_currentloc);
- }
- }
- else
- {
- ;
- }
- } end_sRefSet_elements ;
- }
- } end_stateClauseList_postElements ;
-
- return res;
- }
- else
- {
- uentryList params;
- 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);
- tref = exprNode_getSref (ecur);
-
- DPRINTF (("Returned reference: %s", sRef_unparseFull (tref)));
-
- if (sRef_isValid (tref))
- {
- tcref = sRef_copy (tref);
-
- if (sRef_isDead (tcref))
- {
- sRef_setDefined (tcref, g_currentloc);
- sRef_setOnly (tcref, g_currentloc);
- }
-
- if (sRef_isRefCounted (tcref))
- {
- /* could be a new ref now (but only if its returned) */
- sRef_setAliasKindComplete (tcref, AK_ERROR, g_currentloc);
- }
-
- sRef_makeSafe (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)
- {
- sRef rref = sRefSet_choose (prefs);
- tref = rref;
- res = sRef_makeType (sRef_getType (rref));
- sRef_copyState (res, tref);
- }
- else
- {
- /* should this ever happen? */ /*@i534 evans 2001-05-27 */
- res = sRefSet_mergeIntoOne (prefs);
- }
-
- if (nstate_isKnown (n))
- {
- sRef_setNullState (res, n, g_currentloc);
- DPRINTF (("Setting null: %s", sRef_unparseFull (res)));
- }
- }
- 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
- {
- DPRINTF (("Making new from %s -->", uentry_unparseFull (u)));
- res = sRef_makeNew (ctype_unknown, u->sref, u->uname);
- }
-
- if (sRef_isRefCounted (res))
- {
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
- }
- }
-
- if (sRef_getNullState (res) == NS_ABSNULL)
- {
- ctype ct = ctype_realType (u->utype);
-
- if (ctype_isAbstract (ct))
- {
- sRef_setNotNull (res, g_currentloc);
- }
- else
- {
- if (ctype_isUser (ct))
- {
- sRef_setStateFromUentry (res, usymtab_getTypeEntry (ctype_typeId (ct)));
- }
- else
- {
- sRef_setNotNull (res, g_currentloc);
- }
- }
- }
-
- if (sRef_isRefCounted (res))
- {
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
- }
- else if (sRef_isKillRef (res))
- {
- sRef_setAliasKind (res, AK_REFCOUNTED, g_currentloc);
- }
- else
- {
- ;
- }
-
- 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));
}
else
{
- /* should this ever happen? */ /*@i534 evans 2001-05-27 */
+ /* should this ever happen? */
res = sRefSet_mergeIntoOne (prefs);
}
return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
}
+
+bool uentry_hasBufStateInfo (uentry ue)
+{
+ llassert (uentry_isValid (ue));
+ return (ue->info->var->bufinfo != NULL);
+}
+
+bool uentry_isNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return ue->info->var->bufinfo->bufstate == BB_NULLTERMINATED;
+}
+
+bool uentry_isPossiblyNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return (ue->info->var->bufinfo->bufstate == BB_POSSIBLYNULLTERMINATED);
+}
+
+bool uentry_isNotNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return (ue->info->var->bufinfo->bufstate == BB_NOTNULLTERMINATED);
+}
+
# ifdef DEBUGSPLINT
/*
andersk / splint.git / blobdiff