/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
**
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
** General Public License for more details.
**
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** exprChecks.c
*/
# include "splintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
# include "transferChecks.h"
# include "exprChecks.h"
/*
** for now, allow exprChecks to access exprNode.
** may remove this in future
*/
/*@access exprNode@*/
static bool checkCallModifyAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
static bool checkModifyValAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
static bool checkModifyAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
static void checkSafeReturnExpr (/*@notnull@*/ exprNode p_e);
/*
** called at end of expression statement
**
** of e->kind is not an assign, empty, body or modop
** verify the the value is void
**
*/
static int inCompoundStatementExpression = 0;
void
exprChecks_inCompoundStatementExpression (void)
{
inCompoundStatementExpression++;
}
void
exprChecks_leaveCompoundStatementExpression (void)
{
inCompoundStatementExpression--;
llassert (inCompoundStatementExpression >= 0);
}
void
exprChecks_checkStatementEffect (exprNode e)
{
bool hasError = FALSE;
if (inCompoundStatementExpression > 0)
{
/*
** Okay to have effectless statments in compound statement expression (should check
** it is the last statement, but we don't for now).
*/
return;
}
if (!exprNode_isError (e))
{
exprKind ek = e->kind;
if (ek == XPR_CALL && !(ctype_isRealVoid (e->typ)))
{
if (ctype_isKnown (e->typ))
{
if (ctype_isManifestBool (ctype_realishType (e->typ)))
{
hasError = optgenerror
(FLG_RETVALBOOL,
message ("Return value (type %t) ignored: %s",
e->typ,
exprNode_unparseFirst (e)),
e->loc);
}
else if (ctype_isDirectInt (e->typ))
{
hasError = optgenerror
(FLG_RETVALINT,
message ("Return value (type %t) ignored: %s",
e->typ,
exprNode_unparseFirst (e)),
e->loc);
}
else
{
hasError = optgenerror
(FLG_RETVALOTHER,
message ("Return value (type %t) ignored: %s",
e->typ,
exprNode_unparseFirst (e)),
e->loc);
}
}
}
if (!hasError && !(exprNode_mayEscape (e))
&& !(e->canBreak)) /* control changes are effects too! */
{
if (sRefSet_hasRealElement (e->sets)
|| sRefSet_hasRealElement (e->msets))
{
; /* okay */
}
else
{
if (sRefSet_isEmpty (e->sets) && sRefSet_isEmpty (e->msets))
{
voptgenerror
(FLG_NOEFFECT,
message ("Statement has no effect: %s",
exprNode_unparseFirst (e)),
e->loc);
}
else
{
if (context_maybeSet (FLG_NOEFFECTUNCON))
{
if (sRefSet_hasUnconstrained (e->sets))
{
voptgenerror
(FLG_NOEFFECTUNCON,
message ("Statement has no effect (possible "
"undected modification through "
"call to %q): %s",
sRefSet_unparseUnconstrained (e->sets),
exprNode_unparseFirst (e)),
e->loc);
}
else if (sRefSet_hasUnconstrained (e->msets))
{
voptgenerror
(FLG_NOEFFECTUNCON,
message ("Statement has no effect (possible "
"undected modification through "
"call to %q): %s",
sRefSet_unparseUnconstrained (e->msets),
exprNode_unparseFirst (e)),
e->loc);
}
else
{
; /* statement has unknown modification */
}
}
}
}
}
}
}
static bool
checkRepExposed (sRef base, /*@notnull@*/ exprNode e, sRef alias,
/*@unused@*/ exprNode unused)
{
ctype btype;
if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
{
btype = sRef_getType (base);
if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
{
voptgenerror (FLG_RETEXPOSE,
message ("Return value exposes rep of %s: %s",
ctype_unparse (btype),
exprNode_unparse (e)),
e->loc);
return TRUE;
}
}
else
{
sRef rbase = sRef_getRootBase (base);
btype = sRef_getType (rbase);
if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
{
voptgenerror
(FLG_RETEXPOSE,
message ("Return value may expose rep of %s through alias %q: %s",
ctype_unparse (btype),
sRef_unparse (rbase),
exprNode_unparse (e)),
e->loc);
return TRUE;
}
}
return FALSE;
}
static bool
checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e,
sRef alias, /*@unused@*/ exprNode unused)
{
if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
{
ctype ct = e->typ;
if (ctype_isUnknown (ct))
{
ct = sRef_getType (base);
}
if (ctype_isVisiblySharable (ct))
{
if (sRef_isFileOrGlobalScope (base))
{
uentry fcn = context_getHeader ();
bool noerror = FALSE;
if (uentry_isValid (fcn) && uentry_isFunction (fcn))
{
sRef res = uentry_getSref (fcn);
/* If result is dependent and global is owned, this is okay... */
if (sRef_isDependent (res)
&& sRef_isOwned (base))
{
noerror = TRUE;
}
}
if (!noerror)
{
voptgenerror
(FLG_RETALIAS,
message ("Function returns reference to global %q: %s",
sRef_unparse (base),
exprNode_unparse (e)),
e->loc);
}
return TRUE;
}
else if (sRef_isAnyParam (base))
{
uentryList params = context_getParams ();
int paramno = sRef_getParam (base);
if (paramno < uentryList_size (params))
{
uentry arg = uentryList_getN (params, paramno);
sRef ref = uentry_getSref (arg);
if (uentry_isReturned (arg)
|| sRef_isOnly (ref)
|| sRef_isExposed (ref)
|| sRef_isRefCounted (ref))
{
; /* okay */
}
else
{
voptgenerror
(FLG_RETALIAS,
message ("Function returns reference to parameter %q: %s",
sRef_unparse (base),
exprNode_unparse (e)),
e->loc);
}
}
else
{
llbuglit ("ret alias: bad paramno");
}
return TRUE;
}
else
{
return FALSE;
}
}
}
else
{
if (ctype_isVisiblySharable (e->typ))
{
if (sRef_isFileOrGlobalScope (base))
{
voptgenerror
(FLG_RETALIAS,
message ("Function may return reference to global %q through alias %q: %s",
sRef_unparse (alias),
sRef_unparse (base),
exprNode_unparse (e)),
e->loc);
return TRUE;
}
else if (sRef_isAnyParam (base) && !(sRef_isOnly (base)))
{
uentryList params = context_getParams ();
int paramno = sRef_getParam (base);
if (paramno < uentryList_size (params))
{
uentry arg = uentryList_getN (params, paramno);
if (!uentry_isReturned (arg))
{
voptgenerror
(FLG_RETALIAS,
message
("Function may return reference to parameter %q through alias %q: %s",
sRef_unparse (base),
sRef_unparse (alias),
exprNode_unparse (e)),
e->loc);
return TRUE;
}
}
else
{
voptgenerror
(FLG_RETALIAS,
message
("Function may return reference to parameter %q through alias %q: %s",
sRef_unparse (base),
sRef_unparse (alias),
exprNode_unparse (e)),
e->loc);
return TRUE;
}
}
else
{
return FALSE;
}
}
}
return FALSE;
}
void
exprNode_checkModify (exprNode e, exprNode err)
{
llassert (exprNode_isDefined (e));
DPRINTF (("Check modify: %s", exprNode_unparse (e)));
if (sRef_isValid (e->sref))
{
sRef_aliasCheckPred (checkModifyAux, sRef_isReference, e->sref, e, err);
}
}
void
exprNode_checkModifyVal (exprNode e, exprNode err)
{
llassert (exprNode_isDefined (e));
DPRINTF (("Check modify val: %s", exprNode_unparse (e)));
if (sRef_isValid (e->sref))
{
sRef_aliasCheckPred (checkModifyValAux, sRef_isReference, e->sref, e, err);
}
}
void
exprChecks_checkNullReturn (fileloc loc)
{
if (!context_inRealFunction ())
{
/*
llmsg ("exprChecks_checkNullReturnExpr: not in function context");
*/
return;
}
else
{
if (ctype_isFunction (context_currentFunctionType ()))
{
ctype tr = ctype_getReturnType (context_currentFunctionType ());
if (!ctype_isFirstVoid (tr))
{
if (ctype_isUnknown (tr))
{
voptgenerror
(FLG_EMPTYRETURN,
cstring_makeLiteral ("Empty return in function declared to implicitly return int"),
loc);
}
else
{
voptgenerror (FLG_EMPTYRETURN,
message ("Empty return in function declared to return %t", tr),
loc);
}
}
}
}
}
void
exprNode_checkReturn (exprNode e)
{
if (!exprNode_isError (e))
{
if (!context_inRealFunction ())
{
if (context_inMacro ())
{
llerror (FLG_MACRORETURN,
message ("Macro %s uses return (not functional)",
context_inFunctionName ()));
}
else
{
/*
llbuglit ("exprNode_checkReturn: not in function context");
*/
}
}
else
{
if (ctype_isFunction (context_currentFunctionType ()))
{
checkSafeReturnExpr (e);
}
else
{
;
}
}
}
}
void
exprNode_checkPred (cstring c, exprNode e)
{
ctype ct;
if (exprNode_isError (e))
return;
ct = exprNode_getType (e);
if (exprNode_isAssign (e))
{
voptgenerror
(FLG_PREDASSIGN,
message ("Test expression for %s is assignment expression: %s",
c, exprNode_unparse (e)),
e->loc);
}
if (ctype_isRealBool (ct) || ctype_isUnknown (ct))
/* evs 2000-12-20 added || ctype_isUnknown to avoid spurious messages */
{
;
}
else if (ctype_isRealPointer (ct))
{
voptgenerror
(FLG_PREDBOOLPTR,
message ("Test expression for %s not %s, type %t: %s", c,
context_printBoolName (),
ct, exprNode_unparse (e)),
e->loc);
}
else if (ctype_isRealInt (ct))
{
voptgenerror
(FLG_PREDBOOLINT,
message ("Test expression for %s not %s, type %t: %s", c,
context_printBoolName (), ct, exprNode_unparse (e)),
e->loc);
}
else
{
voptgenerror
(FLG_PREDBOOLOTHERS,
message ("Test expression for %s not %s, type %t: %s", c,
context_printBoolName (), ct, exprNode_unparse (e)),
e->loc);
}
}
void
exprChecks_checkUsedGlobs (globSet decl, globSet used)
{
fileloc fl = uentry_whereSpecified (context_getHeader ());
if (fileloc_isUndefined (fl))
{
fl = uentry_whereDeclared (context_getHeader ());
}
globSet_allElements (decl, el)
{
if (!globSet_member (used, el))
{
if (sRef_isSpecInternalState (el)
|| sRef_isNothing (el))
{
;
}
else
{
cstring sname = sRef_unparse (el);
if (fileloc_isLib (fl))
{
voptgenerror (FLG_USEALLGLOBS,
message ("Global %s listed (%q) but not used",
sname, fileloc_unparse (fl)),
g_currentloc);
}
else
{
voptgenerror (FLG_USEALLGLOBS,
message ("Global %s listed but not used", sname),
fl);
}
cstring_free (sname);
}
}
} end_globSet_allElements;
}
void
exprNode_checkAllMods (sRefSet mods, uentry ue)
{
bool realParams = FALSE;
uentry le = context_getHeader ();
fileloc fl = uentry_whereSpecified (le);
uentryList specParamNames = uentryList_undefined;
uentryList paramNames = context_getParams ();
if (uentry_isFunction (le))
{
specParamNames = uentry_getParams (le);
if (uentryList_isUndefined (specParamNames))
{
; /* unknown params */
}
else if (uentryList_size (paramNames) != uentryList_size (specParamNames))
{
llbug
(message ("exprNode_checkAllMods: parameter lists have different sizes: "
"%q (%d) / %q (%d)",
uentryList_unparse (paramNames),
uentryList_size (paramNames),
uentryList_unparse (specParamNames),
uentryList_size (specParamNames)));
}
else if (uentryList_size (paramNames) > 0
&& !uentry_hasRealName (uentryList_getN (specParamNames, 0)))
{
/* loaded from a library */
}
else
{
realParams = TRUE;
}
}
sRefSet_allElements (mods, sr)
{
if (sRef_isNothing (sr) || sRef_isSpecState (sr))
{
; /* should report on anything? */
}
else if (sRef_isInternalState (sr))
{
if (!sRef_isModified (sr))
{
if (sRefSet_hasStatic (mods))
{
; /* okay */
}
else
{
if (optgenerror
(FLG_MUSTMOD,
message
("Function %s specified to modify internal state "
"but no internal state is modified",
uentry_rawName (ue)),
uentry_whereLast (ue)))
{
uentry_showWhereSpecified (le);
}
}
}
}
else
{
if (!sRef_isModified (sr))
{
cstring sname = realParams ? sRef_unparse (sr) : sRef_unparse (sr);
if (fileloc_isLib (fl) && !realParams)
{
voptgenerror
(FLG_MUSTMOD,
message ("Suspect object listed (%q) in modifies "
"clause of %s not modified: %s",
fileloc_unparse (fl),
uentry_rawName (ue),
sname),
uentry_whereLast (ue));
}
else
{
if (optgenerror
(FLG_MUSTMOD,
message ("Suspect object listed in modifies of %s "
"not modified: %s",
uentry_rawName (ue),
sname),
uentry_whereLast (ue)))
{
uentry_showWhereSpecified (le);
}
}
cstring_free (sname);
}
}
} end_sRefSet_allElements;
}
void exprNode_checkMacroBody (/*@only@*/ exprNode e)
{
if (!exprNode_isError (e))
{
uentry hdr;
if (!(context_inFunctionLike () || context_inMacroConstant ()
|| context_inUnknownMacro ()))
{
llcontbug
(message
("exprNode_checkMacroBody: not in macro function or constant: %q",
context_unparse ()));
exprNode_free (e);
return;
}
hdr = context_getHeader ();
if (e->kind == XPR_STMTLIST || e->kind == XPR_BODY)
{
voptgenerror
(FLG_MACROSTMT,
message
("Macro %q definition is statement list (recommend "
"do { ... } while (0) constuction to ensure multiple "
"statement macro is syntactic function)",
uentry_getName (hdr)),
fileloc_isDefined (e->loc) ? e->loc : g_currentloc);
}
if (context_inMacroConstant ())
{
ctype t = uentry_getType (hdr);
uentry_setDefined (hdr, e->loc);
if (!(exprNode_matchType (t, e)))
{
cstring uname = uentry_getName (hdr);
if (cstring_equal (uname, context_getTrueName ())
|| cstring_equal (uname, context_getFalseName ()))
{
/*
** We need to do something special to allow FALSE and TRUE
** to be defined without reporting errors. This is a tad
** bogus, but otherwise lots of things would break.
*/
llassert (ctype_isManifestBool (t));
/* Should also check type of e is a reasonable (?) bool type. */
}
else
{
if (optgenerror
(FLG_INCONDEFS,
message
("Constant %q specified as %s, but defined as %s: %s",
uentry_getName (hdr),
ctype_unparse (t),
ctype_unparse (e->typ),
exprNode_unparse (e)),
e->loc))
{
uentry_showWhereSpecified (hdr);
}
}
cstring_free (uname);
}
else
{
if (context_maybeSet (FLG_NULLSTATE)
&& ctype_isUA(t)
&& ctype_isRealPointer (t)
&& exprNode_isNullValue (e))
{
uentry ue = usymtab_getTypeEntry (ctype_typeId (t));
sRef sr = uentry_getSref (ue);
if (!sRef_possiblyNull (sr))
{
vgenhinterror
(FLG_NULLSTATE,
message ("Constant %q of non-null type %s defined "
"as null: %s",
uentry_getName (hdr), ctype_unparse (t),
exprNode_unparse (e)),
message ("If %s can be null, add a /*@null@*/ "
"qualifer to its typedef.",
ctype_unparse (t)),
e->loc);
}
uentry_mergeConstantValue (hdr, e->val);
e->val = multiVal_undefined;
}
}
}
else if (context_inMacroFunction () || context_inUnknownMacro ())
{
ctype rettype = context_getRetType ();
if (context_isMacroMissingParams ())
{
llassert (context_inMacroFunction ());
/*
** # define newname oldname
**
** newname is a function
** specification of oldname should match
** specification of newname.
*/
if (!ctype_isFunction (e->typ))
{
voptgenerror
(FLG_INCONDEFS,
message ("Function %s defined by unparameterized "
"macro not corresponding to function",
context_inFunctionName ()),
e->loc);
}
else
{
uentry ue = exprNode_getUentry (e);
if (uentry_isValid (ue))
{
/*
** Okay, for now --- should check for consistency
*/
/*
** uentry oldue = usymtab_lookup (cfname);
*/
/* check var conformance here! */
}
else
{
voptgenerror
(FLG_INCONDEFS,
message ("Function %s defined by unparameterized "
"macro not corresponding to function",
context_inFunctionName ()),
e->loc);
}
e->typ = ctype_getReturnType (e->typ);
rettype = e->typ; /* avoid aditional errors */
}
}
if (ctype_isVoid (rettype) || ctype_isUnknown (rettype))
{
; /* don't complain when void macros have values */
}
else if (!exprNode_matchType (rettype, e))
{
if (optgenerror
(FLG_INCONDEFS,
message ("Function %q specified to return %s, "
"implemented as macro having type %s: %s",
uentry_getName (hdr),
ctype_unparse (rettype), ctype_unparse (e->typ),
exprNode_unparse (e)),
e->loc))
{
uentry_showWhereSpecified (hdr);
}
}
else
{
switch (e->kind)
{
/* these expressions have values: */
case XPR_PARENS: case XPR_ASSIGN:
case XPR_EMPTY: case XPR_VAR:
case XPR_OP: case XPR_POSTOP:
case XPR_PREOP: case XPR_CALL:
case XPR_SIZEOFT: case XPR_SIZEOF:
case XPR_ALIGNOFT: case XPR_ALIGNOF:
case XPR_CAST: case XPR_FETCH:
case XPR_COMMA: case XPR_COND:
case XPR_ARROW: case XPR_CONST:
case XPR_STRINGLITERAL: case XPR_NUMLIT:
case XPR_FACCESS: case XPR_OFFSETOF:
transferChecks_return (e, hdr);
break;
/* these expressions don't */
case XPR_LABEL:
case XPR_VAARG: case XPR_ITER:
case XPR_FOR: case XPR_FORPRED:
case XPR_GOTO: case XPR_CONTINUE:
case XPR_BREAK: case XPR_RETURN:
case XPR_NULLRETURN: case XPR_IF:
case XPR_IFELSE: case XPR_DOWHILE:
case XPR_WHILE: case XPR_STMT:
case XPR_STMTLIST: case XPR_SWITCH:
case XPR_INIT: case XPR_BODY:
case XPR_NODE: case XPR_ITERCALL:
case XPR_TOK: case XPR_CASE:
case XPR_FTCASE: case XPR_FTDEFAULT:
case XPR_DEFAULT: case XPR_WHILEPRED:
case XPR_BLOCK: case XPR_INITBLOCK:
if (optgenerror
(FLG_INCONDEFS,
message ("Function %q specified to return %s, "
"implemented as macro with no result: %s",
uentry_getName (hdr),
ctype_unparse (rettype),
exprNode_unparse (e)),
e->loc))
{
uentry_showWhereSpecified (hdr);
}
}
}
usymtab_checkFinalScope (FALSE);
}
else
{
llbug (message ("exprNode_checkMacroBody: not in macro function: %q", context_unparse ()));
}
exprNode_free (e);
}
context_exitFunction ();
return;
}
void exprNode_checkFunctionBody (exprNode body)
{
if (!exprNode_isError (body))
{
bool noret = context_getFlag (FLG_NORETURN);
bool checkret = exprNode_mustEscape (body);
if (!checkret
&& noret
&& !exprNode_errorEscape (body)
&& context_inRealFunction ()
&& ctype_isFunction (context_currentFunctionType ()))
{
ctype tr = ctype_getReturnType (context_currentFunctionType ());
if (!ctype_isFirstVoid (tr))
{
if (ctype_isUnknown (tr))
{
voptgenerror
(FLG_NORETURN,
cstring_makeLiteral ("Path with no return in function declared to implicity return int"),
g_currentloc);
}
else
{
voptgenerror
(FLG_NORETURN,
message ("Path with no return in function declared to return %t",
tr),
g_currentloc);
}
}
}
if (!checkret)
{
context_returnFunction ();
}
}
}
/*drl modified */
void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
{
constraintList c, t, post;
constraintList c2, fix;
context_enterInnerContext ();
llassert (exprNode_isDefined (body));
DPRINTF (("Checking body: %s", exprNode_unparse (body)));
/*
if we're not going to be printing any errors for buffer overflows
we can skip the checking to improve performance
FLG_DEBUGFUNCTIONCONSTRAINT controls wheather we perform the check anyway
in order to find potential problems like assert failures and seg faults...
*/
if (!(context_getFlag (FLG_DEBUGFUNCTIONCONSTRAINT)
|| context_getFlag (FLG_BOUNDSWRITE)
|| context_getFlag (FLG_BOUNDSREAD)
|| context_getFlag (FLG_LIKELYBOUNDSWRITE)
|| context_getFlag (FLG_LIKELYBOUNDSREAD)
|| context_getFlag (FLG_CHECKPOST)
|| context_getFlag (FLG_ALLOCMISMATCH)))
{
exprNode_free (body);
context_exitInnerPlain();
return;
}
exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
dependent... fix it! */
c = uentry_getFcnPreconditions (ue);
if (constraintList_isDefined (c))
{
DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
body->requiresConstraints =
constraintList_reflectChangesFreePre (body->requiresConstraints, c);
c2 = constraintList_copy (c);
fix = constraintList_makeFixedArrayConstraints (body->uses);
c2 = constraintList_reflectChangesFreePre (c2, fix);
constraintList_free (fix);
if (context_getFlag (FLG_ORCONSTRAINT))
{
t = constraintList_reflectChangesOr (body->requiresConstraints, c2 );
}
else
{
t = constraintList_reflectChanges(body->requiresConstraints, c2);
}
constraintList_free (body->requiresConstraints);
DPRINTF ((message ("The body has the required constraints: %s", constraintList_unparseDetailed (t) ) ) );
body->requiresConstraints = t;
t = constraintList_mergeEnsures (c, body->ensuresConstraints);
constraintList_free(body->ensuresConstraints);
body->ensuresConstraints = t;
DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_unparseDetailed (t) ) ) );
constraintList_free(c2);
}
if (constraintList_isDefined(c))
{
DPRINTF ((message ("The Function %s has the preconditions %s",
uentry_unparse(ue), constraintList_unparseDetailed(c))));
}
else
{
DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue))));
}
if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
{
constraintList implicitFcnConstraints = context_getImplicitFcnConstraints (ue);
if (constraintList_isDefined (implicitFcnConstraints))
{
DPRINTF (("Implicit constraints: %s", constraintList_unparse (implicitFcnConstraints)));
body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints,
implicitFcnConstraints);
constraintList_free (implicitFcnConstraints);
}
else
{
DPRINTF (("No implicit constraints"));
}
}
body->requiresConstraints = constraintList_sort (body->requiresConstraints);
constraintList_printError(body->requiresConstraints, g_currentloc);
post = uentry_getFcnPostconditions (ue);
if (context_getFlag (FLG_CHECKPOST))
{
if (constraintList_isDefined (post))
{
constraintList post2;
DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n",
constraintList_unparseDetailed (post) ) ) );
post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
post2 = constraintList_copy (post);
fix = constraintList_makeFixedArrayConstraints (body->uses);
post2 = constraintList_reflectChangesFreePre (post2, fix);
constraintList_free(fix);
if ( context_getFlag (FLG_ORCONSTRAINT) )
{
t = constraintList_reflectChangesOr (post2, body->ensuresConstraints);
}
else
{
t = constraintList_reflectChanges(post2, body->ensuresConstraints);
}
constraintList_free(post2);
constraintList_free(post);
post = t;
printf("Unresolved post conditions\n");
constraintList_printErrorPostConditions(post, g_currentloc);
}
}
if (constraintList_isDefined (post))
{
constraintList_free (post);
}
body->ensuresConstraints = constraintList_sort(body->ensuresConstraints);
if ( context_getFlag (FLG_FUNCTIONPOST) )
{
constraintList_printError(body->ensuresConstraints, g_currentloc);
}
/* ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
ConPrint (message ("Splint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
*/
if (constraintList_isDefined (c))
constraintList_free(c);
context_exitInnerPlain();
/* is it okay not to free this? */
DPRINTF (("Done checking constraints..."));
exprNode_free (body);
}
void exprChecks_checkEmptyMacroBody (void)
{
uentry hdr;
if (!(context_inFunctionLike () || context_inMacroConstant ()
|| context_inUnknownMacro ()))
{
llcontbug
(message ("exprNode_checkEmptyMacroBody: not in macro function or constant: %q",
context_unparse ()));
return;
}
hdr = context_getHeader ();
beginLine ();
if (uentry_isFunction (hdr))
{
voptgenerror
(FLG_MACROEMPTY,
message
("Macro definition for %q is empty", uentry_getName (hdr)),
g_currentloc);
usymtab_checkFinalScope (FALSE);
}
context_exitFunction ();
return;
}
void exprNode_checkIterBody (/*@only@*/ exprNode body)
{
context_exitAllClauses ();
context_exitFunction ();
exprNode_free (body);
}
void exprNode_checkIterEnd (/*@only@*/ exprNode body)
{
context_exitAllClauses ();
context_exitFunction ();
exprNode_free (body);
}
static
bool checkModifyAuxAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
bool hasMods = context_hasMods ();
flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
if (exprNode_isDefined (f))
{
f->sets = sRefSet_insert (f->sets, s);
}
if (context_getFlag (FLG_MODIFIES)
&& (hasMods || context_getFlag (FLG_MODNOMODS)))
{
sRefSet mods = context_modList ();
if (!sRef_canModify (s, mods))
{
sRef rb = sRef_getRootBase (s);
if (sRef_isFileOrGlobalScope (rb))
{
if (!context_checkGlobMod (rb))
{
return FALSE;
}
}
if (sRef_isInvalid (alias) || sRef_sameName (s, alias))
{
if (sRef_isLocalVar (sRef_getRootBase (s)))
{
voptgenerror
(errCode,
message
("Undocumented modification of internal state (%q): %s",
sRef_unparse (s), exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
else
{
if (sRef_isSystemState (s))
{
if (errCode == FLG_MODNOMODS)
{
if (context_getFlag (FLG_MODNOMODS))
{
errCode = FLG_MODFILESYSTEM;
}
}
else
{
errCode = FLG_MODFILESYSTEM;
}
}
voptgenerror
(errCode,
message ("Undocumented modification of %q: %s",
sRef_unparse (s), exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
return TRUE;
}
else
{
if (sRef_isReference (s) && !sRef_isAddress (alias))
{
voptgenerror
(errCode,
message
("Possible undocumented modification of %q through alias %q: %s",
sRef_unparse (s),
sRef_unparse (alias),
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
return TRUE;
}
}
}
}
else
{
if (context_maybeSet (FLG_MUSTMOD))
{
(void) sRef_canModify (s, context_modList ());
}
if (sRef_isRefsField (s))
{
sRef_setModified (s);
}
}
return FALSE;
}
static
bool checkModifyAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
DPRINTF (("Check modify aux: %s", sRef_unparseFull (s)));
if (sRef_isReference (s) && sRef_isObserver (s)
&& context_maybeSet (FLG_MODOBSERVER))
{
cstring sname;
if (sRef_isPointer (s))
{
sRef base = sRef_getBase (s);
sname = sRef_unparse (base);
}
else
{
if (sRef_isAddress (s))
{
sRef p = sRef_constructPointer (s);
sname = sRef_unparse (p);
}
else
{
sname = sRef_unparse (s);
}
}
if (!sRef_isValid (alias) || sRef_sameName (s, alias))
{
if (sRef_isMeaningful (s))
{
if (optgenerror
(FLG_MODOBSERVER,
message ("Suspect modification of observer %s: %s",
sname, exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc))
{
sRef_showExpInfo (s);
}
}
else
{
voptgenerror
(FLG_MODOBSERVER,
message ("Suspect modification of observer returned by "
"function call: %s",
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
}
else
{
if (optgenerror
(FLG_MODOBSERVER,
message ("Suspect modification of observer %s through alias %q: %s",
sname, sRef_unparse (alias), exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc))
{
sRef_showExpInfo (s);
}
}
cstring_free (sname);
}
(void) checkModifyAuxAux (s, f, alias, err);
return FALSE;
}
static
bool checkModifyValAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
(void) checkModifyAuxAux (s, f, alias, err);
return FALSE;
}
static
bool checkCallModifyAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
bool result = FALSE;
DPRINTF (("Check modify aux: %s / %s",
sRef_unparse (s), sRef_unparse (alias)));
if (sRef_isObserver (s) && context_maybeSet (FLG_MODOBSERVER))
{
sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
cstring sname = sRef_unparse (p);
if (!sRef_isValid (alias) || sRef_sameName (s, alias))
{
if (sRef_isMeaningful (s))
{
result = optgenerror
(FLG_MODOBSERVER,
message ("Suspect modification of observer %s: %s",
sname, exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
else
{
result = optgenerror
(FLG_MODOBSERVER,
message ("Suspect modification of observer returned by "
"function call: %s",
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
}
else
{
result = optgenerror
(FLG_MODOBSERVER,
message
("Suspect modification of observer %s through alias %q: %s",
sname, sRef_unparse (alias), exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
cstring_free (sname);
}
else if (context_maybeSet (FLG_MODIFIES))
{
DPRINTF (("can modify: %s / %s",
sRef_unparse (s),
sRefSet_unparse (context_modList ())));
if (!(sRef_canModifyVal (s, context_modList ())))
{
sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
cstring sname = sRef_unparse (p);
bool hasMods = context_hasMods ();
sRef rb = sRef_getRootBase (s);
flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
bool check = TRUE;
DPRINTF (("Can't modify! %s", sRef_unparse (s)));
if (sRef_isFileOrGlobalScope (rb))
{
uentry ue = sRef_getUentry (rb);
/* be more specific here! */
if (!uentry_isCheckedModify (ue))
{
check = FALSE;
}
}
if (check)
{
if (!sRef_isValid (alias) || sRef_sameName (s, alias))
{
if (sRef_isLocalVar (sRef_getRootBase (s)))
{
voptgenerror
(errCode,
message
("Undocumented modification of internal "
"state (%q) through call to %s: %s",
sRef_unparse (s), exprNode_unparse (f),
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
else
{
if (sRef_isSystemState (s))
{
if (errCode == FLG_MODNOMODS)
{
if (context_getFlag (FLG_MODNOMODS))
{
errCode = FLG_MODFILESYSTEM;
}
}
else
{
errCode = FLG_MODFILESYSTEM;
}
}
result = optgenerror
(errCode,
message ("Undocumented modification of %s "
"possible from call to %s: %s",
sname,
exprNode_unparse (f),
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
}
else
{
result = optgenerror
(errCode,
message ("Undocumented modification of %s possible "
"from call to %s (through alias %q): %s",
sname,
exprNode_unparse (f),
sRef_unparse (alias),
exprNode_unparse (err)),
exprNode_isDefined (f) ? f->loc : g_currentloc);
}
}
cstring_free (sname);
}
}
else
{
if (context_maybeSet (FLG_MUSTMOD))
{
(void) sRef_canModifyVal (s, context_modList ());
}
}
return result;
}
void exprNode_checkCallModifyVal (sRef s, exprNodeList args, exprNode f, exprNode err)
{
s = sRef_fixBaseParam (s, args);
DPRINTF (("Check call modify: %s", sRef_unparse (s)));
sRef_aliasCheckPred (checkCallModifyAux, NULL, s, f, err);
}
void
exprChecks_checkExport (uentry e)
{
if (context_checkExport (e))
{
fileloc fl = uentry_whereDeclared (e);
if (fileloc_isHeader (fl) && !fileloc_isLib (fl)
&& !fileloc_isImport (fl) && !uentry_isStatic (e))
{
if (uentry_isFunction (e) ||
(uentry_isVariable (e) && ctype_isFunction (uentry_getType (e))))
{
voptgenerror
(FLG_EXPORTFCN,
message ("Function exported, but not specified: %q",
uentry_getName (e)),
fl);
}
else if (uentry_isExpandedMacro (e))
{
voptgenerror
(FLG_EXPORTMACRO,
message ("Expanded macro exported, but not specified: %q",
uentry_getName (e)),
fl);
}
else if (uentry_isVariable (e) && !uentry_isParam (e))
{
voptgenerror
(FLG_EXPORTVAR,
message ("Variable exported, but not specified: %q",
uentry_getName (e)),
fl);
}
else if (uentry_isEitherConstant (e))
{
voptgenerror
(FLG_EXPORTCONST,
message ("Constant exported, but not specified: %q",
uentry_getName (e)),
fl);
}
else if (uentry_isIter (e) || uentry_isEndIter (e))
{
voptgenerror
(FLG_EXPORTITER,
message ("Iterator exported, but not specified: %q",
uentry_getName (e)),
fl);
}
else if (uentry_isDatatype (e))
{
; /* error already reported */
}
else
{
BADEXIT;
}
}
}
}
static void checkSafeReturnExpr (/*@notnull@*/ exprNode e)
{
ctype tr = ctype_getReturnType (context_currentFunctionType ());
ctype te = exprNode_getType (e);
/* evans 2001-08-21: added test to warn about void returns from void functions */
if (ctype_isVoid (tr))
{
(void) gentypeerror
(te, e, tr, exprNode_undefined,
message ("Return expression from function declared void: %s", exprNode_unparse (e)),
e->loc);
return;
}
if (!ctype_forceMatch (tr, te) && !exprNode_matchLiteral (tr, e))
{
(void) gentypeerror
(te, e, tr, exprNode_undefined,
message ("Return value type %t does not match declared type %t: %s",
te, tr, exprNode_unparse (e)),
e->loc);
}
else
{
sRef ret = e->sref;
uentry rval = context_getHeader ();
sRef resultref = uentry_getSref (rval);
DPRINTF (("Check return: %s / %s / %s",
exprNode_unparse (e),
sRef_unparseFull (e->sref),
uentry_unparse (rval)));
transferChecks_return (e, rval);
DPRINTF (("After return: %s / %s / %s",
exprNode_unparse (e),
sRef_unparseFull (e->sref),
uentry_unparse (rval)));
if (!(sRef_isExposed (uentry_getSref (context_getHeader ()))
|| sRef_isObserver (uentry_getSref (context_getHeader ())))
&& (context_getFlag (FLG_RETALIAS)
|| context_getFlag (FLG_RETEXPOSE)))
{
sRef base = sRef_getRootBase (ret);
ctype rtype = e->typ;
if (ctype_isUnknown (rtype))
{
rtype = tr;
}
if (ctype_isVisiblySharable (rtype))
{
if (context_getFlag (FLG_RETALIAS))
{
sRef_aliasCheckPred (checkRefGlobParam, NULL, base,
e, exprNode_undefined);
}
if (context_getFlag (FLG_RETEXPOSE) && sRef_isIReference (ret)
&& !sRef_isExposed (resultref) && !sRef_isObserver (resultref))
{
sRef_aliasCheckPred (checkRepExposed, NULL, base, e,
exprNode_undefined);
}
}
}
}
}
syntax highlighted by Code2HTML, v. 0.9.1