/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
**
** 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
*/
/*
** exprChecks.c
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
-# include "aliasChecks.h"
+# include "transferChecks.h"
# include "exprChecks.h"
/*
/*@access exprNode@*/
-static bool checkCallModifyAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
-static bool checkModifyValAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
-static bool checkModifyAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
+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);
/*
if (ctype_isVisiblySharable (ct))
{
- if (sRef_isGlobal (base))
+ if (sRef_isFileOrGlobalScope (base))
{
- voptgenerror
- (FLG_RETALIAS,
- message ("Function returns reference to global %q: %s",
- sRef_unparse (base),
- exprNode_unparse (e)),
- e->loc);
+ 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;
}
{
if (ctype_isVisiblySharable (e->typ))
{
- if (sRef_isGlobal (base))
+ if (sRef_isFileOrGlobalScope (base))
{
voptgenerror
(FLG_RETALIAS,
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);
{
if (ctype_isFunction (context_currentFunctionType ()))
{
- ctype tr = ctype_returnValue (context_currentFunctionType ());
+ ctype tr = ctype_getReturnType (context_currentFunctionType ());
if (!ctype_isFirstVoid (tr))
{
e->loc);
}
- if (ctype_isRealBool (ct))
+ if (ctype_isRealBool (ct) || ctype_isUnknown (ct))
+ /* evs 2000-12-20 added || ctype_isUnknown to avoid spurious messages */
{
;
}
uentry hdr;
if (!(context_inFunctionLike () || context_inMacroConstant ()
- || context_inMacroUnknown ()))
+ || context_inUnknownMacro ()))
{
llcontbug
(message
}
}
}
- else if (context_inMacroFunction () || context_inMacroUnknown ())
+ else if (context_inMacroFunction () || context_inUnknownMacro ())
{
ctype rettype = context_getRetType ();
e->loc);
}
- e->typ = ctype_returnValue (e->typ);
+ e->typ = ctype_getReturnType (e->typ);
rettype = e->typ; /* avoid aditional errors */
}
}
&& context_inRealFunction ()
&& ctype_isFunction (context_currentFunctionType ()))
{
- ctype tr = ctype_returnValue (context_currentFunctionType ());
+ ctype tr = ctype_getReturnType (context_currentFunctionType ());
if (!ctype_isFirstVoid (tr))
{
}
}
}
-
- /*@i44*/ /* drl added call*/
- // exprNode_checkFunction (context_getHeader (), body);
if (!checkret)
{
}
/*drl modified */
-extern constraintList implicitFcnConstraints;
-void exprNode_checkFunction (/*@unused@*/ uentry ue, exprNode body)
+void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode fcnBody)
{
- constraintList c, t;
- constraintList c2, fix;
+ constraintList c, t, post;
+ constraintList c2, fix;
+ constraintList implicitFcnConstraints;
- // return;
+ /*@owned@*/ exprNode body;
- // context_setFlag(FLG_ORCONSTRAINT, TRUE);
context_enterInnerContext ();
+ body = fcnBody;
+
+ /*
+ 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) )
+ /* check if errors will printed */
+ if (! (context_getFlag(FLG_DEBUGFUNCTIONCONSTRAINT) ||
+ context_getFlag(FLG_FUNCTIONCONSTRAINT) ||
+ context_getFlag(FLG_ARRAYBOUNDS) ||
+ context_getFlag(FLG_ARRAYBOUNDSREAD) ||
+ context_getFlag(FLG_CHECKPOST)
+ )
+ )
+ {
+ exprNode_free (body);
+ context_exitInnerPlain();
+
+ return;
+ }
+
exprNode_generateConstraints (body);
+
c = uentry_getFcnPreconditions (ue);
DPRINTF(("function constraints\n"));
DPRINTF (("\n\n\n\n\n\n\n"));
- if (c)
+ if (constraintList_isDefined(c) )
{
DPRINTF ( (message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
- body->requiresConstraints = reflectChangesFreePre (body->requiresConstraints, c);
+ body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, c);
c2 = constraintList_copy (c);
fix = constraintList_makeFixedArrayConstraints (body->uses);
- c2 = reflectChangesFreePre (c2, fix);
+ c2 = constraintList_reflectChangesFreePre (c2, fix);
constraintList_free(fix);
if ( context_getFlag (FLG_ORCONSTRAINT) )
{
- t = reflectChangesOr (body->requiresConstraints, c2 );
+ t = constraintList_reflectChangesOr (body->requiresConstraints, c2 );
}
else
{
- t = reflectChanges (body->requiresConstraints, c2);
+ t = constraintList_reflectChanges(body->requiresConstraints, c2);
}
constraintList_free(body->requiresConstraints);
constraintList_free(c2);
}
- if (c)
+ if (constraintList_isDefined(c) )
{
DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
}
DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
}
- if ( implicitFcnConstraints)
+ implicitFcnConstraints = getImplicitFcnConstraints();
+
+ if (constraintList_isDefined(implicitFcnConstraints) )
{
if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
{
- body->requiresConstraints = reflectChangesFreePre (body->requiresConstraints, implicitFcnConstraints );
+ body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, implicitFcnConstraints );
}
}
+
+ body->requiresConstraints = constraintList_sort (body->requiresConstraints);
constraintList_printError(body->requiresConstraints, g_currentloc);
- constraintList_printError(body->ensuresConstraints, g_currentloc);
- // ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(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_printDetailed (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);
- // ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
+ 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_printDetailed(body->ensuresConstraints) );
+ printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
+ printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+ */
- if (c)
+ if (constraintList_isDefined(c) )
constraintList_free(c);
context_exitInnerPlain();
/*is it okay not to free this?*/
- exprNode_free (body);
-}
+ exprNode_free (body);
+ }
void exprChecks_checkEmptyMacroBody (void)
{
uentry hdr;
if (!(context_inFunctionLike () || context_inMacroConstant ()
- || context_inMacroUnknown ()))
+ || context_inUnknownMacro ()))
{
llcontbug
(message ("exprNode_checkEmptyMacroBody: not in macro function or constant: %q",
}
static
-bool checkModifyAuxAux (sRef s, exprNode f, sRef alias, exprNode err)
+bool checkModifyAuxAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
bool hasMods = context_hasMods ();
flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
&& (hasMods || context_getFlag (FLG_MODNOMODS)))
{
sRefSet mods = context_modList ();
-
+
if (!sRef_canModify (s, mods))
{
sRef rb = sRef_getRootBase (s);
-
- if (sRef_isGlobal (rb))
+
+ if (sRef_isFileOrGlobalScope (rb))
{
if (!context_checkGlobMod (rb))
{
- return FALSE;
+ return FALSE;
}
}
-
+
if (sRef_isInvalid (alias) || sRef_sameName (s, alias))
{
if (sRef_isLocalVar (sRef_getRootBase (s)))
}
static
-bool checkModifyAux (sRef s, exprNode f, sRef alias, exprNode err)
+bool checkModifyAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
DPRINTF (("Check modify aux: %s", sRef_unparseFull (s)));
}
static
-bool checkModifyValAux (sRef s, exprNode f, sRef alias, exprNode err)
+bool checkModifyValAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
{
(void) checkModifyAuxAux (s, f, alias, err);
return FALSE;
}
static
-bool checkCallModifyAux (sRef s, exprNode f, sRef alias, exprNode err)
+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;
}
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;
sRef rb = sRef_getRootBase (s);
flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
bool check = TRUE;
-
- if (sRef_isGlobal (rb))
+
+ DPRINTF (("Can't modify! %s", sRef_unparse (s)));
+
+ if (sRef_isFileOrGlobalScope (rb))
{
uentry ue = sRef_getUentry (rb);
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);
}
static void checkSafeReturnExpr (/*@notnull@*/ exprNode e)
{
- ctype tr = ctype_returnValue (context_currentFunctionType ());
+ 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
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)));
+
checkReturnTransfer (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)
}
}
+
+
+
+
andersk / splint.git / blobdiff