*** empty log message ***

diff --git a/LICENSE b/LICENSE
index 581403c6f6b43e4109a99a3710468d4f3505c352..32d00d9b58183ee405cdc1e80d38fb2a63a51c6e 100644 (file)
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
          Splint - annotation-assisted static program checker
                         http://www.splint.org
 
-                       Copyright (C) 1994-2002
+                       Copyright (C) 1994-2007
                        University of Virginia,
                 Massachusetts Institute of Technology
 

diff --git a/configure b/configure
index 9093d9fe5e9034ba068a4e78a2fd8834749a57ea..a092ae6a5805d5f0eb2a3bc284a93cf9aaf9a862 100755 (executable)
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.59 for Splint 3.1.1.2.
+# Generated by GNU Autoconf 2.59 for Splint 3.1.2.
 #
 # Report bugs to <splint-bug@splint.org>.
 #
@@ -269,8 +269,8 @@ SHELL=${CONFIG_SHELL-/bin/sh}
 # Identity of this package.
 PACKAGE_NAME='Splint'
 PACKAGE_TARNAME='splint'
-PACKAGE_VERSION='3.1.1.2'
-PACKAGE_STRING='Splint 3.1.1.2'
+PACKAGE_VERSION='3.1.2'
+PACKAGE_STRING='Splint 3.1.2'
 PACKAGE_BUGREPORT='splint-bug@splint.org'
 
 ac_unique_file="src/lclinit.c"
