Fixed some /@*i@*/ comments in the code.

Also changed the version number to 3.0.1.8 to differentiate it from the version in redhat 9.

diff --git a/configure b/configure
index bbe3df9583f462fcabec4665b8cf2db329dd9b4c..cce3ae0c686ad7689ae8349d4cf2d6a7d408001f 100755 (executable)
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.

-# Generated by GNU Autoconf 2.53 for Splint 3.0.1.7.
+# Generated by GNU Autoconf 2.53 for Splint 3.0.1.8.

 #
 # Report bugs to <splint-bug@splint.org>.
 #
 #
 # Report bugs to <splint-bug@splint.org>.
 #


@@ -256,8 +256,8 @@ SHELL=${CONFIG_SHELL-/bin/sh}
 # Identity of this package.
 PACKAGE_NAME='Splint'
 PACKAGE_TARNAME='splint'
 # Identity of this package.
 PACKAGE_NAME='Splint'
 PACKAGE_TARNAME='splint'

-PACKAGE_VERSION='3.0.1.7'
-PACKAGE_STRING='Splint 3.0.1.7'
+PACKAGE_VERSION='3.0.1.8'
+PACKAGE_STRING='Splint 3.0.1.8'

 PACKAGE_BUGREPORT='splint-bug@splint.org'
 
 ac_unique_file="src/lclinit.c"
 PACKAGE_BUGREPORT='splint-bug@splint.org'
 
 ac_unique_file="src/lclinit.c"


@@ -725,7 +725,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF

