static void checkLeaveTrans (uentry p_actual, transferKind p_transferType);
static void checkTransfer (exprNode p_fexp, /*@dependent@*/ sRef p_fref,
exprNode p_texp, /*@dependent@*/ sRef p_tref,
+ exprNode p_fcn, /* for printing better error messages */
fileloc p_loc, transferKind p_transferType);
static void checkGlobTrans (uentry p_glob, transferKind p_type);
}
static /*@only@*/ cstring
-transferErrorExcerpt (transferKind transferType, exprNode fexp, exprNode texp) /*@*/
+transferErrorExcerpt (transferKind transferType, exprNode fexp, exprNode texp, exprNode fcn) /*@*/
{
switch (transferType)
{
case TT_GLOBINIT:
return (message ("%s = %s", exprNode_unparse (texp), exprNode_unparse (fexp)));
case TT_FCNPASS:
- /*@i32 make it so called fcn is known here! */
- return cstring_copy (exprNode_unparse (fexp));
+ if (exprNode_isDefined (fcn))
+ {
+ return message ("%s(..., %s, ...)",
+ exprNode_unparse (fcn),
+ exprNode_unparse (fexp));
+ }
+ else
+ {
+ return cstring_copy (exprNode_unparse (fexp));
+ }
BADDEFAULT;
}
BADEXIT;
ctype ct;
alkind fkind = sRef_getAliasKind (fref);
alkind tkind = sRef_getAliasKind (tref);
-
+
DPRINTF (("Check completely defined: %s [%s] / %s [%s]",
exprNode_unparse (fexp), sRef_unparseFull (fref),
exprNode_unparse (texp), sRef_unparseFull (tref)));
sRef_undefined, TT_FCNPASS)),
loc))
{
+ DPRINTF (("fref: %s", sRef_unparseFull (fref)));
+ DPRINTF (("tref: %s", sRef_unparseFull (tref)));
sRef_showNullInfo (fref);
sRef_setNullError (fref);
}
ct = ctype_realType (sRef_getType (fref));
+ DPRINTF (("Here: %s", ctype_unparse (ct)));
+
if (!(sRef_isAnyDefined (fref)
|| sRef_isPdefined (fref)
|| sRef_isAllocated (fref)
{
sRef rb = sRef_getRootBase (fref);
sRef_showStateInfo (fref);
+
+ DPRINTF (("fref: %s", sRef_unparseFull (fref)));
+ DPRINTF (("rb: %s", sRef_unparseFull (rb)));
sRef_setDefinedComplete (rb, loc);
}
}
{
return YES;
}
- else if (ctype_isPointer (ct))
+ else if (ctype_isPointer (ct) || ctype_isArray (ct)) /* evans 2001-07-12 added ctype_isArray */
{
ctype tct = ctype_realType (sRef_getType (tref));
}
else
{
+ DPRINTF (("Here fref: %s", sRef_unparseFull (fref)));
+ DPRINTF (("Here tref: %s", sRef_unparseFull (tref)));
+
if (ctype_isAP (tct) || ctype_isUnknown (tct))
{
sRef fptr = sRef_constructDeref (fref);
sRef tptr = sRef_constructDeref (tref);
+ DPRINTF (("Here tptr: %s", sRef_unparseFull (tptr)));
+
return (checkCompletelyDefined (fexp, fptr, ofref,
texp, tptr,
FALSE, inUnion, FALSE, loc,
}
}
}
- else if (ctype_isArray (ct))
- {
- return YES;
- }
else if (ctype_isStruct (ct))
{
ctype tct = ctype_realType (sRef_getType (tref));
sRef_unparse (fref)),
loc);
}
+ /* evans 2001-08-21: added this branch for global returns */
+ else if (transferType == TT_GLOBRETURN)
+ {
+ voptgenerror
+ (FLG_UNIONDEF,
+ message ("Union %q reachable from global %q has "
+ "no defined field",
+ sRef_unparse (fref),
+ sRef_unparse (sRef_getRootBase (fref))),
+ loc);
+ }
else if (transferType == TT_DOASSIGN
|| transferType == TT_FIELDASSIGN
|| transferType == TT_GLOBINIT)
{
(void) checkTransfer (fexp, exprNode_getSref (fexp),
exprNode_undefined, rref,
+ exprNode_undefined,
exprNode_loc (fexp), TT_FCNRETURN);
}
}
(void) checkTransfer (fexp, exprNode_getSref (fexp),
exprNode_undefined, tref,
+ fcn,
exprNode_loc (fexp), TT_FCNPASS);
setCodePoint ();
sRef lfld = sRef_makeField (slhs, fieldname);
(void) checkTransfer (rhs, sr, lhs, lfld,
+ exprNode_undefined,
exprNode_loc (lhs), tt);
}
} end_sRefSet_realElements ;
{
sRef rfld = sRef_makeField (srhs, uentry_rawName (field));
sRef lfld = sRef_makeField (slhs, uentry_rawName (field));
- (void) checkTransfer (rhs, rfld, lhs, lfld, exprNode_loc (lhs), tt);
+ (void) checkTransfer (rhs, rfld, lhs, lfld,
+ exprNode_undefined,
+ exprNode_loc (lhs), tt);
} end_uentryList_elements ;
}
if (sRef_isFileOrGlobalScope (slhs) || (!sRef_isCvar (slhs)))
{
(void) checkTransfer (rhs, exprNode_getSref (rhs),
- lhs, slhs, exprNode_loc (rhs), TT_GLOBINIT);
+ lhs, slhs,
+ exprNode_undefined,
+ exprNode_loc (rhs), TT_GLOBINIT);
}
else
{
DPRINTF (("lhs: %s", sRef_unparseFull (slhs)));
DPRINTF (("rhs: %s", sRef_unparseFull (srhs)));
(void) checkTransfer (rhs, srhs, lhs, slhs,
+ exprNode_undefined,
exprNode_loc (lhs), TT_DOASSIGN);
DPRINTF (("lhs: %s", sRef_unparseFull (slhs)));
DPRINTF (("rhs: %s", sRef_unparseFull (srhs)));
;
}
}
- else if (transferType == TT_DOASSIGN)
+ else if (transferType == TT_DOASSIGN
+ /* evans 2001-10-05: added TT_FIELDASSIGN: */
+ || transferType == TT_FIELDASSIGN)
{
if (!(sRef_isExposed (tref)
|| !sRef_isCvar (tref)
{
;
}
- else if (!stateValue_sameValue (fval, tval))
+ else if (sRef_isDefinitelyNull (fref)
+ || usymtab_isDefinitelyNull (fref))
{
- DPRINTF (("Check: %s / %s / %s / %s", fkey,
- metaStateInfo_unparse (minfo),
- stateValue_unparse (fval),
- stateValue_unparse (tval)));
+ ; /* No errors for null values in state transfers. */
+ }
+
+ else
+ {
+ stateCombinationTable sctable = metaStateInfo_getTransferTable (minfo);
+ cstring msg = cstring_undefined;
+ int nval = stateCombinationTable_lookup (sctable,
+ stateValue_getValue (fval),
+ stateValue_getValue (tval),
+ &msg);
- if (sRef_isDefinitelyNull (fref)
- || usymtab_isDefinitelyNull (fref))
- {
- ; /* No errors for null values in state transfers. */
- }
- else
+ if (nval == stateValue_error)
{
- if (optgenerror
- (FLG_STATETRANSFER,
- message
- ("Invalid transfer from %q %x to %q",
- stateValue_unparseValue (fval, minfo),
- sRef_unparse (fref),
- stateValue_unparseValue (tval, minfo)),
- loc))
+ if (transferType == TT_LEAVETRANS)
+ {
+ BADBRANCH;
+ }
+ else if (transferType == TT_GLOBRETURN)
+ {
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Function returns with global %q in inconsistent state (%q is %q, should be %q)%q",
+ sRef_unparse (sRef_getRootBase (fref)),
+ sRef_unparse (fref),
+ stateValue_unparseValue (fval, minfo),
+ stateValue_unparseValue (tval, minfo),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
+ loc))
+ {
+ sRef_showMetaStateInfo (fref, fkey);
+ }
+ }
+ else if (transferType == TT_GLOBPASS)
{
- sRef_showMetaStateInfo (fref, fkey);
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Function called with global %q in inconsistent state (%q is %q, should be %q)%q",
+ sRef_unparse (sRef_getRootBase (fref)),
+ stateValue_unparseValue (fval, minfo),
+ sRef_unparse (fref),
+ stateValue_unparseValue (tval, minfo),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
+ loc))
+ {
+ sRef_showMetaStateInfo (fref, fkey);
+ }
}
+ else if (transferType == TT_PARAMRETURN)
+ {
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Function returns with parameter %q in inconsistent state (%q is %q, should be %q)%q",
+ sRef_unparse (sRef_getRootBase (fref)),
+ sRef_unparse (fref),
+ stateValue_unparseValue (fval, minfo),
+ stateValue_unparseValue (tval, minfo),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
+ loc))
+ {
+ sRef_showMetaStateInfo (fref, fkey);
+ }
+ }
+ else
+ {
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Invalid transfer from %q %x to %q (%q)%q",
+ stateValue_unparseValue (fval, minfo),
+ sRef_unparse (fref),
+ stateValue_unparseValue (tval, minfo),
+ sRef_unparse (tref),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
+ loc))
+ {
+ sRef_showMetaStateInfo (fref, fkey);
+ }
+ }
+
+ }
+
+ if (stateValue_getValue (fval) != nval)
+ {
+ stateValue_updateValueLoc (fval, nval, loc);
}
- }
- else
- {
- ; /* Match okay */
}
}
static void
checkMetaStateTransfer (exprNode fexp, sRef fref, exprNode texp, sRef tref,
+ exprNode fcn,
fileloc loc, transferKind /*@i32@*/ transferType)
{
valueTable fvalues = sRef_getValueTable (fref);
valueTable tvalues = sRef_getValueTable (tref);
DPRINTF (("Metastate transfer: from %s", exprNode_unparse (fexp)));
-
+
DPRINTF (("Metastate transfer: %s => %s",
sRef_unparseFull (fref),
sRef_unparseFull (tref)));
}
else
{
- if (cstring_isDefined (msg))
+ if (nval == stateValue_error)
{
/*@i32 print extra info for assignments@*/
if (optgenerror
(FLG_STATETRANSFER,
message
- ("Invalid transfer from %q %x to %q (%s): %q",
+ ("Invalid transfer from %q %x to %q%q: %q",
stateValue_unparseValue (fval, minfo),
sRef_unparse (fref),
stateValue_unparseValue (tval, minfo),
- msg,
- transferErrorExcerpt (transferType, fexp, texp)),
+ cstring_isDefined (msg)
+ ? message (" (%s)", msg) : cstring_undefined,
+ transferErrorExcerpt (transferType, fexp, texp, fcn)),
loc))
{
sRef_showMetaStateInfo (fref, fkey);
+ sRef_showMetaStateInfo (tref, fkey);
}
else
{
static void
checkTransfer (exprNode fexp, /*@dependent@*/ sRef fref,
exprNode texp, /*@dependent@*/ sRef tref,
+ exprNode fcn,
fileloc loc, transferKind transferType)
{
setCodePoint ();
exprNode_unparse (fexp),
exprNode_unparse (texp)));
- checkMetaStateTransfer (fexp, fref, texp, tref, loc, transferType);
+ checkMetaStateTransfer (fexp, fref, texp, tref, fcn,
+ loc, transferType);
/*
** for local references, we need to check
andersk / splint.git / blobdiff