@@ -743,7 +743,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
-\`configure' configures Splint 3.1.1.2 to adapt to many kinds of systems.
+\`configure' configures Splint 3.1.2 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -810,7 +810,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of Splint 3.1.1.2:";;
+     short | recursive ) echo "Configuration of Splint 3.1.2:";;
    esac
   cat <<\_ACEOF
 
@@ -933,7 +933,7 @@ fi
 test -n "$ac_init_help" && exit 0
 if $ac_init_version; then
   cat <<\_ACEOF
-Splint configure 3.1.1.2
+Splint configure 3.1.2
 generated by GNU Autoconf 2.59
 
 Copyright (C) 2003 Free Software Foundation, Inc.
@@ -947,7 +947,7 @@ cat >&5 <<_ACEOF
 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.1.1.2, which was
+It was created by Splint $as_me 3.1.2, which was
 generated by GNU Autoconf 2.59.  Invocation command line was
 
   $ $0 $@
@@ -1626,7 +1626,7 @@ fi
 
 # Define the identity of the package.
  PACKAGE=splint
- VERSION=3.1.1.2
+ VERSION=3.1.2
 
 
 # Some tools Automake needs.
@@ -3946,7 +3946,7 @@ _ACEOF
 
 
 # These used to be in herald.h
-LCL_PARSE_VERSION="Splint 3.1.1.2"
+LCL_PARSE_VERSION="Splint 3.1.2"
 
 cat >>confdefs.h <<_ACEOF
 #define SPLINT_VERSION "$LCL_PARSE_VERSION --- `date +"%d %b %Y"`"
@@ -4433,7 +4433,7 @@ _ASBOX
 } >&5
 cat >&5 <<_CSEOF
 
-This file was extended by Splint $as_me 3.1.1.2, which was
+This file was extended by Splint $as_me 3.1.2, which was
 generated by GNU Autoconf 2.59.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -4496,7 +4496,7 @@ _ACEOF
 
 cat >>$CONFIG_STATUS <<_ACEOF
 ac_cs_version="\\
-Splint config.status 3.1.1.2
+Splint config.status 3.1.2
 configured by $0, generated by GNU Autoconf 2.59,
   with options \\"`echo "$ac_configure_args" | sed 's/[\\""\`\$]/\\\\&/g'`\\"
 

diff --git a/configure.ac b/configure.ac
index 366916ae630f64b463bb4e6eeb02f87b8ae4d113..515e60c001c8df3e822af8d13dee4eccb1bd0ce7 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)
 
-AC_INIT([Splint], [3.1.1.2], [splint-bug@splint.org], [splint])
+AC_INIT([Splint], [3.1.2], [splint-bug@splint.org], [splint])
 
 dnl This MUST precede any other macro
 AC_CONFIG_AUX_DIR([config])

diff --git a/src/Headers/cgrammar_tokens.h b/src/Headers/cgrammar_tokens.h
index 65e6cf9fa3d1545cbb5bb9e17ad51742ee65a66d..4b838a37783e3b22ed524e103abebf726ad6c2f2 100644 (file)
--- a/src/Headers/cgrammar_tokens.h
+++ b/src/Headers/cgrammar_tokens.h
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -602,3 +604,5 @@ extern cgrammar_YYSTYPE yylval;
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/Headers/llgrammar_gen.h b/src/Headers/llgrammar_gen.h
index e1f420d20a81af005bf7facce26fae52d588cb83..955da8e6928dfed6cd054f9221a78c78d54751bd 100644 (file)
--- a/src/Headers/llgrammar_gen.h
+++ b/src/Headers/llgrammar_gen.h
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -499,3 +501,5 @@ extern YYSTYPE yllval;
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/Headers/llgrammar_gen2.h b/src/Headers/llgrammar_gen2.h
index e1f420d20a81af005bf7facce26fae52d588cb83..955da8e6928dfed6cd054f9221a78c78d54751bd 100644 (file)
--- a/src/Headers/llgrammar_gen2.h
+++ b/src/Headers/llgrammar_gen2.h
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -499,3 +501,5 @@ extern YYSTYPE yllval;
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/Headers/signature_gen.h b/src/Headers/signature_gen.h
index 15352952f392042898fb2771dcd31d1ee1c10bcd..078d0f02a0b1cd118e95e48000f3dd50080c0b19 100644 (file)
--- a/src/Headers/signature_gen.h
+++ b/src/Headers/signature_gen.h
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -266,3 +268,5 @@ typedef union YYSTYPE
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/Makefile.in b/src/Makefile.in
index dffda81e4fda0dda5473076ababaf1f13ce1ec2a..7615e79f995fb10fd840804b607cd9be703bc56d 100644 (file)
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -632,7 +632,7 @@ CCLD = $(CC)
 LINK = $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@
 CFLAGS = @CFLAGS@
 DIST_SOURCES = $(lcl_SOURCES) $(splint_SOURCES)
-DIST_COMMON = Makefile.am Makefile.in TODO
+DIST_COMMON = Makefile.am Makefile.in
 SOURCES = $(lcl_SOURCES) $(splint_SOURCES)
 
 all: $(BUILT_SOURCES)
@@ -1111,11 +1111,11 @@ nocheck:
 
 .PHONY: test
 test:
-       ${MAKE} ; cd ../test; ${MAKE} --no-print-directory
+       cd ../test; ${MAKE} --no-print-directory
 
 .PHONY: libs
 libs:
-       ${MAKE} ; cd ../lib; ${MAKE} --no-print-directory
+       cd ../lib; ${MAKE} --no-print-directory
 
 ### Automake generates wrong tags
 .PHONY: etags

diff --git a/src/bison.head b/src/bison.head
index 9e8212d7c05f8697fc14e60cf197805f1110bd98..681fd145627cc8afb0e8f1d1d5aff630a3029565 100644 (file)
--- a/src/bison.head
+++ b/src/bison.head
@@ -52,5 +52,7 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 

diff --git a/src/bison.reset b/src/bison.reset
index 45e00aa91c20eadd688ebf8b675b291238b08e2e..5c0ab748ebbbdfdff6c7dd368fc3dba718cd9dd2 100644 (file)
--- a/src/bison.reset
+++ b/src/bison.reset
@@ -48,3 +48,5 @@
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der
index 929defc028573e35517c34c996d47144cda382c2..061da3af1168fa0d90608870ee3f4004e7cffccf 100644 (file)
--- a/src/cgrammar.c.der
+++ b/src/cgrammar.c.der
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -7881,3 +7883,5 @@ void yyerror (/*@unused@*/ char *s)
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/cpplib.c b/src/cpplib.c
index d927c7b7193e74e891b6c73fe50eed8bff43fa31..b054f61f3631c61cb49803646fdb8e42f6e3fcb9 100644 (file)
--- a/src/cpplib.c
+++ b/src/cpplib.c
@@ -373,7 +373,7 @@ typedef unsigned int mode_t;
 
 # endif
 
-static int file_size_and_mode (int p_fd, /*@out@*/ __mode_t *p_mode_pointer,
+static int file_size_and_mode (int p_fd, /*@out@*/ mode_t *p_mode_pointer,
                               /*@out@*/ size_t *p_size_pointer);
 static int safe_read (int p_desc, /*@out@*/ char *p_ptr, int p_len);
 
@@ -1563,6 +1563,7 @@ collect_expansion (cppReader *pfile, char *buf, char *limit,
   defn->predefined = NULL;
 
   exp_p = defn->expansion = (char *) defn + sizeof (*defn);
+  *defn->expansion = '\0'; /* convince splint it is initialized */
 
   defn->line = 0;
   defn->rest_args = NULL;
@@ -1830,7 +1831,7 @@ collect_expansion (cppReader *pfile, char *buf, char *limit,
       llfatalbug (cstring_makeLiteral ("Maximum definition size exceeded."));
     }
 
-  /*@i1@*/ return defn; /* Spurious warning here */
+  return defn; /* Spurious warning here */
 }
 
 /*
@@ -2175,8 +2176,10 @@ collect_expansionLoc (fileloc loc, char *buf, char *limit,
     {
       llfatalbug (cstring_makeLiteral ("Maximum definition size exceeded."));
     }
-
-  /*@i1@*/ return defn; /* Spurious warning here */
+  
+  /*@-compdef@*/ /* defn->expansion defined? */
+  return defn; 
+  /*@=compdef@*/
 }
 
 /*
@@ -7073,7 +7076,7 @@ finclude (cppReader *pfile, int f,
          bool system_header_p,
          /*@dependent@*/ struct file_name_list *dirptr)
 {
-  __mode_t st_mode;
+  mode_t st_mode; /* was __mode_t */
   size_t st_size;
   long i;
   int length = 0;
@@ -7276,19 +7279,23 @@ cppCleanup (/*@special@*/ cppReader *pfile)
 */
 
 static int
-file_size_and_mode (int fd, __mode_t *mode_pointer, size_t *size_pointer)
+file_size_and_mode (int fd, mode_t *mode_pointer, size_t *size_pointer)
 {
   struct stat sbuf;
 
   if (fstat (fd, &sbuf) < 0) {
     *mode_pointer = 0;
     *size_pointer = 0;
-    /*@i2@*/ return (-1); /* Spurious warnings! */
+    /*@-compdestroy@*/ /* possibly spurious warnings here (or memory leak) */
+    return (-1);
+    /*@=compdestroy@*/
   }
 
   if (mode_pointer != NULL)
     {
+      /*@-type@*/ /* confusion between __mode_t and mode_t types */
       *mode_pointer = sbuf.st_mode;
+      /*@=type@*/
     }
 
   if (size_pointer != NULL)
@@ -7296,7 +7303,9 @@ file_size_and_mode (int fd, __mode_t *mode_pointer, size_t *size_pointer)
       *size_pointer = (size_t) sbuf.st_size;
     }
 
-  /*@i4@*/ return 0; /* spurious warnings here */
+  /*@-compdestroy@*/ /* possibly spurious warnings here (or memory leak) */
+  return 0;
+  /*@=compdestroy@*/
 }
 
 /* Read LEN bytes at PTR from descriptor DESC, for file FILENAME,

diff --git a/src/lclscan.c b/src/lclscan.c
index bf968b69c21115556a6876f8c78aaa547532407b..3109788829dc928363c9bad20149c74c20046d0a 100644 (file)
--- a/src/lclscan.c
+++ b/src/lclscan.c
@@ -69,7 +69,7 @@ static /*@dependent@*/ /*@null@*/ char *line;  /* input text */
 static unsigned int lineNumber;                       /* current line number */
 
 ltokenCode yllex (void)
-  /*@globals killed restoretok@*/ 
+  /*@globals killed restoretok@*/ /* only if restore is TRUE */
 {
   lsymbol tokenSym;
 
@@ -80,7 +80,9 @@ ltokenCode yllex (void)
     }
   else
     {
+      /*@-onlyunqglobaltrans@*/
       yllval.ltok = ltoken_copy (LCLScanNextToken ());
+      /*@=onlyunqglobaltrans@*/
     }
 
   tokenSym = ltoken_getText (yllval.ltok);
@@ -109,7 +111,11 @@ ltokenCode yllex (void)
        }
     }
 
+  /*@-onlyunqglobaltrans@*/ /* restoretok not released on non-restore path */
+  /*@-globstate@*/
   return (ltoken_getCode (yllval.ltok));
+  /*@=onlyunqglobaltrans@*/
+  /*@=globstate@*/
 }
 
 /* useful for scanning LCL init files and LSL init files ? */

diff --git a/src/llgrammar.c.der b/src/llgrammar.c.der
index 8bd351114c1abb8b1024684164b56028ef093a33..409ba914ae41e1114024c67771a9840be1043472 100644 (file)
--- a/src/llgrammar.c.der
+++ b/src/llgrammar.c.der
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -5177,3 +5179,5 @@ static void yyprint (FILE *f, int t, YYSTYPE value)
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/osd.c b/src/osd.c
index 171d8777c364e0017d9c411aa0a74e72d9cf3339..ebe214a9ac2ec7a4e56f42d86530f344e13f5aa3 100644 (file)
--- a/src/osd.c
+++ b/src/osd.c
@@ -338,13 +338,15 @@ osd_fileExists (cstring filespec)
 bool
 osd_executableFileExists (/*@unused@*/ char *filespec)
 {
+  /*@-compdestroy@*/ /* possible memory leaks here? */
 # ifdef UNIX
   struct stat buf;
   if (stat (filespec, &buf) == 0)
     { 
       /* mask by file type */
-      /*@-unrecog@*/ /* S_IFMT is not defined */
-      /*@i32@*/ if ((buf.st_mode & S_IFMT) != S_IFDIR /*@=unrecog@*/) /* not a directory */ /* spurious */
+      /*@-type@*/ /* confusion about __mode_t and mode_t types */
+      if ((buf.st_mode & S_IFMT) != S_IFDIR) /* not a directory */ 
+       /*@=type@*/
        {
          /* as long as it is an executable file */
 # if defined(__IBMC__) && defined(OS2)
@@ -359,13 +361,13 @@ osd_executableFileExists (/*@unused@*/ char *filespec)
                   | (buf.st_mode & S_IXGRP) |
                   (buf.st_mode & S_IXOTH)
 # endif
-                  /*@i4@*/ ) != 0); /* spurious */
+                  ) != 0); /* spurious */
 # endif
        }
     }
 # endif
-  /*@i4@*/ return (FALSE); /* spurious */
-
+  return (FALSE); 
+  /*@=compdestroy@*/
 }
 
 /*

diff --git a/src/scan.c b/src/scan.c
index 8c38a02780cdd7a10326be668a9f072a34b68c1a..cc5085812fcef03ae5bcf30c318bfb053943cd24 100644 (file)
--- a/src/scan.c
+++ b/src/scan.c
@@ -61,8 +61,9 @@ static unsigned int lineNumber;       /* current line number */
 unsigned int lsllex (YYSTYPE *lval)
 {
   /* This is important!  Bison expects this */
-  lval->ltok = LSLScanNextToken ();
-  return (ltoken_getCode (lval->ltok));
+  /* splint doesn't know the type of YYSTYPE, so we need to ignore warnings here */
+  /*@i1@*/ lval->ltok = LSLScanNextToken ();
+  /*@i1@*/ return (ltoken_getCode (lval->ltok));
 }
 
 ltoken LSLScanNextToken (void)

diff --git a/src/signature.c.der b/src/signature.c.der
index aba1cb0f4e9a5c8481dc05dded36e0a8ffb13de7..1c270a8101f9eda87c3d71307da83fab7c03c73c 100644 (file)
--- a/src/signature.c.der
+++ b/src/signature.c.der
@@ -52,6 +52,8 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */
 
 /* A Bison parser, made by GNU Bison 2.3.  */
@@ -2106,3 +2108,5 @@ extern void PrintToken (ltoken tok) {
 
 /*drl added 12/11/2002*/
 /*@=type@*/
+
+/*@=enummemuse@*/

diff --git a/src/signature.y b/src/signature.y
index b52657da27ffa5ea20c6d0faa282569888f4faf5..a5b3fd96c6c52e5da793e6025c31b6219957af81 100644 (file)
--- a/src/signature.y
+++ b/src/signature.y
@@ -99,7 +99,7 @@ static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */);
 %token <ltok> LST_COMMA             /* , */
 %token <ltok> LST_EOL LST_COMMENTSYM LST_WHITESPACE 
 
-%token LST_WHITESPACE
+ /* %token LST_WHITESPACE */ /* Duplicate tokey removed */
 %token LST_QUANTIFIERSYM
 %token LST_EQUATIONSYM
 %token LST_EQSEPSYM