-\`configure' configures Splint 3.0.1.7 to adapt to many kinds of systems.
+\`configure' configures Splint 3.0.1.8 to adapt to many kinds of systems.

 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 


@@ -792,7 +792,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in

-     short | recursive ) echo "Configuration of Splint 3.0.1.7:";;
+     short | recursive ) echo "Configuration of Splint 3.0.1.8:";;

    esac
   cat <<\_ACEOF
 
    esac
   cat <<\_ACEOF
 


@@ -882,7 +882,7 @@ fi
 test -n "$ac_init_help" && exit 0
 if $ac_init_version; then
   cat <<\_ACEOF
 test -n "$ac_init_help" && exit 0
 if $ac_init_version; then
   cat <<\_ACEOF

-Splint configure 3.0.1.7
+Splint configure 3.0.1.8

 generated by GNU Autoconf 2.53
 
 Copyright 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001, 2002
 generated by GNU Autoconf 2.53
 
 Copyright 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001, 2002


@@ -897,7 +897,7 @@ cat >&5 <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 

-It was created by Splint $as_me 3.0.1.7, which was
+It was created by Splint $as_me 3.0.1.8, which was

 generated by GNU Autoconf 2.53.  Invocation command line was
 
   $ $0 $@
 generated by GNU Autoconf 2.53.  Invocation command line was
 
   $ $0 $@


@@ -1516,7 +1516,7 @@ fi
 
 # Define the identity of the package.
  PACKAGE=splint
 
 # Define the identity of the package.
  PACKAGE=splint

- VERSION=3.0.1.7
+ VERSION=3.0.1.8

 
 
 # Some tools Automake needs.
 
 
 # Some tools Automake needs.


@@ -3580,7 +3580,7 @@ _ACEOF
 
 
 # These used to be in herald.h
 
 
 # These used to be in herald.h

-LCL_PARSE_VERSION="Splint 3.0.1.7"
+LCL_PARSE_VERSION="Splint 3.0.1.8"

 
 cat >>confdefs.h <<_ACEOF
 #define SPLINT_VERSION "$LCL_PARSE_VERSION --- `date +"%d %b %Y"`"
 
 cat >>confdefs.h <<_ACEOF
 #define SPLINT_VERSION "$LCL_PARSE_VERSION --- `date +"%d %b %Y"`"


@@ -4014,7 +4014,7 @@ _ASBOX
 } >&5
 cat >&5 <<_CSEOF
 
 } >&5
 cat >&5 <<_CSEOF
 

-This file was extended by Splint $as_me 3.0.1.7, which was
+This file was extended by Splint $as_me 3.0.1.8, which was

 generated by GNU Autoconf 2.53.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
 generated by GNU Autoconf 2.53.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES


@@ -4076,7 +4076,7 @@ _ACEOF
 
 cat >>$CONFIG_STATUS <<_ACEOF
 ac_cs_version="\\
 
 cat >>$CONFIG_STATUS <<_ACEOF
 ac_cs_version="\\

-Splint config.status 3.0.1.7
+Splint config.status 3.0.1.8

 configured by $0, generated by GNU Autoconf 2.53,
   with options \\"`echo "$ac_configure_args" | sed 's/[\\""\`\$]/\\\\&/g'`\\"
 
 configured by $0, generated by GNU Autoconf 2.53,
   with options \\"`echo "$ac_configure_args" | sed 's/[\\""\`\$]/\\\\&/g'`\\"
 

diff --git a/configure.ac b/configure.ac
index cf9dc1d1d46875695c6f8567648bce10632c080f..5c03300508896c3ed5f89f4eafee2bb799fe74f9 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -1,7 +1,7 @@
 dnl Process with autoconf to create a configure script  -*- Autoconf -*-
 AC_PREREQ(2.50)
 
 dnl Process with autoconf to create a configure script  -*- Autoconf -*-
 AC_PREREQ(2.50)
 

-AC_INIT([Splint], [3.0.1.7], [splint-bug@splint.org], [splint])
+AC_INIT([Splint], [3.0.1.8], [splint-bug@splint.org], [splint])

 
 dnl This MUST precede any other macro
 AC_CONFIG_AUX_DIR([config])
 
 dnl This MUST precede any other macro
 AC_CONFIG_AUX_DIR([config])

diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h
index 3ad571c2b252b2d1f19a899996a7fa4a475c36d4..1bebd5b2932eb130d0954068a020a92eeebda8e6 100644 (file)
--- a/src/Headers/constraintTerm.h
+++ b/src/Headers/constraintTerm.h
@@ -25,7 +25,7 @@ struct s_constraintTerm {
 
 abst_typedef struct s_constraintTerm *constraintTerm;
 
 
 abst_typedef struct s_constraintTerm *constraintTerm;
 

-/*@i311 shouldn't need this...never null */
+

 extern bool constraintTerm_isDefined (constraintTerm p_t) /*@*/ ;
 
 extern constraintTermType constraintTerm_getKind (constraintTerm) ;
 extern bool constraintTerm_isDefined (constraintTerm p_t) /*@*/ ;
 
 extern constraintTermType constraintTerm_getKind (constraintTerm) ;

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 93cb25641f1b0d3265bc8b145885776000e1f566..8c0fe3a2ef1c155f888f0e4a1f57c5962ec4afa4 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -780,19 +780,18 @@ static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt
       return;
     }
 
       return;
     }
 

-  /*@i22*/

   DPRINTF((message("")));
   
   if (body->kind == XPR_BLOCK)
     body = exprData_getSingle(body->edata);
 
   DPRINTF((message("")));
   
   if (body->kind == XPR_BLOCK)
     body = exprData_getSingle(body->edata);
 

-  /*
+  

   constraintsRequires = constraintList_undefined;
   constraintsEnsures = constraintList_undefined;
 
   lastRequires = constraintList_makeNew();
   lastEnsures = constraintList_makeNew();
   constraintsRequires = constraintList_undefined;
   constraintsEnsures = constraintList_undefined;
 
   lastRequires = constraintList_makeNew();
   lastEnsures = constraintList_makeNew();

-  */
+  

 
   /*@-mustfree@*/ 
   /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
 
   /*@-mustfree@*/ 
   /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */


@@ -1251,7 +1250,6 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de
       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
       
       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
       

-      /*@i325 Should check which is array/index. */

       break;
       
     case XPR_PARENS: 
       break;
       
     case XPR_PARENS: 


@@ -1333,7 +1331,7 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de
 
       break;
     case XPR_SIZEOFT:
 
       break;
     case XPR_SIZEOFT:

-      /*@i43 drl possible problem : warning make sure the case can be ignored.. */
+      /*drl 4-11-03 I think this is the same as the next case...*/

       
       break;
       
       
       break;
       


@@ -1694,7 +1692,6 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret,
                                     exprNode_traversTrueEnsuresConstraints
                                    (exprData_getFcn (data)));
       ret = constraintList_addListFree (ret,
                                     exprNode_traversTrueEnsuresConstraints
                                    (exprData_getFcn (data)));

-      /*@i11*/  /* exprNodeList_unparse (exprData_getArgs (data)); */

       break;
       
     case XPR_RETURN:
       break;
       
     case XPR_RETURN:


@@ -1827,7 +1824,6 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret,
                                     exprNode_traversFalseEnsuresConstraints
                                    (exprData_getFcn (data)));
       ret = constraintList_addListFree (ret,
                                     exprNode_traversFalseEnsuresConstraints
                                    (exprData_getFcn (data)));

-      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */

       break;
       
     case XPR_RETURN:
       break;
       
     case XPR_RETURN:


@@ -1963,7 +1959,6 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret,
                                     exprNode_traversRequiresConstraints
                                    (exprData_getFcn (data)));
       ret = constraintList_addListFree (ret,
                                     exprNode_traversRequiresConstraints
                                    (exprData_getFcn (data)));

-      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */

       break;
       
     case XPR_RETURN:
       break;
       
     case XPR_RETURN:


@@ -2106,7 +2101,6 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
       ret = constraintList_addListFree (ret,
                                        exprNode_traversEnsuresConstraints
                                        (exprData_getFcn (data)));
       ret = constraintList_addListFree (ret,
                                        exprNode_traversEnsuresConstraints
                                        (exprData_getFcn (data)));

-      /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */

       break;
     case XPR_RETURN:
       ret = constraintList_addListFree (ret,
       break;
     case XPR_RETURN:
       ret = constraintList_addListFree (ret,

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 1616acf83dce37f7ee0c9690df09c7519325703b..098d9fe324d553c13636fb7fd1e8acc53416fdad 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -663,7 +663,7 @@ static bool constraint_conflict (constraint c1, constraint c2)
      strlen(str) == maxRead(s) + strlen(str);
   */
 
      strlen(str) == maxRead(s) + strlen(str);
   */
 

-  /*@i324234*/ /*this code is functional but it may be worth cleaning up at some point. */
+  /*this code is functional but it may be worth cleaning up at some point. */

   
   if (c1->ar == EQ)
     if (c1->ar == c2->ar)
   
   if (c1->ar == EQ)
     if (c1->ar == c2->ar)


@@ -850,11 +850,12 @@ static bool  sizeofBufComp(constraintExpr buf1, constraintExpr expr2)
 
   s2 = constraintTerm_getsRef(constraintExprData_termGetTerm(buf1->data) );
 
 
   s2 = constraintTerm_getsRef(constraintExprData_termGetTerm(buf1->data) );
 

-  /*@i223@*/ /*this may be the wronge thing to test for */
+  /*drl this may be the wronge thing to test for but this
+    seems to work correctly*/

   if (sRef_similarRelaxed(s1, s2)   || sRef_sameName (s1, s2) )
     {
   if (sRef_similarRelaxed(s1, s2)   || sRef_sameName (s1, s2) )
     {

-      /*@i22*/ /* get rid of this test of now */
-      /* if (ctype_isFixedArray (sRef_getType (s2) ) ) */
+      /* origly checked that ctype_isFixedArray(sRef_getType(s2)) but
+        removed that test */

        return TRUE;
     }
   return FALSE;
        return TRUE;
     }
   return FALSE;


@@ -864,7 +865,8 @@ static bool  sizeofBufComp(constraintExpr buf1, constraintExpr expr2)
    maxSet(buf) >= sizeof(buf) - 1
 */
 
    maxSet(buf) >= sizeof(buf) - 1
 */
 

-/*@i223@*/ /*need to add some type checking */
+/*drl eventually it would be good to check that
+  buf is of type char.*/

 
 static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c)
 {
 
 static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c)
 {


@@ -944,8 +946,6 @@ static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c)
     {
      return FALSE;
     } 
     {
      return FALSE;
     } 

-    
-

 }
 /*@noaccess constraintExpr@*/
 
 }
 /*@noaccess constraintExpr@*/
 


@@ -1249,12 +1249,9 @@ constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p
       llassert(constraint_isDefined(el) );
       
       if ((el->ar == LT )  )
       llassert(constraint_isDefined(el) );
       
       if ((el->ar == LT )  )

-       /* if (!constraint_conflict (c, el) ) */ /*@i523 explain this! */

           {
             constraintExpr  temp2;
             
           {
             constraintExpr  temp2;
             

-            /*@i22*/
-

             if (constraintExpr_same (el->expr, c->expr) )
               {
                 DPRINTF((message ("inequalitySubstitute Replacing %q in %q with  %q",
             if (constraintExpr_same (el->expr, c->expr) )
               {
                 DPRINTF((message ("inequalitySubstitute Replacing %q in %q with  %q",


@@ -1310,12 +1307,9 @@ static constraint  inequalitySubstituteStrong  (/*@returned@*/ constraint c, con
 
       llassert(constraint_isDefined(el) );
       if ((el->ar == LT ) ||  (el->ar == LTE )  )
 
       llassert(constraint_isDefined(el) );
       if ((el->ar == LT ) ||  (el->ar == LTE )  )

-       /* if (!constraint_conflict (c, el) ) */ /*@i523@*/

           {
             constraintExpr  temp2;
             
           {
             constraintExpr  temp2;
             

-            /*@i22*/
-

             if (constraintExpr_same (el->lexpr, c->expr) )
               {
                 DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",
             if (constraintExpr_same (el->lexpr, c->expr) )
               {
                 DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",


@@ -1367,7 +1361,6 @@ static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, co
 
       DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));      
        if (( el->ar == LTE) || (el->ar == LT) )
 
       DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));      
        if (( el->ar == LTE) || (el->ar == LT) )

-        /* if (!constraint_conflict (c, el) ) */ /*@i532@*/

           {
             constraintExpr  temp2;
 
           {
             constraintExpr  temp2;
 

diff --git a/src/cstring.c b/src/cstring.c
index 4b125d361992b12f57d6b735bedb58bb2aa38117..4c9f2c05cd548aa6679f82e8c0b81348b573d606 100644 (file)
--- a/src/cstring.c
+++ b/src/cstring.c
@@ -901,9 +901,6 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
   return cstring_undefined;
 }
 
   return cstring_undefined;
 }
 

-/*@i3534 @*/
-/*@ignore@*/ /* !!! DRL don't ignore large segments like this without a good reason! */
-

 /* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/
 /* This function understands that "sdf\"  \"sdfsdf" is okay*/
 static mstring doMergeString (cstring s)
 /* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/
 /* This function understands that "sdf\"  \"sdfsdf" is okay*/
 static mstring doMergeString (cstring s)


@@ -1163,7 +1160,7 @@ cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar
 
   return c;
 }
 
   return c;
 }

-/*@end@*/
+

 
 
 
 
 
 

diff --git a/src/exprNode.c b/src/exprNode.c
index 0342eedbecddbd5362045bd69443c5d6cb2b2390..41b0a6d1a829f272f70cbe6a2d5e3cbeaffd580f 100644 (file)
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -4420,8 +4420,6 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
   /*DRL 6/8/01 I decided to disable all Splint warnings here since the code 
     probably needs a rewrite any way */
 
   /*DRL 6/8/01 I decided to disable all Splint warnings here since the code 
     probably needs a rewrite any way */
 

-  /*@i65234@*/
-  /*@ignore@*/

 
   /* updateEnvironmentForPostOp (e); */
   
 
   /* updateEnvironmentForPostOp (e); */
   


@@ -4455,6 +4453,8 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
          printf ("ret->sref is Possibly Null Terminated\n");
        else if (sRef_isNotNullTerminated (ret->sref))
          printf ("ret->sref is Not Null Terminated\n");
          printf ("ret->sref is Possibly Null Terminated\n");
        else if (sRef_isNotNullTerminated (ret->sref))
          printf ("ret->sref is Not Null Terminated\n");

+       else
+         {}

       }
     }
     
       }
     }
     


@@ -4466,7 +4466,6 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
       }
     }
   }
       }
     }
   }

-  /*@end@*/

   /* end modifications */
 
   return ret;
   /* end modifications */
 
   return ret;

diff --git a/src/osd.c b/src/osd.c
index 3716f303a7c717d47741498d2903ed62f7d40742..24dcbf4d835eb30ceb8cf9c90f7a0a0d958eccb0 100644 (file)
--- a/src/osd.c
+++ b/src/osd.c
@@ -1133,7 +1133,7 @@ cstring osd_outputPath (cstring filename)
         {
           /* Give up if the result gets to be longer
              than the absolute path name.  */
         {
           /* Give up if the result gets to be longer
              than the absolute path name.  */

-          /*@i423@*/ if (rel_buffer + filename_len <= rel_buf_p + 3)
+          if (rel_buffer + filename_len <= rel_buf_p + 3)

            {
              sfree (rel_buffer);
              return cstring_copy (filename);
            {
              sfree (rel_buffer);
              return cstring_copy (filename);