}
}
-
-/*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);
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
{
- BADBRANCH; /* should conjoin */
- /*@notreached@*/
ue->info->fcn->postconditions = functionConstraint_conjoin (ue->info->fcn->postconditions, postconditions);
}
}
{
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
{
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;
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));
}
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
e->whereDeclared = f;
e->whereDefined = fileloc_undefined;
}
+
+ llassert (fileloc_storable (f));
}
static void
ucinfo_free (/*@only@*/ ucinfo u)
{
- multiVal_free (u->val);
sfree (u);
}
ucinfo_copy (ucinfo u)
{
ucinfo ret = (ucinfo) dmalloc (sizeof (*ret));
-
- ret->val = multiVal_copy (u->val);
ret->access = u->access;
-
return ret;
}
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);
+ }
}
}
}
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));
}
}
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
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;
}
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)
}
else
{
- uentry_setDefined (old, unewdef);
+ uentry_setDeclared (old, unewdef); /* evans 2001-07-23 was setDefined */
}
}
}
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));
}
llassert (uentry_isValid (unew));
llassert (uentry_isValid (old));
+ DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
+
unew->ukind = old->ukind;
llassert (cstring_equal (unew->uname, old->uname));
unew->utype = old->utype;
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;
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 ();
}
}
-metaStateConstraint uentry_getMetaStateEnsures (uentry e)
+metaStateConstraintList uentry_getMetaStateEnsures (uentry e)
{
- llassert (uentry_hasMetaStateEnsures (e));
- return functionConstraint_getMetaStateConstraint (e->info->fcn->postconditions);
+ llassert (uentry_isValid (e) && uentry_isFunction (e));
+ return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
}
andersk / splint.git / blobdiff