uentry_makeVariableAux (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
/*@exposed@*/ sRef p_s, bool p_priv, vkind p_kind);
+static void uentry_convertVarFunction (uentry ue) /*@modifies ue@*/
+{
+ if (uentry_isVariable (ue)
+ && (ctype_isFunction (ctype_realType (uentry_getType (ue)))
+ || ctype_isUnknown (uentry_getType (ue))))
+ {
+ uentry_makeVarFunction (ue);
+ }
+}
+
static /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/
{
uentry ue = (uentry) dmalloc (sizeof (*ue));
}
static cstring uentry_getOptName (uentry p_e) /*@*/ ;
-static void uentry_copyInto (/*@out@*/ /*@unique@*/ uentry p_unew, uentry p_old);
+static void uentry_updateInto (/*@unique@*/ uentry p_unew, uentry p_old) /*@modifies p_unew, p_old@*/ ;
+
static void uentry_setNullState (/*@notnull@*/ uentry p_ue, nstate p_ns);
static void uentry_setAliasKind (/*@notnull@*/ uentry p_ue, alkind p_ak);
static /*@only@*/ /*@null@*/ uinfo uinfo_copy (uinfo p_u, ekind p_kind);
static void uinfo_free (/*@only@*/ uinfo p_u, ekind p_kind);
+static void ucinfo_free (/*@only@*/ ucinfo p_u);
static void uvinfo_free (/*@only@*/ uvinfo p_u);
# ifdef DOANNOTS
}
}
-
-/*drl7x*/
-/*@only@*/ constraintList uentry_getFcnPreconditions (uentry ue)
+static constraintList uentry_getFunctionConditions (uentry ue, bool isPost)
{
if (uentry_isValid (ue))
{
- {
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- DPRINTF(( (message( "Function pointer %s not doing uentry_getFcnPreconditions", uentry_unparse(ue) )) ));
- // uentry_makeVarFunction (ue);
- }
-
- //llassert (uentry_isFunction (ue));
- //llassert ((ue->info->fcn->preconditions));
- //llassert ((ue->info->fcn->preconditions));
-
- if (!uentry_isFunction (ue))
- {
- DPRINTF( (message ("called uentry_getFcnPreconditions on nonfunction %s",
- uentry_unparse (ue) ) ) );
- if (!uentry_isSpecified (ue) )
- {
- DPRINTF((message ("called uentry_getFcnPreconditions on nonfunction %s",
- uentry_unparse (ue) ) ));
- return constraintList_undefined;
- }
-
-
- return constraintList_undefined;
- }
-
- if (functionConstraint_hasBufferConstraint (ue->info->fcn->preconditions))
- {
- return constraintList_copy (functionConstraint_getBufferConstraint (ue->info->fcn->preconditions));
- }
- else
- {
- return NULL;
- }
- }
- }
-
- return constraintList_undefined;
-}
-
-
-
+ functionConstraint constraint;
-/*drl
- 12/28/2000
-*/
-constraintList uentry_getFcnPostconditions (uentry ue)
-{
- if (uentry_isValid (ue))
- {
DPRINTF( (message ("called uentry_getFcnPostconditions on %s",
- uentry_unparse (ue) ) ) );
+ uentry_unparse (ue) ) ) );
+
+ if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- DPRINTF( (message ("called uentry_getFcnPostconditions on nonfunction %s",
- uentry_unparse (ue) ) ) );
- if (!uentry_isFunction (ue) )
- {
- DPRINTF((message ("called uentry_getFcnPostconditions on nonfunction %s",
- uentry_unparse (ue) ) ));
- return constraintList_undefined;
- }
-
-
- return constraintList_undefined;
- }
-
- // llassert (uentry_isFunction (ue));
- if (!uentry_isFunction(ue) )
+ DPRINTF( (message ("called uentry_getFunctionConditions on nonfunction %s",
+ uentry_unparse (ue) ) ) );
+ if (!uentry_isFunction (ue) )
{
-
- DPRINTF( (message ("called uentry_getFcnPostconditions on non function %s",
- uentry_unparse (ue) ) ) );
- return constraintList_undefined;
-
+ DPRINTF((message ("called uentry_getFunctionConditions on nonfunction %s",
+ uentry_unparse (ue) ) ));
+ return constraintList_undefined;
}
+
+
+ return constraintList_undefined;
+ }
+
+ if (!uentry_isFunction(ue))
+ {
+
+ DPRINTF( (message ("called uentry_getFunctionConditions on non function %s",
+ uentry_unparse (ue) ) ) );
+ return constraintList_undefined;
+
+ }
- if (functionConstraint_hasBufferConstraint (ue->info->fcn->postconditions))
- {
- DPRINTF((message ("called uentry_getFcnPostconditions on %s and returned %q",
- uentry_unparse (ue),
- constraintList_unparse (functionConstraint_getBufferConstraint (ue->info->fcn->postconditions)))));
+ llassert (uentry_isFunction (ue));
- return constraintList_copy (functionConstraint_getBufferConstraint (ue->info->fcn->postconditions));
- }
- else
- {
- return NULL;
- }
+ if (isPost)
+ {
+ constraint = ue->info->fcn->postconditions;
}
-
+ else
+ {
+ constraint = ue->info->fcn->preconditions;
+ }
+
+ return functionConstraint_getBufferConstraints (constraint);
}
return constraintList_undefined;
}
+/*drl7x*/
+/*@only@*/ constraintList uentry_getFcnPreconditions (uentry ue)
+{
+ return uentry_getFunctionConditions (ue, FALSE);
+}
+
+/*drl
+ 12/28/2000
+*/
+
+constraintList uentry_getFcnPostconditions (uentry ue)
+{
+ return uentry_getFunctionConditions (ue, TRUE);
+}
static /*@only@*/ fileloc setLocation (void)
{
}
}
+static void uentry_setConstantValue (uentry ue, /*@only@*/ multiVal val)
+{
+ llassert (uentry_isEitherConstant (ue));
+ sRef_setValue (ue->sref, val);
+}
+
/*@notnull@*/ uentry uentry_makeEnumConstant (cstring n, ctype t)
{
fileloc loc = setLocation ();
llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
+ DPRINTF (("Make function: %s", n));
+
if (ctype_isFunction (t))
{
ret = ctype_getReturnType (t);
e->utype = t;
e->storageclass = SCNONE;
- e->sref = sRef_makeType (ret);
+ e->sref = sRef_makeResult (ret); /* evans 2001-07-19 - was sRef_makeType */
+
+ DPRINTF (("Result: %s", sRef_unparseFull (e->sref)));
if (ctype_isUA (ret))
{
else if (functionClause_isEnsures (el))
{
functionConstraint cl = functionClause_takeEnsures (el);
+ DPRINTF (("Setting post: %s / %s",
+ uentry_unparse (ue), functionConstraint_unparse (cl)));
uentry_setPostconditions (ue, cl);
}
else if (functionClause_isRequires (el))
else if (functionClause_isState (el))
{
stateClause sc = functionClause_takeState (el);
+
+ if (stateClause_isBefore (sc) && stateClause_setsMetaState (sc))
+ {
+ sRefSet rfs = stateClause_getRefs (sc);
+
+ sRefSet_elements (rfs, s)
+ {
+ if (sRef_isParam (s))
+ {
+ /*
+ ** Can't use requires on parameters
+ */
+
+ voptgenerror
+ (FLG_ANNOTATIONERROR,
+ message ("Requires clauses for %q concerns parameters %q should be "
+ "a parameter annotation instead: %q",
+ uentry_unparse (ue),
+ sRef_unparse (s),
+ stateClause_unparse (sc)),
+ stateClause_loc (sc));
+ }
+ } end_sRefSet_elements ;
+ }
+
+ DPRINTF (("State clause: %s", stateClause_unparse (sc)));
uentry_addStateClause (ue, sc);
}
else if (functionClause_isWarn (el))
}
} end_functionClauseList_elements ;
+ DPRINTF (("Checking all: %s", sRef_unparseFull (ue->sref)));
stateClauseList_checkAll (ue);
}
sRefSet_undefined, warnClause_undefined,
setLocation ());
+ DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
+
/*
** This makes parameters names print out correctly.
** (But we might be a local variable declaration for a function type...)
leaveFunc = TRUE;
}
+ DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
uentry_reflectQualifiers (ue, idDecl_getQuals (id));
+ DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
reflectImplicitFunctionQualifiers (ue, FALSE);
-
+ DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
uentry_reflectClauses (ue, idDecl_getClauses (id));
+ DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
if (!uentry_isStatic (ue)
&& cstring_equalLit (ue->uname, "main"))
}
static /*@only@*/ /*@notnull@*/ uentry
-uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, sstate defstate) /*@i32 exposed*/
+uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s,
+ /*@only@*/ fileloc loc, sstate defstate) /*@i32 exposed*/
{
cstring pname = makeParam (n);
uentry e;
DPRINTF (("Sref: %s", sRef_unparseFull (s)));
- e = uentry_makeVariableAux (pname, t, setLocation (), s, FALSE, VKPARAM);
+ e = uentry_makeVariableAux (pname, t, loc, s, FALSE, VKPARAM);
cstring_free (pname);
DPRINTF (("Param: %s", uentry_unparseFull (e)));
}
uentry
-uentry_makeVariableSrefParam (cstring n, ctype t, /*@exposed@*/ sRef s)
+uentry_makeVariableSrefParam (cstring n, ctype t, /*@only@*/ fileloc loc, /*@exposed@*/ sRef s)
{
- return (uentry_makeVariableParamAux (n, t, s, SS_UNKNOWN));
+ return (uentry_makeVariableParamAux (n, t, s, loc, SS_UNKNOWN));
}
void
}
else
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
llassertfatal (uentry_isFunction (ue));
llassert (sRefSet_isUndefined (ue->info->fcn->mods));
if (uentry_isValid (ue))
{
- {
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
- llassertfatal (uentry_isFunction (ue));
-
- if (functionConstraint_isDefined (ue->info->fcn->preconditions))
- {
- BADBRANCH; /* should conjoin constraints? */
- functionConstraint_free (ue->info->fcn->preconditions);
- ue->info->fcn->preconditions = preconditions;
- }
- else
- {
- ue->info->fcn->preconditions = preconditions;
- }
- }
+ uentry_convertVarFunction (ue);
+ llassertfatal (uentry_isFunction (ue));
+ if (functionConstraint_isDefined (ue->info->fcn->preconditions))
+ {
+ BADBRANCH; /* should conjoin constraints? */
+ /*@notreached@*/
+ ue->info->fcn->preconditions = functionConstraint_conjoin (ue->info->fcn->preconditions, preconditions);
+ }
+ else
+ {
+ ue->info->fcn->preconditions = preconditions;
+ }
}
else
{
if (uentry_isValid (ue))
{
- {
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
- llassertfatal (uentry_isFunction (ue));
-
- if (functionConstraint_isUndefined (ue->info->fcn->postconditions))
- {
- ue->info->fcn->postconditions = postconditions;
- }
- else
- {
- BADBRANCH; /* should conjoin */
- functionConstraint_free (ue->info->fcn->postconditions);
- ue->info->fcn->postconditions = postconditions;
- }
- }
+ uentry_convertVarFunction (ue);
+ llassertfatal (uentry_isFunction (ue));
+
+ if (functionConstraint_isUndefined (ue->info->fcn->postconditions))
+ {
+ ue->info->fcn->postconditions = postconditions;
+ }
+ else
+ {
+ ue->info->fcn->postconditions = functionConstraint_conjoin (ue->info->fcn->postconditions, postconditions);
+ }
}
else
{
}
else if (qual_isNullPred (qel))
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
+
if (uentry_isFunction (ue))
{
ctype typ = uentry_getType (ue);
{
if (optgenerror
(FLG_ANNOTATIONERROR,
- message ("Meta state anntation %s used in inconsistent context: %q",
+ message ("Meta state annotation %s used in inconsistent context: %q",
qual_unparse (qel),
uentry_unparse (ue)),
uentry_whereLast (ue)))
{
llassert (uentry_isValid (ue));
+ DPRINTF (("Reflect qualifiers: %s / %s",
+ uentry_unparseFull (ue), qualList_unparse (q)));
+
qualList_elements (q, qel)
{
if (qual_isStatic (qel))
} end_qualList_elements;
qualList_clear (q);
+
+ DPRINTF (("Done: %s", sRef_unparseFull (ue->sref)));
}
bool
void
uentry_setPrintfLike (uentry ue)
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
llassertfatal (uentry_isFunction (ue));
ue->info->fcn->specialCode = SPC_PRINTFLIKE;
checkSpecialFunction (ue);
void
uentry_setScanfLike (uentry ue)
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
llassertfatal (uentry_isFunction (ue));
ue->info->fcn->specialCode = SPC_SCANFLIKE;
checkSpecialFunction (ue);
void
uentry_setMessageLike (uentry ue)
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
llassertfatal (uentry_isFunction (ue));
ue->info->fcn->specialCode = SPC_MESSAGELIKE;
checkSpecialFunction (ue);
{
ctype ct = idDecl_getCtype (t);
ctype base = ct;
- sRef pref = sRef_makeParam (i, ct);
- uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, pref);
+ fileloc loc = setLocation ();
+ sRef pref = sRef_makeParam (i, ct, stateInfo_makeLoc (loc));
+ uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, loc, pref);
+ DPRINTF (("Make param: %s", uentry_unparseFull (ue)));
uentry_reflectQualifiers (ue, idDecl_getQuals (t));
uentry_implicitParamAnnots (ue);
}
# ifndef NOLCL
-/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t)
+/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t, fileloc loc)
{
- return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), SS_DEFINED));
+ return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), fileloc_copy (loc), SS_DEFINED));
}
# endif
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
- e->info->uconst->val = m;
e->info->uconst->access = typeIdSet_undefined;
uentry_setSpecDef (e, f);
sRef_setDefNull (e->sref, uentry_whereDeclared (e));
}
+ uentry_setConstantValue (e, m);
+
return (e);
}
llassert (fileloc_isUndefined (ue->whereDeclared));
ue->whereDeclared = setLocation ();
-
uentry_reflectQualifiers (ue, idDecl_getQuals (t));
+ DPRINTF (("Constant: %s", uentry_unparseFull (ue)));
return ue;
}
e->info->var->defstate = sRef_getDefState (e->sref);
e->info->var->nullstate = sRef_getNullState (e->sref);
-/* start modifications */
-/* This function sets the uentry for a pointer or array variable declaration,
- 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 */
-
+ /* start modifications */
+ /* This function sets the uentry for a pointer or array variable declaration,
+ 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;
ak = sRef_getOrigAliasKind (ue->sref);
ek = sRef_getOrigExKind (ue->sref);
+ llassert (uentry_isVariable (ue));
oldInfo = ue->info->var;
llassert (ctype_isUnknown (ue->utype) || ctype_isFunction (ue->utype));
** expanded macro is marked used (until I write a pre-processor)
*/
- ue->used |= (oldInfo->kind == VKEXPMACRO);
+ ue->used = ue->used || (oldInfo->kind == VKEXPMACRO);
ue->ukind = KFCN;
ue->info->fcn = (ufinfo) dmalloc (sizeof (*ue->info->fcn));
/*end */
/*drl 12/28/2000*/
- ue->info->fcn->postconditions = functionConstraint_undefined;
+ ue->info->fcn->postconditions = functionConstraint_undefined;
/*end */
-
if (ctype_isFunction (ue->utype))
{
if (oldInfo->kind == VKEXPMACRO)
{
- fileloc_free (loc);
- ue->whereDeclared = fileloc_undefined;
+ ;
}
else
{
uvinfo_free (oldInfo);
}
+void uentry_makeConstantFunction (uentry ue)
+{
+ alkind ak;
+ exkind ek;
+ ucinfo oldInfo;
+ fileloc loc;
+
+ llassert (uentry_isValid (ue));
+ llassert (!sRef_modInFunction ());
+
+ ak = sRef_getOrigAliasKind (ue->sref);
+ ek = sRef_getOrigExKind (ue->sref);
+
+ llassert (uentry_isConstant (ue));
+ oldInfo = ue->info->uconst;
+
+ llassert (ctype_isUnknown (ue->utype) || ctype_isFunction (ue->utype));
+
+ /*
+ ** expanded macro is marked used (until I write a pre-processor)
+ */
+
+ ue->ukind = KFCN;
+ ue->info->fcn = (ufinfo) dmalloc (sizeof (*ue->info->fcn));
+ ue->info->fcn->exitCode = XK_UNKNOWN;
+ ue->info->fcn->nullPred = qual_createUnknown ();
+ ue->info->fcn->specialCode = SPC_NONE;
+ ue->info->fcn->access = typeIdSet_undefined;
+ ue->info->fcn->hasGlobs = FALSE;
+ ue->info->fcn->globs = globSet_undefined;
+ ue->info->fcn->hasMods = FALSE;
+ ue->info->fcn->mods = sRefSet_undefined;
+ ue->info->fcn->specclauses = NULL;
+ ue->info->fcn->defparams = uentryList_undefined;
+
+ /*drl*/
+ ue->info->fcn->preconditions = functionConstraint_undefined;
+ /*end */
+
+ /*drl 12/28/2000*/
+ ue->info->fcn->postconditions = functionConstraint_undefined;
+ /*end */
+
+
+ if (ctype_isFunction (ue->utype))
+ {
+ ue->sref = sRef_makeType (ctype_getReturnType (ue->utype));
+ }
+ else
+ {
+ ue->sref = sRef_makeType (ctype_unknown);
+ }
+
+ if (sRef_isRefCounted (ue->sref))
+ {
+ ak = AK_NEWREF;
+ }
+ else
+ {
+ if (alkind_isUnknown (ak))
+ {
+ if (exkind_isKnown (ek))
+ {
+ DPRINTF (("imp dep: %s", uentry_unparseFull (ue)));
+ ak = AK_IMPDEPENDENT;
+ }
+ else
+ {
+ if (context_getFlag (FLG_RETIMPONLY))
+ {
+ if (ctype_isFunction (ue->utype)
+ && ctype_isVisiblySharable
+ (ctype_realType (ctype_getReturnType (ue->utype))))
+ {
+ if (uentryList_hasReturned (uentry_getParams (ue)))
+ {
+ ;
+ }
+ else
+ {
+ if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype)))
+ {
+ ;
+ }
+ else
+ {
+ ak = AK_IMPONLY;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ loc = ue->whereDeclared;
+
+ sRef_setAliasKind (ue->sref, ak, loc);
+ sRef_setExKind (ue->sref, ek, loc);
+
+ fileloc_free (ue->whereDefined);
+ ue->whereDefined = fileloc_undefined;
+ ucinfo_free (oldInfo);
+}
+
void
uentry_setGlobals (uentry ue, /*@owned@*/ globSet globs)
{
}
else
{
- if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
- {
- uentry_makeVarFunction (ue);
- }
+ uentry_convertVarFunction (ue);
llassert (uentry_isFunction (ue));
llassert (!ue->info->fcn->hasGlobs
return 0;
case KENUMCONST:
case KCONST:
- return (multiVal_compare (u1->info->uconst->val,
- u2->info->uconst->val));
+ return (multiVal_compare (uentry_getConstantValue (u1),
+ uentry_getConstantValue (u2)));
case KSTRUCTTAG:
case KUNIONTAG:
case KENUMTAG:
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
- e->info->uconst->val = m;
e->info->uconst->access = access;
+ uentry_setConstantValue (e, m);
sRef_storeState (e->sref);
return (e);
return (uentry_isFunction (ue) && stateClauseList_isDefined (ue->info->fcn->specclauses));
}
+bool uentry_hasConditions (uentry ue)
+{
+ return (uentry_isFunction (ue)
+ && (functionConstraint_isDefined (ue->info->fcn->preconditions)
+ || functionConstraint_isDefined (ue->info->fcn->postconditions)));
+}
+
stateClauseList uentry_getStateClauseList (uentry ue)
{
if (!uentry_isFunction (ue))
{
cstring sdump;
- if (multiVal_isUnknown (v->info->uconst->val)
+ if (multiVal_isUnknown (uentry_getConstantValue (v))
&& typeIdSet_isEmpty (uentry_accessType (v))
&& (sRef_getNullState (v->sref) == NS_UNKNOWN))
{
else
{
sdump = message ("@%q@%q@%d",
- multiVal_dump (v->info->uconst->val),
+ multiVal_dump (uentry_getConstantValue (v)),
typeIdSet_dump (uentry_accessType (v)),
(int) sRef_getNullState (v->sref));
}
else if (uentry_isFunction (v))
{
res = message ("%q / sref: %q / mods: %q / "
- "globs: %q / clauses: %q",
+ "globs: %q / clauses: %q / pre: %q / post: %q",
res,
sRef_unparseFull (v->sref),
sRefSet_unparse (v->info->fcn->mods),
globSet_unparse (v->info->fcn->globs),
- stateClauseList_unparse (v->info->fcn->specclauses));
+ stateClauseList_unparse (v->info->fcn->specclauses),
+ functionConstraint_unparse (v->info->fcn->preconditions),
+ functionConstraint_unparse (v->info->fcn->postconditions));
}
else if (uentry_isIter (v))
{
DPRINTF (("sref: %s", sRef_unparseDebug (v->sref)));
/* DPRINTF (("sref: %s", sRef_unparseDeep (v->sref))); */
}
+ else if (uentry_isConstant (v))
+ {
+ res = message ("%q = %q",
+ res, multiVal_unparse (uentry_getConstantValue (v)));
+ }
else
{
res = message ("%q :: %q", res, uentry_unparse (v));
/*@observer@*/ multiVal uentry_getConstantValue (uentry e)
{
- llassert (uentry_isEitherConstant (e));
-
- return (e->info->uconst->val);
+ llassert (uentry_isEitherConstant (e));
+ return (sRef_getValue (e->sref));
}
/*@observer@*/ uentryList
bool
uentry_isCodeDefined (uentry e)
{
- return (uentry_isValid (e) && fileloc_isDefined (e->whereDefined));
+ llassert (uentry_isValid (e));
+
+ return (fileloc_isDefined (e->whereDefined));
}
bool
llassert (uentry_isValid (ue));
- rct = ctype_realType (ue->utype);
-
- if (uentry_isVariable (ue) && (ctype_isFunction (rct) || ctype_isUnknown (rct)))
- {
- uentry_makeVarFunction (ue);
- }
-
+ uentry_convertVarFunction (ue);
llassert (uentry_isFunction (ue));
+ rct = ctype_realType (ue->utype);
+
if (ctype_isFunction (rct))
{
rettype = ctype_getReturnType (rct);
void
uentry_setRefParam (uentry e)
{
-
if (!uentry_isVar (e))
{
llbug (message ("uentry_setParam: not variable: %q", uentry_unparse (e)));
e->whereDeclared = f;
e->whereDefined = fileloc_undefined;
}
+
+ llassert (fileloc_storable (f));
}
static void
ucinfo_free (/*@only@*/ ucinfo u)
{
- multiVal_free (u->val);
sfree (u);
}
uvinfo_free (/*@only@*/ uvinfo u)
{
/*drl7x added 6/29/01 */
- /*free null terminated stuff */
- /*@i22*/
- // free(u->bufinfo);
+ free (u->bufinfo); /* evans - 2001-07-19 fixed this bug */
sfree (u);
}
ucinfo_copy (ucinfo u)
{
ucinfo ret = (ucinfo) dmalloc (sizeof (*ret));
-
- ret->val = multiVal_copy (u->val);
ret->access = u->access;
-
return ret;
}
}
}
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
}
/*
if (hasError)
{
+ DPRINTF (("Here: %s / %s",
+ uentry_unparseFull (oldCurrent),
+ uentry_unparseFull (newCurrent)));
+
if (!uentry_isUndefined (oldCurrent))
{
if (!uentry_isUndefined (newCurrent)
&& newState != SS_UNKNOWN
&& newState != SS_DEFINED)
{
- DPRINTF (("Where declared: %s / %s",
- fileloc_unparse (uentry_whereDeclared (unew)),
- bool_unparse (fileloc_isXHFile (uentry_whereDeclared (unew)))));
-
if (mustConform)
{
if (optgenerror
}
else
{
- if (!stateValue_isError (newval))
+ if (!stateValue_isError (newval)
+ && !stateValue_isImplicit (newval))
{
- if (mustConform
- && optgenerror
- (FLG_INCONDEFS,
- message ("%s %q inconsistently %rdeclared %s %s, %s as %s",
- uentry_ekindName (unew),
- uentry_getName (unew),
- uentry_isDeclared (old),
- fcnErrName (unew),
- metaStateInfo_unparseValue (msinfo,
- stateValue_getValue (newval)),
- uentry_specOrDefName (old),
- metaStateInfo_unparseValue (msinfo,
- stateValue_getValue (oldval))),
- uentry_whereDeclared (unew)))
+ if (uentry_hasName (unew)
+ || !sRef_isParam (uentry_getSref (unew)))
{
- uentry_showWhereSpecified (old);
+ if (mustConform
+ && optgenerror
+ (FLG_INCONDEFS,
+ message ("%s %q inconsistently %rdeclared %s %q, %s as %q",
+ uentry_ekindName (unew),
+ uentry_getName (unew),
+ uentry_isDeclared (old),
+ fcnErrName (unew),
+ stateValue_unparseValue (newval, msinfo),
+ uentry_specOrDefName (old),
+ stateValue_unparseValue (oldval, msinfo)),
+ uentry_whereDeclared (unew)))
+ {
+ uentry_showWhereSpecified (old);
+ }
+ }
+ else
+ {
+ if (mustConform
+ && optgenerror
+ (FLG_INCONDEFS,
+ message ("%s %d inconsistently %rdeclared %s %q, %s as %q",
+ uentry_ekindName (unew),
+ sRef_getParam (uentry_getSref (unew)),
+ uentry_isDeclared (old),
+ fcnErrName (unew),
+ stateValue_unparseValue (newval, msinfo),
+ uentry_specOrDefName (old),
+ stateValue_unparseValue (oldval, msinfo)),
+ uentry_whereDeclared (unew)))
+ {
+ uentry_showWhereSpecified (old);
+ }
}
}
}
if (uentry_isForward (old))
{
mustConform = FALSE;
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
return;
}
/*@=branchstate@*/ /*@i23 shouldn't need this@*/
}
- DPRINTF (("After state: %s",
- uentry_unparseFull (old)));
-
if (fileloc_isUndefined (old->whereDeclared))
{
old->whereDeclared = fileloc_copy (unew->whereDeclared);
llassert (uentry_isValid (ue));
llassert (uentry_isEitherConstant (ue));
- uval = ue->info->uconst->val;
+ DPRINTF (("Constant value: %s / %s", uentry_unparse (ue), multiVal_unparse (m)));
+ uval = uentry_getConstantValue (ue);
if (multiVal_isDefined (uval))
{
}
else
{
- ue->info->uconst->val = m;
- multiVal_free (uval);
+ uentry_setConstantValue (ue, m);
}
}
bool mustConform,
/*@unused@*/ bool completeConform)
{
- multiVal oldVal = old->info->uconst->val;
- multiVal newVal = unew->info->uconst->val;
+ multiVal oldval = uentry_getConstantValue (old);
+ multiVal newval = uentry_getConstantValue (unew);
- if (multiVal_isDefined (oldVal))
+ if (multiVal_isDefined (oldval))
{
- if (multiVal_isDefined (newVal))
+ if (multiVal_isDefined (newval))
{
- if (!multiVal_equiv (oldVal, newVal))
+ if (!multiVal_equiv (oldval, newval))
{
if (mustConform
&& optgenerror
ekind_capName (unew->ukind),
uentry_getName (unew),
uentry_isDeclared (old),
- multiVal_unparse (newVal)),
+ multiVal_unparse (newval)),
uentry_whereDeclared (unew)))
{
- uentry_showWhereLastExtra (old, multiVal_unparse (oldVal));
+ uentry_showWhereLastExtra (old, multiVal_unparse (oldval));
}
}
- unew->info->uconst->val = multiVal_copy (oldVal);
- multiVal_free (newVal);
+ uentry_setConstantValue (unew, multiVal_copy (oldval));
}
else
{
}
else
{
- old->info->uconst->val = multiVal_copy (newVal);
+ uentry_setConstantValue (old, multiVal_copy (newval));
}
}
** When a function is defined with an unparam macro
*/
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
return;
}
if (uentry_isExpandedMacro (old)
&& uentry_isEitherConstant (unew))
{
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
return;
}
}
}
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
return;
}
else
old->whereDefined);
}
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
old->used = unew->used = TRUE;
return;
}
sRef_storeState (unew->sref);
}
+static void uentry_mergeConstraints (uentry spec, uentry def)
+{
+ if (uentry_isFunction (def))
+ {
+ DPRINTF (("Here: %s / %s",
+ uentry_unparseFull (spec),
+ uentry_unparseFull (def)));
+ /* evans 2001-07-21 */
+ llassert (uentry_isFunction (spec));
+
+ if (functionConstraint_isDefined (def->info->fcn->preconditions))
+ {
+ if (fileloc_isXHFile (uentry_whereLast (def)))
+ {
+ llassert (uentry_isFunction (spec));
+ spec->info->fcn->preconditions = functionConstraint_conjoin (spec->info->fcn->preconditions,
+ def->info->fcn->preconditions);
+ }
+ else if (fileloc_equal (uentry_whereLast (spec), uentry_whereLast (def)))
+ {
+ ;
+ }
+ else
+ {
+ /* Check if the constraints are identical */
+
+ if (optgenerror
+ (FLG_INCONDEFS,
+ message
+ ("Preconditions for %q redeclared. Dropping previous precondition: %q",
+ uentry_getName (spec),
+ functionConstraint_unparse (spec->info->fcn->preconditions)),
+ uentry_whereLast (def)))
+ {
+ uentry_showWhereSpecified (spec);
+ }
+
+ functionConstraint_free (spec->info->fcn->preconditions);
+ spec->info->fcn->preconditions = def->info->fcn->preconditions;
+ }
+
+ def->info->fcn->preconditions = functionConstraint_undefined;
+ }
+
+ if (functionConstraint_isDefined (def->info->fcn->postconditions))
+ {
+ if (fileloc_isXHFile (uentry_whereLast (def)))
+ {
+ llassert (uentry_isFunction (spec));
+ DPRINTF (("Post: %s /++/ %s",
+ functionConstraint_unparse (spec->info->fcn->postconditions),
+ functionConstraint_unparse (def->info->fcn->postconditions)));
+ spec->info->fcn->postconditions = functionConstraint_conjoin (spec->info->fcn->postconditions,
+ def->info->fcn->postconditions);
+ def->info->fcn->postconditions = functionConstraint_undefined;
+ DPRINTF (("Conjoined post: %s", functionConstraint_unparse (spec->info->fcn->postconditions)));
+ }
+ else
+ {
+ if (optgenerror
+ (FLG_INCONDEFS,
+ message
+ ("Postconditions for %q redeclared. Dropping previous postcondition: %q",
+ uentry_getName (spec),
+ functionConstraint_unparse (spec->info->fcn->postconditions)),
+ uentry_whereLast (def)))
+ {
+ uentry_showWhereSpecified (spec);
+ }
+
+ functionConstraint_free (spec->info->fcn->postconditions);
+ spec->info->fcn->postconditions = def->info->fcn->postconditions;
+ def->info->fcn->postconditions = functionConstraint_undefined;
+ }
+ }
+ }
+}
+
/*
** modifies spec to reflect def, reports any inconsistencies
*/
llassert (uentry_isValid (spec));
llassert (uentry_isValid (def));
llassert (cstring_equal (spec->uname, def->uname));
+
+ if (uentry_isFunction (def))
+ {
+ if (uentry_isConstant (spec))
+ {
+ llassert (ctype_isUnknown (spec->utype) || ctype_isFunction (spec->utype));
+ uentry_makeConstantFunction (spec);
+ }
+ else
+ {
+ uentry_convertVarFunction (spec);
+ }
+
+ llassert (uentry_isFunction (spec));
+ }
DPRINTF (("Merge entries: %s / %s",
uentry_unparseFull (spec),
uentry_unparseFull (def)));
+ uentry_mergeConstraints (spec, def);
+
uentry_checkConformance (spec, def, TRUE,
context_getFlag (FLG_NEEDSPEC));
void
uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
{
- fileloc olddef = uentry_whereDeclared (old);
+ fileloc olddef = uentry_whereDeclared (old);
fileloc unewdef = uentry_whereDeclared (unew);
bool mustConform;
bool wasForward;
uentry_unparseFull (old),
uentry_unparseFull (unew)));
- if (uentry_isExtern (unew))
- {
- uentry_setUsed (old, unewdef);
- }
-
wasForward =
fileloc_isUndefined (olddef)
- && fileloc_isDefined (uentry_whereDefined (old))
- && !uentry_isExpandedMacro (old);
+ && fileloc_isDefined (uentry_whereDefined (old))
+ && !uentry_isExpandedMacro (old);
if (!context_getFlag (FLG_INCONDEFSLIB)
&& (fileloc_isLib (olddef) || fileloc_isImport (olddef)))
llassert (uentry_isValid (unew));
llassert (cstring_equal (old->uname, unew->uname));
+ if (uentry_isFunction (unew) && !uentry_isFunction (old))
+ {
+ if (uentry_isConstant (old))
+ {
+ llassert (ctype_isUnknown (old->utype) || ctype_isFunction (old->utype));
+ uentry_makeConstantFunction (old);
+ }
+ else
+ {
+ uentry_convertVarFunction (old);
+ }
+
+ llassert (uentry_isFunction (old));
+ }
+
+ DPRINTF (("uentry merge: %s / %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
+
+ if (uentry_isExtern (unew))
+ {
+ uentry_setUsed (old, unewdef);
+ }
+
/*
** should check old one was extern!
*/
}
else
{
- if (!uentry_isExtern (unew) && !uentry_isForward (old)
+ if (!uentry_isExtern (unew)
+ && !uentry_isForward (old)
&& !fileloc_equal (olddef, unewdef)
&& !fileloc_isUndefined (olddef)
&& !fileloc_isUndefined (unewdef)
/*
if (uentry_isDatatype (old) || uentry_isAnyTag (old))
{
- uentry_copyInto (old, unew);
+ uentry_updateInto (old, unew);
old->sref = sRef_saveCopy (old->sref);
}
*/
}
else
{
- uentry_setDefined (old, unewdef);
+ uentry_setDeclared (old, unewdef); /* evans 2001-07-23 was setDefined */
}
}
}
}
+ DPRINTF (("uentry merge: %s / %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
+
+ uentry_mergeConstraints (old, unew);
+ DPRINTF (("uentry merge: %s / %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
+
uentry_checkConformance (old, unew, mustConform, FALSE);
+ DPRINTF (("uentry merge: %s / %s",
+ uentry_unparseFull (old),
+ uentry_unparseFull (unew)));
old->used = old->used || unew->used;
old->uses = filelocList_append (old->uses, unew->uses);
fileloc_undefined);
}
+ DPRINTF (("here: %s", uentry_unparseFull (old)));
+
/*
** No redeclaration errors for functions here, since we
** don't know if this is the definition of the function.
uentry_checkName (old);
}
+ DPRINTF (("After: %s", uentry_unparseFull (old)));
llassert (!ctype_isUndefined (old->utype));
}
return FALSE;
}
-static void uentry_copyInto (/*@unique@*/ uentry unew, uentry old)
+static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old)
{
+ ekind okind = unew->ukind;
llassert (uentry_isValid (unew));
llassert (uentry_isValid (old));
+ DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
+
unew->ukind = old->ukind;
- unew->uname = cstring_copy (old->uname);
+ llassert (cstring_equal (unew->uname, old->uname));
unew->utype = old->utype;
- unew->whereSpecified = fileloc_copy (old->whereSpecified);
- unew->whereDefined = fileloc_copy (old->whereDefined);
- unew->whereDeclared = fileloc_copy (old->whereDeclared);
+ if (fileloc_isDefined (unew->whereSpecified)
+ && !fileloc_isDefined (old->whereSpecified))
+ {
+ ; /* Keep the old value */
+ }
+ else
+ {
+ fileloc_free (unew->whereSpecified); /*@i523 why no error without this? */
+ unew->whereSpecified = fileloc_copy (old->whereSpecified);
+ }
+
+ if (fileloc_isDefined (unew->whereDefined)
+ && !fileloc_isDefined (old->whereDefined))
+ {
+ ; /* Keep the old value */
+ }
+ else
+ {
+ fileloc_free (unew->whereDefined); /*@i523 why no error without this? */
+ unew->whereDefined = fileloc_copy (old->whereDefined);
+ }
+
+ if (fileloc_isDefined (unew->whereDeclared)
+ && !fileloc_isDefined (old->whereDeclared))
+ {
+ ; /* Keep the old value */
+ }
+ else
+ {
+ fileloc_free (unew->whereDeclared); /*@i523 why no error without this? */
+ unew->whereDeclared = fileloc_copy (old->whereDeclared);
+ }
+
+ DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
unew->sref = sRef_saveCopy (old->sref); /* Memory leak! */
unew->used = old->used;
unew->lset = FALSE;
unew->isPrivate = old->isPrivate;
unew->hasNameError = old->hasNameError;
- unew->uses = filelocList_undefined;
+ unew->uses = filelocList_append (unew->uses, old->uses);
+ old->uses = filelocList_undefined;
unew->storageclass = old->storageclass;
+ uinfo_free (unew->info, okind);
unew->info = uinfo_copy (old->info, old->ukind);
}
{
uentry enew = uentry_alloc ();
DPRINTF (("copy: %s", uentry_unparseFull (e)));
- uentry_copyInto (enew, e);
+ enew->ukind = e->ukind;
+ enew->uname = cstring_copy (e->uname);
+ enew->utype = e->utype;
+
+ enew->whereSpecified = fileloc_copy (e->whereSpecified);
+ enew->whereDefined = fileloc_copy (e->whereDefined);
+ enew->whereDeclared = fileloc_copy (e->whereDeclared);
+
+ enew->sref = sRef_saveCopy (e->sref); /* Memory leak! */
+ enew->used = e->used;
+ enew->lset = FALSE;
+ enew->isPrivate = e->isPrivate;
+ enew->hasNameError = e->hasNameError;
+ enew->uses = filelocList_undefined;
+
+ enew->storageclass = e->storageclass;
+ enew->info = uinfo_copy (e->info, e->ukind);
+ enew->warn = warnClause_copy (e->warn);
+
DPRINTF (("Here we are..."));
DPRINTF (("original: %s", uentry_unparseFull (e)));
DPRINTF (("copy: %s", uentry_unparse (enew)));
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))
} end_sRefSet_elements ;
}
} end_stateClauseList_postElements ;
-
+
return res;
}
else
}
}
-/*@exposed@*/ uentry uentry_makeUnrecognized (cstring c, /*@keep@*/ fileloc loc)
+/*@exposed@*/ uentry uentry_makeUnrecognized (cstring c, /*@only@*/ fileloc loc)
{
uentry ue;
fileloc tloc;
/*
- ** Can't but unrecognized ids in macros in global scope, because srefs will break! */
+ ** Can't but unrecognized ids in macros in global scope, because srefs will break!
+ */
+
if (!context_inMacro ())
{
sRef_setGlobalScopeSafe ();
/*@ignore@*/
-
+# if 0
static void uentry_testInRange (uentry p_e, uentry cconstant) {
- if( uentry_isValid(p_e) ) {
- if( sRef_isValid (p_e->sref) ) {
- char * t = cstring_toCharsSafe (uentry_unparse(cconstant) );
+ if (uentry_isValid(p_e)) {
+ if (sRef_isValid (p_e->sref)) {
+ /* char * t = cstring_toCharsSafe (uentry_unparse(cconstant) );
int index = atoi( t );
free (t);
+ */
+ long index = multiVal_forceInt (uentry_getConstantValue (cconstant));
// usymtab_testInRange (p_e->sref, index);
}//end if
}//endif
}//end if
}
+# endif
+
/* start modifications */
/*
}
/*@end@*/
/*@=type*/
+
+bool uentry_hasMetaStateEnsures (uentry e)
+{
+ if (uentry_isValid (e) && uentry_isFunction (e))
+ {
+ return functionConstraint_hasMetaStateConstraint (e->info->fcn->postconditions);
+ }
+ else
+ {
+ return FALSE;
+ }
+}
+
+metaStateConstraintList uentry_getMetaStateEnsures (uentry e)
+{
+ llassert (uentry_isValid (e) && uentry_isFunction (e));
+ return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
+}
andersk / splint.git / blobdiff