Flip 4.0.4 devel changes back here.

More splint fiddles.

CVS patchset: 5311
CVS date: 2002/02/10 16:50:06

28 files changed, 565 insertions, 205 deletions

diff --git a/zlib/.cvsignore b/zlib/.cvsignore
index e9823b933..0da19cf29 100644
--- a/zlib/.cvsignore
+++ b/zlib/.cvsignore
@@ -8,6 +8,8 @@ Makefile.in
 apidocs
 config.cache
 config.guess
+config.h
+config.h.in
 config.log
 config.status
 config.sub
diff --git a/zlib/.lclintrc b/zlib/.lclintrc
index 3cdbb7fd8..64a631d07 100644
--- a/zlib/.lclintrc
+++ b/zlib/.lclintrc
@@ -1,4 +1,4 @@
--I. -DHAVE_CONFIG_H -D_GNU_SOURCE -DSTDC -DHAVE_UNISTD_H -DUSE_MMAP -DWITH_RSYNC_PAD
+-I. -DHAVE_CONFIG_H -D_GNU_SOURCE -DSTDC -DHAVE_UNISTD_H -DHAS_snprintf -DHAS_vsnprintf -DUSE_MMAP -DWITH_RSYNC_PAD
 
 +partial
 +forcehints
@@ -16,55 +16,13 @@
 
 # --- not yet
 -retvalint		# painful
--nullret
--retalias
-
--protoparammatch
-
--mustmod
--mods
--infloops
--evalorder
--bufferoverflowhigh
--assignexpose
--moduncon
-
--modunconnomods
--noeffectuncon
--evalorderuncon
--infloopsuncon
--modobserveruncon
--modnomods
-
--statictrans
--staticinittrans
--observertrans
--dependenttrans
--unqualifiedtrans
--kepttrans
--immediatetrans
--temptrans
-
--castfcnptr
--sizeoftype
--globs
--globstate
--redef
--nullpass
--internalglobs
--compdef
--branchstate
--compmempass
--nullstate
--shiftsigned
--usereleased
--type
--unsignedcompare
--nullderef
--exportheader
-
--nullptrarith
--noeffect
+
+-protoparammatch	# 22
+
+-noeffectuncon		# 22
+
+-sizeoftype		# 110
+-nullstate		# 36
 
 # --- +partial artifacts
 -declundef
@@ -92,6 +50,12 @@
 -numenummembers 1024	# RPMTAG has 138 members
 -numstructfields 256	# Java jni.h has 229 fields
 -ptrarith		# tedious
+
+-compdestroy
+-mustdefine
+-shiftimplementation
+-shiftnegative
+
 -strictops
 -strictusereleased
 -stringliterallen 4096	# redhat*PubKey's are big
diff --git a/zlib/Makefile.am b/zlib/Makefile.am
index 8cc7ceac8..154fcfb82 100644
--- a/zlib/Makefile.am
+++ b/zlib/Makefile.am
@@ -24,6 +24,14 @@ example_LDFLAGS = -L. -lz
 minigzip_SOURCES = minigzip.c
 minigzip_LDFLAGS = -L. -lz
 
+.PHONY: sources
+sources:
+	@echo $(libz_la_SOURCES:%=zlib/%)
+
+.PHONY: lclint
+lclint:
+	lclint $(DEFS) $(INCLUDES) $(libz_la_SOURCES)
+
 .PHONY: doxygen
 doxygen apidocs: Doxyfile
 	rm -rf $@
diff --git a/zlib/Makefile.in b/zlib/Makefile.in
index 304966fba..05de276b3 100644
--- a/zlib/Makefile.in
+++ b/zlib/Makefile.in
@@ -439,6 +439,14 @@ mostlyclean-generic distclean-generic clean-generic \
 maintainer-clean-generic clean mostlyclean distclean maintainer-clean
 
 
+.PHONY: sources
+sources:
+	@echo $(libz_la_SOURCES:%=zlib/%)
+
+.PHONY: lclint
+lclint:
+	lclint $(DEFS) $(INCLUDES) $(libz_la_SOURCES)
+
 .PHONY: doxygen
 doxygen apidocs: Doxyfile
 	rm -rf $@
diff --git a/zlib/compress.c b/zlib/compress.c
index f589bee5b..0dc458ec1 100644
--- a/zlib/compress.c
+++ b/zlib/compress.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: compress.c,v 1.2 2001/11/22 21:12:46 jbj Exp $ */
+/* @(#) $Id: compress.c,v 1.3 2001/12/27 21:00:17 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -10,6 +10,9 @@
  */
 
 #include "zlib.h"
+#include "zutil.h"	/* XXX for zmemzero() */
+
+/*@access z_streamp@*/
 
 /* ========================================================================= */
 /**
@@ -28,6 +31,7 @@ int ZEXPORT compress2 (Bytef *dest, uLongf *destLen, const Bytef *source, uLong
     z_stream stream;
     int err;
 
+    zmemzero(&stream, sizeof(stream));
     stream.next_in = (Bytef*)source;
     stream.avail_in = (uInt)sourceLen;
 #ifdef MAXSEG_64K
@@ -38,9 +42,9 @@ int ZEXPORT compress2 (Bytef *dest, uLongf *destLen, const Bytef *source, uLong
     stream.avail_out = (uInt)*destLen;
     if ((uLong)stream.avail_out != *destLen) return Z_BUF_ERROR;
 
-    stream.zalloc = (alloc_func)0;
-    stream.zfree = (free_func)0;
-    stream.opaque = (voidpf)0;
+    stream.zalloc = (alloc_func)NULL;
+    stream.zfree = (free_func)NULL;
+    stream.opaque = (voidpf)NULL;
 
     err = deflateInit(&stream, level);
     if (err != Z_OK) return err;
diff --git a/zlib/configure.in b/zlib/configure.in
index b85febce1..6bef28b7e 100644
--- a/zlib/configure.in
+++ b/zlib/configure.in
@@ -8,6 +8,7 @@ AC_PROG_CC
 AM_DISABLE_SHARED
 AC_PROG_LIBTOOL
 
+CFLAGS="-DHAS_snprintf -DHAS_snprintf"
 if test "$ac_cv_prog_gcc" = yes; then
     CFLAGS="-DWITH_RSYNC_PAD -O3 -fomit-frame-pointer -Wall -Wpointer-arith -Wstrict-prototypes -Wmissing-prototypes -Wno-char-subscripts"
 fi
diff --git a/zlib/crc32.c b/zlib/crc32.c
index 0af89a1c0..4608d0466 100644
--- a/zlib/crc32.c
+++ b/zlib/crc32.c
@@ -1,4 +1,5 @@
-/* @(#) $Id: crc32.c,v 1.4 2001/11/22 21:12:46 jbj Exp $ */
+/* @(#) $Id: crc32.c,v 1.5.2.1 2002/01/25 19:18:55 jbj Exp $ */
+/*@-globs@*/
 /*
  * Copyright (C) 1995-1998 Mark Adler
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -17,8 +18,11 @@
 
 #ifdef DYNAMIC_CRC_TABLE
 
+/*@unchecked@*/
 local int crc_table_empty = 1;
+/*@unchecked@*/
 local uLongf crc_table[256];
+
 local void make_crc_table OF((void))
 	/*@*/;
 
@@ -139,6 +143,8 @@ const uLongf * ZEXPORT get_crc_table(void)
   return (const uLongf *)crc_table;
 }
 
+#if defined(__i386__)
+
 uLong partial_crc32_copy(uLong crc, const Bytef *buf, uInt len, Bytef *dst)
 {
 /*@-sysunrecog@*/
@@ -162,3 +168,33 @@ uLong ZEXPORT crc32(uLong crc, const Bytef *buf, uInt len)
 	return 0L;
 }
 
+#else	/* !__i386__ */
+
+/* ========================================================================= */
+#define DO1(buf) crc = crc_table[((int)crc ^ (*buf++)) & 0xff] ^ (crc >> 8);
+#define DO2(buf)  DO1(buf); DO1(buf);
+#define DO4(buf)  DO2(buf); DO2(buf);
+#define DO8(buf)  DO4(buf); DO4(buf);
+ 
+/* ========================================================================= */
+uLong ZEXPORT crc32(uLong crc, const Bytef * buf, uInt len)
+{
+    if (buf == Z_NULL) return 0L;
+#ifdef DYNAMIC_CRC_TABLE
+    if (crc_table_empty)
+      make_crc_table();
+#endif
+    crc = crc ^ 0xffffffffL;
+    while (len >= 8)
+    {
+      DO8(buf);
+      len -= 8;
+    }
+    if (len) do {
+      DO1(buf);
+    } while (--len);
+    return crc ^ 0xffffffffL;
+ }
+
+#endif	/* !__i386__ */
+/*@=globs@*/
diff --git a/zlib/crc32.h b/zlib/crc32.h
index ea555e7eb..8b5f0187e 100644
--- a/zlib/crc32.h
+++ b/zlib/crc32.h
@@ -2,10 +2,11 @@
  * \file crc32.h
  */
 
+#if defined(__i386__)	/* { */
+
 #define partial_crc32		__z_partial_crc32
 #define partial_crc32_copy	__z_partial_crc32_copy
 
-#ifdef __i386__	/* { */
 struct __crc32_fool_gcc {
 	char	x[32768];
 };
@@ -38,6 +39,7 @@ static inline uLong get_crc_from_partial(uLong *crcp)
 	return *crcp ^ 0xffffffffL;
 }
 
+/*@observer@*/ /*@unchecked@*/
 extern const uLongf crc_table[256];
 
 #define DO1(buf) crc = crc_table[((int)crc ^ (*buf++)) & 0xff] ^ (crc >> 8);
diff --git a/zlib/deflate.c b/zlib/deflate.c
index 902382450..51c3879bd 100644
--- a/zlib/deflate.c
+++ b/zlib/deflate.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: deflate.c,v 1.3 2001/12/08 17:12:13 jbj Exp $ */
+/* @(#) $Id: deflate.c,v 1.4.2.1 2002/01/25 19:18:55 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -55,9 +55,12 @@
 
 #include "deflate.h"
 
-/*@observer@*/
+/*@-exportheadervar@*/
+/*@unused@*/ /*@observer@*/
 const char deflate_copyright[] =
    " deflate 1.1.3 Copyright 1995-1998 Jean-loup Gailly ";
+/*@=exportheadervar@*/
+
 /*
   If you use the zlib library in a product, an acknowledgment is welcome
   in the documentation of your product. If for some reason you cannot
@@ -133,6 +136,7 @@ local  void check_match OF((deflate_state *s, IPos start, IPos match,
  */
 
 #if defined(WITH_RSYNC_PAD)
+/*@unchecked@*/
 local int rsync = 0;
 /* Perform rsync padding? */
 
@@ -159,6 +163,7 @@ typedef struct config_s {
    compress_func func;
 } config;
 
+/*@observer@*/ /*@unchecked@*/
 local const config configuration_table[10] = {
 /*      good lazy nice chain */
 /* 0 */ {0,    0,  0,    0, deflate_stored},  /* store only */
@@ -181,8 +186,6 @@ local const config configuration_table[10] = {
 #define EQUAL 0
 /* result of memcmp for equal strings */
 
-struct static_tree_desc_s {int dummy;}; /* for buggy compilers */
-
 /* ========================================================================= */
 /**
  * Update a hash value with the given input byte.
@@ -338,7 +341,9 @@ int ZEXPORT deflateSetDictionary (z_streamp strm, const Bytef *dictionary, uInt
 	dictionary += dictLength - length; /* use the tail of the dictionary */
 #endif
     }
+/*@-mayaliasunique@*/ /* FIX: dictionary may alias s->window */
     zmemcpy(s->window, dictionary, length);
+/*@=mayaliasunique@*/
     s->strstart = length;
     s->block_start = (long)length;
 
@@ -385,6 +390,7 @@ int ZEXPORT deflateReset (z_streamp strm)
 }
 
 /* ========================================================================= */
+/*@-compmempass@*/
 int ZEXPORT deflateParams(z_streamp strm, int level, int strategy)
 {
     deflate_state *s;
@@ -416,6 +422,7 @@ int ZEXPORT deflateParams(z_streamp strm, int level, int strategy)
     s->strategy = strategy;
     return err;
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
@@ -455,6 +462,7 @@ local void flush_pending(z_streamp strm)
 }
 
 /* ========================================================================= */
