/*
-** LCLint - annotation-assisted static program checker
+** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2001 University of Virginia,
** Massachusetts Institute of Technology
**
**
** For information on lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For more information: http://www.splint.org
*/
/*
** uentry.c
}
}
-
-/*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_getFunctionConditions on nonfunction %s",
+ uentry_unparse (ue) ) ) );
+ if (!uentry_isFunction (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_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
if (uentry_isVariable (ue))
{
+ /*@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);
}
if (functionConstraint_isDefined (ue->info->fcn->preconditions))
{
- BADBRANCH; /* should conjoin constraints? */
+ /* drl 11-29-2001
+ 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
+ prints an error and tries to conjoin the lists.
+ */
+ llparseerror
+ (message ("Duplicate precondition list"
+ "Attemping the conjoin the requires clauses"
+ ));
+
+
+ /* should conjoin constraints? */
/*@notreached@*/
ue->info->fcn->preconditions = functionConstraint_conjoin (ue->info->fcn->preconditions, preconditions);
}
}
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 ("Attribute 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)));
+ DPRINTF (("Value: %s", multiVal_unparse (uentry_getConstantValue (ue))));
return ue;
}
e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
e->info->var->kind = kind;
+ /*@i523 e->info->var->origsref = sRef_saveCopy (e->sref); */
e->info->var->checked = CH_UNKNOWN;
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);
-/* 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;
/*@=mustfree@*/
}
- /*@i23 ???
+ /*@i23*/
+ /* ??? - evans 2001-09-09 not sure what's going on here...?
if (globSet_hasStatic (globs))
{
context_recordFileGlobals (globs);
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:
** Functions are never equivalent
*/
- if ((int) u1 < (int) u2)
+ if (u1 - u2 < 0) /* evans 2001-08-21: was: ((int) u1 < (int) u2), changed to remove gcc warning */
{
return -1;
}
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
sRef uentry_getOrigSref (uentry e)
{
+ /*@i523*/ /* evans 2001-09-09 - need to fix this
+ if (uentry_isValid (e))
+ {
+ if (uentry_isVariable (e))
+ {
+ return e->info->var->origsref;
+ }
+ else
+ {
+ sRef sr = sRef_copy (uentry_getSref (e));
+
+ sRef_resetState (sr);
+ sRef_clearDerived (sr);
+ return (sr);
+ }
+ }
+ else
+ {
+ return sRef_undefined;
+ }
+ */
+
if (uentry_isValid (e))
{
sRef sr = sRef_copy (uentry_getSref (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);
}
ucinfo_copy (ucinfo u)
{
ucinfo ret = (ucinfo) dmalloc (sizeof (*ret));
-
- ret->val = multiVal_copy (u->val);
ret->access = u->access;
-
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 */
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);
+ }
}
}
}
cstring nnamefix;
if (cstring_isDefined (pfx)
- && cstring_equalPrefix (oldname, cstring_toCharsSafe (pfx)))
+ && cstring_equalPrefix (oldname, pfx))
{
oname = cstring_suffix (oldname, cstring_length (pfx));
}
/*@-branchstate@*/ } /*@=branchstate@*/
if (cstring_isDefined (pfx)
- && cstring_equalPrefix (nname, cstring_toCharsSafe (pfx)))
+ && cstring_equalPrefix (nname, pfx))
{
nnamefix = cstring_suffix (nname, cstring_length (pfx));
}
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;
}
}
-static bool incompatibleStates (sRef rs, sRef os)
+static bool uentry_incompatibleMemoryStates (sRef rs, sRef os)
{
alkind rk = sRef_getAliasKind (rs);
alkind ok = sRef_getAliasKind (os);
bool mustReturn, bool flip, bool opt,
clause cl)
{
+ sRef rs = res->sref;
+ sRef os = other->sref;
+
DPRINTF (("Merge alias states: %s / %s",
uentry_unparseFull (res),
uentry_unparseFull (other)));
- if (sRef_isValid (res->sref))
+ if (sRef_isValid (rs))
{
if (!mustReturn)
{
- DPRINTF (("1"));
- if (incompatibleStates (res->sref, other->sref))
+ if (uentry_incompatibleMemoryStates (rs, os))
{
- DPRINTF (("2"));
+ DPRINTF (("Incompatible: \n\t%s / \n\t%s",
+ sRef_unparseFull (rs), sRef_unparseFull (os)));
- if (sRef_isThroughArrayFetch (res->sref)
+ if (sRef_isThroughArrayFetch (rs)
&& !context_getFlag (FLG_STRICTBRANCHSTATE))
{
- if (sRef_isKept (res->sref) || sRef_isKept (other->sref))
+ if (sRef_isKept (rs) || sRef_isKept (os))
{
- sRef_maybeKill (res->sref, loc);
+ sRef_maybeKill (rs, loc);
}
- else if (sRef_isPossiblyDead (other->sref))
+ else if (sRef_isPossiblyDead (os))
{
- sRef_maybeKill (res->sref, loc);
+ sRef_maybeKill (rs, loc);
}
else
{
}
else
{
- if (uentry_relevantReference (other->sref, flip))
+ if (uentry_relevantReference (os, flip))
{
- DPRINTF (("4"));
- if (sRef_isLocalParamVar (res->sref)
- && (sRef_isLocalState (other->sref)
- || sRef_isDependent (other->sref)))
+ if (sRef_isLocalParamVar (rs)
+ && (sRef_isLocalState (os)
+ || sRef_isDependent (os)))
{
- if (sRef_isDependent (res->sref))
+ if (sRef_isDependent (rs))
{
- sRef_setDependent (other->sref, loc);
+ sRef_setDependent (os, loc);
}
else
{
- sRef_setDefState (res->sref, SS_UNUSEABLE, loc);
+ sRef_setDefState (rs, SS_UNUSEABLE, loc);
}
}
else
}
}
- if (sRef_isKept (res->sref))
+ if (sRef_isKept (rs))
{
- sRef_setKept (other->sref, loc);
+ DPRINTF (("Setting kept: %s", sRef_unparseFull (os)));
+ sRef_setKept (os, loc);
}
}
else
{
- if (incompatibleStates (other->sref, res->sref))
+ if (uentry_incompatibleMemoryStates (os, rs))
{
- if (uentry_relevantReference (res->sref, !flip))
+ if (uentry_relevantReference (rs, !flip))
{
- if (sRef_isLocalParamVar (res->sref)
- && (sRef_isDependent (res->sref)
- || sRef_isLocalState (res->sref)))
+ if (sRef_isLocalParamVar (rs)
+ && (sRef_isDependent (rs)
+ || sRef_isLocalState (rs)))
{
- if (sRef_isDependent (other->sref))
+ if (sRef_isDependent (os))
{
- sRef_setDependent (res->sref, loc);
+ sRef_setDependent (rs, loc);
}
else
{
- sRef_setDefState (res->sref, SS_UNUSEABLE, loc);
+ sRef_setDefState (rs, SS_UNUSEABLE, loc);
}
}
else
{
- if (sRef_isParam (other->sref))
+ if (sRef_isParam (os))
{
/*
** If the local variable associated
uentry uvar = usymtab_lookupSafe (other->uname);
if (uentry_isValid (uvar)
- && ((sRef_isDead (other->sref)
+ && ((sRef_isDead (os)
&& sRef_isOnly (uvar->sref))
- || (sRef_isDependent (other->sref)
+ || (sRef_isDependent (os)
&& sRef_isOwned (uvar->sref))))
{
/* no error */
}
}
- if (sRef_isKept (other->sref))
+ if (sRef_isKept (os))
{
- sRef_setKept (res->sref, loc);
+ sRef_setKept (rs, loc);
}
}
if (opt)
{
DPRINTF (("Merge opt..."));
- sRef_mergeOptState (res->sref, other->sref, cl, loc);
+ sRef_mergeOptState (rs, os, cl, loc);
DPRINTF (("Done!"));
}
else
{
- sRef_mergeState (res->sref, other->sref, cl, loc);
+ DPRINTF (("Merging states: \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os)));
+ sRef_mergeState (rs, os, cl, loc);
+ DPRINTF (("After merging : \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os)));
}
}
else
{
- if (sRef_isModified (other->sref))
+ if (sRef_isModified (os))
{
- sRef_setModified (res->sref);
+ sRef_setModified (rs);
}
}
}
+
+ DPRINTF (("After merge: %s", sRef_unparseFull (res->sref)));
}
static void
-uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
+uentry_mergeValueStates (uentry res, uentry other, fileloc loc, bool mustReturn, /*@unused@*/ bool flip)
{
valueTable rvalues;
valueTable ovalues;
DPRINTF (("Merge values: %s / %s", sRef_unparseFull (res->sref), sRef_unparseFull (other->sref)));
+ if (mustReturn)
+ {
+ return;
+ }
+ /* flip? */
+
rvalues = sRef_getValueTable (res->sref);
ovalues = sRef_getValueTable (other->sref);
{
sRef_setMetaStateValueComplete (res->sref,
fkey, stateValue_getValue (fval),
- loc);
+ stateValue_getLoc (fval));
DPRINTF (("Setting res: %s", sRef_unparseFull (res->sref)));
}
else if (stateValue_isError (tval)
{
DPRINTF (("Other branch is definitely null!"));
}
+ else if (sRef_isStateUndefined (res->sref)
+ || sRef_isDead (res->sref))
+ {
+ ; /* Combination state doesn't matter if it is undefined or dead */
+ }
else
{
DPRINTF (("Check: %s / %s / %s / %s", fkey,
DPRINTF (("nval: %d / %d / %d", nval,
stateValue_getValue (fval), stateValue_getValue (tval)));
- if (cstring_isDefined (msg))
+ if (nval == stateValue_error)
{
/*@i32 print extra info for assignments@*/
if (optgenerror
(FLG_STATEMERGE,
message
- ("Control branches merge with incompatible global states (%s and %s): %s",
+ ("Control branches merge with incompatible global states (%s and %s)%q",
metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)),
metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)),
- msg),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
loc))
{
sRef_showMetaStateInfo (res->sref, fkey);
if (optgenerror
(FLG_STATEMERGE,
message
- ("Control branches merge with incompatible states for %q (%s and %s): %s",
+ ("Control branches merge with incompatible states for %q (%s and %s)%q",
uentry_getName (res),
metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)),
metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)),
- msg),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
loc))
{
sRef_showMetaStateInfo (res->sref, fkey);
uentry_unparseFull (other)));
uentry_mergeAliasStates (res, other, loc, mustReturn, flip, opt, cl);
- uentry_mergeValueStates (res, other, loc);
+ uentry_mergeValueStates (res, other, loc, mustReturn, flip);
uentry_mergeSetStates (res, other, loc, flip, cl);
}
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 ();
&& (cstring_equal (uentry_rawName (ue), GLOBAL_MARKER_NAME)));
}
-
-//
/* new start modifications */
-/*@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) );
- int index = atoi( t );
- free (t);
- */
- long index = multiVal_forceInt (uentry_getConstantValue (cconstant));
- // usymtab_testInRange (p_e->sref, index);
- }//end if
- }//endif
-}
-
-
-/* void uentry_setStringLength (uentry p_e, uentry cconstant) { */
-/* if( uentry_isValid(p_e) ) { */
-/* if( p_e->info != NULL) { */
-/* if( p_e->info->var != NULL) { */
-/* char *t = cstring_toCharsSafe (uentry_unparse(cconstant)); */
-/* int length = atoi( t ); */
-/* free (t); */
-/* p_e->info->var->bufinfo->len = length; */
-/* p_e->sref->bufinfo.len = length; */
-/* printf("Set string length of buff to %d \n", p_e->sref->bufinfo.size); */
-/* }//end if */
-/* }//endif */
-/* }//end if */
-/* } */
-
-
-static void uentry_setBufferSize (uentry p_e, exprNode cconstant) {
-if( uentry_isValid(p_e) ) {
- if( p_e->info != NULL) {
- if( p_e->info->var != NULL) {
- int size = atoi(cstring_toCharsSafe(exprNode_unparse(cconstant) ) );
- p_e->info->var->bufinfo->size = size;
- p_e->sref->bufinfo.size = size;
- printf("Set buffer size to %d \n", p_e->sref->bufinfo.size);
- // fprintf(stderr, "For %s and %s\n", uentry_unparse(p_e) );
- // fprintf(stderr, "and %d\n", size );
-
- }//end if
- }//endif
-}//end if
-}
-
-# endif
-
-
/* start modifications */
/*
requires: p_e is defined, is a ptr/array variable
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;
- }/* End if */
- }/* End if */
- }/* End if */
+ }
+ }
+ }
+ /*@noaccess sRef@*/
fprintf(stderr, "uentry:Error in setPossiblyNullTerminatedState\n");
}
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;
- }//End if
- }//End if
- }//End if
+ }
+ }
+ }
fprintf(stderr, "uentry:Error in setNullTerminatedState\n");
}
-
-/*
-requires: p_e is defined, is a ptr/array variable
-modifies: p_e
-effects: sets the state of the variable
-*/
-
-/* void uentry_setNotNullTerminatedState (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_NOTNULLTERMINATED; */
-/* p_e->sref->bufinfo.bufstate = BB_NOTNULLTERMINATED; */
-/* return; */
-/* }//End if */
-/* }//End if */
-/* }//End if */
-
-/* fprintf(stderr, "uentry:Error in setNotNullTerminatedState\n"); */
-/* } */
-
-
/*
requires: p_e is defined, is a ptr/array variable
modifies: 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;
- }//End if
- }//End if
- }//End if
+ }
+ }
+ }
fprintf(stderr, "uentry:Error in setSize\n");
}
effects: sets the length of the buffer
*/
- void uentry_setLen (uentry p_e, int len) {
+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;
- }//End if
- }//End if
- }//End if
-
+ }
+ }
+ }
+
fprintf(stderr, "uentry:Error in setLen\n");
}
-/*@end@*/
+
/*@=type*/
bool uentry_hasMetaStateEnsures (uentry e)
}
}
-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