Fixed /*@i@*/ warning in splintme

diff --git a/src/clabstract.c b/src/clabstract.c
index 1131f590095f1c4545310cedbe8a8d91dead79d3..f1da5b09c50a700a9c8ce56d94c88785342d2a1f 100644 (file)
--- 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 <type> <name>=<value>@*/ 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\r
+#if 0
                  /*@unused@*/    uentryList ueL;
          /*@unused@*/ uentry ue2;
          /*@unused@*/ ctype ct;\r
-# 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;
            }
-         */\r
-# endif\r
+         
+#endif
 
          voptgenerror 
            (FLG_UNRECOG, 

diff --git a/src/constraint.c b/src/constraint.c
index 0d39b6eb4d8bd468a0de07a2ccbc36b5dd00a27a..3706574599ec1cf2e2881a2934b392d19973cd73 100644 (file)
--- 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 8c0fe3a2ef1c155f888f0e4a1f57c5962ec4afa4..3dfcf9070af8094c2da037cc87b546a28974c1d7 100644 (file)
--- 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 3c97c988fcb878dc9fa7090396a307e8568f8087..8182205af963c9a4898e8c5daa4c6c8456d15e29 100644 (file)
--- 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 41b0a6d1a829f272f70cbe6a2d5e3cbeaffd580f..403dbabab809c52e87b9cdaada8190b68f0be9a4 100644 (file)
--- 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 24ebb7531062bccb5f323d36435beacebd527fa2..4c0429c0dca2aacda4d7b86b934107b69646adb2 100644 (file)
--- 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 3aaf720bdbbc0a918e50ddb4b0e3416677e2384d..1dae1a94c1c6a29064b1a5ffbc58631846ead140 100644 (file)
--- 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 0f5fb176072ea0bbd1fbed114be3fa566f7d70bb..5077fafffef556e57b068e350687ed3271ee46fc 100644 (file)
--- 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 */