From 6317f163d6dd13ef058d98c91a6f9eb29a9f87f4 Mon Sep 17 00:00:00 2001 From: evans1629 Date: Tue, 10 Jun 2003 05:58:24 +0000 Subject: [PATCH] Made allocations involving sizeof work correctly (test/malloc.c). Fixed implicit constraints for functions. --- src/Headers/clabstract.h | 4 +- src/Headers/constraint.h | 2 +- src/Headers/constraintExprData.h | 17 +-- src/Headers/constraintList.h | 3 - src/Headers/context.h | 6 +- src/Headers/functionClauseList.h | 2 +- src/Makefile.am | 3 + src/Makefile.in | 3 + src/cgrammar.c.der | 10 +- src/cgrammar.y | 10 +- src/clabstract.c | 4 +- src/constraint.c | 192 ++++++++++++------------ src/constraintExpr.c | 104 +++++++------ src/constraintExprData.c | 4 +- src/constraintGeneration.c | 9 +- src/constraintList.c | 33 ---- src/constraintResolve.c | 66 ++++---- src/context.c | 131 ++++------------ src/ctbase.i | 2 +- src/ctype.c | 3 +- src/exprChecks.c | 52 ++++--- src/exprNode.c | 3 - src/flags.def | 2 +- src/functionClauseList.c | 9 +- src/uentry.c | 3 +- test/Makefile.am | 19 ++- test/Makefile.in | 19 ++- test/compdestroy.expect | 7 +- test/constannot.expect | 6 +- test/decl.expect | 8 +- test/for.expect | 3 +- test/malloc.c | 38 +++++ test/malloc.expect | 35 +++++ test/manual.expect | 6 +- test/maxset.expect | 3 +- test/moreBufferTests.expect | 12 +- test/moreBufferTests2.expect | 6 +- test/simplebufferConstraintTests.expect | 12 +- test/sizeoftest.expect | 3 +- 39 files changed, 425 insertions(+), 429 deletions(-) create mode 100644 test/malloc.c create mode 100644 test/malloc.expect diff --git a/src/Headers/clabstract.h b/src/Headers/clabstract.h index 169f7d1..afa1455 100644 --- a/src/Headers/clabstract.h +++ b/src/Headers/clabstract.h @@ -101,9 +101,9 @@ extern void declareStaticFunction (/*@only@*/ idDecl p_tid) */ extern sRef checkbufferConstraintClausesId (uentry p_ue); -extern void setImplictfcnConstraints (void); +extern void setImplicitfcnConstraints (void); -/*@observer@*/ constraintList getImplicitFcnConstraints (void); +/*@observer@*/ constraintList getImplicitFcnConstraints (void); /* end drl*/ diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 8c82f9d..57676f4 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -4,7 +4,7 @@ typedef enum { - LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE, CASTEQ + LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE, } arithType; diff --git a/src/Headers/constraintExprData.h b/src/Headers/constraintExprData.h index c034882..e4a4bec 100644 --- a/src/Headers/constraintExprData.h +++ b/src/Headers/constraintExprData.h @@ -1,8 +1,6 @@ #ifndef __constraintExprData_h__ - #define __constraintExprData_h__ - typedef enum { BINARYOP_UNDEFINED, @@ -18,7 +16,6 @@ typedef enum } constraintExprUnaryOpKind; - typedef struct constraintExprBinaryOp_ { constraintExpr expr1; @@ -26,14 +23,12 @@ typedef struct constraintExprBinaryOp_ constraintExpr expr2; } constraintExprBinaryOp; - typedef struct constraintExprUnaryOp_ { constraintExpr expr; constraintExprUnaryOpKind unaryOp; } constraintExprUnaryOp; - typedef union constraintExprData { constraintExprBinaryOp binaryOp; @@ -50,13 +45,17 @@ extern void constraintExprData_freeTerm (/*@only@*/ constraintExprData) ; 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); diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index c9f455c..5c826c9 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -86,9 +86,6 @@ extern void constraintList_printError (constraintList p_s, /*@observer@*/ filelo 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); diff --git a/src/Headers/context.h b/src/Headers/context.h index 4d5929e..c8ba6c3 100644 --- a/src/Headers/context.h +++ b/src/Headers/context.h @@ -58,6 +58,8 @@ extern /*@observer@*/ cstring context_getTrueName (void) /*@*/ ; 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); @@ -340,13 +342,9 @@ extern valueTable context_createGlobalMarkerValueTable (/*@only@*/ stateInfo p_i 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*/ diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h index 24ff040..8860385 100644 --- a/src/Headers/functionClauseList.h +++ b/src/Headers/functionClauseList.h @@ -49,7 +49,7 @@ extern /*@unused@*/ /*@only@*/ cstring functionClauseList_unparse (functionClaus 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 diff --git a/src/Makefile.am b/src/Makefile.am index 635811c..86f467f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -399,6 +399,9 @@ lintnew: splintme 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 diff --git a/src/Makefile.in b/src/Makefile.in index be75a1a..dffda81 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -1127,6 +1127,9 @@ lintnew: splintme 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 diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der index 500eb7b..bd5ac4a 100644 --- a/src/cgrammar.c.der +++ b/src/cgrammar.c.der @@ -3582,14 +3582,14 @@ case 26: 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); @@ -3609,7 +3609,7 @@ case 27: case 28: { functionClauseList fcl; - setImplictfcnConstraints (); + setImplicitfcnConstraints (); clearCurrentParams (); yyval.ntyp = idDecl_replaceCtype (yyvsp[-6].ntyp, ctype_makeFunction (idDecl_getCtype (yyvsp[-6].ntyp), yyvsp[-3].entrylist)); @@ -3618,7 +3618,7 @@ case 28: ) )) ; - fcl = functionClauseList_setImplictConstraints(yyvsp[0].funcclauselist); + fcl = functionClauseList_setImplicitConstraints(yyvsp[0].funcclauselist); idDecl_addClauses (yyval.ntyp, fcl); @@ -4775,7 +4775,7 @@ case 405: { 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 (); ; diff --git a/src/cgrammar.y b/src/cgrammar.y index e91de36..c9937b3 100644 --- a/src/cgrammar.y +++ b/src/cgrammar.y @@ -409,14 +409,14 @@ namedDeclBase $$ = 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); @@ -434,7 +434,7 @@ namedDeclBase functionClauses { functionClauseList fcl; - setImplictfcnConstraints (); + setImplicitfcnConstraints (); clearCurrentParams (); $$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4)); @@ -443,7 +443,7 @@ namedDeclBase ) )) ; - fcl = functionClauseList_setImplictConstraints($7); + fcl = functionClauseList_setImplicitConstraints($7); idDecl_addClauses ($$, fcl); @@ -1472,7 +1472,7 @@ suSpc 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 (); } diff --git a/src/clabstract.c b/src/clabstract.c index 6538a6d..3bf4168 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -505,7 +505,7 @@ The current semantics are generated constraints of the form MaxSet(p) >= 0 and M 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; @@ -521,7 +521,7 @@ void setImplictfcnConstraints (void) uentryList_elements (params, el) { - DPRINTF (("setImplictfcnConstraints doing: %s", uentry_unparse(el))); + DPRINTF (("setImplicitfcnConstraints doing: %s", uentry_unparse(el))); if (uentry_isVariable (el)) { diff --git a/src/constraint.c b/src/constraint.c index 674dee5..ac18923 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -110,32 +110,35 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r 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*/ @@ -203,8 +206,10 @@ static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void) constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e) { - - llassert (constraint_isDefined (c) ); + if (!constraint_isDefined (c)) + { + return c; + } if (c->generatingExpr == NULL) { @@ -391,14 +396,20 @@ static constraint 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 @@ -423,16 +434,7 @@ constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode 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 */ @@ -555,25 +557,22 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq 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) /*@*/ @@ -596,9 +595,6 @@ cstring arithType_print (arithType ar) /*@*/ case EQ: st = cstring_makeLiteral ("=="); break; - case CASTEQ: - st = cstring_makeLiteral ("(!)=="); - break; case NONNEGATIVE: st = cstring_makeLiteral ("NONNEGATIVE"); break; @@ -815,7 +811,7 @@ cstring constraint_unparseDetailed (constraint c) cstring genExpr; bool isLikely; - llassert (constraint_isDefined (c) ); + llassert (constraint_isDefined (c)); if (!c->post) { @@ -826,17 +822,17 @@ cstring constraint_unparseDetailed (constraint c) 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 @@ -844,11 +840,11 @@ cstring constraint_unparseDetailed (constraint c) 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: "); } } @@ -996,41 +992,43 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp 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; } diff --git a/src/constraintExpr.c b/src/constraintExpr.c index 74a97ee..e0ff371 100644 --- a/src/constraintExpr.c +++ b/src/constraintExpr.c @@ -60,7 +60,7 @@ static ctype constraintExpr_getCType (constraintExpr p_e); 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 @ */ ; @@ -438,7 +438,10 @@ constraintExpr constraintExpr_makeExprNode (exprNode e) exprNode t, t1, t2; lltok tok; - llassert (e != NULL); + if (exprNode_isUndefined (e)) + { + return constraintExpr_undefined; + } data = e->edata; @@ -555,7 +558,7 @@ constraintExpr constraintExpr_makeExprNode (exprNode e) ret = constraintExpr_makeExprNode (t); break; case XPR_COMMA: - t = exprData_getPairA(data); + t = exprData_getPairA (data); ret = constraintExpr_makeExprNode(t); break; default: @@ -2484,6 +2487,7 @@ static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e float fnewval; long newval; + llassert (e != NULL); llassert (e->kind == term); ct = constraintExprData_termGetTerm (e->data); llassert (constraintTerm_canGetValue (ct)); @@ -2491,18 +2495,19 @@ static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e 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); } @@ -2544,71 +2549,80 @@ static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode (/*@only@* 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 */ } - } } diff --git a/src/constraintExprData.c b/src/constraintExprData.c index ec5427b..1ce4e37 100644 --- a/src/constraintExprData.c +++ b/src/constraintExprData.c @@ -149,9 +149,7 @@ constraintExprData_termSetTerm (/*@returned@*/ constraintExprData data, return data; } - - -/*@observer@*/ constraintTerm +/*@exposed@*/ constraintTerm constraintExprData_termGetTerm (/*@observer@*/ constraintExprData data) { llassert (constraintExprData_isDefined (data)); diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index aa8657e..3a94efd 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -53,7 +53,7 @@ static constraintList exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprN 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) { @@ -155,7 +155,6 @@ static void exprNode_stmt (/*@temp@*/ exprNode e) { exprNode snode; fileloc loc; - //! cstring s; DPRINTF (("Generating constraint for: %s", exprNode_unparse (e))); @@ -1337,7 +1336,7 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints, - checkCall (fcn, exprData_getArgs (data) )); + checkCall (fcn, exprData_getArgs (data))); fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints, @@ -2260,14 +2259,14 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) 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) ) diff --git a/src/constraintList.c b/src/constraintList.c index c834ec6..ea27121 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -635,39 +635,6 @@ void constraintList_dump (/*@observer@*/ constraintList c, FILE *f) 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) ) diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 4896a3a..10aa3c9 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -632,9 +632,10 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai 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)) { @@ -740,8 +741,15 @@ constraintList constraintList_fixConflicts (constraintList list1, constraintList 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; @@ -995,7 +1003,6 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) { switch (c->ar) { - case CASTEQ: case EQ: case GTE: case LTE: @@ -1388,41 +1395,34 @@ static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, co /*@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; } diff --git a/src/context.c b/src/context.c index 60d5125..ad99f13 100644 --- a/src/context.c +++ b/src/context.c @@ -4913,111 +4913,46 @@ valueTable context_createGlobalMarkerValueTable (stateInfo info) } } - -/*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@*/ - - - diff --git a/src/ctbase.i b/src/ctbase.i index de8346e..c59eb76 100644 --- a/src/ctbase.i +++ b/src/ctbase.i @@ -2664,7 +2664,7 @@ int ctbase_getSize (ctbase ct) return ctype_getSize (ct->contents.base); } } - case CT_FIXEDARRAY: //! + case CT_FIXEDARRAY: case CT_ARRAY: case CT_FCN: case CT_STRUCT: diff --git a/src/ctype.c b/src/ctype.c index d3af606..8253a71 100644 --- a/src/ctype.c +++ b/src/ctype.c @@ -460,7 +460,8 @@ ctype_baseArrayPtr (ctype c) 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; diff --git a/src/exprChecks.c b/src/exprChecks.c index db425a7..219387b 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -942,11 +942,12 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) { 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 @@ -955,21 +956,18 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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! */ @@ -978,8 +976,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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); @@ -1023,14 +1020,21 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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")); } } @@ -1093,7 +1097,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) ); */ - if (constraintList_isDefined(c) ) + if (constraintList_isDefined (c)) constraintList_free(c); context_exitInnerPlain(); diff --git a/src/exprNode.c b/src/exprNode.c index 15eb9c3..62b44f8 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -5012,9 +5012,6 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) 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); diff --git a/src/flags.def b/src/flags.def index 248f91f..fbce747 100644 --- a/src/flags.def +++ b/src/flags.def @@ -1981,7 +1981,7 @@ static flaglist flags = { FK_BOUNDS, FK_MEMORY, plainFlag, "impboundsconstraints", - FLG_IMPLICTCONSTRAINT, + FLG_IMPBOUNDSCONSTRAINTS, "generate implicit constraints for functions", NULL, 0, 0 diff --git a/src/functionClauseList.c b/src/functionClauseList.c index a78acf3..cb1a432 100644 --- a/src/functionClauseList.c +++ b/src/functionClauseList.c @@ -173,17 +173,16 @@ functionClauseList_free (functionClauseList s) } 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) ) @@ -203,14 +202,14 @@ functionClauseList_setImplictConstraints (/*@returned@*/ functionClauseList s) { 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)))); } diff --git a/src/uentry.c b/src/uentry.c index a35ff69..1d9243f 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -9489,8 +9489,7 @@ uentry_mergeEntries (uentry spec, /*@only@*/ uentry def) 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); diff --git a/test/Makefile.am b/test/Makefile.am index 07acfc9..5c25a8c 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -46,7 +46,7 @@ UNITTESTS = \ 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 \ @@ -300,12 +300,16 @@ controldepth: -$(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: @@ -368,7 +372,7 @@ deadparam: .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 @@ -555,6 +559,10 @@ macrosef: -$(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 @@ -576,7 +584,7 @@ modtest: .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: @@ -675,7 +683,7 @@ parentype: 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: @@ -1136,6 +1144,7 @@ EXTRA_DIST = ./abst_t.lcl \ ./longconstants.c \ ./macros.c \ ./macrosef.c \ + ./malloc.c \ ./merge.c \ ./modclient.c \ ./modifies.c \ diff --git a/test/Makefile.in b/test/Makefile.in index ab267a7..f06bd53 100644 --- a/test/Makefile.in +++ b/test/Makefile.in @@ -134,7 +134,7 @@ UNITTESTS = \ 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 \ @@ -356,6 +356,7 @@ EXTRA_DIST = ./abst_t.lcl \ ./longconstants.c \ ./macros.c \ ./macrosef.c \ + ./malloc.c \ ./merge.c \ ./modclient.c \ ./modifies.c \ @@ -1106,12 +1107,16 @@ controldepth: -$(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: @@ -1174,7 +1179,7 @@ deadparam: .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 @@ -1359,6 +1364,10 @@ macrosef: -$(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 @@ -1380,7 +1389,7 @@ modtest: .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: @@ -1478,7 +1487,7 @@ parentype: 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: diff --git a/test/compdestroy.expect b/test/compdestroy.expect index 9e05b62..6f34476 100644 --- a/test/compdestroy.expect +++ b/test/compdestroy.expect @@ -32,8 +32,13 @@ compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter: 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 diff --git a/test/constannot.expect b/test/constannot.expect index 467493b..c0c2071 100644 --- a/test/constannot.expect +++ b/test/constannot.expect @@ -1,14 +1,12 @@ 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 <= 19 needed to satisfy precondition: diff --git a/test/decl.expect b/test/decl.expect index cf21fbb..2dcbe24 100644 --- a/test/decl.expect +++ b/test/decl.expect @@ -9,10 +9,16 @@ decl.c:3:5: Function main declared without parameter list 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 * diff --git a/test/for.expect b/test/for.expect index e75990d..e1054c9 100644 --- a/test/for.expect +++ b/test/for.expect @@ -1,7 +1,6 @@ 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: diff --git a/test/malloc.c b/test/malloc.c new file mode 100644 index 0000000..01f1458 --- /dev/null +++ b/test/malloc.c @@ -0,0 +1,38 @@ +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); + } +} diff --git a/test/malloc.expect b/test/malloc.expect new file mode 100644 index 0000000..2bc1196 --- /dev/null +++ b/test/malloc.expect @@ -0,0 +1,35 @@ + +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 diff --git a/test/manual.expect b/test/manual.expect index e975c00..e1b3995 100644 --- a/test/manual.expect +++ b/test/manual.expect @@ -202,8 +202,7 @@ ignore.c:10: Return value (type bool) ignored: fb() 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: @@ -211,8 +210,7 @@ setChar.c:5: Likely out-of-bounds store: 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: diff --git a/test/maxset.expect b/test/maxset.expect index 6a34ab0..306c5d1 100644 --- a/test/maxset.expect +++ b/test/maxset.expect @@ -2,8 +2,7 @@ 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) diff --git a/test/moreBufferTests.expect b/test/moreBufferTests.expect index 4ac2542..64e5ccf 100644 --- a/test/moreBufferTests.expect +++ b/test/moreBufferTests.expect @@ -3,28 +3,24 @@ unrecogCall.c: (in function foo) 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: diff --git a/test/moreBufferTests2.expect b/test/moreBufferTests2.expect index 1119c82..f46f3b9 100644 --- a/test/moreBufferTests2.expect +++ b/test/moreBufferTests2.expect @@ -1,7 +1,6 @@ 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: @@ -10,8 +9,7 @@ unknownsize.c:9:3: Possible out-of-bounds store: 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: diff --git a/test/simplebufferConstraintTests.expect b/test/simplebufferConstraintTests.expect index 3db1c55..c8d41a1 100644 --- a/test/simplebufferConstraintTests.expect +++ b/test/simplebufferConstraintTests.expect @@ -3,8 +3,7 @@ m.c: (in function t) 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: @@ -12,8 +11,7 @@ sizeof.c:17:1: Likely out-of-bounds store: 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: @@ -21,14 +19,12 @@ test3.c:9:3: Likely out-of-bounds store: 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: diff --git a/test/sizeoftest.expect b/test/sizeoftest.expect index 8bbef3c..5d6a0e9 100644 --- a/test/sizeoftest.expect +++ b/test/sizeoftest.expect @@ -1,7 +1,6 @@ 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: -- 2.45.1