Fixed implicit constraints for functions.
*/
extern sRef checkbufferConstraintClausesId (uentry p_ue);
-extern void setImplictfcnConstraints (void);
+extern void setImplicitfcnConstraints (void);
-/*@observer@*/ constraintList getImplicitFcnConstraints (void);
+/*@observer@*/ constraintList getImplicitFcnConstraints (void);
/* end drl*/
typedef enum
{
- LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE, CASTEQ
+ LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE,
}
arithType;
#ifndef __constraintExprData_h__
-
#define __constraintExprData_h__
-
typedef enum
{
BINARYOP_UNDEFINED,
}
constraintExprUnaryOpKind;
-
typedef struct constraintExprBinaryOp_
{
constraintExpr expr1;
constraintExpr expr2;
} constraintExprBinaryOp;
-
typedef struct constraintExprUnaryOp_
{
constraintExpr expr;
constraintExprUnaryOpKind unaryOp;
} constraintExprUnaryOp;
-
typedef union constraintExprData
{
constraintExprBinaryOp binaryOp;
extern constraintExprData constraintExprData_termSetTerm ( /*@returned@*/ /*@partial@*/ constraintExprData p_data, /*@only@*/ constraintTerm p_term);
-extern /*@observer@*/ constraintTerm constraintExprData_termGetTerm (/*@observer@*/ constraintExprData p_data) /*@*/;
+extern /*@exposed@*/ constraintTerm
+constraintExprData_termGetTerm (/*@observer@*/ constraintExprData p_data) /*@*/;
-extern constraintExprUnaryOpKind constraintExprData_unaryExprGetOp (/*@observer@*/ /*@reldef@*/ constraintExprData p_data) /*@*/;
+extern constraintExprUnaryOpKind
+constraintExprData_unaryExprGetOp (/*@observer@*/ /*@reldef@*/ constraintExprData p_data) /*@*/;
-extern /*@observer@*/ constraintExpr constraintExprData_unaryExprGetExpr (/*@observer@*/ /*@reldef@*/constraintExprData p_data) /*@*/;
+extern /*@observer@*/ constraintExpr
+constraintExprData_unaryExprGetExpr (/*@observer@*/ /*@reldef@*/constraintExprData p_data) /*@*/;
-extern constraintExprData constraintExprData_unaryExprSetOp (/*@partial@*/ /*@returned@*/ constraintExprData p_data, constraintExprUnaryOpKind p_op);
+extern constraintExprData
+constraintExprData_unaryExprSetOp (/*@partial@*/ /*@returned@*/ constraintExprData p_data, constraintExprUnaryOpKind p_op);
extern constraintExprData constraintExprData_unaryExprSetExpr (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr);
extern constraintList constraintList_sort (/*@returned@*/ constraintList p_ret)
/*@modifies p_ret@*/ ;
-extern void constraintList_castConstraints (constraintList p_c, ctype p_tfrom, ctype p_tto)
- /*@modifies p_c@*/ ;
-
extern void constraintList_dump (/*@observer@*/ constraintList p_c, FILE * p_f);
/*@only@*/ constraintList constraintList_undump (FILE * p_f);
extern /*@observer@*/ cstring context_getLarchPath (void) /*@*/ ;
extern /*@observer@*/ cstring context_getLCLImportDir (void) /*@*/ ;
+extern constraintList context_getImplicitFcnConstraints (uentry p_ue) /*@*/ ;
+
extern bool context_checkExport (uentry p_e) /*@*/ ;
extern bool context_checkGlobMod (sRef p_el) /*@*/ ;
extern bool context_checkGlobUse (uentry p_glob);
extern int context_getBugsLimit (void) /*@*/ ;
# define context_getBugsLimit() ((int)context_getValue(FLG_BUGSLIMIT))
-extern ctype context_setLastStruct (/*@returned@*/ ctype p_s) /*@modifies internalState@*/;
-extern ctype context_getLastStruct (/*@returned@*/ /*ctype p_s*/) /*@modifies internalState@*/;
-
/*drl added 2/4/2002*/
extern bool context_inOldStyleScope (void) /*@*/ ;
-extern void context_setGlobalStructInfo (ctype p_ct, constraintList p_list) /*@modifies internalState@*/ ;
/*drl added 3/5/2003*/
extern void functionClauseList_free (/*@only@*/ functionClauseList p_s) ;
functionClauseList
-functionClauseList_setImplictConstraints (/*@returned@*/ functionClauseList p_s);
+functionClauseList_setImplicitConstraints (/*@returned@*/ functionClauseList p_s);
/*@constant int functionClauseListBASESIZE;@*/
# define functionClauseListBASESIZE MIDBASESIZE
splintme:
./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted
+splintmebounds:
+ ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted +bounds +impboundsconstraints
+
splintmesupcounts:
./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw
splintme:
./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted
+splintmebounds:
+ ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted +bounds +impboundsconstraints
+
splintmesupcounts:
./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw
yyval.ntyp = idDecl_replaceCtype (yyvsp[-5].ntyp, ct);
/*drl 7/25/01 added*/
- setImplictfcnConstraints();
+ setImplicitfcnConstraints();
DPRINTF((message("namedDeclBase PushType TLPAREN TRPAREN...:\n adding implict constraints to functionClause List: %s",
functionClauseList_unparse(yyvsp[0].funcclauselist)
)
));
- fcl = functionClauseList_setImplictConstraints(yyvsp[0].funcclauselist);
+ fcl = functionClauseList_setImplicitConstraints(yyvsp[0].funcclauselist);
idDecl_addClauses (yyval.ntyp, fcl);
case 28:
{
functionClauseList fcl;
- setImplictfcnConstraints ();
+ setImplicitfcnConstraints ();
clearCurrentParams ();
yyval.ntyp = idDecl_replaceCtype (yyvsp[-6].ntyp, ctype_makeFunction (idDecl_getCtype (yyvsp[-6].ntyp), yyvsp[-3].entrylist));
)
)) ;
- fcl = functionClauseList_setImplictConstraints(yyvsp[0].funcclauselist);
+ fcl = functionClauseList_setImplicitConstraints(yyvsp[0].funcclauselist);
idDecl_addClauses (yyval.ntyp, fcl);
{ sRef_clearGlobalScopeSafe (); ;
break;}
case 406:
-{ ctype ct; ct = declareStruct (yyvsp[-9].cname, yyvsp[-4].flist); context_setGlobalStructInfo(ct, yyvsp[0].conL); yyval.ctyp = ct; ;
+{ ctype ct; ct = declareStruct (yyvsp[-9].cname, yyvsp[-4].flist); /* context_setGlobalStructInfo(ct, $12); */ yyval.ctyp = ct; ;
break;}
case 407:
{ sRef_setGlobalScopeSafe (); ;
$$ = idDecl_replaceCtype ($1, ct);
/*drl 7/25/01 added*/
- setImplictfcnConstraints();
+ setImplicitfcnConstraints();
DPRINTF((message("namedDeclBase PushType TLPAREN TRPAREN...:\n adding implict constraints to functionClause List: %s",
functionClauseList_unparse($6)
)
));
- fcl = functionClauseList_setImplictConstraints($6);
+ fcl = functionClauseList_setImplicitConstraints($6);
idDecl_addClauses ($$, fcl);
functionClauses
{
functionClauseList fcl;
- setImplictfcnConstraints ();
+ setImplicitfcnConstraints ();
clearCurrentParams ();
$$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4));
)
)) ;
- fcl = functionClauseList_setImplictConstraints($7);
+ fcl = functionClauseList_setImplicitConstraints($7);
idDecl_addClauses ($$, fcl);
structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
TRBRACE
optStructInvariant
- { ctype ct; ct = declareStruct ($3, $8); context_setGlobalStructInfo(ct, $12); $$ = ct; }
+ { ctype ct; ct = declareStruct ($3, $8); /* context_setGlobalStructInfo(ct, $12); */ $$ = ct; }
| NotType CUNION newId IsType TLBRACE { sRef_setGlobalScopeSafe (); }
CreateStructInnerScope
structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
unless the @out@ annotation has been applied to a parameter, then we only want to generate maxSet(p) > = 0
*/
-void setImplictfcnConstraints (void)
+void setImplicitfcnConstraints (void)
{
uentryList params;
sRef s;
uentryList_elements (params, el)
{
- DPRINTF (("setImplictfcnConstraints doing: %s", uentry_unparse(el)));
+ DPRINTF (("setImplicitfcnConstraints doing: %s", uentry_unparse(el)));
if (uentry_isVariable (el))
{
constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
{
- constraint ret;
-
- llassert (constraint_isDefined (c));
-
- ret = constraint_makeNew ();
- ret->lexpr = constraintExpr_copy (c->lexpr);
- ret->ar = c->ar;
- ret->expr = constraintExpr_copy (c->expr);
- ret->post = c->post;
- /*@-assignexpose@*/
- ret->generatingExpr = c->generatingExpr;
- /*@=assignexpose@*/
-
- if (c->orig != NULL)
- ret->orig = constraint_copy (c->orig);
- else
- ret->orig = NULL;
-
- if (c->or != NULL)
- ret->or = constraint_copy (c->or);
+ if (!constraint_isDefined (c))
+ {
+ return constraint_undefined;
+ }
else
- ret->or = NULL;
-
- ret->fcnPre = c->fcnPre;
-
- return ret;
+ {
+ constraint ret = constraint_makeNew ();
+ ret->lexpr = constraintExpr_copy (c->lexpr);
+ ret->ar = c->ar;
+ ret->expr = constraintExpr_copy (c->expr);
+ ret->post = c->post;
+ /*@-assignexpose@*/
+ ret->generatingExpr = c->generatingExpr;
+ /*@=assignexpose@*/
+
+ if (c->orig != NULL)
+ ret->orig = constraint_copy (c->orig);
+ else
+ ret->orig = NULL;
+
+ if (c->or != NULL)
+ ret->or = constraint_copy (c->or);
+ else
+ ret->or = NULL;
+
+ ret->fcnPre = c->fcnPre;
+
+ return ret;
+ }
}
/*like copy except it doesn't allocate memory for the constraint*/
constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
{
-
- llassert (constraint_isDefined (c) );
+ if (!constraint_isDefined (c))
+ {
+ return c;
+ }
if (c->generatingExpr == NULL)
{
constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2,
fileloc sequencePoint, arithType ar)
{
- constraint ret = constraint_makeNew ();
- llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
- ret->lexpr = c1;
- ret->ar = ar;
- ret->post = TRUE;
- ret->expr = c2;
- ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
- return ret;
+ if (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2))
+ {
+ constraint ret = constraint_makeNew ();
+ ret->lexpr = c1;
+ ret->ar = ar;
+ ret->post = TRUE;
+ ret->expr = c2;
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+ return ret;
+ }
+ else
+ {
+ return constraint_undefined;
+ }
}
static constraint
constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- if (FALSE) /* (!ctype_almostEqual (exprNode_getType (e1), exprNode_getType (e2))) */
- {
- /* If the types are not identical, need to be careful the element sizes may be different. */
- //! return (constraint_makeEnsuresOp (e1, e2, sequencePoint, CASTEQ));
- BADBRANCH;
- }
- else
- {
- return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
- }
+ return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
}
/* make constraint ensures e1 < e2 */
void constraint_free (/*@only@*/ constraint c)
{
- llassert (constraint_isDefined (c));
-
-
- if (constraint_isDefined (c->orig))
- constraint_free (c->orig);
- if ( constraint_isDefined (c->or))
- constraint_free (c->or);
+ if (constraint_isDefined (c))
+ {
+ constraint_free (c->orig);
+ c->orig = NULL;
-
- constraintExpr_free (c->lexpr);
- constraintExpr_free (c->expr);
+ constraint_free (c->or);
+ c->or = NULL;
- c->orig = NULL;
- c->or = NULL;
- c->lexpr = NULL;
- c->expr = NULL;
+ constraintExpr_free (c->lexpr);
+ c->lexpr = NULL;
- free (c);
-
+ constraintExpr_free (c->expr);
+ c->expr = NULL;
+
+ free (c);
+ }
}
cstring arithType_print (arithType ar) /*@*/
case EQ:
st = cstring_makeLiteral ("==");
break;
- case CASTEQ:
- st = cstring_makeLiteral ("(!)==");
- break;
case NONNEGATIVE:
st = cstring_makeLiteral ("NONNEGATIVE");
break;
cstring genExpr;
bool isLikely;
- llassert (constraint_isDefined (c) );
+ llassert (constraint_isDefined (c));
if (!c->post)
{
st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_unparseDeep (c));
}
- isLikely = constraint_isConstantOnly(c);
+ isLikely = constraint_isConstantOnly (c);
if (isLikely)
{
if (constraint_hasMaxSet (c))
{
- temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
+ temp = cstring_makeLiteral ("Likely out-of-bounds store: ");
}
else
{
- temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
+ temp = cstring_makeLiteral ("Likely out-of-bounds read: ");
}
}
else
if (constraint_hasMaxSet (c))
{
- temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
+ temp = cstring_makeLiteral ("Possible out-of-bounds store: ");
}
else
{
- temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
+ temp = cstring_makeLiteral ("Possible out-of-bounds read: ");
}
}
constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
{
- DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
- llassert (constraint_isDefined (c));
-
- if (c->orig == constraint_undefined)
+ if (constraint_isDefined (c))
{
- c->orig = constraint_copy (c);
- }
- else if (c->orig->fcnPre)
- {
- constraint temp = c->orig;
+ DPRINTF (("Doing constraint_preserverOrig for %q", constraint_printDetailed (c)));
- /* avoid infinite loop */
- c->orig = NULL;
- c->orig = constraint_copy (c);
- /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
- llassert (constraint_isDefined (c->orig) );
-
- if (c->orig->orig == NULL)
+ if (c->orig == constraint_undefined)
+ {
+ c->orig = constraint_copy (c);
+ }
+ else if (c->orig->fcnPre)
{
- c->orig->orig = temp;
- temp = NULL;
+ constraint temp = c->orig;
+
+ /* avoid infinite loop */
+ c->orig = NULL;
+ c->orig = constraint_copy (c);
+ /*drl 03/2/2003 if c != NULL then the copy of c will != null*/
+ llassert (constraint_isDefined (c->orig) );
+
+ if (c->orig->orig == NULL)
+ {
+ c->orig->orig = temp;
+ temp = NULL;
+ }
+ else
+ {
+ llcontbug ((message ("Expected c->orig->orig to be null")));
+ constraint_free (c->orig->orig);
+ c->orig->orig = temp;
+ temp = NULL;
+ }
}
else
{
- llcontbug ((message ("Expected c->orig->orig to be null")));
- constraint_free (c->orig->orig);
- c->orig->orig = temp;
- temp = NULL;
+ DPRINTF (("Not changing constraint"));
}
}
- else
- {
- DPRINTF (("Not changing constraint"));
- }
-
+
DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_unparseDetailed (c))));
return c;
}
static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr p_e,
ctype p_tfrom, ctype p_tto,
- fileloc loc);
+ fileloc p_loc);
/*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
/* @allocates result->data @ @sets result->kind @ */ ;
exprNode t, t1, t2;
lltok tok;
- llassert (e != NULL);
+ if (exprNode_isUndefined (e))
+ {
+ return constraintExpr_undefined;
+ }
data = e->edata;
ret = constraintExpr_makeExprNode (t);
break;
case XPR_COMMA:
- t = exprData_getPairA(data);
+ t = exprData_getPairA (data);
ret = constraintExpr_makeExprNode(t);
break;
default:
float fnewval;
long newval;
+ llassert (e != NULL);
llassert (e->kind == term);
ct = constraintExprData_termGetTerm (e->data);
llassert (constraintTerm_canGetValue (ct));
DPRINTF (("Scaling constraints by: %ld * %f", val, scale));
- // If scale * val is not an integer, give a warning
- fnewval = val * scale;
+ fnewval = ((float) val) * scale;
newval = (long) fnewval;
DPRINTF (("Values: %f / %ld", fnewval, newval));
+
if ((fnewval - (float) newval) > FLT_EPSILON)
{
voptgenerror (FLG_ALLOCMISMATCH,
message ("Allocated memory is converted to type %s of (size %d), "
- "which is not divisible into original allocation of space for %d elements of type %s (size %d)",
+ "which is not divisible into original allocation of space "
+ "for %d elements of type %s (size %d)",
ctype_unparse (tto), sizeto,
- val, ctype_unparse (tfrom), sizefrom),
+ long_toInt (val), ctype_unparse (tfrom), sizefrom),
loc);
}
if (lltok_isMult (tok))
{
- llassert (exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+ /*
+ ** If the sizeof is first, flip them.
+ */
+
+ llassert (exprNode_isDefined(t1) && exprNode_isDefined(t2));
+
+ if (t2->kind == XPR_SIZEOF || t2->kind == XPR_SIZEOFT)
+ {
+ exprNode tmp = t1;
+ t1 = t2;
+ t2 = tmp;
+ }
+
/*drl 3/2/2003 we know this from the fact that it's a
multiplication operation...*/
- if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT))
+ if (t1->kind == XPR_SIZEOF || t1->kind == XPR_SIZEOFT)
{
- ctype ct2;
+ ctype multype;
if (t1->kind == XPR_SIZEOFT)
{
- ct2 = qtype_getType (exprData_getType (t1->edata));
+ multype = qtype_getType (exprData_getType (t1->edata));
}
else
{
exprNode tempE = exprData_getSingle (t1->edata);
- ct2 = exprNode_getType (tempE);
+ multype = exprNode_getType (tempE);
}
- if (ctype_match (ctype_makePointer(ct2), tfrom)) //!
+ DPRINTF (("Here we go sizeof: %s / %s / %s",
+ ctype_unparse (multype), ctype_unparse (tfrom), ctype_unparse (tto)));
+ llassert (ctype_isPointer (tfrom));
+
+ if (ctype_almostEqual (ctype_makePointer (multype), tto))
{
/* this is a bit sloopy but ... */
- constraintExpr_free(e);
+ constraintExpr_free (e);
+ DPRINTF (("Sizeof types match okay!"));
return constraintExpr_makeExprNode (t2);
}
else
{
- /* nothing was here */
- DPRINTF (("MISMATCHING TYPES!"));
- }
- }
- else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT))
- {
- ctype ct2;
-
- if (t2->kind == XPR_SIZEOFT)
- {
- ct2 = qtype_getType (exprData_getType (t2->edata));
- }
- else
- {
- exprNode exprTemp;
- exprData eDTemp;
-
- exprTemp = exprData_getSingle (t2->edata);
+ int sizemul = ctype_getSize (multype);
+ ctype tobase = ctype_baseArrayPtr (tto);
+ int sizeto = ctype_getSize (tobase);
- llassert (exprNode_isDefined (exprTemp));
- eDTemp = exprTemp->edata;
-
- ct2 = qtype_getType (exprData_getType(eDTemp ));
-
- }
+ DPRINTF (("Types: %s / %s / %s",
+ ctype_unparse (tfrom), ctype_unparse (tto), ctype_unparse (multype)));
- if (ctype_match (ctype_makePointer (ct2), tfrom))
- {
- /*a bit of a sloopy way to do this but... */
- constraintExpr_free(e);
- return constraintExpr_makeExprNode (t1);
+ voptgenerror (FLG_ALLOCMISMATCH,
+ message ("Allocated memory is used as a different type (%s) from the sizeof type (%s)",
+ ctype_unparse (tobase), ctype_unparse (multype)),
+ loc);
+
+ if (sizemul == sizeto)
+ {
+ constraintExpr_free (e);
+ DPRINTF (("Sizeof types match okay!"));
+ return constraintExpr_makeExprNode (t2);
+ }
+ else
+ {
+ /* nothing was here */
+ DPRINTF (("MISMATCHING TYPES!"));
+ return (constraintExpr_div (constraintExpr_makeExprNode (t2), multype, tto, loc));
+ }
}
}
else
{
DPRINTF (("NOT A SIZEOF!"));
- /*empty*/
+ /* empty */
}
-
}
}
return data;
}
-
-
-/*@observer@*/ constraintTerm
+/*@exposed@*/ constraintTerm
constraintExprData_termGetTerm (/*@observer@*/ constraintExprData data)
{
llassert (constraintExprData_isDefined (data));
static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
-static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
+static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e)
{
{
exprNode snode;
fileloc loc;
- //! cstring s;
DPRINTF (("Generating constraint for: %s", exprNode_unparse (e)));
fcn->requiresConstraints =
constraintList_addListFree (fcn->requiresConstraints,
- checkCall (fcn, exprData_getArgs (data) ));
+ checkCall (fcn, exprData_getArgs (data)));
fcn->ensuresConstraints =
constraintList_addListFree (fcn->ensuresConstraints,
preconditions = constraintList_makeNew();
}
- if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+ if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
{
/*
uentryList_elements (arglist, el)
{
sRef s;
- TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+ TPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
s = uentry_getSref(el);
if (sRef_isReference (s) )
end_constraintList_elements; ;
}
-//! don't use this!
-void constraintList_castConstraints (constraintList c, ctype tfrom, ctype tto)
-{
- if (TRUE) /* flag to allow casting */
- {
- int fsize = ctype_getSize (tfrom);
- int tsize = ctype_getSize (tto);
-
- DPRINTF (("Sizes: [%s] [%s] %d / %d", ctype_unparse (tfrom),
- ctype_unparse (tto), fsize, tsize));
-
- if (fsize == tsize)
- {
- return; /* Sizes match, no change to constraints */
- }
- else
- {
- float scale = fsize / tsize;
-
- DPRINTF (("Scaling constraints by: %f", scale));
-
- constraintList_elements (c, el)
- {
- DPRINTF (("Scale: %s", constraint_unparse (el)));
- // constraint_scaleSize (el, scale);
- DPRINTF ((" ==> %s", constraint_unparse (el)));
- }
- end_constraintList_elements;
- }
- }
-}
-
-
constraintList constraintList_sort (/*@returned@*/ constraintList ret)
{
if (constraintList_isUndefined(ret) )
static bool constraint_conflict (constraint c1, constraint c2)
{
-
- llassert(constraint_isDefined(c1) );
- llassert(constraint_isDefined(c2) );
+ if (!constraint_isDefined(c1) || !constraint_isDefined(c2))
+ {
+ return FALSE;
+ }
if (constraintExpr_similar (c1->lexpr, c2->lexpr))
{
static bool constraintResolve_satisfies (constraint pre, constraint post)
{
- llassert (constraint_isDefined(pre));
- llassert (constraint_isDefined(post));
+ if (!constraint_isDefined (pre))
+ {
+ return TRUE;
+ }
+
+ if (!constraint_isDefined(post))
+ {
+ return FALSE;
+ }
if (constraint_isAlwaysTrue (pre))
return TRUE;
{
switch (c->ar)
{
- case CASTEQ:
case EQ:
case GTE:
case LTE:
/*@only@*/ constraint constraint_substitute (/*@observer@*/ /*@temp@*/ constraint c, constraintList p)
{
- constraint ret;
+ constraint ret = constraint_copy (c);
- ret = constraint_copy(c);
constraintList_elements (p, el)
{
- llassert(constraint_isDefined(el) );
- if ( el->ar == EQ)
- if (!constraint_conflict (ret, el) )
-
- {
- constraint temp;
-
- temp = constraint_copy(el);
-
- temp = constraint_adjust(temp, ret);
-
- llassert(constraint_isDefined(temp) );
-
-
- DPRINTF((message ("constraint_substitute :: Substituting in %s using %s",
- constraint_print (ret), constraint_print (temp)
- ) ) );
-
+ if (constraint_isDefined (el))
+ {
+ if ( el->ar == EQ)
+ if (!constraint_conflict (ret, el))
+ {
+ constraint temp = constraint_copy(el);
+ temp = constraint_adjust(temp, ret);
+
+ llassert(constraint_isDefined(temp) );
+
+
+ DPRINTF (("constraint_substitute :: Substituting in %s using %s",
+ constraint_print (ret), constraint_print (temp)));
- ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
- DPRINTF(( message (" constraint_substitute :: The new constraint is %s", constraint_print (ret) ) ));
- constraint_free(temp);
- }
+ ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
+ DPRINTF (("constraint_substitute :: The new constraint is %s", constraint_print (ret)));;
+ constraint_free(temp);
+ }
+ }
}
end_constraintList_elements;
- ret = constraint_simplify(ret);
-
+ ret = constraint_simplify (ret);
DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_print (ret) ) ));
-
return ret;
}
}
}
-
-/*drl 12/30/01 these are some ugly functions that were added to facilitate struct annotations */
-
-
-/*drl added */
-static ctype lastStruct;
-
-ctype context_setLastStruct (/*@returned@*/ ctype s) /*@globals lastStruct@*/
+constraintList context_getImplicitFcnConstraints (uentry ue)
{
- lastStruct = s;
- return s;
-}
-
-ctype context_getLastStruct (/*@returned@*/ /*ctype s*/) /*@globals lastStruct@*/
-{
- return lastStruct;
-}
-
-/*
-** Why is this stuff in context.c?
-*/
-
-/*@unused@*/ static int sInfoNum = 0;
-
-
-struct getUe {
- /*@unused@*/ uentry ue;
- /*@unused@*/ sRef s;
-};
-
-struct sInfo {
- /*@unused@*/ ctype ct;
- /*@unused@*/ constraintList inv;
- /*@unused@*/ int ngetUe;
- /*@unused@*/ struct getUe * t ;
-};
-
-/* unused: static struct sInfo globalStructInfo; */
+ constraintList ret = constraintList_makeNew ();
+ uentryList params = uentry_getParams (ue);
-/*drl 1/6/2001: I didn't think these functions were solid enough to include in the
- stable release of splint. I coomented them out so that they won't break anything
- but didn't delete them because they will be fixed and included later
-
-
-*/
-
-/*@-paramuse@*/
-
-void context_setGlobalStructInfo (ctype ct, constraintList list)
-{
-# if 0
- /* int i;
- uentryList f;
-
- f = ctype_getFields (ct);
-
- if (constraintList_isDefined(list) )
+ uentryList_elements (params, el)
{
- globalStructInfo.ct = ct;
- globalStructInfo.inv = list;
-
- globalStructInfo.ngetUe = 0;
+ DPRINTF (("setImplicitfcnConstraints doing: %s", uentry_unparse(el)));
- /* abstraction violation fix it * /
- globalStructInfo.t = dmalloc(f->nelements * sizeof(struct getUe) );
-
- globalStructInfo.ngetUe = f->nelements;
-
- i = 0;
-
- uentryList_elements(f, ue)
+ if (uentry_isElipsisMarker (el))
{
- globalStructInfo.t[i].ue = ue;
- globalStructInfo.t[i].s = uentry_getSref(ue);
- TPRINTF(( message(" setGlobalStructInfo:: adding ue=%s and sRef=%s",
- uentry_unparse(ue), sRef_unparse( uentry_getSref(ue) )
- )
- ));
- i++;
+ ;
}
- end_uentryList_elements;
- }
- */
-# endif
-}
-
-# if 0
-/*
-
-bool hasInvariants (ctype ct) /*@* /
-{
- if ( ctype_sameName(globalStructInfo.ct, ct) )
+ else
+ {
+ sRef s = uentry_getSref (el);
+
+ DPRINTF (("Trying: %s", sRef_unparse (s)));
- return TRUE;
+ if (ctype_isPointer (sRef_getType (s)))
+ {
+ constraint c = constraint_makeSRefWriteSafeInt (s, 0);
+ ret = constraintList_add (ret, c);
+
+ /*drl 10/23/2002 added support for out*/
+
+ if (!uentry_isOut(el))
+ {
+ c = constraint_makeSRefReadSafeInt (s, 0);
+ ret = constraintList_add (ret , c);
+ }
+ }
+ else
+ {
+ DPRINTF (("%s is NOT a pointer", sRef_unparseFull (s)));
+ }
+ }
+ } end_uentryList_elements;
- else
-
- return FALSE;
-
+ DPRINTF (("Returns ==> %s", constraintList_unparse (ret)));
+ return ret;
}
-*/
-# endif
-
-/*@=paramuse@*/
-
-
-
return ctype_getSize (ct->contents.base);
}
}
- case CT_FIXEDARRAY: //!
+ case CT_FIXEDARRAY:
case CT_ARRAY:
case CT_FCN:
case CT_STRUCT:
if (ctype_isBroken (clp))
{
- llbuglit ("ctype_baseArrayPtr: bogus ctype");
+ llcontbug (message ("ctype_baseArrayPtr: bogus ctype getting base of: %s", ctype_unparse (c)));
+ return ctype_unknown;
}
return clp;
{
constraintList c, t, post;
constraintList c2, fix;
- constraintList implicitFcnConstraints;
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
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_LIKELYBOUNDSWRITE) ||
- context_getFlag(FLG_LIKELYBOUNDSREAD) ||
- 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); /* evans 2002-03-02: this should not be declared to take a
dependent... fix it! */
if (constraintList_isDefined (c))
{
- DPRINTF ((message ("Function preconditions are %s \n\n\n\n\n",
- constraintList_unparseDetailed (c) ) ) );
+ DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
body->requiresConstraints =
constraintList_reflectChangesFreePre (body->requiresConstraints, c);
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"));
}
}
printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
*/
- if (constraintList_isDefined(c) )
+ if (constraintList_isDefined (c))
constraintList_free(c);
context_exitInnerPlain();
DPRINTF (("Cast: -> %s", sRef_unparseFull (ret->sref)));
- constraintList_castConstraints (ret->requiresConstraints, t, c);
- constraintList_castConstraints (ret->ensuresConstraints, t, c);
-
if (!sRef_isConst (e->sref))
{
usymtab_addForceMustAlias (ret->sref, e->sref);
{
FK_BOUNDS, FK_MEMORY, plainFlag,
"impboundsconstraints",
- FLG_IMPLICTCONSTRAINT,
+ FLG_IMPBOUNDSCONSTRAINTS,
"generate implicit constraints for functions",
NULL,
0, 0
}
functionClauseList
-functionClauseList_setImplictConstraints (/*@returned@*/ functionClauseList s)
+functionClauseList_setImplicitConstraints (/*@returned@*/ functionClauseList s)
{
bool addedConstraints;
constraintList c;
- DPRINTF ((message ("functionClauseList_setImplictConstraints called ") ));
+ DPRINTF ((message ("functionClauseList_setImplicitConstraints called ") ));
addedConstraints = FALSE;
-
c = getImplicitFcnConstraints ();
if (constraintList_isEmpty(c) )
{
constraintList implCons = getImplicitFcnConstraints ();
- DPRINTF ((message ("functionClauseList_ImplictConstraints adding the implict constraints: %s to %s",
+ DPRINTF ((message ("functionClauseList_ImplicitConstraints adding the implict constraints: %s to %s",
constraintList_print(implCons), constraintList_print (con->constraint.buffer))));
functionConstraint_addBufferConstraints (con, constraintList_copy (implCons) );
addedConstraints = TRUE;
- DPRINTF ((message ("functionClauseList_ImplictConstraints the new constraint is %s",
+ DPRINTF ((message ("functionClauseList_ImplicitConstraints the new constraint is %s",
functionConstraint_unparse (con))));
}
llassert (uentry_isFunction (spec));
}
- DPRINTF (("Merge entries: %s / %s",
- uentry_unparseFull (spec),
+ DPRINTF (("Merge entries: %s / %s", uentry_unparseFull (spec),
uentry_unparseFull (def)));
uentry_mergeConstraints (spec, def);
decl divzero enum enumtag exports external fields flags forbody format freearray \
funcpointer functionmacro glob globals impabstract info init inparam internal iter keep libs \
linked lintcomments list longint loopexec looptesteffect \
- macros macrosef merge mergenull modifies modtest moduncon \
+ macros macrosef malloc merge mergenull modifies modtest moduncon \
mongoincludes mystrncat noeffect null nullret nullassign numabstract observer oldstyle outglob outparam \
parentype postnotnull preds prefixes printflike rc refcounts release repexpose \
returned russian sharing shifts sizesigns slovaknames \
-$(SPLINTR) +hints -controlnestdepth 2 controldepth.c -expect 2
-$(SPLINTR) +hints -controlnestdepth 1 controldepth.c -expect 2
+###
+### 1 extra warning reported for +strict now because of out-of-bounds read
+###
+
.PHONY: compdestroy
compdestroy:
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader -expect 1
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader +strictdestroy -expect 2
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader +strictdestroy +strictusereleased -expect 3
- -$(SPLINTRN) compdestroy.c +strict +partial -exportheader -expect 3
+ -$(SPLINTRN) compdestroy.c +strict +partial -exportheader -expect 4
.PHONY: compoundliterals
compoundliterals:
.PHONY: decl
decl:
-$(SPLINTR) decl.c -expect 2
- -$(SPLINTRN) decl.c +strict -exportlocal -expect 5
+ -$(SPLINTRN) decl.c +strict -exportlocal -expect 6
-$(SPLINTR) decl2 -expect 4
.PHONY: divzero
-$(SPLINTR) macrosef.c +allmacros -expect 3
-$(SPLINTR) macrosef.c +allmacros +sefuncon -expect 4
+.PHONY: malloc
+malloc:
+ -$(SPLINTRN) malloc.c +bounds -exportlocal -expect 7
+
.PHONY: merge
merge:
-$(SPLINTRN) merge.c +checks -exportlocal -exportheadervar -exportheader -expect 3
.PHONY: moduncon
moduncon:
-$(SPLINTR) moduncon.c +moduncon -memchecks -expect 4
- -$(SPLINTRN) moduncon.c +strict -exportlocal -expect 22
+ -$(SPLINTRN) moduncon.c +strict +impboundsconstraints -exportlocal -expect 22
.PHONY: mongoincludes
mongoincludes:
preds:
-$(SPLINTR) +hints preds.c -expect 6
-$(SPLINTRN) +hints preds.c -weak -expect 1
- -$(SPLINTRN) +hints preds.c -strict -exportlocal -exportheader -expect 10
+ -$(SPLINTRN) +hints preds.c -strict +impboundsconstraints -exportlocal -exportheader -expect 10
.PHONY: prefixes
prefixes:
./longconstants.c \
./macros.c \
./macrosef.c \
+ ./malloc.c \
./merge.c \
./modclient.c \
./modifies.c \
decl divzero enum enumtag exports external fields flags forbody format freearray \
funcpointer functionmacro glob globals impabstract info init inparam internal iter keep libs \
linked lintcomments list longint loopexec looptesteffect \
- macros macrosef merge mergenull modifies modtest moduncon \
+ macros macrosef malloc merge mergenull modifies modtest moduncon \
mongoincludes mystrncat noeffect null nullret nullassign numabstract observer oldstyle outglob outparam \
parentype postnotnull preds prefixes printflike rc refcounts release repexpose \
returned russian sharing shifts sizesigns slovaknames \
./longconstants.c \
./macros.c \
./macrosef.c \
+ ./malloc.c \
./merge.c \
./modclient.c \
./modifies.c \
-$(SPLINTR) +hints -controlnestdepth 2 controldepth.c -expect 2
-$(SPLINTR) +hints -controlnestdepth 1 controldepth.c -expect 2
+###
+### 1 extra warning reported for +strict now because of out-of-bounds read
+###
+
.PHONY: compdestroy
compdestroy:
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader -expect 1
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader +strictdestroy -expect 2
-$(SPLINTRN) compdestroy.c +checks -exportlocal -exportheader +strictdestroy +strictusereleased -expect 3
- -$(SPLINTRN) compdestroy.c +strict +partial -exportheader -expect 3
+ -$(SPLINTRN) compdestroy.c +strict +partial -exportheader -expect 4
.PHONY: compoundliterals
compoundliterals:
.PHONY: decl
decl:
-$(SPLINTR) decl.c -expect 2
- -$(SPLINTRN) decl.c +strict -exportlocal -expect 5
+ -$(SPLINTRN) decl.c +strict -exportlocal -expect 6
-$(SPLINTR) decl2 -expect 4
.PHONY: divzero
-$(SPLINTR) macrosef.c +allmacros -expect 3
-$(SPLINTR) macrosef.c +allmacros +sefuncon -expect 4
+.PHONY: malloc
+malloc:
+ -$(SPLINTRN) malloc.c +bounds -exportlocal -expect 7
+
.PHONY: merge
merge:
-$(SPLINTRN) merge.c +checks -exportlocal -exportheadervar -exportheader -expect 3
.PHONY: moduncon
moduncon:
-$(SPLINTR) moduncon.c +moduncon -memchecks -expect 4
- -$(SPLINTRN) moduncon.c +strict -exportlocal -expect 22
+ -$(SPLINTRN) moduncon.c +strict +impboundsconstraints -exportlocal -expect 22
.PHONY: mongoincludes
mongoincludes:
preds:
-$(SPLINTR) +hints preds.c -expect 6
-$(SPLINTRN) +hints preds.c -weak -expect 1
- -$(SPLINTRN) +hints preds.c -strict -exportlocal -exportheader -expect 10
+ -$(SPLINTRN) +hints preds.c -strict +impboundsconstraints -exportlocal -exportheader -expect 10
.PHONY: prefixes
prefixes:
compdestroy.c:15:13: Storage x->ips[] possibly released
compdestroy.c:19:9: Only storage x->ips[] (type oip) derived from released
storage may not have been released: x->ips
+compdestroy.c:15:13: Possible out-of-bounds read: x->ips[i]
+ Unable to resolve constraint:
+ requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
+ needed to satisfy precondition:
+ requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
compdestroy.c: (in function sip_free2)
compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
storage is not released (memory leak): x->ips
-Finished checking --- 3 code warnings, as expected
+Finished checking --- 4 code warnings, as expected
constannot.c: (in function foo2)
-constannot.c:11:3: Possible out-of-bounds store:
- str[20]
+constannot.c:11:3: Possible out-of-bounds store: str[20]
Unable to resolve constraint:
requires maxSet(str @ constannot.c:11:3) >= 20
needed to satisfy precondition:
requires maxSet(str @ constannot.c:11:3) >= 20
constannot.c: (in function foo3)
-constannot.c:20:3: Likely out-of-bounds store:
- foo(buf)
+constannot.c:20:3: Likely out-of-bounds store: foo(buf)
Unable to resolve constraint:
requires <const int=20> <= 19
needed to satisfy precondition:
decl.c: (in function main)
decl.c:7:3: Call to non-function (type [function (int) returns int] **): x
decl.c:8:2: Path with no return in function declared to return int
+decl.c: (in function foo1)
+decl.c:13:3: Likely out-of-bounds store: buf[10]
+ Unable to resolve constraint:
+ requires 9 >= 10
+ needed to satisfy precondition:
+ requires maxSet(buf @ decl.c:13:3) >= 10
decl.c:1:5: Function test declared but not defined
decl.c:1:5: Function test exported but not declared in header file
-Finished checking --- 5 code warnings, as expected
+Finished checking --- 6 code warnings, as expected
decl2.c:3:6: Variable glob2 defined with inconsistent type (arrays and pointers
are not identical in variable declarations): int *
for.c: (in function f)
-for.c:13:5: Possible out-of-bounds store:
- t[i]
+for.c:13:5: Possible out-of-bounds store: t[i]
Unable to resolve constraint:
requires i @ for.c:13:7 <= 10
needed to satisfy precondition:
--- /dev/null
+void f1 ()
+{
+ int *ip = (int *) malloc (89); /* not divisible */
+ if (ip != NULL) {
+ ip[88]=23; /* out of range */
+ free (ip);
+ }
+}
+
+void f2 ()
+{
+ int *ip = (int *) malloc (88); /* divisible okay */
+ if (ip != NULL) {
+ ip[21]=23; /* okay */
+ ip[22]=23; /* bad */
+ free (ip);
+ }
+}
+
+void f3 ()
+{
+ int *ip = (int *) malloc (87 * sizeof (int));
+ if (ip != NULL) {
+ ip[21]=23; /* okay */
+ ip[86]=23; /* okay */
+ ip[87]=23; /* bad */
+ free (ip);
+ }
+}
+
+void f4 ()
+{
+ int *ip = (int *) malloc (87 * sizeof (short)); /* not divisible */
+ if (ip != NULL) {
+ ip[86]=23; /* bad */
+ free (ip);
+ }
+}
--- /dev/null
+
+malloc.c: (in function f1)
+malloc.c:3:21: Allocated memory is converted to type int * of (size 32), which
+ is not divisible into original allocation of space for 89 elements of type
+ void * (size 8)
+malloc.c:5:5: Likely out-of-bounds store: ip[88]
+ Unable to resolve constraint:
+ requires 21 >= 88
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:5:5) >= 88
+malloc.c: (in function f2)
+malloc.c:15:5: Likely out-of-bounds store: ip[22]
+ Unable to resolve constraint:
+ requires 21 >= 22
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:15:5) >= 22
+malloc.c: (in function f3)
+malloc.c:26:5: Likely out-of-bounds store: ip[87]
+ Unable to resolve constraint:
+ requires 86 >= 87
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:26:5) >= 87
+malloc.c: (in function f4)
+malloc.c:33:21: Allocated memory is used as a different type (int) from the
+ sizeof type (short int)
+malloc.c:33:21: Allocated memory is converted to type int * of (size 32), which
+ is not divisible into original allocation of space for 87 elements of type
+ short int (size 8)
+malloc.c:35:5: Likely out-of-bounds store: ip[86]
+ Unable to resolve constraint:
+ requires 20 >= 86
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:35:5) >= 86
+
+Finished checking --- 7 code warnings, as expected
Finished checking --- 1 code warning, as expected
-setChar.c:5: Likely out-of-bounds store:
- buf[10]
+setChar.c:5: Likely out-of-bounds store: buf[10]
Unable to resolve constraint:
requires 9 >= 10
needed to satisfy precondition:
Finished checking --- 1 code warning, as expected
-multiError.c:4: Possible out-of-bounds store:
- buf[2]
+multiError.c:4: Possible out-of-bounds store: buf[2]
Unable to resolve constraint:
requires maxSet(buf @ multiError.c:4) >= 2
needed to satisfy precondition:
Finished checking --- no warnings
maxsetnoannotations.c: (in function noancopy)
-maxsetnoannotations.c:2:3: Possible out-of-bounds store:
- strcpy(a, b)
+maxsetnoannotations.c:2:3: Possible out-of-bounds store: strcpy(a, b)
Unable to resolve constraint:
requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @
maxsetnoannotations.c:2:13)
unrecogCall.c:8:3: Unrecognized identifier: bar
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
-initialization.c:5:14: Possible out-of-bounds read:
- e[22]
+initialization.c:5:14: Possible out-of-bounds read: e[22]
Unable to resolve constraint:
requires maxRead(d @ initialization.c:3:14) >= 22
needed to satisfy precondition:
requires maxRead(e @ initialization.c:5:14) >= 22
-initialization.c:8:3: Possible out-of-bounds store:
- f[2]
+initialization.c:8:3: Possible out-of-bounds store: f[2]
Unable to resolve constraint:
requires maxSet(d @ initialization.c:3:14) >= 2
needed to satisfy precondition:
requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
-simplifyTest.c:3:3: Possible out-of-bounds store:
- s[i]
+simplifyTest.c:3:3: Possible out-of-bounds store: s[i]
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
needed to satisfy precondition:
requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5
simplifyTest.c: (in function fooAdd)
-simplifyTest.c:10:3: Possible out-of-bounds store:
- s[i + 2]
+simplifyTest.c:10:3: Possible out-of-bounds store: s[i + 2]
Unable to resolve constraint:
requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2
needed to satisfy precondition:
unknownsize.c: (in function uknSize1)
-unknownsize.c:9:3: Possible out-of-bounds store:
- c[9]
+unknownsize.c:9:3: Possible out-of-bounds store: c[9]
Unable to resolve constraint:
requires maxSet(c @ unknownsize.c:9:3) >= 9
needed to satisfy precondition:
Finished checking --- 1 code warning, as expected
fixedArrayType.c: (in function fixedArrayTouch)
-fixedArrayType.c:9:3: Possible out-of-bounds store:
- buffer[sizeof(Array) - 1]
+fixedArrayType.c:9:3: Possible out-of-bounds store: buffer[sizeof(Array) - 1]
Unable to resolve constraint:
requires sizeof(Array) @ fixedArrayType.c:9:25 <= 10
needed to satisfy precondition:
m.c:9:1: Index of possibly null pointer f: f
m.c:8:5: Storage f may become null
sizeof.c: (in function f)
-sizeof.c:17:1: Likely out-of-bounds store:
- x[(sizeof(x))]
+sizeof.c:17:1: Likely out-of-bounds store: x[(sizeof(x))]
Unable to resolve constraint:
requires 2 >= 3
needed to satisfy precondition:
test3.c:2:6: Function t defined more than once
m.c:11:1: Previous definition of t
test3.c: (in function t)
-test3.c:9:3: Likely out-of-bounds store:
- g[101]
+test3.c:9:3: Likely out-of-bounds store: g[101]
Unable to resolve constraint:
requires 99 >= 101
needed to satisfy precondition:
test7.c:2:6: Function t defined more than once
m.c:11:1: Previous definition of t
test7.c: (in function t)
-test7.c:6:3: Possible out-of-bounds store:
- g[2]
+test7.c:6:3: Possible out-of-bounds store: g[2]
Unable to resolve constraint:
requires maxSet(g @ test7.c:4:3) >= 4
needed to satisfy precondition:
requires maxSet(g @ test7.c:6:3) >= 2
-test7.c:8:3: Possible out-of-bounds store:
- j[0]
+test7.c:8:3: Possible out-of-bounds store: j[0]
Unable to resolve constraint:
requires maxSet(j @ test7.c:8:3) >= 0
needed to satisfy precondition:
sizeof.c: (in function main)
-sizeof.c:6:2: Likely out-of-bounds store:
- x[(sizeof(x))]
+sizeof.c:6:2: Likely out-of-bounds store: x[(sizeof(x))]
Unable to resolve constraint:
requires 2 >= 3
needed to satisfy precondition:
andersk / splint.git / commitdiff
