/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
**
*/
+static int inCompoundStatementExpression = 0;
+
+void
+exprChecks_inCompoundStatementExpression (void)
+{
+ inCompoundStatementExpression++;
+}
+
void
-exprNode_checkStatement (exprNode e)
+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;
{
uentry arg = uentryList_getN (params, paramno);
sRef ref = uentry_getSref (arg);
-
+
if (uentry_isReturned (arg)
|| sRef_isOnly (ref)
|| sRef_isExposed (ref)
/*drl modified */
-void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode fcnBody)
+void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
{
constraintList c, t, post;
constraintList c2, fix;
- constraintList implicitFcnConstraints;
-
- /*@owned@*/ exprNode body;
-
context_enterInnerContext ();
- body = fcnBody;
+ llassert (exprNode_isDefined (body));
+
+ DPRINTF (("Checking body: %s", exprNode_unparse (body)));
/*
if we're not going to be printing any errors for buffer overflows
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_BOUNDSWRITE) ||
- context_getFlag(FLG_BOUNDSREAD) ||
- context_getFlag(FLG_CHECKPOST)))
- {
- exprNode_free (body);
- context_exitInnerPlain();
-
- return;
- }
- }
+ 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);
+ exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
+ dependent... fix it! */
- c = uentry_getFcnPreconditions (ue);
- DPRINTF(("function constraints\n"));
- DPRINTF (("\n\n\n\n\n\n\n"));
+ c = uentry_getFcnPreconditions (ue);
- if (constraintList_isDefined(c) )
+ if (constraintList_isDefined (c))
{
- DPRINTF ((message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+ DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
- body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, 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))
}
constraintList_free (body->requiresConstraints);
- DPRINTF ((message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+ DPRINTF ((message ("The body has the required constraints: %s", constraintList_unparseDetailed (t) ) ) );
body->requiresConstraints = t;
constraintList_free(body->ensuresConstraints);
body->ensuresConstraints = t;
-
- DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_printDetailed (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_printDetailed(c))));
+ uentry_unparse(ue), constraintList_unparseDetailed(c))));
}
else
{
DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue))));
}
- implicitFcnConstraints = getImplicitFcnConstraints();
-
- if (constraintList_isDefined(implicitFcnConstraints) )
+ if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
{
- if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+ constraintList implicitFcnConstraints = context_getImplicitFcnConstraints (ue);
+
+ if (constraintList_isDefined (implicitFcnConstraints))
{
+ DPRINTF (("Implicit constraints: %s", constraintList_unparse (implicitFcnConstraints)));
+
body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints,
- implicitFcnConstraints );
+ implicitFcnConstraints);
+ constraintList_free (implicitFcnConstraints);
+ }
+ else
+ {
+ DPRINTF (("No implicit constraints"));
}
}
constraintList post2;
DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n",
- constraintList_printDetailed (post) ) ) );
+ constraintList_unparseDetailed (post) ) ) );
post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
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 ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
*/
- if (constraintList_isDefined(c) )
+ if (constraintList_isDefined (c))
constraintList_free(c);
context_exitInnerPlain();
-
- /*is it okay not to free this?*/
- exprNode_free (body);
- }
+
+ /* is it okay not to free this? */
+ DPRINTF (("Done checking constraints..."));
+ exprNode_free (body);
+}
void exprChecks_checkEmptyMacroBody (void)
{
andersk / splint.git / blobdiff