+/*@-compmempass@*/
 int ZEXPORT deflate (z_streamp strm, int flush)
 {
     int old_flush; /* value of flush param for previous deflate call */
@@ -469,9 +477,15 @@ int ZEXPORT deflate (z_streamp strm, int flush)
     if (strm->next_out == Z_NULL ||
         (strm->next_in == Z_NULL && strm->avail_in != 0) ||
 	(s->status == FINISH_STATE && flush != Z_FINISH)) {
+/*@-assignexpose@*/
         ERR_RETURN(strm, Z_STREAM_ERROR);
+/*@=assignexpose@*/
     }
+/*@-mods@*/
+/*@-assignexpose@*/
     if (strm->avail_out == 0) ERR_RETURN(strm, Z_BUF_ERROR);
+/*@=assignexpose@*/
+/*@=mods@*/
 
     s->strm = strm; /* just in case */
     old_flush = s->last_flush;
@@ -519,12 +533,20 @@ int ZEXPORT deflate (z_streamp strm, int flush)
      */
     } else if (strm->avail_in == 0 && flush <= old_flush &&
 	       flush != Z_FINISH) {
+/*@-mods@*/
+/*@-assignexpose@*/
         ERR_RETURN(strm, Z_BUF_ERROR);
+/*@=assignexpose@*/
+/*@=mods@*/
     }
 
     /* User must not provide more input after the first FINISH: */
     if (s->status == FINISH_STATE && strm->avail_in != 0) {
+/*@-mods@*/
+/*@-assignexpose@*/
         ERR_RETURN(strm, Z_BUF_ERROR);
+/*@=assignexpose@*/
+/*@=mods@*/
     }
 
     /* Start a new block or continue the current one.
@@ -585,6 +607,7 @@ int ZEXPORT deflate (z_streamp strm, int flush)
     s->noheader = -1; /* write the trailer only once! */
     return s->pending != 0 ? Z_OK : Z_STREAM_END;
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 int ZEXPORT deflateEnd (z_streamp strm)
@@ -617,6 +640,7 @@ int ZEXPORT deflateEnd (z_streamp strm)
  * To simplify the source, this is not supported for 16-bit MSDOS (which
  * doesn't have enough memory anyway to duplicate compression states).
  */
+/*@-compmempass@*/
 int ZEXPORT deflateCopy (z_streamp dest, z_streamp source)
 {
 #ifdef MAXSEG_64K
@@ -633,12 +657,18 @@ int ZEXPORT deflateCopy (z_streamp dest, z_streamp source)
 
     ss = source->state;
 
-    *dest = *source;
+/*@-assignexpose@*/
+    *dest = *source;	/* structure assignment */
+/*@=assignexpose@*/
 
     ds = (deflate_state *) ZALLOC(dest, 1, sizeof(deflate_state));
+/*@-usereleased -compdef@*/ /* FIX: structure copy above? @*/
     if (ds == Z_NULL) return Z_MEM_ERROR;
+/*@=usereleased =compdef@*/
     dest->state = (struct internal_state FAR *) ds;
-    *ds = *ss;
+/*@-usereleased -compdef@*/ /* FIX: structure copy above? @*/
+    *ds = *ss;		/* structure assignment */
+/*@=usereleased =compdef@*/
     ds->strm = dest;
 
     ds->window = (Bytef *) ZALLOC(dest, ds->w_size, 2*sizeof(Byte));
@@ -650,7 +680,9 @@ int ZEXPORT deflateCopy (z_streamp dest, z_streamp source)
     if (ds->window == Z_NULL || ds->prev == Z_NULL || ds->head == Z_NULL ||
         ds->pending_buf == Z_NULL) {
         deflateEnd (dest);
+/*@-usereleased -compdef@*/ /* FIX: structure copy above? @*/
         return Z_MEM_ERROR;
+/*@=usereleased =compdef@*/
     }
     /* following zmemcpy do not work for 16-bit MSDOS */
     zmemcpy(ds->window, ss->window, ds->w_size * 2 * sizeof(Byte));
@@ -666,9 +698,12 @@ int ZEXPORT deflateCopy (z_streamp dest, z_streamp source)
     ds->d_desc.dyn_tree = ds->dyn_dtree;
     ds->bl_desc.dyn_tree = ds->bl_tree;
 
+/*@-usereleased -compdef@*/ /* FIX: structure copy above? @*/
     return Z_OK;
+/*@=usereleased =compdef@*/
 #endif
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
@@ -701,6 +736,7 @@ local int read_buf(z_streamp strm, Bytef *buf, unsigned size)
 /**
  * Initialize the "longest match" routines for a new zlib stream
  */
+/*@-compmempass@*/
 local void lm_init (deflate_state *s)
 {
     s->window_size = (ulg)2L*s->w_size;
@@ -731,6 +767,7 @@ local void lm_init (deflate_state *s)
     s->rsync_win = RSYNC_WIN;
 #endif
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
@@ -1075,6 +1112,7 @@ local void fill_window(deflate_state *s)
 
 #if defined(WITH_RSYNC_PAD)
 local void rsync_roll(deflate_state *s, unsigned num)
+	/*@modifies *s @*/
 {
     unsigned start = s->strstart;
     unsigned i;
@@ -1206,10 +1244,11 @@ local block_state deflate_stored(deflate_state *s, int flush)
  * new strings in the dictionary only for unmatched strings or for short
  * matches. It is used only for the fast compression options.
  */
+/*@-compmempass@*/
 local block_state deflate_fast(deflate_state *s, int flush)
 {
     IPos hash_head = NIL; /* head of the hash chain */
-    int bflush;           /* set if current block must be flushed */
+    int bflush = 0;	/* set if current block must be flushed */
 
     for (;;) {
         /* Make sure that we always have enough lookahead, except
@@ -1302,6 +1341,7 @@ local block_state deflate_fast(deflate_state *s, int flush)
     FLUSH_BLOCK(s, flush == Z_FINISH);
     return flush == Z_FINISH ? finish_done : block_done;
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
@@ -1309,10 +1349,11 @@ local block_state deflate_fast(deflate_state *s, int flush)
  * evaluation for matches: a match is finally adopted only if there is
  * no better match at the next window position.
  */
+/*@-compmempass@*/
 local block_state deflate_slow(deflate_state *s, int flush)
 {
     IPos hash_head = NIL;    /* head of hash chain */
-    int bflush;              /* set if current block must be flushed */
+    int bflush = 0;	/* set if current block must be flushed */
 
     /* Process the input block. */
     for (;;) {
@@ -1446,3 +1487,4 @@ local block_state deflate_slow(deflate_state *s, int flush)
     FLUSH_BLOCK(s, flush == Z_FINISH);
     return flush == Z_FINISH ? finish_done : block_done;
 }
+/*@=compmempass@*/
diff --git a/zlib/deflate.h b/zlib/deflate.h
index fe31858a2..1dcd62f0d 100644
--- a/zlib/deflate.h
+++ b/zlib/deflate.h
@@ -1,4 +1,4 @@
-/* @(#) $Id: deflate.h,v 1.3 2001/12/08 17:12:13 jbj Exp $ */
+/* @(#) $Id: deflate.h,v 1.4 2001/12/27 21:00:17 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -84,10 +84,13 @@ typedef unsigned IPos;
  */
 
 typedef struct internal_state {
+/*@dependent@*/
     z_streamp strm;      /*!< pointer back to this zlib stream */
     int   status;        /*!< as the name implies */
+/*@owned@*/
     Bytef *pending_buf;  /*!< output still pending */
     ulg   pending_buf_size; /*!< size of pending_buf */
+/*@dependent@*/
     Bytef *pending_out;  /*!< next pending byte to output to the stream */
     int   pending;       /*!< nb of bytes in the pending buffer */
     int   noheader;      /*!< suppress zlib header and adler32 */
@@ -101,6 +104,7 @@ typedef struct internal_state {
     uInt  w_bits;        /*!< log2(w_size)  (8..16) */
     uInt  w_mask;        /*!< w_size - 1 */
 
+/*@owned@*/
     Bytef *window;
     /*!< Sliding window. Input bytes are read into the second half of the
      * window, and move to the first half later to keep a dictionary of at
@@ -116,12 +120,14 @@ typedef struct internal_state {
      * is directly used as sliding window.
      */
 
+/*@owned@*/
     Posf *prev;
     /*!< Link to older string with same hash index. To limit the size of this
      * array to 64K, this link is maintained only for the last 32K strings.
      * An index in this array is thus a window index modulo 32K.
      */
 
+/*@owned@*/
     Posf *head; /*!< Heads of the hash chains or NIL. */
 
     uInt  ins_h;          /*!< hash index of string to be inserted */
@@ -180,8 +186,11 @@ typedef struct internal_state {
 
                 /* used by trees.c: */
     /* Didn't use ct_data typedef below to supress compiler warning */
+/*@only@*/
     struct ct_data_s dyn_ltree[HEAP_SIZE];   /*!< literal and length tree */
+/*@only@*/
     struct ct_data_s dyn_dtree[2*D_CODES+1]; /*!< distance tree */
+/*@only@*/
     struct ct_data_s bl_tree[2*BL_CODES+1];  /*!< Huffman tree for bit lengths */
 
     struct tree_desc_s l_desc;               /*!< desc. for literal tree */
@@ -202,6 +211,7 @@ typedef struct internal_state {
     /*!< Depth of each subtree used as tie breaker for trees of equal frequency
      */
 
+/*@dependent@*/
     uchf *l_buf;          /*!< buffer for literals or lengths */
 
     uInt  lit_bufsize;
@@ -287,8 +297,8 @@ void _tr_flush_block  OF((deflate_state *s, charf *buf, ulg stored_len,
 	/*@modifies *s @*/;
 void _tr_align        OF((deflate_state *s))
 	/*@modifies *s @*/;
-void _tr_stored_block OF((deflate_state *s, charf *buf, ulg stored_len,
-                          int eof))
+void _tr_stored_block OF((deflate_state *s, /*@null@*/ charf *buf,
+			  ulg stored_len, int eof))
 	/*@modifies *s @*/;
 
 #define d_code(dist) \
@@ -302,10 +312,14 @@ void _tr_stored_block OF((deflate_state *s, charf *buf, ulg stored_len,
 /* Inline versions of _tr_tally for speed: */
 
 #if defined(GEN_TREES_H) || !defined(STDC)
+/*@unchecked@*/
   extern uch _length_code[];
+/*@unchecked@*/
   extern uch _dist_code[];
 #else
+/*@unchecked@*/
   extern const uch _length_code[];
+/*@unchecked@*/
   extern const uch _dist_code[];
 #endif
 
diff --git a/zlib/gzio.c b/zlib/gzio.c
index 633602867..15547e00a 100644
--- a/zlib/gzio.c
+++ b/zlib/gzio.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: gzio.c,v 1.5 2001/12/06 18:35:38 jbj Exp $ */
+/* @(#) $Id: gzio.c,v 1.6.2.2 2002/01/30 00:30:45 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h
@@ -20,13 +20,17 @@
 
 #include "crc32.h"
 
-struct internal_state {int dummy;}; /* for buggy compilers */
+/*@access z_streamp@*/
 
 #ifndef Z_BUFSIZE
 #  ifdef MAXSEG_64K
 #    define Z_BUFSIZE 4096 /* minimize memory usage for 16-bit DOS */
 #  else
+#if defined(__i386__)
 #    define Z_BUFSIZE (16 * 1024 * 1024) /*262144 16384*/
+#else
+#    define Z_BUFSIZE (256 * 1024) /*262144 16384*/
+#endif
 #  endif
 #endif
 #ifndef Z_PRINTF_BUFSIZE
@@ -39,6 +43,7 @@ static int z_bufsize = Z_BUFSIZE;
 #define ALLOC(size) malloc(size)
 #define TRYFREE(p) {if (p) free(p);}
 
+/*@observer@*/ /*@unchecked@*/
 static int gz_magic[2] = {0x1f, 0x8b}; /*!< gzip magic header */
 
 /* gzip flag byte */
@@ -53,10 +58,15 @@ typedef struct gz_stream {
     z_stream stream;
     int      z_err;   /*!< error code for last stream operation */
     int      z_eof;   /*!< set if end of input file */
+/*@dependent@*/
     FILE     *file;   /*!< .gz file */
+/*@owned@*/
     Byte     *inbuf;  /*!< input buffer */
+/*@owned@*/
     Byte     *outbuf; /*!< output buffer */
+/*@owned@*/
     char     *msg;    /*!< error message */
+/*@only@*/
     char     *path;   /*!< path name for debugging only */
     int      transparent; /*!< 1 if input file is not a .gz file */
     char     mode;    /*!< 'w' or 'r' */
@@ -68,6 +78,7 @@ typedef struct gz_stream {
 } gz_stream;
 
 
+/*@null@*/
 local gzFile gz_open      OF((const char *path, const char *mode, int  fd))
 	/*@globals errno, fileSystem @*/
 	/*@modifies errno, fileSystem @*/;
@@ -80,7 +91,7 @@ local int    get_byte     OF((gz_stream *s))
 local void   check_header OF((gz_stream *s))
 	/*@globals fileSystem@*/
 	/*@modifies s, fileSystem @*/;
-local int    destroy      OF((/*@only@*/ gz_stream *s))
+local int    destroy      OF((/*@only@*/ /*@out@*/ gz_stream *s))
 	/*@globals fileSystem@*/
 	/*@modifies s, fileSystem @*/;
 local void   putLong      OF((FILE *file, uLong x))
@@ -100,6 +111,7 @@ local uLong  getLong      OF((gz_stream *s))
  * can be checked to distinguish the two cases (if errno is zero, the
  * zlib error is Z_MEM_ERROR).
  */
+/*@-compmempass -compdef@*/
 local gzFile gz_open (const char *path, const char *mode, int fd)
 {
     int err;
@@ -114,20 +126,23 @@ local gzFile gz_open (const char *path, const char *mode, int fd)
 
     s = (gz_stream *)ALLOC(sizeof(gz_stream));
     if (!s) return Z_NULL;
+    zmemzero(s, sizeof(*s));
 
-    s->stream.zalloc = (alloc_func)0;
-    s->stream.zfree = (free_func)0;
-    s->stream.opaque = (voidpf)0;
+    s->stream.zalloc = (alloc_func)NULL;
+    s->stream.zfree = (free_func)NULL;
+    s->stream.opaque = (voidpf)NULL;
     s->stream.next_in = s->inbuf = Z_NULL;
     s->stream.next_out = s->outbuf = Z_NULL;
     s->stream.avail_in = s->stream.avail_out = 0;
     s->file = NULL;
     s->z_err = Z_OK;
     s->z_eof = 0;
-/*@-unrecog@*/
     s->stream.crc = /*crc32(0L, Z_NULL, 0)*/0;
-	partial_crc32_prep(&s->stream.crc);
+#if defined(__i386__)
+/*@-unrecog@*/
+    partial_crc32_prep(&s->stream.crc);
 /*@=unrecog@*/
+#endif
     s->msg = NULL;
     s->transparent = 0;
     s->mmap_mode = 0;
@@ -184,34 +199,41 @@ local gzFile gz_open (const char *path, const char *mode, int fd)
     s->stream.avail_out = z_bufsize;
 
     errno = 0;
-	if ((fd >= 0) && (s->mode == 'r')) {
-		struct stat stat;
-		if (!fstat(fd, &stat) && S_ISREG(stat.st_mode) && (lseek(fd, 0, SEEK_CUR) != -1)) {
-			char *test = mmap(0, z_bufsize, PROT_READ, MAP_SHARED, fd, 0);
-			if (test != (char *)-1) {
-				long n;
-				off_t pos;
-				s->mmap_mode = 1;
-				s->fd = fd;
-				TRYFREE(s->inbuf);
-				munmap(test, z_bufsize);
-				pos = lseek(fd, 0, SEEK_CUR);
-				s->mmap_end = lseek(fd, 0, SEEK_END);
-				(void) lseek(fd, 0, SEEK_SET);
-
-				s->mmap_pos = pos & ~(off_t)(z_bufsize - 1);
-				s->inbuf = mmap(0, z_bufsize, PROT_READ, MAP_SHARED, fd, s->mmap_pos);
-				(void) madvise(s->inbuf, z_bufsize, MADV_SEQUENTIAL);
-				s->mmap_pos += z_bufsize;
-				s->stream.next_in = s->inbuf + (pos & (z_bufsize - 1));
-				s->stream.avail_in = s->mmap_end - pos;
-				if (s->stream.avail_in > (s->mmap_pos - pos))
-					s->stream.avail_in = s->mmap_pos - pos;
-				for (n=0; n<s->stream.avail_in; n+=4096)
-					((volatile char *)s->inbuf)[n];
-			}
-		}
+
+#if defined(__i386__)
+    if ((fd >= 0) && (s->mode == 'r')) {
+	struct stat stat;
+	if (!fstat(fd, &stat) && S_ISREG(stat.st_mode)
+	&& (lseek(fd, 0, SEEK_CUR) != -1))
+	{
+	    char *test = mmap(0, z_bufsize, PROT_READ, MAP_SHARED, fd, 0);
+	    if (test != (char *)-1) {
+		long n;
+		off_t pos;
+		s->mmap_mode = 1;
+		s->fd = fd;
+		TRYFREE(s->inbuf);
+		munmap(test, z_bufsize);
+		pos = lseek(fd, 0, SEEK_CUR);
+		s->mmap_end = lseek(fd, 0, SEEK_END);
+		(void) lseek(fd, 0, SEEK_SET);
+
+		s->mmap_pos = pos & ~(off_t)(z_bufsize - 1);
+		s->inbuf = mmap(0, z_bufsize, PROT_READ, MAP_SHARED, fd, s->mmap_pos);
+#if defined(MADV_SEQUENTIAL)
+		(void) madvise(s->inbuf, z_bufsize, MADV_SEQUENTIAL);
+#endif
+		s->mmap_pos += z_bufsize;
+		s->stream.next_in = s->inbuf + (pos & (z_bufsize - 1));
+		s->stream.avail_in = s->mmap_end - pos;
+		if (s->stream.avail_in > (s->mmap_pos - pos))
+		    s->stream.avail_in = s->mmap_pos - pos;
+		for (n=0; n<s->stream.avail_in; n+=4096)
+		    ((volatile char *)s->inbuf)[n];
+	    }
 	}
+    }
+#endif
 
     if (!s->mmap_mode) {
 /*@-abstract@*/
@@ -225,8 +247,10 @@ local gzFile gz_open (const char *path, const char *mode, int fd)
     if (s->mode == 'w') {
         /* Write a very simple .gz header:
          */
+/*@-nullpass@*/ /* FIX: s->file may be NULL */
         fprintf(s->file, "%c%c%c%c%c%c%c%c%c%c", gz_magic[0], gz_magic[1],
              Z_DEFLATED, 0 /*flags*/, 0,0,0,0 /*time*/, 0 /*xflags*/, OS_CODE);
+/*@=nullpass@*/
 	s->startpos = 10L;
 	/* We use 10L instead of ftell(s->file) to because ftell causes an
          * fflush on some systems. This version of the library doesn't use
@@ -236,13 +260,16 @@ local gzFile gz_open (const char *path, const char *mode, int fd)
     } else {
 	check_header(s); /* skip the .gz header */
 	if (s->mmap_mode)
-		s->startpos = s->mmap_pos - s->stream.avail_in;
+	    s->startpos = s->mmap_pos - s->stream.avail_in;
 	else
-		s->startpos = (ftell(s->file) - s->stream.avail_in);
+/*@-nullpass@*/ /* FIX: s->file may be NULL */
+	    s->startpos = (ftell(s->file) - s->stream.avail_in);
+/*@=nullpass@*/
     }
     
     return (gzFile)s;
 }
+/*@=compmempass =compdef@*/
 
 /* ========================================================================= */
 /**
@@ -279,6 +306,7 @@ int ZEXPORT gzsetparams (gzFile file, int level, int strategy)
     if (s == NULL || s->mode != 'w') return Z_STREAM_ERROR;
 
     /* Make room to allow flushing */
+/*@-branchstate@*/
     if (s->stream.avail_out == 0) {
 
 	s->stream.next_out = s->outbuf;
@@ -287,10 +315,12 @@ int ZEXPORT gzsetparams (gzFile file, int level, int strategy)
 	}
 	s->stream.avail_out = z_bufsize;
     }
+/*@=branchstate@*/
 
     return deflateParams (&(s->stream), level, strategy);
 }
 
+#if defined(__i386__)
 static inline int gz_refill_inbuf(gz_stream *s)
 	/*@globals fileSystem @*/
 	/*@modifies *s, fileSystem @*/
@@ -310,7 +340,9 @@ static inline int gz_refill_inbuf(gz_stream *s)
 			s->z_err = errno;
 			return 1;
 		}
+#if defined(MADV_SEQUENTIAL)
 		(void) madvise(s->inbuf, z_bufsize, MADV_SEQUENTIAL);
+#endif
 		s->stream.next_in = s->inbuf;
 		s->stream.avail_in = z_bufsize;
 		s->mmap_pos += z_bufsize;
@@ -332,6 +364,7 @@ static inline int gz_refill_inbuf(gz_stream *s)
 	s->stream.next_in = s->inbuf;
 	return 0;
 }
+#endif
 
 /* ========================================================================= */
 /**
@@ -339,17 +372,31 @@ static inline int gz_refill_inbuf(gz_stream *s)
  * for end of file.
  * IN assertion: the stream s has been sucessfully opened for reading.
  */
+/*@-compmempass@*/
 local inline int get_byte(gz_stream *s)
 {
     if (s->z_eof) return EOF;
+/*@-branchstate@*/
     if (s->stream.avail_in == 0) {
 	errno = 0;
+#if defined(__i386__)
 	if(gz_refill_inbuf(s))
 	    return EOF;
+#else
+	s->stream.avail_in = fread(s->inbuf, 1, Z_BUFSIZE, s->file);
+	if (s->stream.avail_in == 0) {
+	    s->z_eof = 1;
+	    if (ferror(s->file)) s->z_err = Z_ERRNO;
+ 	    return EOF;
+	}
+	s->stream.next_in = s->inbuf;
+#endif
     }
+/*@=branchstate@*/
     s->stream.avail_in--;
     return *(s->stream.next_in)++;
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
@@ -414,6 +461,7 @@ local void check_header(gz_stream *s)
  * Cleanup then free the given gz_stream. Return a zlib error code.
  * Try freeing in the reverse order of allocations.
  */
+/*@-compdef@*/
 local int destroy (gz_stream *s)
 {
     int err = Z_OK;
@@ -422,14 +470,17 @@ local int destroy (gz_stream *s)
 
     TRYFREE(s->msg);
 
-	if (s->mmap_mode) {
-		if (s->inbuf)
-			munmap(s->inbuf, z_bufsize);
-		s->inbuf = NULL;
-		close(s->fd);
-		s->mmap_mode = 0;
-	}
+#if defined(__i386__)
+    if (s->mmap_mode) {
+	if (s->inbuf)
+	    munmap(s->inbuf, z_bufsize);
+	s->inbuf = NULL;
+	close(s->fd);
+	s->mmap_mode = 0;
+    }
+#endif
 
+/*@-branchstate@*/
     if (s->stream.state != NULL) {
 	if (s->mode == 'w') {
 #ifdef NO_DEFLATE
@@ -441,6 +492,7 @@ local int destroy (gz_stream *s)
 	    err = inflateEnd(&(s->stream));
 	}
     }
+/*@=branchstate@*/
     if (s->file != NULL && fclose(s->file)) {
 #ifdef ESPIPE
 	if (errno != ESPIPE) /* fclose is broken for pipes in HP/UX */
@@ -452,15 +504,20 @@ local int destroy (gz_stream *s)
     TRYFREE(s->inbuf);
     TRYFREE(s->outbuf);
     TRYFREE(s->path);
+/*@-branchstate@*/
     TRYFREE(s);
+/*@=branchstate@*/
     return err;
 }
+/*@=compdef@*/
 
 /* ========================================================================= */
 /**
  * Reads the given number of uncompressed bytes from the compressed file.
  * gzread returns the number of bytes actually read (0 for end of file).
  */
+/*@-compmempass@*/
+/*@-compdef@*/
 int ZEXPORT gzread (gzFile file, voidp buf, unsigned len)
 {
     gz_stream *s = (gz_stream*)file;
@@ -473,16 +530,21 @@ int ZEXPORT gzread (gzFile file, voidp buf, unsigned len)
     if (s->z_err == Z_STREAM_END) return 0;  /* EOF */
 
     next_out = (Byte*)buf;
+/*@-temptrans@*/
     s->stream.next_out = (Bytef*)buf;
+/*@=temptrans@*/
     s->stream.avail_out = len;
 
+/*@-branchstate@*/
     while (s->stream.avail_out != 0) {
 
 	if (s->transparent) {
 	    /* Copy first the lookahead bytes: */
 	    uInt n;
+#if defined(__i386__)
 again:
-		n = s->stream.avail_in;
+#endif
+	    n = s->stream.avail_in;
 	    if (n > s->stream.avail_out) n = s->stream.avail_out;
 	    if (n > 0) {
 		zmemcpy(s->stream.next_out, s->stream.next_in, n);
@@ -493,8 +555,13 @@ again:
 		s->stream.avail_in  -= n;
 	    }
 	    if (s->stream.avail_out > 0) {
+#if defined(__i386__)
 		if (!s->stream.avail_in && !gz_refill_inbuf(s))
 			goto again;
+#else
+		s->stream.avail_out -= fread(next_out, 1, s->stream.avail_out,
+					     s->file);
+#endif
 	    }
 	    len -= s->stream.avail_out;
 	    s->stream.total_in  += (uLong)len;
@@ -505,17 +572,39 @@ again:
         if (s->stream.avail_in == 0 && !s->z_eof) {
 
             errno = 0;
+#if defined(__i386__)
 	    if (gz_refill_inbuf(s))
 		break;
+#else
+	    s->stream.avail_in = fread(s->inbuf, 1, Z_BUFSIZE, s->file);
+	    if (s->stream.avail_in == 0) {
+		s->z_eof = 1;
+		if (ferror(s->file)) {
+		    s->z_err = Z_ERRNO;
+		    break;
+		}
+	    }
+	    s->stream.next_in = s->inbuf;
+#endif
         }
         s->z_err = inflate(&(s->stream), Z_NO_FLUSH);
 
 	if (s->z_err == Z_STREAM_END) {
 	    /* Check CRC and original size */
-	    start = s->stream.next_out;
 
-/*@-unrecog@*/
-	    if (getLong(s) != get_crc_from_partial(&s->stream.crc)) {
+#if defined(__i386__)
+	    start = s->stream.next_out;
+	    /*@-unrecog@*/
+	    if (getLong(s) != get_crc_from_partial(&s->stream.crc))
+	    /*@=unrecog@*/
+#else
+	    s->stream.crc = crc32(s->stream.crc, start, (uInt)(s->stream.next_out - start));
+	    start = s->stream.next_out;
+/*@-evalorder@*/
+	    if (getLong(s) != s->stream.crc)
+/*@=evalorder@*/
+#endif
+	    {
 		s->z_err = Z_DATA_ERROR;
 	    } else {
 	        (void)getLong(s);
@@ -532,16 +621,26 @@ again:
 		    s->stream.total_in = total_in;
 		    s->stream.total_out = total_out;
 		    s->stream.crc = /*crc32(0L, Z_NULL, 0)*/0;
-			partial_crc32_prep(&s->stream.crc);
+#if defined(__i386__)
+		    /*@-unrecog@*/
+		    partial_crc32_prep(&s->stream.crc);
+		    /*@=unrecog@*/
+#endif
 		}
 	    }
-/*@=unrecog@*/
 	}
 	if (s->z_err != Z_OK || s->z_eof) break;
     }
+/*@=branchstate@*/
+
+#if !defined(__i386__)
+    s->stream.crc = crc32(s->stream.crc, start, (uInt)(s->stream.next_out - start));
+#endif
 
     return (int)(len - s->stream.avail_out);
 }
+/*@=compdef@*/
+/*@=compmempass@*/
 
 
 /* ========================================================================= */
@@ -590,9 +689,13 @@ int ZEXPORT gzwrite (gzFile file, const voidp buf, unsigned len)
 
     if (s == NULL || s->mode != 'w') return Z_STREAM_ERROR;
 
+/*@-temptrans@*/
     s->stream.next_in = (Bytef*)buf;
+/*@=temptrans@*/
     s->stream.avail_in = len;
 
+/*@-infloops@*/
+/*@-branchstate@*/
     while (s->stream.avail_in != 0) {
 
         if (s->stream.avail_out == 0) {
@@ -607,7 +710,13 @@ int ZEXPORT gzwrite (gzFile file, const voidp buf, unsigned len)
         s->z_err = deflate(&(s->stream), Z_NO_FLUSH);
         if (s->z_err != Z_OK) break;
     }
+/*@=branchstate@*/
+/*@=infloops@*/
+#if defined(__i386__)
     s->stream.crc = partial_crc32(s->stream.crc, (const Bytef *)buf, len);
+#else
+    s->stream.crc = crc32(s->stream.crc, (const Bytef *)buf, len);
+#endif
 
     return (int)(len - s->stream.avail_in);
 }
@@ -703,6 +812,7 @@ local int do_flush (gzFile file, int flush)
 
     s->stream.avail_in = 0; /* should be zero already anyway */
 
+/*@-branchstate@*/
     for (;;) {
         len = z_bufsize - s->stream.avail_out;
 
@@ -727,6 +837,7 @@ local int do_flush (gzFile file, int flush)
  
         if (s->z_err != Z_OK && s->z_err != Z_STREAM_END) break;
     }
+/*@=branchstate@*/
     return  s->z_err == Z_STREAM_END ? Z_OK : s->z_err;
 }
 
@@ -771,13 +882,17 @@ z_off_t ZEXPORT gzseek (gzFile file, z_off_t offset, int whence)
 	/* At this point, offset is the number of zero bytes to write. */
 	if (s->inbuf == Z_NULL) {
 	    s->inbuf = (Byte*)ALLOC(z_bufsize); /* for seeking */
+/*@-nullpass@*/ /* FIX: s->inbuf may be NULL */
 	    zmemzero(s->inbuf, z_bufsize);
+/*@=nullpass@*/
 	}
 	while (offset > 0)  {
 	    uInt size = z_bufsize;
 	    if (offset < z_bufsize) size = (uInt)offset;
 
+/*@-nullpass@*/ /* FIX: s->inbuf may be NULL */
 	    size = gzwrite(file, s->inbuf, size);
+/*@=nullpass@*/
 	    if (size == 0) return -1L;
 
 	    offset -= size;
@@ -818,7 +933,9 @@ z_off_t ZEXPORT gzseek (gzFile file, z_off_t offset, int whence)
 	int size = z_bufsize;
 	if (offset < z_bufsize) size = (int)offset;
 
+/*@-nullpass@*/ /* FIX: s->outbuf may be NULL */
 	size = gzread(file, s->outbuf, (uInt)size);
+/*@=nullpass@*/
 	if (size <= 0) return -1L;
 	offset -= size;
     }
@@ -839,8 +956,10 @@ int ZEXPORT gzrewind (gzFile file)
     s->z_eof = 0;
     s->stream.avail_in = 0;
     s->stream.next_in = s->inbuf;
-    s->stream.crc = 0;
-	partial_crc32_prep(&s->stream.crc);
+    s->stream.crc = /*crc32(0L, Z_NULL, 0)*/0;
+#if defined(__i386__)
+    partial_crc32_prep(&s->stream.crc);
+#endif
 	
     if (s->startpos == 0) { /* not a compressed file */
 	rewind(s->file);
@@ -924,7 +1043,12 @@ int ZEXPORT gzclose (gzFile file)
         err = do_flush (file, Z_FINISH);
         if (err != Z_OK) return destroy((gz_stream*)file);
 
+#if defined(__i386__)
         putLong (s->file, get_crc_from_partial(&s->stream.crc));
+#else
+	putLong (s->file, s->stream.crc);
+#endif
+
         putLong (s->file, s->stream.total_in);
 #endif
     }
@@ -939,6 +1063,7 @@ int ZEXPORT gzclose (gzFile file)
  * errnum is set to Z_ERRNO and the application may consult errno
  * to get the exact error code.
  */
+/*@-compmempass@*/
 const char*  ZEXPORT gzerror (gzFile file, int *errnum)
 {
     char *m;
@@ -953,12 +1078,19 @@ const char*  ZEXPORT gzerror (gzFile file, int *errnum)
 
     m =  (char*)(*errnum == Z_ERRNO ? zstrerror(errno) : s->stream.msg);
 
+/*@-branchstate@*/
     if (m == NULL || *m == '\0') m = (char*)ERR_MSG(s->z_err);
+/*@=branchstate@*/
 
     TRYFREE(s->msg);
     s->msg = (char*)ALLOC(strlen(s->path) + strlen(m) + 3);
+    if (s->msg == NULL) {
+        *errnum = Z_MEM_ERROR;
+        return (const char*)ERR_MSG(Z_MEM_ERROR);
+    }
     strcpy(s->msg, s->path);
     strcat(s->msg, ": ");
     strcat(s->msg, m);
     return (const char*)s->msg;
 }
+/*@=compmempass@*/
diff --git a/zlib/infblock.c b/zlib/infblock.c
index 63bb78739..f7fe4dc2a 100644
--- a/zlib/infblock.c
+++ b/zlib/infblock.c
@@ -17,15 +17,14 @@
 //#include "infutil.c"
 #include "inffast.h"
 
-#if 0
-struct inflate_codes_state {int dummy;}; /* for buggy compilers */
-#endif
+/*@access z_streamp@*/
 
 /* simplify the use of the inflate_huft type with some defines */
 #define exop word.what.Exop
 #define bits word.what.Bits
 
 /* Table for deflate from PKZIP's appnote.txt. */
+/*@observer@*/ /*@unchecked@*/
 local const uInt border[] = { /* Order of the bit length code lengths */
         16, 17, 18, 0, 8, 7, 9, 6, 10, 5, 11, 4, 12, 3, 13, 2, 14, 1, 15};
 
@@ -81,8 +80,12 @@ void inflate_blocks_reset(inflate_blocks_statef *s, z_streamp z, uLongf *c)
     *c = s->check;
   if (s->mode == BTREE || s->mode == DTREE)
     ZFREE(z, s->sub.trees.blens);
-  if (s->mode == CODES)
+  if (s->mode == CODES) {
+/*@-noeffect@*/
     inflate_codes_free(s->sub.decode.codes, z);
+/*@=noeffect@*/
+    s->sub.decode.codes = NULL;
+  }
   s->mode = TYPE;
   s->bitk = 0;
   s->bitb = 0;
@@ -121,6 +124,7 @@ inflate_blocks_statef *inflate_blocks_new(z_streamp z, check_func c, uInt w)
 }
 
 
+/*@-compmempass@*/
 int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
 {
   uInt t;               /* temporary storage */
@@ -177,8 +181,10 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
           /*@innerbreak@*/ break;
         case 3:                         /* illegal */
           DUMPBITS(3)
+/*@-type@*/
           s->mode = BAD;
-          z->msg = (char*)"invalid block type";
+/*@=type@*/
+          z->msg = "invalid block type";
           r = Z_DATA_ERROR;
           goto leave;
       }
@@ -187,8 +193,10 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
       NEEDBITS(32)
       if ((((~b) >> 16) & 0xffff) != (b & 0xffff))
       {
+/*@-type@*/
         s->mode = BAD;
-        z->msg = (char*)"invalid stored block lengths";
+/*@=type@*/
+        z->msg = "invalid stored block lengths";
         r = Z_DATA_ERROR;
         goto leave;
       }
@@ -220,8 +228,10 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
 #ifndef PKZIP_BUG_WORKAROUND
       if ((t & 0x1f) > 29 || ((t >> 5) & 0x1f) > 29)
       {
+/*@-type@*/
         s->mode = BAD;
-        z->msg = (char*)"too many length or distance symbols";
+/*@=type@*/
+        z->msg = "too many length or distance symbols";
         r = Z_DATA_ERROR;
         goto leave;
       }
@@ -254,7 +264,9 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
         r = t;
         if (r == Z_DATA_ERROR) {
 	  ZFREE(z, s->sub.trees.blens);
+/*@-type@*/
           s->mode = BAD;
+/*@=type@*/
 	}
         goto leave;
       }
@@ -293,8 +305,10 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
               (c == 16 && i < 1))
           {
             ZFREE(z, s->sub.trees.blens);
+/*@-type@*/
             s->mode = BAD;
-            z->msg = (char*)"invalid bit length repeat";
+/*@=type@*/
+            z->msg = "invalid bit length repeat";
             r = Z_DATA_ERROR;
             goto leave;
           }
@@ -321,7 +335,9 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
         {
           if (t == (uInt)Z_DATA_ERROR) {
 	    ZFREE(z, s->sub.trees.blens);
+/*@-type@*/
             s->mode = BAD;
+/*@=type@*/
 	  }
           r = t;
           goto leave;
@@ -342,7 +358,10 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
       if ((r = inflate_codes(s, z, r)) != Z_STREAM_END)
         return inflate_flush(s, z, r);
       r = Z_OK;
+/*@-noeffect@*/
       inflate_codes_free(s->sub.decode.codes, z);
+/*@=noeffect@*/
+      s->sub.decode.codes = NULL;
       LOAD
       Tracev((stderr, "inflate:       codes end, %lu total out\n",
               z->total_out + (q >= s->read ? q - s->read :
@@ -358,7 +377,9 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
       FLUSH
       if (s->read != s->write)
         goto leave;
+/*@-type@*/
       s->mode = DONE;
+/*@=type@*/
       /*@fallthrough@*/
     case DONE:
       r = Z_STREAM_END;
@@ -374,6 +395,7 @@ int inflate_blocks(inflate_blocks_statef *s, z_streamp z, int r)
 leave:
 	LEAVE
 }
+/*@=compmempass@*/
 
 
 int inflate_blocks_free(inflate_blocks_statef *s, z_streamp z)
@@ -389,7 +411,9 @@ int inflate_blocks_free(inflate_blocks_statef *s, z_streamp z)
 
 void inflate_set_dictionary(inflate_blocks_statef *s, const Bytef *d, uInt n)
 {
+/*@-mayaliasunique@*/ /* FIX: d may alias s->window */
   zmemcpy(s->window, d, n);
+/*@=mayaliasunique@*/
   s->read = s->write = s->window + n;
 }
 
@@ -434,6 +458,7 @@ inflate_codes_statef *inflate_codes_new(uInt bl, uInt bd, inflate_huft *tl, infl
 }
 
 
+/*@-compmempass@*/
 int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
 {
   uInt j;               /* temporary storage */
@@ -456,6 +481,7 @@ int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
   {             /* waiting for "i:"=input, "o:"=output, "x:"=nothing */
     case START:         /* x: set up for LEN */
 #ifndef SLOW
+/*@-branchstate@*/
       if (m >= 258 && n >= 10)
       {
         UPDATE
@@ -467,6 +493,7 @@ int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
           /*@switchbreak@*/ break;
         }
       }
+/*@=branchstate@*/
 #endif /* !SLOW */
       c->sub.code.need = c->lbits;
       c->sub.code.tree = c->ltree;
@@ -507,7 +534,7 @@ int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
         /*@switchbreak@*/ break;
       }
       c->mode = BADCODE;        /* invalid code */
-      z->msg = (char*)"invalid literal/length code";
+      z->msg = "invalid literal/length code";
       r = Z_DATA_ERROR;
       goto leave;
     case LENEXT:        /* i: getting length extra (have base) */
@@ -540,7 +567,7 @@ int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
         /*@switchbreak@*/ break;
       }
       c->mode = BADCODE;        /* invalid code */
-      z->msg = (char*)"invalid distance code";
+      z->msg = "invalid distance code";
       r = Z_DATA_ERROR;
       goto leave;
     case DISTEXT:       /* i: getting distance extra */
@@ -606,6 +633,7 @@ int inflate_codes(inflate_blocks_statef *s, z_streamp z, int r)
 leave:
 	LEAVE
 }
+/*@=compmempass@*/
 
 
 void inflate_codes_free(inflate_codes_statef *c, z_streamp z)
diff --git a/zlib/infblock.h b/zlib/infblock.h
index 90504ec57..a5143d9d7 100644
--- a/zlib/infblock.h
+++ b/zlib/infblock.h
@@ -16,28 +16,29 @@
 struct inflate_blocks_state;
 typedef struct inflate_blocks_state FAR inflate_blocks_statef;
 
+/*@null@*/
 extern inflate_blocks_statef * inflate_blocks_new OF((
     z_streamp z,
-    check_func c,               /* check function */
+    /*@null@*/ check_func c,    /* check function */
     uInt w))                    /* window size */
-	/*@*/;
+	/*@modifies z @*/;
 
 extern int inflate_blocks OF((
     inflate_blocks_statef *s,
     z_streamp z,
     int r))                       /* initial return code */
-	/*@modifies s @*/;
+	/*@modifies s, z @*/;
 
 extern void inflate_blocks_reset OF((
     inflate_blocks_statef *s,
     z_streamp z,
-    uLongf *c))                   /* check value on output */
-	/*@modifies s, *c @*/;
+    /*@null@*/ uLongf *c))                   /* check value on output */
+	/*@modifies s, *c, z @*/;
 
 extern int inflate_blocks_free OF((
-    inflate_blocks_statef *s,
+    /*@only@*/ inflate_blocks_statef *s,
     z_streamp z)) 
-	/*@modifies s @*/;
+	/*@modifies s, z @*/;
 
 extern void inflate_set_dictionary OF((
     inflate_blocks_statef *s,
diff --git a/zlib/infcodes.h b/zlib/infcodes.h
index 32afc9253..aff80598b 100644
--- a/zlib/infcodes.h
+++ b/zlib/infcodes.h
@@ -35,6 +35,7 @@ struct inflate_codes_state {
   uInt len;
   union {
     struct {
+/*@dependent@*/
       inflate_huft *tree;       /*!< pointer into tree */
       uInt need;                /*!< bits needed */
     } code;             /*!< if LEN or DIST, where in tree */
@@ -48,16 +49,19 @@ struct inflate_codes_state {
   /* mode independent information */
   Byte lbits;           /*!< ltree bits decoded per branch */
   Byte dbits;           /*!< dtree bits decoder per branch */
+/*@dependent@*/
   inflate_huft *ltree;          /*!< literal/length/eob tree */
+/*@dependent@*/
   inflate_huft *dtree;          /*!< distance tree */
 
 };
 
 typedef struct inflate_codes_state FAR inflate_codes_statef;
 
+/*@null@*/
 extern inflate_codes_statef *inflate_codes_new OF((
     uInt bl, uInt bd,
-    inflate_huft *tl, inflate_huft *td,
+    /*@dependent@*/ inflate_huft *tl, /*@dependent@*/ inflate_huft *td,
     z_streamp z))
 	/*@*/;
 
@@ -65,10 +69,10 @@ extern int inflate_codes OF((
     inflate_blocks_statef *s,
     z_streamp z,
     int r))
-	/*@modifies s @*/;
+	/*@modifies s, z @*/;
 
 extern void inflate_codes_free OF((
-    inflate_codes_statef *s,
+    /*@only@*/ inflate_codes_statef *s,
     z_streamp z))
-	/*@modifies s @*/;
+	/*@*/;
 
diff --git a/zlib/inffast.c b/zlib/inffast.c
index 5ec2687e0..0124d1b35 100644
--- a/zlib/inffast.c
+++ b/zlib/inffast.c
@@ -16,6 +16,8 @@
 #include "inffast.h"
 #include "crc32.h"
 
+/*@access z_streamp@*/
+
 /* simplify the use of the inflate_huft type with some defines */
 #define exop word.what.Exop
 #define bits word.what.Bits
@@ -55,10 +57,12 @@ int ret;
   /* load input, output, bit values */
   LOAD
 
+#if defined(__i386__)
 /*@-unrecog@*/
   PREFETCH(p);
   PREFETCH(p+32);
 /*@=unrecog@*/
+#endif
   /* initialize masks */
   ml = inflate_mask[bl];
   md = inflate_mask[bd];
@@ -66,9 +70,11 @@ int ret;
   /* do until not enough input or output space for fast loop */
   do {                          /* assume called with m >= 258 && n >= 10 */
     /* get literal/length code */
+#if defined(__i386__)
 /*@-unrecog@*/
     PREFETCH(p+64);
 /*@=unrecog@*/
+#endif
     GRABBITS(20)                /* max bits for literal/length code */
     if ((e = (t = tl + ((uInt)b & ml))->exop) == 0)
     {
@@ -198,7 +204,7 @@ ungrab:
 
 data_error:
       {
-        z->msg = (char*)"invalid literal/length code";
+        z->msg = "invalid literal/length code";
         ret = Z_DATA_ERROR;
 	goto ungrab;
       }
@@ -212,7 +218,7 @@ stream_end:
 
 inv_dist_code:
           {
-            z->msg = (char*)"invalid distance code";
+            z->msg = "invalid distance code";
             ret = Z_DATA_ERROR;
 	    goto ungrab;
           }
diff --git a/zlib/inffast.h b/zlib/inffast.h
index 6d908a00f..15c810aea 100644
--- a/zlib/inffast.h
+++ b/zlib/inffast.h
@@ -15,4 +15,4 @@
 extern int inflate_fast OF((
     inflate_blocks_statef * s,
     z_streamp z))  // __attribute__((regparm(3)));
-	/*@modifies s @*/;
+	/*@modifies s, z @*/;
diff --git a/zlib/inffixed.h b/zlib/inffixed.h
index 6fa3b2965..7b71e5eaa 100644
--- a/zlib/inffixed.h
+++ b/zlib/inffixed.h
@@ -9,8 +9,11 @@
    subject to change. Applications should only use zlib.h.
  */
 
+/*@unchecked@*/
 local uInt fixed_bl = 9;
+/*@unchecked@*/
 local uInt fixed_bd = 5;
+/*@unchecked@*/
 local inflate_huft fixed_tl[] = {
     {{{96,7}},256}, {{{0,8}},80}, {{{0,8}},16}, {{{84,8}},115},
     {{{82,7}},31}, {{{0,8}},112}, {{{0,8}},48}, {{{0,9}},192},
@@ -141,6 +144,7 @@ local inflate_huft fixed_tl[] = {
     {{{82,7}},27}, {{{0,8}},111}, {{{0,8}},47}, {{{0,9}},191},
     {{{0,8}},15}, {{{0,8}},143}, {{{0,8}},79}, {{{0,9}},255}
   };
+/*@unchecked@*/
 local inflate_huft fixed_td[] = {
     {{{80,5}},1}, {{{87,5}},257}, {{{83,5}},17}, {{{91,5}},4097},
     {{{81,5}},5}, {{{89,5}},1025}, {{{85,5}},65}, {{{93,5}},16385},
diff --git a/zlib/inflate.c b/zlib/inflate.c
index 6ede5f7ce..8608b1eca 100644
--- a/zlib/inflate.c
+++ b/zlib/inflate.c
@@ -10,7 +10,7 @@
 #include "zutil.h"
 #include "infblock.h"
 
-struct inflate_blocks_state {int dummy;}; /* for buggy compilers */
+/*@access z_streamp@*/
 
 typedef enum {
       METHOD,	/*!< waiting for method byte */
@@ -30,6 +30,7 @@ typedef enum {
 } inflate_mode;
 
 /** inflate private state */
+/*@-redef@*/ /* FIX: deflate.h has duplicate */
 struct internal_state {
 
   /* mode */
@@ -52,6 +53,7 @@ struct internal_state {
     *blocks;            /*!< current inflate_blocks state */
 
 };
+/*@=redef@*/
 
 
 int ZEXPORT inflateReset(z_streamp z)
@@ -71,8 +73,12 @@ int ZEXPORT inflateEnd(z_streamp z)
 {
   if (z == Z_NULL || z->state == Z_NULL || z->zfree == Z_NULL)
     return Z_STREAM_ERROR;
+/*@-usereleased@*/
+/*@-compdef@*/ /* FIX: z->state->blocks may be undefined */
   if (z->state->blocks != Z_NULL)
     inflate_blocks_free(z->state->blocks, z);
+/*@=compdef@*/
+/*@=usereleased@*/
   ZFREE(z, z->state);
   z->state = Z_NULL;
   Tracev((stderr, "inflate: end\n"));
@@ -118,6 +124,7 @@ int ZEXPORT inflateInit2_(z_streamp z, int w, const char *version, int stream_si
   z->state->wbits = (uInt)w;
 
   /* create inflate_blocks state */
+/*@-evalorder -type@*/
   if ((z->state->blocks =
       inflate_blocks_new(z, z->state->nowrap ? Z_NULL : adler32, (uInt)1 << w))
       == Z_NULL)
@@ -125,6 +132,7 @@ int ZEXPORT inflateInit2_(z_streamp z, int w, const char *version, int stream_si
     inflateEnd(z);
     return Z_MEM_ERROR;
   }
+/*@=evalorder =type@*/
   Tracev((stderr, "inflate: allocated\n"));
 
   /* reset state */
@@ -159,14 +167,14 @@ int ZEXPORT inflate(z_streamp z, int f)
       if (((z->state->sub.method = NEXTBYTE) & 0xf) != Z_DEFLATED)
       {
         z->state->mode = BAD;
-        z->msg = (char*)"unknown compression method";
+        z->msg = "unknown compression method";
         z->state->sub.marker = 5;       /* can't try inflateSync */
         /*@switchbreak@*/ break;
       }
       if ((z->state->sub.method >> 4) + 8 > z->state->wbits)
       {
         z->state->mode = BAD;
-        z->msg = (char*)"invalid window size";
+        z->msg = "invalid window size";
         z->state->sub.marker = 5;       /* can't try inflateSync */
         /*@switchbreak@*/ break;
       }
@@ -178,7 +186,7 @@ int ZEXPORT inflate(z_streamp z, int f)
       if (((z->state->sub.method << 8) + b) % 31)
       {
         z->state->mode = BAD;
-        z->msg = (char*)"incorrect header check";
+        z->msg = "incorrect header check";
         z->state->sub.marker = 5;       /* can't try inflateSync */
         /*@switchbreak@*/ break;
       }
@@ -213,7 +221,7 @@ int ZEXPORT inflate(z_streamp z, int f)
       return Z_NEED_DICT;
     case DICT0:
       z->state->mode = BAD;
-      z->msg = (char*)"need dictionary";
+      z->msg = "need dictionary";
       z->state->sub.marker = 0;       /* can try inflateSync */
       return Z_STREAM_ERROR;
     case BLOCKS:
@@ -259,7 +267,7 @@ int ZEXPORT inflate(z_streamp z, int f)
       if (z->state->sub.check.was != z->state->sub.check.need)
       {
         z->state->mode = BAD;
-        z->msg = (char*)"incorrect data check";
+        z->msg = "incorrect data check";
         z->state->sub.marker = 5;       /* can't try inflateSync */
         /*@switchbreak@*/ break;
       }
@@ -303,6 +311,7 @@ int ZEXPORT inflateSetDictionary(z_streamp z, const Bytef *dictionary, uInt dict
 }
 
 
+/*@-compmempass@*/
 int ZEXPORT inflateSync(z_streamp z)
 {
   uInt n;       /* number of bytes to look at */
@@ -351,6 +360,7 @@ int ZEXPORT inflateSync(z_streamp z)
   z->state->mode = BLOCKS;
   return Z_OK;
 }
+/*@=compmempass@*/
 
 
 /**
diff --git a/zlib/inftrees.c b/zlib/inftrees.c
index fd089d017..6af13261f 100644
--- a/zlib/inftrees.c
+++ b/zlib/inftrees.c
@@ -41,42 +41,49 @@
 #include "zutil.h"
 #include "inftrees.h"
 
+/*@access z_streamp@*/
+
 #if !defined(BUILDFIXED) && !defined(STDC)
 #  define BUILDFIXED   /* non ANSI compilers may not accept inffixed.h */
 #endif
 
-/*@observer@*/
+/**
+ * If you use the zlib library in a product, an acknowledgment is welcome
+ * in the documentation of your product. If for some reason you cannot
+ * include such an acknowledgment, I would appreciate that you keep this
+ * copyright string in the executable of your product.
+ */
+/*@-exportheadervar@*/
+/*@unused@*/ /*@observer@*/
 const char inflate_copyright[] =
    " inflate 1.1.3 Copyright 1995-1998 Mark Adler ";
-/*
-  If you use the zlib library in a product, an acknowledgment is welcome
-  in the documentation of your product. If for some reason you cannot
-  include such an acknowledgment, I would appreciate that you keep this
-  copyright string in the executable of your product.
- */
-struct internal_state  {int dummy;}; /* for buggy compilers */
+/*@=exportheadervar@*/
 
 /* simplify the use of the inflate_huft type with some defines */
 #define exop word.what.Exop
 #define bits word.what.Bits
 
-local int huft_build(uIntf *b, uInt n, uInt s, const uIntf *d,
-		const uIntf *e, inflate_huft * FAR *t, uIntf *m,
-		inflate_huft *hp, uInt *hn, uIntf *v)
+local int huft_build(uIntf *b, uInt n, uInt s, /*@null@*/ const uIntf *d,
+		/*@null@*/ const uIntf *e, /*@out@*/ inflate_huft * FAR *t,
+		uIntf *m, inflate_huft *hp, uInt *hn, uIntf *v)
 	/*@modifies *t, *m, *hp, *hn, *v @*/;
 
 /* Tables for deflate from PKZIP's appnote.txt. */
+/*@observer@*/ /*@unchecked@*/
 local const uInt cplens[31] = { /* Copy lengths for literal codes 257..285 */
         3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31,
         35, 43, 51, 59, 67, 83, 99, 115, 131, 163, 195, 227, 258, 0, 0};
         /* see note #13 above about 258 */
+/*@observer@*/ /*@unchecked@*/
 local const uInt cplext[31] = { /* Extra bits for literal codes 257..285 */
         0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2,
         3, 3, 3, 3, 4, 4, 4, 4, 5, 5, 5, 5, 0, 112, 112}; /* 112==invalid */
+/*@observer@*/ /*@unchecked@*/
 local const uInt cpdist[30] = { /* Copy offsets for distance codes 0..29 */
         1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193,
         257, 385, 513, 769, 1025, 1537, 2049, 3073, 4097, 6145,
         8193, 12289, 16385, 24577};
+/*@observer@*/ /*@unchecked@*/
 local const uInt cpdext[30] = { /* Extra bits for distance codes */
         0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6,
         7, 7, 8, 8, 9, 9, 10, 10, 11, 11,
@@ -166,11 +173,13 @@ local int huft_build(uIntf *b, uInt n, uInt s, const uIntf *d,
 
 
   /* Adjust last length count to fill out codes, if needed */
+/*@-unsignedcompare@*/
   for (y = 1 << j; j < i; j++, y <<= 1)
     if ((y -= c[j]) < 0)
       return Z_DATA_ERROR;
   if ((y -= c[i]) < 0)
     return Z_DATA_ERROR;
+/*@=unsignedcompare@*/
   c[i] += y;
 
 
@@ -261,14 +270,20 @@ local int huft_build(uIntf *b, uInt n, uInt s, const uIntf *d,
       }
       else
       {
+/*@-nullderef@*/ /* FIX: d and e might be NULL */
         r.exop = (Byte)(e[*p - s] + 16 + 64);/* non-simple--look up in lists */
         r.base = d[*p++ - s];
+/*@=nullderef@*/
       }
 
       /* fill code-like entries with r */
       f = 1 << (k - w);
+/*@-nullderef@*/ /* FIX: q might be NULL */
+/*@-compdef@*/ /* FIX: r.base may be undefined */
       for (j = i >> w; j < z; j += f)
         q[j] = r;
+/*@=compdef@*/
+/*@=nullderef@*/
 
       /* backwards increment the k-bit code i */
       for (j = 1 << (k - 1); i & j; j >>= 1)
@@ -311,10 +326,10 @@ int inflate_trees_bits( uIntf *c, uIntf *bb, inflate_huft * FAR *tb,
   r = huft_build(c, 19, 19, (uIntf*)Z_NULL, (uIntf*)Z_NULL,
                  tb, bb, hp, &hn, v);
   if (r == Z_DATA_ERROR)
-    z->msg = (char*)"oversubscribed dynamic bit lengths tree";
+    z->msg = "oversubscribed dynamic bit lengths tree";
   else if (r == Z_BUF_ERROR || *bb == 0)
   {
-    z->msg = (char*)"incomplete dynamic bit lengths tree";
+    z->msg = "incomplete dynamic bit lengths tree";
     r = Z_DATA_ERROR;
   }
   ZFREE(z, v);
@@ -350,10 +365,10 @@ int inflate_trees_dynamic( uInt nl, uInt nd, uIntf *c, uIntf *bl,
   if (r != Z_OK || *bl == 0)
   {
     if (r == Z_DATA_ERROR)
-      z->msg = (char*)"oversubscribed literal/length tree";
+      z->msg = "oversubscribed literal/length tree";
     else if (r != Z_MEM_ERROR)
     {
-      z->msg = (char*)"incomplete literal/length tree";
+      z->msg = "incomplete literal/length tree";
       r = Z_DATA_ERROR;
     }
     ZFREE(z, v);
@@ -365,18 +380,18 @@ int inflate_trees_dynamic( uInt nl, uInt nd, uIntf *c, uIntf *bl,
   if (r != Z_OK || (*bd == 0 && nl > 257))
   {
     if (r == Z_DATA_ERROR)
-      z->msg = (char*)"oversubscribed distance tree";
+      z->msg = "oversubscribed distance tree";
     else if (r == Z_BUF_ERROR) {
 #ifdef PKZIP_BUG_WORKAROUND
       r = Z_OK;
     }
 #else
-      z->msg = (char*)"incomplete distance tree";
+      z->msg = "incomplete distance tree";
       r = Z_DATA_ERROR;
     }
     else if (r != Z_MEM_ERROR)
     {
-      z->msg = (char*)"empty distance tree with lengths";
+      z->msg = "empty distance tree with lengths";
       r = Z_DATA_ERROR;
     }
     ZFREE(z, v);
diff --git a/zlib/inftrees.h b/zlib/inftrees.h
index 8463da401..331d17794 100644
--- a/zlib/inftrees.h
+++ b/zlib/inftrees.h
@@ -44,7 +44,7 @@ extern int inflate_trees_bits OF((
     inflate_huft * FAR *tb,	/* bits tree result */
     inflate_huft *hp,		/* space for trees */
     z_streamp z))		/* for messages */
-	/*@modifies *bb, *tb, *hp @*/;
+	/*@modifies *bb, *tb, *hp, z @*/;
 
 extern int inflate_trees_dynamic OF((
     uInt nl,			/* number of literal/length codes */
@@ -52,16 +52,22 @@ extern int inflate_trees_dynamic OF((
     uIntf *c,			/* that many (total) code lengths */
     uIntf *bl,			/* literal desired/actual bit depth */
     uIntf *bd,			/* distance desired/actual bit depth */
+/*@out@*/
     inflate_huft * FAR *tl,	/* literal/length tree result */
+/*@out@*/
     inflate_huft * FAR *td,	/* distance tree result */
     inflate_huft *hp,		/* space for trees */
     z_streamp z))		/* for messages */
-	/*@modifies *bl, *bd, *tl, *td, *hp @*/;
+	/*@modifies *bl, *bd, *tl, *td, *hp, z @*/;
 
 extern int inflate_trees_fixed OF((
+/*@out@*/
     uIntf *bl,			/* literal desired/actual bit depth */
+/*@out@*/
     uIntf *bd,			/* distance desired/actual bit depth */
+/*@out@*/
     inflate_huft * FAR *tl,	/* literal/length tree result */
+/*@out@*/
     inflate_huft * FAR *td,	/* distance tree result */
     z_streamp z))		/* for memory allocation */
-	/*@modifies *bl, *bd, *tl, *td @*/;
+	/*@modifies *bl, *bd, *tl, *td, z @*/;
diff --git a/zlib/infutil.c b/zlib/infutil.c
index 13739b5a0..b3d131086 100644
--- a/zlib/infutil.c
+++ b/zlib/infutil.c
@@ -17,6 +17,8 @@
 
 #include "crc32.h"
 
+/*@access z_streamp@*/
+
 /* And'ing with mask[n] masks the lower n bits */
 uInt inflate_mask[17] = {
     0x0000,
@@ -49,6 +51,7 @@ int inflate_flush(inflate_blocks_statef *s, z_streamp z, int r)
 
   /* update check information */
 /*@-moduncon@*/
+#if defined(__i386__)
   if (s->checkfn == Z_NULL)
     z->crc = partial_crc32_copy(z->crc, q, n, p);
   else if (s->checkfn != Z_NULL) {
@@ -58,6 +61,13 @@ int inflate_flush(inflate_blocks_statef *s, z_streamp z, int r)
     /* copy as far as end of window */
     zmemcpy(p, q, n);
   }
+#else
+  if (s->checkfn != Z_NULL)
+    z->adler = s->check = (*s->checkfn)(s->check, q, n);
+
+  /* copy as far as end of window */
+  zmemcpy(p, q, n);
+#endif
 
   p += n;
   q += n;
@@ -80,18 +90,28 @@ int inflate_flush(inflate_blocks_statef *s, z_streamp z, int r)
     z->total_out += n;
 
     /* update check information */
+#if defined(__i386__)
 /*@-moduncon@*/
     if (!s->checkfn)
 	z->crc = partial_crc32_copy(z->crc, q, n, p);
     else if (s->checkfn != Z_NULL) {
       z->adler = s->check = (*s->checkfn)(s->check, q, n);
 /*@=moduncon@*/
-
       /* copy */
 /*@-aliasunique@*/
       zmemcpy(p, q, n);
 /*@=aliasunique@*/
     }
+#else
+    if (s->checkfn != Z_NULL)
+      z->adler = s->check = (*s->checkfn)(s->check, q, n);
+
+    /* copy */
+/*@-aliasunique@*/
+    zmemcpy(p, q, n);
+/*@=aliasunique@*/
+#endif
+
     p += n;
     q += n;
   }
diff --git a/zlib/infutil.h b/zlib/infutil.h
index a38457b4c..a03b04067 100644
--- a/zlib/infutil.h
+++ b/zlib/infutil.h
@@ -25,8 +25,10 @@ typedef enum {
       DTREE,	/*!< get length, distance trees for a dynamic block */
       CODES,	/*!< processing fixed or dynamic block */
       DRY,	/*!< output remaining window bytes */
+/*@-redef@*/ /* FIX: inflate .c has duplicates */
       DONE,	/*!< finished last block, done */
       BAD	/*!< got a data error--stuck here */
+/*@=redef@*/
 } inflate_block_mode;
 
 /* inflate blocks semi-private state */
@@ -55,11 +57,17 @@ struct inflate_blocks_state {
   /* mode independent information */
   uInt bitk;            /*!< bits in bit buffer */
   uLong bitb;           /*!< bit buffer */
+/*@only@*/
   inflate_huft *hufts;  /*!< single malloc for tree space */
+/*@owned@*/
   Bytef *window;        /*!< sliding window */
+/*@dependent@*/
   Bytef *end;           /*!< one byte after sliding window */
+/*@dependent@*/
   Bytef *read;          /*!< window read pointer */
+/*@dependent@*/
   Bytef *write;         /*!< window write pointer */
+/*@null@*/
   check_func checkfn;   /*!< check function */
   uLong check;          /*!< check on output */
 
@@ -95,15 +103,17 @@ struct inflate_blocks_state {
 #define LOAD {LOADIN LOADOUT}
 
 /* masks for lower bits (size given to avoid silly warnings with Visual C++) */
+/*@unchecked@*/
 extern uInt inflate_mask[17];
 
 /* copy as much as possible from the sliding window to the output area */
 int inflate_flush OF((
     inflate_blocks_statef *s,
     z_streamp z,
-    int r)) __attribute__((regparm(3)))
-	/*@modifies s @*/;
-
-struct internal_state      {int dummy;}; /* for buggy compilers */
+    int r))
+#if defined(__i386__)
+      __attribute__((regparm(3)))
+#endif
+	/*@modifies s, z @*/;
 
 #endif
diff --git a/zlib/trees.c b/zlib/trees.c
index c8bf1278c..09a988f8d 100644
--- a/zlib/trees.c
+++ b/zlib/trees.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: trees.c,v 1.4 2001/12/08 17:12:13 jbj Exp $ */
+/* @(#) $Id: trees.c,v 1.5 2001/12/27 21:00:18 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -61,15 +61,19 @@
 #define REPZ_11_138  18
 /*!< repeat a zero length 11-138 times  (7 bits of repeat count) */
 
+/*@observer@*/ /*@unchecked@*/
 local const int extra_lbits[LENGTH_CODES] /* extra bits for each length code */
    = {0,0,0,0,0,0,0,0,1,1,1,1,2,2,2,2,3,3,3,3,4,4,4,4,5,5,5,5,0};
 
+/*@observer@*/ /*@unchecked@*/
 local const int extra_dbits[D_CODES] /* extra bits for each distance code */
    = {0,0,0,0,1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9,10,10,11,11,12,12,13,13};
 
+/*@observer@*/ /*@unchecked@*/
 local const int extra_blbits[BL_CODES]/* extra bits for each bit length code */
    = {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,3,7};
 
+/*@observer@*/ /*@unchecked@*/
 local const uch bl_order[BL_CODES]
    = {16,17,18,0,8,7,9,6,10,5,11,4,12,3,13,2,14,1,15};
 /*!< The lengths of the bit length codes are sent in order of decreasing
@@ -111,9 +115,11 @@ uch _dist_code[DIST_CODE_LEN];
 uch _length_code[MAX_MATCH-MIN_MATCH+1];
 /*!< length code for each normalized match length (0 == MIN_MATCH) */
 
+/*@unchecked@*/
 local int base_length[LENGTH_CODES];
 /*!< First normalized length for each code (0 = MIN_MATCH) */
 
+/*@unchecked@*/
 local int base_dist[D_CODES];
 /*!< First normalized distance for each code (0 = distance of 1) */
 
@@ -122,21 +128,24 @@ local int base_dist[D_CODES];
 #endif /* GEN_TREES_H */
 
 struct static_tree_desc_s {
-/*@null@*/
+/*@observer@*/ /*@null@*/
     const ct_data *static_tree;  /*!< static tree or NULL */
-/*@null@*/
+/*@observer@*/ /*@null@*/
     const intf *extra_bits;      /*!< extra bits for each code or NULL */
     int     extra_base;          /*!< base index for extra_bits */
     int     elems;               /*!< max number of elements in the tree */
     int     max_length;          /*!< max bit length for the codes */
 };
 
+/*@observer@*/ /*@unchecked@*/
 local static_tree_desc  static_l_desc =
 {static_ltree, extra_lbits, LITERALS+1, L_CODES, MAX_BITS};
 
+/*@observer@*/ /*@unchecked@*/
 local static_tree_desc  static_d_desc =
 {static_dtree, extra_dbits, 0,          D_CODES, MAX_BITS};
 
+/*@observer@*/ /*@unchecked@*/
 local static_tree_desc  static_bl_desc =
 {(const ct_data *)0, extra_blbits, 0,   BL_CODES, MAX_BL_BITS};
 
@@ -176,8 +185,8 @@ local void bi_windup      OF((deflate_state *s))
 	/*@modifies *s @*/;
 local void bi_flush       OF((deflate_state *s))
 	/*@modifies *s @*/;
-local void copy_block     OF((deflate_state *s, charf *buf, unsigned len,
-                              int header))
+local void copy_block     OF((deflate_state *s, /*@null@*/ charf *buf,
+				unsigned len, int header))
 	/*@modifies *s @*/;
 
 #ifdef GEN_TREES_H
@@ -408,10 +417,14 @@ void gen_trees_header()
 /**
  * Initialize the tree data structures for a new zlib stream.
  */
+/*@-compmempass@*/
 void _tr_init(deflate_state *s)
 {
+/*@-noeffect@*/
     tr_static_init();
+/*@=noeffect@*/
 
+/*@-immediatetrans@*/
     s->l_desc.dyn_tree = s->dyn_ltree;
     s->l_desc.stat_desc = &static_l_desc;
 
@@ -420,6 +433,7 @@ void _tr_init(deflate_state *s)
 
     s->bl_desc.dyn_tree = s->bl_tree;
     s->bl_desc.stat_desc = &static_bl_desc;
+/*@=immediatetrans@*/
 
     s->bi_buf = 0;
     s->bi_valid = 0;
@@ -432,11 +446,13 @@ void _tr_init(deflate_state *s)
     /* Initialize the first block of the first file: */
     init_block(s);
 }
+/*@=compmempass@*/
 
 /* ========================================================================= */
 /**
  * Initialize a new block.
  */
+/*@-compmempass@*/
 local void init_block(deflate_state *s)
 {
     int n; /* iterates over tree elements */
@@ -450,6 +466,7 @@ local void init_block(deflate_state *s)
     s->opt_len = s->static_len = 0L;
     s->last_lit = s->matches = 0;
 }
+/*@=compmempass@*/
 
 #define SMALLEST 1
 /* Index within the heap array of least frequent node in the Huffman tree */
@@ -554,7 +571,9 @@ local void gen_bitlen(deflate_state *s, tree_desc *desc)
 
         s->bl_count[bits]++;
         xbits = 0;
+/*@-nullderef@*/ /* FIX: extra may be NULL */
         if (n >= base) xbits = extra[n-base];
+/*@=nullderef@*/
         f = tree[n].Freq;
         s->opt_len += (ulg)f * (bits + xbits);
         if (stree) s->static_len += (ulg)f * (stree[n].Len + xbits);
@@ -743,6 +762,7 @@ local void build_tree(deflate_state *s, tree_desc *desc)
  * @param tree		the tree to be scanned
  * @param max_code	and its largest code of non zero frequency
  */
+/*@-compmempass@*/
 local void scan_tree (deflate_state *s, ct_data *tree, int max_code)
 {
     int n;                     /* iterates over all tree elements */
@@ -780,6 +800,7 @@ local void scan_tree (deflate_state *s, ct_data *tree, int max_code)
         }
     }
 }
+/*@=compmempass@*/
 
 /**
  * Send a literal or distance tree in compressed form, using the codes in
@@ -1074,6 +1095,7 @@ void _tr_flush_block(deflate_state *s, charf *buf, ulg stored_len,
  * @param dist		distance of matched string
  * @param lc		match length-MIN_MATCH or unmatched char (if dist == 0)
  */
+/*@-compmempass@*/
 int _tr_tally (deflate_state *s, unsigned dist, unsigned lc)
 {
     s->d_buf[s->last_lit] = (ush)dist;
@@ -1117,6 +1139,7 @@ int _tr_tally (deflate_state *s, unsigned dist, unsigned lc)
      * 64K-1 bytes.
      */
 }
+/*@=compmempass@*/
 
 /**
  * Send the block data compressed using the given Huffman trees
@@ -1267,6 +1290,7 @@ local void copy_block(deflate_state *s, charf *buf, unsigned len, int header)
 #ifdef DEBUG
     s->bits_sent += (ulg)len<<3;
 #endif
+    if (buf != NULL)
     while (len--) {
         put_byte(s, *buf++);
     }
diff --git a/zlib/trees.h b/zlib/trees.h
index b5145143a..bb8f62e2f 100644
--- a/zlib/trees.h
+++ b/zlib/trees.h
@@ -3,6 +3,7 @@
  * Header created automatically with -DGEN_TREES_H
  */
 
+/*@observer@*/ /*@unchecked@*/
 local const ct_data static_ltree[L_CODES+2] = {
 {{ 12},{  8}}, {{140},{  8}}, {{ 76},{  8}}, {{204},{  8}}, {{ 44},{  8}},
 {{172},{  8}}, {{108},{  8}}, {{236},{  8}}, {{ 28},{  8}}, {{156},{  8}},
@@ -64,6 +65,7 @@ local const ct_data static_ltree[L_CODES+2] = {
 {{163},{  8}}, {{ 99},{  8}}, {{227},{  8}}
 };
 
+/*@observer@*/ /*@unchecked@*/
 local const ct_data static_dtree[D_CODES] = {
 {{ 0},{ 5}}, {{16},{ 5}}, {{ 8},{ 5}}, {{24},{ 5}}, {{ 4},{ 5}},
 {{20},{ 5}}, {{12},{ 5}}, {{28},{ 5}}, {{ 2},{ 5}}, {{18},{ 5}},
@@ -73,6 +75,7 @@ local const ct_data static_dtree[D_CODES] = {
 {{19},{ 5}}, {{11},{ 5}}, {{27},{ 5}}, {{ 7},{ 5}}, {{23},{ 5}}
 };
 
+/*@observer@*/ /*@unchecked@*/
 const uch _dist_code[DIST_CODE_LEN] = {
  0,  1,  2,  3,  4,  4,  5,  5,  6,  6,  6,  6,  7,  7,  7,  7,  8,  8,  8,  8,
  8,  8,  8,  8,  9,  9,  9,  9,  9,  9,  9,  9, 10, 10, 10, 10, 10, 10, 10, 10,
@@ -102,6 +105,7 @@ const uch _dist_code[DIST_CODE_LEN] = {
 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29
 };
 
+/*@observer@*/ /*@unchecked@*/
 const uch _length_code[MAX_MATCH-MIN_MATCH+1]= {
  0,  1,  2,  3,  4,  5,  6,  7,  8,  8,  9,  9, 10, 10, 11, 11, 12, 12, 12, 12,
 13, 13, 13, 13, 14, 14, 14, 14, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16,
@@ -118,11 +122,13 @@ const uch _length_code[MAX_MATCH-MIN_MATCH+1]= {
 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 28
 };
 
+/*@observer@*/ /*@unchecked@*/
 local const int base_length[LENGTH_CODES] = {
 0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 20, 24, 28, 32, 40, 48, 56,
 64, 80, 96, 112, 128, 160, 192, 224, 0
 };
 
+/*@observer@*/ /*@unchecked@*/
 local const int base_dist[D_CODES] = {
     0,     1,     2,     3,     4,     6,     8,    12,    16,    24,
    32,    48,    64,    96,   128,   192,   256,   384,   512,   768,
diff --git a/zlib/uncompr.c b/zlib/uncompr.c
index ca93d678b..454495ecf 100644
--- a/zlib/uncompr.c
+++ b/zlib/uncompr.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: uncompr.c,v 1.2 2001/11/22 21:12:46 jbj Exp $ */
+/* @(#) $Id: uncompr.c,v 1.3 2001/12/27 21:00:18 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -10,6 +10,9 @@
  */
 
 #include "zlib.h"
+#include "zutil.h"	/* XXX for zmemzero() */
+
+/*@access z_streamp@*/
 
 /* ========================================================================= */
 /**
@@ -32,6 +35,7 @@ int ZEXPORT uncompress (Bytef *dest, uLongf *destLen, const Bytef *source, uLong
     z_stream stream;
     int err;
 
+    zmemzero(&stream, sizeof(stream));
     stream.next_in = (Bytef*)source;
     stream.avail_in = (uInt)sourceLen;
     /* Check for source > 64K on 16-bit machine: */
@@ -41,8 +45,8 @@ int ZEXPORT uncompress (Bytef *dest, uLongf *destLen, const Bytef *source, uLong
     stream.avail_out = (uInt)*destLen;
     if ((uLong)stream.avail_out != *destLen) return Z_BUF_ERROR;
 
-    stream.zalloc = (alloc_func)0;
-    stream.zfree = (free_func)0;
+    stream.zalloc = (alloc_func)NULL;
+    stream.zfree = (free_func)NULL;
 
     err = inflateInit(&stream);
     if (err != Z_OK) return err;
diff --git a/zlib/zlib.h b/zlib/zlib.h
index f8985208b..1f2af85cd 100644
--- a/zlib/zlib.h
+++ b/zlib/zlib.h
@@ -61,9 +61,9 @@ extern "C" {
 
 #define ZLIB_VERSION "1.1.3"
 
-typedef voidpf (*alloc_func) OF((voidpf opaque, uInt items, uInt size))
+typedef /*@only@*/ voidpf (*alloc_func) OF((voidpf opaque, uInt items, uInt size))
 	/*@*/;
-typedef void   (*free_func)  OF((voidpf opaque, voidpf address))
+typedef void   (*free_func)  OF((voidpf opaque, /*@only@*/ voidpf address))
 	/*@*/;
 
 struct internal_state;
@@ -108,8 +108,8 @@ typedef struct z_stream_s {
     uInt     avail_out; /*!< remaining free space at next_out */
     uLong    total_out; /*!< total nb of bytes output so far */
 
-/*@observer@*/
-    char     *msg;      /*!< last error message, NULL if no error */
+/*@observer@*/ /*@null@*/
+    const char *msg;    /*!< last error message, NULL if no error */
     struct internal_state FAR *state; /*!< not visible by applications */
 
     alloc_func zalloc;  /*!< used to allocate the internal state */
@@ -164,7 +164,7 @@ typedef /*@abstract@*/ z_stream FAR *z_streamp;
 #define Z_DEFLATED   8
 /* The deflate compression method (the only one supported in this version) */
 
-#define Z_NULL  0  /* for initializing zalloc, zfree, opaque */
+#define Z_NULL  NULL  /* for initializing zalloc, zfree, opaque */
 
 #define zlib_version zlibVersion()
 /* for compatibility with versions < 1.0.2 */
@@ -278,7 +278,7 @@ ZEXTERN int ZEXPORT deflateInit OF((z_streamp strm, int level));
  * if next_in or next_out was NULL), Z_BUF_ERROR if no progress is possible
  * (for example avail_in or avail_out was zero).
  */
-ZEXTERN int ZEXPORT deflate OF((z_streamp strm, int flush))
+ZEXTERN int ZEXPORT deflate OF((/*@dependent@*/ /*@null@*/ z_streamp strm, int flush))
 	/*@modifies strm @*/;
 
 
@@ -501,7 +501,7 @@ ZEXTERN int ZEXPORT deflateSetDictionary OF((z_streamp strm,
  * (such as zalloc being NULL). msg is left unchanged in both source and
  * destination.
  */
-ZEXTERN int ZEXPORT deflateCopy OF((z_streamp dest,
+ZEXTERN int ZEXPORT deflateCopy OF((/*@dependent@*/ z_streamp dest,
                                     z_streamp source))
 	/*@modifies dest, source @*/;
 
@@ -534,7 +534,7 @@ ZEXTERN int ZEXPORT deflateReset OF((z_streamp strm))
  * stream state was inconsistent or if a parameter was invalid, Z_BUF_ERROR
  * if strm->avail_out was zero.
  */
-ZEXTERN int ZEXPORT deflateParams OF((z_streamp strm,
+ZEXTERN int ZEXPORT deflateParams OF((/*@dependent@*/ /*@null@*/ z_streamp strm,
 				      int level,
 				      int strategy))
 	/*@modifies strm @*/;
@@ -581,7 +581,7 @@ ZEXTERN int ZEXPORT inflateInit2 OF((z_streamp strm,
 ZEXTERN int ZEXPORT inflateSetDictionary OF((z_streamp strm,
                                              const Bytef *dictionary,
                                              uInt  dictLength))
-	/*@*/;
+	/*@modifies strm @*/;
 
 /**
  * Skips invalid compressed data until a full flush point (see above the
@@ -694,6 +694,7 @@ typedef voidp gzFile;
  * @param mode		file open mode
  * @return 		compressed stream
  */
+/*@null@*/
 ZEXTERN gzFile ZEXPORT gzopen  OF((const char *path, const char *mode))
 	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
@@ -712,7 +713,8 @@ ZEXTERN gzFile ZEXPORT gzopen  OF((const char *path, const char *mode))
  * @param fd		file descriptor
  * @param mode		file open mode
  * @return 		compressed stream
-*/
+ */
+/*@null@*/
 ZEXTERN gzFile ZEXPORT gzdopen  OF((int fd, const char *mode))
 	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
@@ -744,7 +746,7 @@ ZEXTERN int ZEXPORT gzsetparams OF((gzFile file, int level, int strategy))
  * @param len
  * @return 		no. of bytes read, 0 on EOF, -1 on error
  */
-ZEXTERN int ZEXPORT    gzread  OF((gzFile file, voidp buf, unsigned len))
+ZEXTERN int ZEXPORT    gzread  OF((gzFile file, /*@out@*/ voidp buf, unsigned len))
 	/*@globals errno, fileSystem @*/
 	/*@modifies file, *buf, errno, fileSystem @*/;
 
@@ -801,6 +803,7 @@ ZEXTERN int ZEXPORT gzputs OF((gzFile file, const char *s))
  * @param len	
  * @return 		buf, Z_NULL on error
  */
+/*@null@*/
 ZEXTERN char * ZEXPORT gzgets OF((gzFile file, char *buf, int len))
 	/*@globals fileSystem @*/
 	/*@modifies file, buf, fileSystem @*/;
@@ -927,6 +930,7 @@ ZEXTERN int ZEXPORT    gzclose OF((/*@only@*/ gzFile file))
  * @param errnum
  * @return
  */
+/*@observer@*/
 ZEXTERN const char * ZEXPORT gzerror OF((gzFile file, int *errnum))
 	/*@modifies *errnum @*/;
 
@@ -979,13 +983,15 @@ ZEXTERN uLong ZEXPORT crc32   OF((uLong crc, const Bytef *buf, uInt len))
 /* deflateInit and inflateInit are macros to allow checking the zlib version
  * and the compiler's view of z_stream:
  */
-ZEXTERN int ZEXPORT deflateInit_ OF((z_streamp strm, int level,
+ZEXTERN int ZEXPORT deflateInit_ OF((/*@dependent@*/ /*@null@*/ z_streamp strm,
+                                     int level,
                                      const char *version, int stream_size))
 	/*@modifies strm @*/;
 ZEXTERN int ZEXPORT inflateInit_ OF((z_streamp strm,
                                      const char *version, int stream_size))
 	/*@modifies strm @*/;
-ZEXTERN int ZEXPORT deflateInit2_ OF((z_streamp strm, int  level, int  method,
+ZEXTERN int ZEXPORT deflateInit2_ OF((/*@dependent@*/ /*@null@*/ z_streamp strm,
+                                      int level, int method,
                                       int windowBits, int memLevel,
                                       int strategy, const char *version,
                                       int stream_size))
@@ -1004,14 +1010,14 @@ ZEXTERN int ZEXPORT inflateInit2_ OF((z_streamp strm, int  windowBits,
         inflateInit2_((strm), (windowBits), ZLIB_VERSION, sizeof(z_stream))
 
 
-#if !defined(_Z_UTIL_H) && !defined(NO_DUMMY_DECL)
-    struct internal_state {int dummy;}; /* hack for buggy compilers */
-#endif
-
+/*@observer@*/
 ZEXTERN const char   * ZEXPORT zError           OF((int err))
 	/*@*/;
+
 ZEXTERN int            ZEXPORT inflateSyncPoint OF((z_streamp z))
 	/*@modifies z @*/;
+
+/*@observer@*/
 ZEXTERN const uLongf * ZEXPORT get_crc_table    OF((void))
 	/*@*/;
 
diff --git a/zlib/zutil.c b/zlib/zutil.c
index 59b12b52d..1b09a1544 100644
--- a/zlib/zutil.c
+++ b/zlib/zutil.c
@@ -1,4 +1,4 @@
-/* @(#) $Id: zutil.c,v 1.2 2001/11/22 21:12:46 jbj Exp $ */
+/* @(#) $Id: zutil.c,v 1.3 2001/12/27 21:00:18 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h 
@@ -11,8 +11,6 @@
 
 #include "zutil.h"
 
-struct internal_state      {int dummy;}; /* for buggy compilers */
-
 #ifndef STDC
 extern void exit OF((int));
 #endif
@@ -53,10 +51,12 @@ void z_error (char *m)
 /* exported to allow conversion of error code to string for compress() and
  * uncompress()
  */
+/*@-compmempass@*/
 const char * ZEXPORT zError(int err)
 {
     return ERR_MSG(err);
 }
+/*@=compmempass@*/
 
 
 #ifndef HAVE_MEMCPY
diff --git a/zlib/zutil.h b/zlib/zutil.h
index 9c69cb19c..7b67ff0a0 100644
--- a/zlib/zutil.h
+++ b/zlib/zutil.h
@@ -1,4 +1,4 @@
-/* @(#) $Id: zutil.h,v 1.3 2001/11/22 21:12:46 jbj Exp $ */
+/* @(#) $Id: zutil.h,v 1.4.2.1 2002/01/25 19:18:55 jbj Exp $ */
 /*
  * Copyright (C) 1995-1998 Jean-loup Gailly.
  * For conditions of distribution and use, see copyright notice in zlib.h
@@ -40,6 +40,7 @@ typedef unsigned short ush;
 typedef ush FAR ushf;
 typedef unsigned long  ulg;
 
+/*@observer@*/ /*@unchecked@*/
 extern const char *z_errmsg[10]; /* indexed by 2-zlib_error */
 /* (size given to avoid silly warnings with Visual C++) */
 
@@ -217,6 +218,7 @@ extern const char *z_errmsg[10]; /* indexed by 2-zlib_error */
 typedef uLong (ZEXPORT *check_func) OF((uLong check, const Bytef *buf,
 				       uInt len))
 	/*@*/;
+/*@only@*/ /*@null@*/
 voidpf zcalloc OF((voidpf opaque, unsigned items, unsigned size))
 	/*@*/;
 void   zcfree  OF((voidpf opaque, /*@only@*/ voidpf ptr))
@@ -253,7 +255,8 @@ __asm__ __volatile__( \
 static __inline__ void quickmemcpy(void *_to, const void *_from, long n)
 	/*@*/
 {
-	char *to = _to, *from = _from;
+	const char *from = _from;
+	char *to = _to;
 	while (n-- > 0)
 		*to++ = *from++;
 }