From: drl7x Date: Sat, 12 Apr 2003 04:12:21 +0000 (+0000) Subject: Fixed /*@i@*/ warning in splintme X-Git-Tag: splint-3_1_0~18 X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/b2a40ced6227156a72f33e0fd47452e10309bc8b Fixed /*@i@*/ warning in splintme --- diff --git a/src/clabstract.c b/src/clabstract.c index 1131f59..f1da5b0 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -2228,7 +2228,9 @@ sRef checkbufferConstraintClausesId (uentry ue) { llfatalerrorLoc (cstring_makeLiteral("Macro defined constants can not be used in function constraints unless they are specifed with the constant annotation. To use a macro defined constant include an annotation of the form /*@constant =@*/ somewhere before the function constraint. This restriction may be removed in future releases if it is determined to be excessively burdensome." )); } - return sRef_saveCopy (sr); /*@i523 why the saveCopy? */ + + /*@ savedCopy to used to mitigate danger of accessing freed memory*/ + return sRef_saveCopy (sr); } void checkModifiesId (uentry ue) @@ -2362,20 +2364,22 @@ sRef fixStateClausesId (cstring s) } else { - /*@i222@*/ - /*drl handle structure invariant */ - /*@i222@*/ + /* drl This is the code for structure invariants + + It is no yet stable enough to be included in a Splint release. + */ + /*check that we're in a structure */ -# if 0 +#if 0 /*@unused@*/ uentryList ueL; /*@unused@*/ uentry ue2; /*@unused@*/ ctype ct; -# endif +#endif fileloc loc = fileloc_decColumn (g_currentloc, size_toInt (cstring_length (s))); ret = sRef_undefined; # if 0 - /*drl commenting this out for now + ct = context_getLastStruct ( ct ); llassert( ctype_isStruct(ct) ); @@ -2394,8 +2398,8 @@ sRef fixStateClausesId (cstring s) return ret; } - */ -# endif + +#endif voptgenerror (FLG_UNRECOG, diff --git a/src/constraint.c b/src/constraint.c index 0d39b6e..3706574 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -123,7 +123,6 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c) ret->generatingExpr = c->generatingExpr; /*@=assignexpose@*/ - /*@i33 fix this*/ if (c->orig != NULL) ret->orig = constraint_copy (c->orig); else @@ -139,7 +138,7 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c) return ret; } -/*like copy expect it doesn't allocate memory for the constraint*/ +/*like copy except it doesn't allocate memory for the constraint*/ void constraint_overWrite (constraint c1, constraint c2) { @@ -166,7 +165,6 @@ void constraint_overWrite (constraint c1, constraint c2) else c1->orig = NULL; - /*@i33 make sure that the or is freed correctly*/ if (c1->or != NULL) constraint_free (c1->or); @@ -327,7 +325,6 @@ constraint constraint_makeSRefSetBufferSize (sRef s, long int size) ret->ar = EQ; ret->expr = constraintExpr_makeIntLiteral ((int)size); ret->post = TRUE; - /*@i1*/ return ret; } @@ -340,7 +337,6 @@ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind) ret->ar = GTE; ret->expr = constraintExpr_makeIntLiteral (ind); ret->post = TRUE; - /*@i1*/ return ret; } diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 8c0fe3a..3dfcf90 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -2331,7 +2331,6 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist) I'm a bit nervous about modifying the exprNode but this is the easy way to do this If I have time I'd like to cause the exprNode to get created correctly in the first place */ -/*@i223*/ void exprNode_findValue(exprNode e) { exprData data; diff --git a/src/cppexp.c b/src/cppexp.c index 3c97c98..8182205 100644 --- a/src/cppexp.c +++ b/src/cppexp.c @@ -276,11 +276,6 @@ cppReader_parseNumber (cppReader *pfile, char *start, int olen) /*@requires maxR } else if (*p == '0') { - /*@i3434*/ - /* drl: see if there is a reason that we shouldn't do - p++; - len--; */ - base = 8; } else diff --git a/src/exprNode.c b/src/exprNode.c index 41b0a6d..403dbab 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -4416,10 +4416,6 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) exprNode_checkModify (e, ret); /* added 7/11/2000 D.L */ - /*@i223*/ - /*DRL 6/8/01 I decided to disable all Splint warnings here since the code - probably needs a rewrite any way */ - /* updateEnvironmentForPostOp (e); */ diff --git a/src/idDecl.c b/src/idDecl.c index 24ebb75..4c0429c 100644 --- a/src/idDecl.c +++ b/src/idDecl.c @@ -247,8 +247,10 @@ void idDecl_addClauses (idDecl d, functionClauseList clauses) { llassert (idDecl_isDefined (d)); - /*@i222*/ + /* + DRL comment out llassert: + This breaks on sometypes of functionPointers. I.e. void (*signal (int sig ) @requires g >= 0 @ ) (int) @requires g >= 0 @ ; diff --git a/src/sRef.c b/src/sRef.c index 3aaf720..1dae1a9 100644 --- a/src/sRef.c +++ b/src/sRef.c @@ -2256,7 +2256,6 @@ sRef_closeEnough (sRef s1, sRef s2) { case SK_RESULT: { - /* s = sRef_saveCopy(s); */ /*@i523@*/ ce = constraintExpr_makeTermsRef (s); return ce; } @@ -2273,7 +2272,6 @@ sRef_closeEnough (sRef s1, sRef s2) { sRef temp; temp = (sRef_makePointer (sRef_fixBaseParam (s->info->ref, args))); - /* temp = sRef_saveCopy(temp); */ /*@i523@*/ ce = constraintExpr_makeTermsRef (temp); return ce; } @@ -3360,7 +3358,7 @@ static bool sRef_isZerothArrayFetch (/*@notnull@*/ sRef s) s->kind = SK_ADR; s->type = ctype_makePointer (t->type); s->info = (sinfo) dmalloc (sizeof (*s->info)); - s->info->ref = t; /* sRef_copy (t); */ /*@i32@*/ + s->info->ref = t; if (t->defstate == SS_UNDEFINED) /* no! it is allocated even still: && !ctype_isPointer (t->type)) */ diff --git a/src/uentry.c b/src/uentry.c index 0f5fb17..5077faf 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -6693,7 +6693,6 @@ uvinfo_copy (uvinfo u) ret->defstate = u->defstate; ret->checked = u->checked; - /*@i523 ret->origsref = sRef_copy (u->origsref); */ /* drl added 07-02-001 */ /* copy null terminated information */