Splint fiddles.

CVS patchset: 6665
CVS date: 2003/03/08 23:18:09

17 files changed, 1222 insertions, 133 deletions

diff --git a/zlib/.splintrc b/zlib/.splintrc
index 1919ecfd8..78da9da2d 100644
--- a/zlib/.splintrc
+++ b/zlib/.splintrc
@@ -3,7 +3,6 @@
 +partial
 +forcehints
 
-
 -warnunixlib
 -warnposix
 
@@ -14,53 +13,46 @@
 +strict			# lclint level
 
 # --- in progress
--abstract
+-abstract		# 4
 -aliasunique
+-assignexpose
 -branchstate
--casebreak
+-bufferoverflowhigh
 -castfcnptr
--commenterror
 -compdef
 -compmempass
--dependenttrans
--evalorder
--globs
+-evalorder		# 2
 -globstate
--immediatetrans
--infloopsuncon
--internalglobs
--kepttrans
--looploopbreak
--looploopcontinue
--loopswitchbreak
 -modfilesys
--modnomods
--modobserveruncon
--moduncon
--modunconnomods
+-mods			# 13
 -mustmod
--noeffect
--noeffectuncon		# 22
--nullderef
--nullpass
--nullret
--nullstate		# 36
--observertrans
--oldstyle
--paramuse
+-noeffectuncon		# 10
+-nullderef		# 9
+-nullpass		# 24
+-nullptrarith
+-nullret		# 13
 -protoparammatch	# 22
--readonlytrans
--redef
--retalias
+-redef			# 4
+-retalias		# 4
 -retvalint		# painful
--sizeoftype		# 110
+-sizeoftype		# 106
+-type
+-usereleased		# 38
+
+-dependenttrans	# 2
+-immediatetrans
+-kepttrans
+-observertrans
+-readonlytrans
 -statictrans
--switchswitchbreak
 -temptrans
--type
 -unqualifiedtrans
--unsignedcompare
--usereleased
+
+-casebreak
+-looploopbreak
+-looploopcontinue
+-loopswitchbreak
+-switchswitchbreak
 -whileempty
 
 # --- +partial artifacts
diff --git a/zlib/Makefile.am b/zlib/Makefile.am
index bdc02536c..a140bc123 100644
--- a/zlib/Makefile.am
+++ b/zlib/Makefile.am
@@ -17,7 +17,7 @@ libz_la_SOURCES = \
 	infback.c inffast.c inflate.c inftrees.c \
 	trees.c uncompr.c zutil.c
 
-noinst_PROGRAMS = example minigzip
+noinst_PROGRAMS = example minigzip ung
 
 example_SOURCES = example.c
 example_LDFLAGS = -L. -lz
@@ -25,6 +25,9 @@ example_LDFLAGS = -L. -lz
 minigzip_SOURCES = minigzip.c
 minigzip_LDFLAGS = -L. -lz
 
+ung_SOURCES = ung.c
+ung_LDFLAGS = -L. -lz
+
 #BUILT_SOURCES = Doxyfile zlib.lcd
 
 zlib.lcd: Makefile.am ${libz_la_SOURCES} ${noinst_HEADERS}
diff --git a/zlib/contrib/inflate86/inffast.S b/zlib/contrib/inflate86/inffast.S
new file mode 100644
index 000000000..d1e80efad
--- /dev/null
+++ b/zlib/contrib/inflate86/inffast.S
@@ -0,0 +1,1095 @@
+/*

+ * inffast.S is a hand tuned assembler version of:

+ *

+ * inffast.c -- fast decoding

+ * Copyright (C) 1995-2003 Mark Adler

+ * For conditions of distribution and use, see copyright notice in zlib.h 

+ *

+ * Copyright (C) 2003 Chris Anderson <christop@charm.net>

+ * Please use the copyright conditions above.

+ * 

+ * This version (Jan-23-2003) of inflate_fast was coded and tested under

+ * GNU/Linux on a pentium 3, using the gcc-3.2 compiler distribution.  On that

+ * machine, I found that gzip style archives decompressed about 20% faster than

+ * the gcc-3.2 -O3 -fomit-frame-pointer compiled version.  Your results will

+ * depend on how large of a buffer is used for z_stream.next_in & next_out

+ * (8K-32K worked best for my 256K cpu cache) and how much overhead there is in

+ * stream processing I/O and crc32/addler32.  In my case, this routine used

+ * 70% of the cpu time and crc32 used 20%.

+ *

+ * I am confident that this version will work in the general case, but I have

+ * not tested a wide variety of datasets or a wide variety of platforms.

+ *

+ * Jan-24-2003 -- Added -DUSE_MMX define for slightly faster inflating.

+ * It should be a runtime flag instead of compile time flag...

+ */

+

+.file "inffast.S"

+

+.globl inflate_fast

+

+.text

+.align 4,0

+.L_invalid_literal_length_code_msg:

+.string "invalid literal/length code"

+

+.align 4,0

+.L_invalid_distance_code_msg:

+.string "invalid distance code"

+

+.align 4,0

+.L_invalid_distance_too_far_msg:

+.string "invalid distance too far back"

+

+#if defined( USE_MMX )

+.align 4,0

+.L_mask: /* mask[N] = ( 1 << N ) - 1 */

+.long 0

+.long 1

+.long 3

+.long 7

+.long 15

+.long 31

+.long 63

+.long 127

+.long 255

+.long 511

+.long 1023

+.long 2047

+.long 4095

+.long 8191

+.long 16383

+.long 32767

+.long 65535

+.long 131071

+.long 262143

+.long 524287

+.long 1048575

+.long 2097151

+.long 4194303

+.long 8388607

+.long 16777215

+.long 33554431

+.long 67108863

+.long 134217727

+.long 268435455

+.long 536870911

+.long 1073741823

+.long 2147483647

+.long 4294967295

+#endif

+

+.text

+

+/*

+ * struct z_stream offsets, in zlib.h

+ */

+#define next_in_strm   0   /* strm->next_in */

+#define avail_in_strm  4   /* strm->avail_in */

+#define next_out_strm  12  /* strm->next_out */

+#define avail_out_strm 16  /* strm->avail_out */

+#define msg_strm       24  /* strm->msg */

+#define state_strm     28  /* strm->state */

+

+/*

+ * struct inflate_state offsets, in inflate.h

+ */

+#define mode_state     0   /* state->mode */

+#define wsize_state    32  /* state->wsize */

+#define write_state    36  /* state->write */

+#define window_state   40  /* state->window */

+#define hold_state     44  /* state->hold */

+#define bits_state     48  /* state->bits */

+#define lencode_state  64  /* state->lencode */

+#define distcode_state 68  /* state->distcode */

+#define lenbits_state  72  /* state->lenbits */

+#define distbits_state 76  /* state->distbits */

+

+/*

+ * inflate_fast's activation record

+ */

+#define local_var_size 56 /* how much local space for vars */

+#define strm_sp        80 /* first arg: z_stream * (local_var_size + 24) */

+#define start_sp       84 /* second arg: unsigned int (local_var_size + 28) */

+

+/*

+ * offsets for local vars on stack

+ */

+#define out            52  /* unsigned char* */

+#define window         48  /* unsigned char* */

+#define wsize          44  /* unsigned int */

+#define write          40  /* unsigned int */

+#define in             36  /* unsigned char* */

+#define beg            32  /* unsigned char* */

+#define dist           28  /* unsigned int */

+#define len            24  /* unsigned int */

+#define last           20  /* unsigned char* */

+#define end            16  /* unsigned char* */

+#define dcode          12  /* code* */

+#define lcode           8  /* code* */

+#define dmask           4  /* unsigned int */

+#define lmask           0  /* unsigned int */

+

+/*

+ * typedef enum inflate_mode consts, in inflate.h

+ */

+#ifndef NO_GUNZIP

+#define GUNZIP

+#endif

+

+#ifdef GUNZIP

+#define INFLATE_MODE_TYPE 11  /* state->mode flags enum-ed in inflate.h */

+#define INFLATE_MODE_BAD  26

+#else

+#define INFLATE_MODE_TYPE 3

+#define INFLATE_MODE_BAD  17

+#endif

+

+

+.align 16,0x90

+inflate_fast:

+        pushl   %edi

+        pushl   %esi

+        pushl   %ebp

+        pushl   %ebx

+        pushf   /* save eflags (strm_sp, state_sp assumes this is 32 bits) */

+        subl    $local_var_size, %esp

+        cld

+#if defined( USE_MMX )

+        emms

+#endif

+

+#define strm_r  %esi

+#define state_r %edi

+

+        movl    strm_sp(%esp), strm_r

+        movl    state_strm(strm_r), state_r

+

+        /* in = strm->next_in;

+         * out = strm->next_out;

+         * last = in + strm->avail_in - 5;

+         * beg = out - (start - strm->avail_out);

+         * end = out + (strm->avail_out - 257);

+         */

+        movl    next_in_strm(strm_r), %eax

+        movl    next_out_strm(strm_r), %ebx

+        movl    avail_in_strm(strm_r), %edx

+        movl    avail_out_strm(strm_r), %ecx

+        movl    start_sp(%esp), %ebp

+

+        addl    %eax, %edx      /* avail_in += next_in */

+        subl    $5, %edx        /* avail_in -= 5 */

+

+        subl    %ecx, %ebp      /* start -= avail_out */

+        negl    %ebp            /* start = -start */

+        addl    %ebx, %ebp      /* start += next_out */

+

+        subl    $257, %ecx      /* avail_out -= 257 */

+        addl    %ebx, %ecx      /* avail_out += out */

+

+        movl    %eax, in(%esp)

+        movl    %ebx, out(%esp)

+        movl    %edx, last(%esp)

+        movl    %ebp, beg(%esp)

+        movl    %ecx, end(%esp)

+

+        /* wsize = state->wsize;

+         * write = state->write;

+         * window = state->window;

+         * hold = state->hold;

+         * bits = state->bits;

+         * lcode = state->lencode;

+         * dcode = state->distcode;

+         * lmask = ( 1 << state->lenbits ) - 1;

+         * dmask = ( 1 << state->distbits ) - 1;

+         */

+

+        movl    lencode_state(state_r), %eax

+        movl    distcode_state(state_r), %ecx

+

+        movl    %eax, lcode(%esp)

+        movl    %ecx, dcode(%esp)

+

+        movl    $1, %eax

+        movl    lenbits_state(state_r), %ecx

+        shll    %cl, %eax

+        decl    %eax

+        movl    %eax, lmask(%esp)

+

+        movl    $1, %eax

+        movl    distbits_state(state_r), %ecx

+        shll    %cl, %eax

+        decl    %eax

+        movl    %eax, dmask(%esp)

+

+        movl    wsize_state(state_r), %eax

+        movl    write_state(state_r), %ecx

+        movl    window_state(state_r), %edx

+

+        movl    %eax, wsize(%esp)

+        movl    %ecx, write(%esp)

+        movl    %edx, window(%esp)

+

+#if ! defined( USE_MMX )

+

+#define hold_r     %ebp

+#define bits_r     %bl

+#define bitslong_r %ebx

+

+        movl    hold_state(state_r), hold_r

+        movl    bits_state(state_r), bitslong_r

+

+#else /* USE_MMX */

+

+#define hold_mm    %mm0

+#define bits_r     %ebp

+#define bitslong_r %ebp

+

+        movl    hold_state(state_r), %ebx

+        movl    bits_state(state_r), bitslong_r

+

+#endif

+

+#undef strm_r

+#undef state_r

+#define in_r       %esi

+#define from_r     %esi

+#define out_r      %edi

+

+        movl    in(%esp), in_r

+

+#if ! defined ( USE_MMX )

+

+        /* align in_r on word boundary */

+        testl   $1, in_r

+        jz      .L_is_aligned

+        xorl    %eax, %eax

+        movb    (in_r), %al

+        incl    in_r

+        movb    bits_r, %cl

+        addb    $8, bits_r

+        shll    %cl, %eax

+        orl     %eax, hold_r

+

+#else

+        /* align in_r on long boundary */

+.L_align_long:

+        testl   $3, in_r

+        jz      .L_is_aligned

+        xorl    %eax, %eax

+        movb    (in_r), %al

+        incl    in_r

+        movl    bits_r, %ecx

+        addl    $8, bits_r

+        shll    %cl, %eax

+        orl     %eax, %ebx

+        jmp     .L_align_long

+

+#endif

+

+.L_is_aligned:

+        movl    out(%esp), out_r

+

+#if defined ( USE_MMX )

+

+#define used_mm   %mm1

+#define dmask2_mm %mm2

+#define lmask2_mm %mm3

+#define lmask_mm  %mm4

+#define dmask_mm  %mm5

+#define tmp_mm    %mm6

+

+        movl    out(%esp), out_r

+        movd    lmask(%esp), lmask_mm 

+        movq    lmask_mm, lmask2_mm

+        movd    dmask(%esp), dmask_mm

+        movq    dmask_mm, dmask2_mm

+        movd    %ebx, hold_mm

+        pxor    used_mm, used_mm

+        movl    lcode(%esp), %ebx       /* ebx = lcode */

+#endif

+

+        jmp     .L_do_loop

+

+.align 16,0x90

+

+#if ! defined ( USE_MMX )

+

+.L_do_loop:

+        /* regs: %esi = in, %ebp = hold, %bl = bits, %edi = out

+         *

+         * do { 

+         *   if (bits < 15) {

+         *     hold |= *((unsigned short *)in)++ << bits;

+         *     bits += 16

+         *   }

+         *   this = lcode[hold & lmask]

+         */

+        cmpb    $15, bits_r

+        ja      .L_get_length_code      /* if (15 < bits) */

+

+        xorl    %eax, %eax

+        lodsw                           /* al = *(ushort *)in++ */

+        movb    bits_r, %cl             /* cl = bits, needs it for shifting */

+        addb    $16, bits_r             /* bits += 16 */

+        shll    %cl, %eax

+        orl     %eax, hold_r            /* hold |= *((ushort *)in)++ << bits */

+

+.L_get_length_code:

+        movl    lmask(%esp), %edx       /* edx = lmask */

+        movl    lcode(%esp), %ecx       /* ecx = lcode */

+        andl    hold_r, %edx            /* edx &= hold */

+        movl    (%ecx,%edx,4), %eax     /* eax = lcode[hold & lmask] */

+

+#else /* USE_MMX */

+

+.L_do_loop:

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+

+        cmpl    $32, bits_r

+        ja      .L_get_length_code      /* if (32 < bits) */

+

+        movd    bits_r, tmp_mm

+        movd    (in_r), %mm7

+        addl    $4, in_r

+        psllq   tmp_mm, %mm7

+        addl    $32, bits_r

+        por     %mm7, hold_mm           /* hold_mm |= *((uint *)in)++ << bits */

+

+.L_get_length_code:

+        pand    hold_mm, lmask_mm

+        movd    lmask_mm, %eax

+        movq    lmask2_mm, lmask_mm

+        movl    (%ebx,%eax,4), %eax     /* eax = lcode[hold & lmask] */

+

+#endif

+

+#if ! defined( USE_MMX )

+

+.L_dolen:

+        /* regs: %esi = in, %ebp = hold, %bl = bits, %edi = out

+         *

+         * dolen:

+         *    bits -= this.bits;

+         *    hold >>= this.bits

+         */

+        movb    %ah, %cl                /* cl = this.bits */

+        subb    %ah, bits_r             /* bits -= this.bits */

+        shrl    %cl, hold_r             /* hold >>= this.bits */

+

+        /* check if op is a literal

+         * if (op == 0) {

+         *    PUP(out) = this.val;

+         *  }

+         */

+        testb   %al, %al

+        jnz     .L_test_for_length_base /* if (op != 0) 45.7% */

+

+        shrl    $16, %eax               /* output this.val char */

+        stosb

+

+#else /* USE_MMX */

+

+#define len_r  %edx

+

+.L_dolen:

+        movzbl  %ah, %ecx               /* ecx = this.bits */

+        movl    %eax, len_r             /* len = this */

+        shrl    $16, len_r              /* len = this.val */

+        movd    %ecx, used_mm

+        subl    %ecx, bits_r            /* bits -= this.bits */

+

+        testb   %al, %al

+        jnz     .L_test_for_length_base /* if (op != 0) 45.7% */

+

+        movb    %dl, (out_r)

+        incl    out_r

+

+#endif

+

+.L_while_test:

+        /* while (in < last && out < end)

+         */

+        cmpl    out_r, end(%esp)

+        jbe     .L_break_loop           /* if (out >= end) */

+

+        cmpl    in_r, last(%esp)

+        ja      .L_do_loop              /* if (in < last) */

+        jmp     .L_break_loop

+

+#if ! defined( USE_MMX )

+

+.L_test_for_length_base:

+        /* regs: %esi = in, %ebp = hold, %bl = bits, %edi = out, %edx = len

+         *

+         * else if (op & 16) {

+         *   len = this.val

+         *   op &= 15

+         *   if (op) {

+         *     if (op > bits) {

+         *       hold |= *((unsigned short *)in)++ << bits;

+         *       bits += 16

+         *     }

+         *     len += hold & mask[op];

+         *     bits -= op;

+         *     hold >>= op;

+         *   }

+         */

+#define len_r %edx

+        movl    %eax, len_r             /* len = this */

+        shrl    $16, len_r              /* len = this.val */

+        movb    %al, %cl

+

+        testb   $16, %al

+        jz      .L_test_for_second_level_length /* if ((op & 16) == 0) 8% */

+        andb    $15, %cl                /* op &= 15 */

+        jz      .L_save_len             /* if (!op) */

+        cmpb    %cl, bits_r

+        jae     .L_add_bits_to_len      /* if (op <= bits) */

+

+        movb    %cl, %ch                /* stash op in ch, freeing cl */

+        xorl    %eax, %eax

+        lodsw                           /* al = *(ushort *)in++ */

+        movb    bits_r, %cl             /* cl = bits, needs it for shifting */

+        addb    $16, bits_r             /* bits += 16 */

+        shll    %cl, %eax

+        orl     %eax, hold_r            /* hold |= *((ushort *)in)++ << bits */

+        movb    %ch, %cl                /* move op back to ecx */

+

+.L_add_bits_to_len:

+        movl    $1, %eax

+        shll    %cl, %eax

+        decl    %eax

+        subb    %cl, bits_r

+        andl    hold_r, %eax            /* eax &= hold */

+        shrl    %cl, hold_r

+        addl    %eax, len_r             /* len += hold & mask[op] */

+

+.L_save_len:

+        movl    len_r, len(%esp)        /* save len */

+#undef  len_r

+

+.L_decode_distance:

+        /* regs: %esi = in, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *

+         *   if (bits < 15) {

+         *     hold |= *((unsigned short *)in)++ << bits;

+         *     bits += 16

+         *   }

+         *   this = dcode[hold & dmask];

+         * dodist:

+         *   bits -= this.bits;

+         *   hold >>= this.bits;

+         *   op = this.op;

+         */

+

+        cmpb    $15, bits_r

+        ja      .L_get_distance_code    /* if (15 < bits) */

+

+        xorl    %eax, %eax

+        lodsw                           /* al = *(ushort *)in++ */

+        movb    bits_r, %cl             /* cl = bits, needs it for shifting */

+        addb    $16, bits_r             /* bits += 16 */

+        shll    %cl, %eax

+        orl     %eax, hold_r            /* hold |= *((ushort *)in)++ << bits */

+

+.L_get_distance_code:

+        movl    dmask(%esp), %edx       /* edx = dmask */

+        movl    dcode(%esp), %ecx       /* ecx = dcode */

+        andl    hold_r, %edx            /* edx &= hold */

+        movl    (%ecx,%edx,4), %eax     /* eax = dcode[hold & dmask] */

+

+#else /* USE_MMX */

+

+.L_test_for_length_base:

+        testb   $16, %al

+        jz      .L_test_for_second_level_length /* if ((op & 16) == 0) 8% */

+        andl    $15, %eax               /* op &= 15 */

+        jz      .L_decode_distance      /* if (!op) */

+

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+        movd    %eax, used_mm

+        movd    hold_mm, %ecx

+        subl    %eax, bits_r

+        andl    .L_mask(,%eax,4), %ecx

+        addl    %ecx, len_r             /* len += hold & mask[op] */

+

+.L_decode_distance:

+

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+

+        cmpl    $32, bits_r

+        ja      .L_get_dist_code        /* if (32 < bits) */

+

+        movd    bits_r, tmp_mm

+        movd    (in_r), %mm7

+        addl    $4, in_r

+        psllq   tmp_mm, %mm7

+        addl    $32, bits_r

+        por     %mm7, hold_mm           /* hold_mm |= *((uint *)in)++ << bits */

+

+.L_get_dist_code:

+        movl    dcode(%esp), %ebx       /* ebx = dcode */

+        pand    hold_mm, dmask_mm

+        movd    dmask_mm, %eax

+        movq    dmask2_mm, dmask_mm

+        movl    (%ebx,%eax,4), %eax     /* eax = dcode[hold & lmask] */

+

+#endif

+

+#if ! defined( USE_MMX )

+

+#define dist_r %edx

+.L_dodist:

+        movl    %eax, dist_r            /* dist = this */

+        shrl    $16, dist_r             /* dist = this.val */

+        movb    %ah, %cl

+        subb    %ah, bits_r             /* bits -= this.bits */

+        shrl    %cl, hold_r             /* hold >>= this.bits */

+

+        /* if (op & 16) {

+         *   dist = this.val

+         *   op &= 15

+         *   if (op > bits) {

+         *     hold |= *((unsigned short *)in)++ << bits;

+         *     bits += 16

+         *   }

+         *   dist += hold & mask[op];

+         *   bits -= op;

+         *   hold >>= op;

+         */

+        movb    %al, %cl                /* cl = this.op */

+

+        testb   $16, %al                /* if ((op & 16) == 0) */

+        jz      .L_test_for_second_level_dist

+        andb    $15, %cl                /* op &= 15 */

+        jz      .L_check_dist_one

+        cmpb    %cl, bits_r

+        jae     .L_add_bits_to_dist     /* if (op <= bits) 97.6% */

+

+        movb    %cl, %ch                /* stash op in ch, freeing cl */

+        xorl    %eax, %eax

+        lodsw                           /* al = *(ushort *)in++ */

+        movb    bits_r, %cl             /* cl = bits, needs it for shifting */

+        addb    $16, bits_r             /* bits += 16 */

+        shll    %cl, %eax

+        orl     %eax, hold_r            /* hold |= *((ushort *)in)++ << bits */

+        movb    %ch, %cl                /* move op back to ecx */

+

+.L_add_bits_to_dist:

+        movl    $1, %eax

+        shll    %cl, %eax

+        decl    %eax                    /* (1 << op) - 1 */

+        subb    %cl, bits_r

+        andl    hold_r, %eax            /* eax &= hold */

+        shrl    %cl, hold_r

+        addl    %eax, dist_r            /* dist += hold & ((1 << op) - 1) */

+        jmp     .L_check_window

+

+#else /* USE_MMX */

+

+#define dist_r %ebx

+.L_dodist:

+        movzbl  %ah, %ecx               /* ecx = this.bits */

+        movl    %eax, dist_r

+        shrl    $16, dist_r             /* dist  = this.val */

+        subl    %ecx, bits_r            /* bits -= this.bits */

+        movd    %ecx, used_mm

+

+        testb   $16, %al                /* if ((op & 16) == 0) */

+        jz      .L_test_for_second_level_dist 

+        andl    $15, %eax               /* op &= 15 */

+        jz      .L_check_dist_one

+

+.L_add_bits_to_dist:

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+        movd    %eax, used_mm           /* save bit length of current op */

+        movd    hold_mm, %ecx           /* get the next bits on input stream */

+        subl    %eax, bits_r            /* bits -= op bits */

+        andl    .L_mask(,%eax,4), %ecx  /* ecx   = hold & mask[op] */

+        addl    %ecx, dist_r            /* dist += hold & mask[op] */

+        jmp     .L_check_window

+

+#endif

+

+.align 16,0x90

+

+.L_check_dist_one:

+        cmpl    $1, dist_r

+        jne     .L_check_window

+        cmpl    out_r, beg(%esp)

+        je      .L_check_window

+

+        decl    out_r

+#if ! defined( USE_MMX )

+        movl    len(%esp), %ecx

+#else

+        movl    len_r, %ecx

+#endif

+        movb    (out_r), %al

+        subl    $3, %ecx

+

+        movb    %al, 1(out_r)

+        movb    %al, 2(out_r)

+        movb    %al, 3(out_r)

+        addl    $4, out_r

+        rep     stosb

+

+#if defined( USE_MMX )

+        movl    lcode(%esp), %ebx       /* move lcode back to %ebx, toss dist */

+#endif

+        jmp     .L_while_test

+

+.align 16,0x90

+

+.L_check_window:

+        /* regs: %esi = from, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *       %ecx = nbytes

+         *

+         * nbytes = out - beg;

+         * if (dist <= nbytes) {

+         *   from = out - dist;

+         *   do {

+         *     PUP(out) = PUP(from);

+         *   } while (--len > 0) {

+         * }

+         */

+

+        movl    in_r, in(%esp)          /* save in so from can use it's reg */

+        movl    out_r, %eax

+        subl    beg(%esp), %eax         /* nbytes = out - beg */

+

+        cmpl    dist_r, %eax

+        jb      .L_clip_window          /* if (dist > nbytes) 4.2% */

+

+#if ! defined( USE_MMX )

+        movl    len(%esp), %ecx

+#else

+        movl    len_r, %ecx

+#endif

+        movl    out_r, from_r

+        subl    dist_r, from_r          /* from = out - dist */

+

+        subl    $3, %ecx

+        movb    (from_r), %al

+        movb    %al, (out_r)

+        movb    1(from_r), %al

+        movb    2(from_r), %dl

+        addl    $3, from_r

+        movb    %al, 1(out_r)

+        movb    %dl, 2(out_r)

+        addl    $3, out_r

+        rep     movsb

+

+        movl    in(%esp), in_r          /* move in back to %esi, toss from */

+#if defined( USE_MMX )

+        movl    lcode(%esp), %ebx       /* move lcode back to %ebx, toss dist */

+#endif

+        jmp     .L_while_test

+

+.align 16,0x90

+

+#if ! defined( USE_MMX )

+

+.L_test_for_second_level_length:

+        /* else if ((op & 64) == 0) {

+         *   this = lcode[this.val + (hold & mask[op])];

+         * }

+         */

+        testb   $64, %al

+        jnz     .L_test_for_end_of_block  /* if ((op & 64) != 0) */

+

+        movl    $1, %eax

+        shll    %cl, %eax

+        decl    %eax

+        andl    hold_r, %eax            /* eax &= hold */

+        addl    %edx, %eax              /* eax += this.val */

+        movl    lcode(%esp), %edx       /* edx = lcode */

+        movl    (%edx,%eax,4), %eax     /* eax = lcode[val + (hold&mask[op])] */

+        jmp     .L_dolen

+

+#else /* USE_MMX */

+

+.L_test_for_second_level_length: 

+        testb   $64, %al

+        jnz     .L_test_for_end_of_block  /* if ((op & 64) != 0) */

+

+        andl    $15, %eax

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+        movd    hold_mm, %ecx

+        andl    .L_mask(,%eax,4), %ecx

+        addl    len_r, %ecx

+        movl    (%ebx,%ecx,4), %eax     /* eax = lcode[hold & lmask] */

+        jmp     .L_dolen

+

+#endif

+

+.align 16,0x90

+

+#if ! defined( USE_MMX )

+

+.L_test_for_second_level_dist:

+        /* else if ((op & 64) == 0) {

+         *   this = dcode[this.val + (hold & mask[op])];

+         * }

+         */

+        testb   $64, %al

+        jnz     .L_invalid_distance_code  /* if ((op & 64) != 0) */

+

+        movl    $1, %eax

+        shll    %cl, %eax

+        decl    %eax

+        andl    hold_r, %eax            /* eax &= hold */

+        addl    %edx, %eax              /* eax += this.val */

+        movl    dcode(%esp), %edx       /* edx = dcode */

+        movl    (%edx,%eax,4), %eax     /* eax = dcode[val + (hold&mask[op])] */

+        jmp     .L_dodist

+

+#else /* USE_MMX */

+

+.L_test_for_second_level_dist:

+        testb   $64, %al

+        jnz     .L_invalid_distance_code  /* if ((op & 64) != 0) */

+

+        andl    $15, %eax

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+        movd    hold_mm, %ecx

+        andl    .L_mask(,%eax,4), %ecx

+        movl    dcode(%esp), %eax       /* ecx = dcode */

+        addl    dist_r, %ecx

+        movl    (%eax,%ecx,4), %eax     /* eax = lcode[hold & lmask] */

+        jmp     .L_dodist

+

+#endif

+

+.align 16,0x90

+.L_clip_window:

+        /* regs: %esi = from, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *       %ecx = nbytes

+         *

+         * else {

+         *   if (dist > wsize) {

+         *     invalid distance

+         *   }

+         *   from = window;

+         *   nbytes = dist - nbytes;

+         *   if (write == 0) {

+         *     from += wsize - nbytes;

+         */

+#define nbytes_r %ecx

+

+        movl    %eax, nbytes_r

+        movl    wsize(%esp), %eax       /* prepare for dist compare */

+        negl    nbytes_r                /* nbytes = -nbytes */

+        movl    window(%esp), from_r    /* from = window */

+

+        cmpl    dist_r, %eax

+        jb      .L_invalid_distance_too_far /* if (dist > wsize) */

+

+        addl    dist_r, nbytes_r        /* nbytes = dist - nbytes */

+        cmpl    $0, write(%esp)

+        jne     .L_wrap_around_window   /* if (write != 0) */

+

+        subl    nbytes_r, %eax

+        addl    %eax, from_r            /* from += wsize - nbytes */

+

+        /* regs: %esi = from, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *       %ecx = nbytes, %eax = len

+         *

+         *     if (nbytes < len) {

+         *       len -= nbytes;

+         *       do {

+         *         PUP(out) = PUP(from);

+         *       } while (--nbytes);

+         *       from = out - dist;

+         *     }

+         *   }

+         */

+

+#if ! defined( USE_MMX )

+#define len_r %eax

+        movl    len(%esp), len_r

+#endif

+        cmpl    nbytes_r, len_r

+        jbe     .L_do_copy1             /* if (nbytes >= len) */

+

+        subl    nbytes_r, len_r         /* len -= nbytes */

+        rep     movsb

+        movl    out_r, from_r

+        subl    dist_r, from_r          /* from = out - dist */

+        jmp     .L_do_copy1

+

+        cmpl    nbytes_r, len_r

+        jbe     .L_do_copy1             /* if (nbytes >= len) */

+

+        subl    nbytes_r, len_r         /* len -= nbytes */

+        rep     movsb

+        movl    out_r, from_r

+        subl    dist_r, from_r          /* from = out - dist */

+        jmp     .L_do_copy1

+

+.L_wrap_around_window:

+        /* regs: %esi = from, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *       %ecx = nbytes, %eax = write, %eax = len

+         *

+         *   else if (write < nbytes) {

+         *     from += wsize + write - nbytes;

+         *     nbytes -= write;

+         *     if (nbytes < len) {

+         *       len -= nbytes;

+         *       do {

+         *         PUP(out) = PUP(from);

+         *       } while (--nbytes);

+         *       from = window;

+         *       nbytes = write;

+         *       if (nbytes < len) {

+         *         len -= nbytes;

+         *         do {

+         *           PUP(out) = PUP(from);

+         *         } while(--nbytes);

+         *         from = out - dist;

+         *       }

+         *     }

+         *   }

+         */

+#define write_r %eax

+

+        movl    write(%esp), write_r

+        cmpl    write_r, nbytes_r

+        jbe     .L_contiguous_in_window /* if (write >= nbytes) */

+

+        addl    wsize(%esp), from_r

+        addl    write_r, from_r

+        subl    nbytes_r, from_r        /* from += wsize + write - nbytes */

+        subl    write_r, nbytes_r       /* nbytes -= write */

+#undef write_r

+

+#if ! defined( USE_MMX )

+        movl    len(%esp), len_r

+#endif

+        cmpl    nbytes_r, len_r

+        jbe     .L_do_copy1             /* if (nbytes >= len) */

+

+        subl    nbytes_r, len_r         /* len -= nbytes */

+        rep     movsb

+        movl    window(%esp), from_r    /* from = window */

+        movl    write(%esp), nbytes_r   /* nbytes = write */

+        cmpl    nbytes_r, len_r

+        jbe     .L_do_copy1             /* if (nbytes >= len) */

+

+        subl    nbytes_r, len_r         /* len -= nbytes */

+        rep     movsb

+        movl    out_r, from_r

+        subl    dist_r, from_r          /* from = out - dist */

+        jmp     .L_do_copy1

+

+.L_contiguous_in_window:

+        /* regs: %esi = from, %ebp = hold, %bl = bits, %edi = out, %edx = dist

+         *       %ecx = nbytes, %eax = write, %eax = len

+         *

+         *   else {

+         *     from += write - nbytes;

+         *     if (nbytes < len) {

+         *       len -= nbytes;

+         *       do {

+         *         PUP(out) = PUP(from);

+         *       } while (--nbytes);

+         *       from = out - dist;

+         *     }

+         *   }

+         */

+#define write_r %eax

+

+        addl    write_r, from_r

+        subl    nbytes_r, from_r        /* from += write - nbytes */

+#undef write_r

+

+#if ! defined( USE_MMX )

+        movl    len(%esp), len_r

+#endif

+        cmpl    nbytes_r, len_r

+        jbe     .L_do_copy1             /* if (nbytes >= len) */

+

+        subl    nbytes_r, len_r         /* len -= nbytes */

+        rep     movsb

+        movl    out_r, from_r

+        subl    dist_r, from_r          /* from = out - dist */

+

+.L_do_copy1:

+        /* regs: %esi = from, %esi = in, %ebp = hold, %bl = bits, %edi = out

+         *       %eax = len

+         *

+         *     while (len > 0) {

+         *       PUP(out) = PUP(from);

+         *       len--;

+         *     }

+         *   }

+         * } while (in < last && out < end);

+         */

+#undef nbytes_r

+#define in_r %esi

+

+        movl    len_r, %ecx

+        rep     movsb

+

+        movl    in(%esp), in_r          /* move in back to %esi, toss from */

+#if defined( USE_MMX )

+        movl    lcode(%esp), %ebx       /* move lcode back to %ebx, toss dist */

+#endif

+        jmp     .L_while_test

+

+#undef len_r

+#undef from_r

+#undef dist_r

+

+.L_invalid_distance_code:

+        /* else {

+         *   strm->msg = "invalid distance code";

+         *   state->mode = BAD;

+         * }

+         */

+        movl    $.L_invalid_distance_code_msg, %ecx

+        movl    $INFLATE_MODE_BAD, %edx

+        jmp     .L_update_stream_state

+

+.L_test_for_end_of_block:

+        /* else if (op & 32) {

+         *   state->mode = TYPE;

+         *   break;

+         * }

+         */

+        testb   $32, %al

+        jz      .L_invalid_literal_length_code  /* if ((op & 32) == 0) */

+

+        movl    $0, %ecx

+        movl    $INFLATE_MODE_TYPE, %edx

+        jmp     .L_update_stream_state

+

+.L_invalid_literal_length_code:

+        /* else {

+         *   strm->msg = "invalid literal/length code";

+         *   state->mode = BAD;

+         * }

+         */

+        movl    $.L_invalid_literal_length_code_msg, %ecx

+        movl    $INFLATE_MODE_BAD, %edx

+        jmp     .L_update_stream_state

+

+.L_invalid_distance_too_far:

+        /* strm->msg = "invalid distance too far back";

+         * state->mode = BAD;

+         */

+        movl    in(%esp), in_r          /* from_r has in's reg, put in back */

+        movl    $.L_invalid_distance_too_far_msg, %ecx

+        movl    $INFLATE_MODE_BAD, %edx

+        jmp     .L_update_stream_state

+

+.L_update_stream_state:

+        /* set strm->msg = %ecx, strm->state->mode = %edx */

+        movl    strm_sp(%esp), %eax

+        testl   %ecx, %ecx              /* if (msg != NULL) */

+        jz      .L_skip_msg

+        movl    %ecx, msg_strm(%eax)    /* strm->msg = msg */

+.L_skip_msg:

+        movl    state_strm(%eax), %eax  /* state = strm->state */

+        movl    %edx, mode_state(%eax)  /* state->mode = edx (BAD | TYPE) */

+

+.L_break_loop:

+

+#define strm_r  %eax

+#define state_r %edx

+

+        /* len = bits >> 3;

+         * in -= len;

+         * bits -= len << 3;

+         * hold &= (1U << bits) - 1;

+         * state->hold = hold;

+         * state->bits = bits;

+         * strm->next_in = in;

+         * strm->next_out = out;

+         */

+        movl    strm_sp(%esp), strm_r

+        movl    bitslong_r, %ecx

+        movl    state_strm(strm_r), state_r

+        shrl    $3, %ecx

+        subl    %ecx, in_r

+        shll    $3, %ecx

+        subl    %ecx, bitslong_r

+        movl    out_r, next_out_strm(strm_r)

+        movl    in_r, next_in_strm(strm_r)

+        movl    bitslong_r, bits_state(state_r)

+

+        movl    bitslong_r, %ecx

+        movl    $1, %ebx                /* overwrites bitslong_r, %bl */

+        shll    %cl, %ebx

+        decl    %ebx

+

+#undef bits_r

+#undef bitslong_r

+

+#if ! defined( USE_MMX )

+

+        andl    %ebx, hold_r

+        movl    hold_r, hold_state(state_r)

+

+#else /* USE_MMX */

+

+        psrlq   used_mm, hold_mm        /* hold_mm >>= last bit length */

+        movd    hold_mm, %ecx

+        andl    %ebx, %ecx

+        movl    %ecx, hold_state(state_r)

+

+#endif

+

+#define last_r %ebx

+

+        /* strm->avail_in = in < last ? 5 + (last - in) : 5 - (in - last) */

+        movl    last(%esp), last_r

+        cmpl    in_r, last_r

+        jbe     .L_last_is_smaller     /* if (in >= last) */

+

+        subl    in_r, last_r           /* last -= in */

+        addl    $5, last_r             /* last += 5 */

+        movl    last_r, avail_in_strm(strm_r)

+        jmp     .L_fixup_out

+.L_last_is_smaller:

+        subl    last_r, in_r           /* in -= last */

+        negl    in_r                   /* in = -in */

+        addl    $5, in_r               /* in += 5 */

+        movl    in_r, avail_in_strm(strm_r)

+

+#undef last_r

+#define end_r %ebx

+

+.L_fixup_out:

+        /* strm->avail_out = out < end ? 257 + (end - out) : 257 - (out - end)*/

+        movl    end(%esp), end_r

+        cmpl    out_r, end_r

+        jbe     .L_end_is_smaller      /* if (out >= end) */

+

+        subl    out_r, end_r           /* end -= out */

+        addl    $257, end_r            /* end += 257 */

+        movl    end_r, avail_out_strm(strm_r)

+        jmp     .L_done

+.L_end_is_smaller:

+        subl    end_r, out_r           /* out -= end */

+        negl    out_r                  /* out = -out */

+        addl    $257, out_r            /* out += 257 */

+        movl    out_r, avail_out_strm(strm_r)

+

+#undef end_r

+

+.L_done:

+#if defined( USE_MMX )

+        emms

+#endif

+        addl    $local_var_size, %esp

+        popf

+        popl    %ebx

+        popl    %ebp

+        popl    %esi

+        popl    %edi

+        ret

+

+.type inflate_fast,@function

+.size inflate_fast,.-inflate_fast

diff --git a/zlib/crc32.c b/zlib/crc32.c
index 0caa44ac9..167fd833d 100644
--- a/zlib/crc32.c
+++ b/zlib/crc32.c
@@ -9,7 +9,7 @@
  * increase in speed on a Power PC using gcc -O3.
  */
 
-/* @(#) $Id$ */
+/* @(#) $Id: crc32.c,v 1.9 2003/03/08 21:47:46 jbj Exp $ */
 
 #ifdef MAKECRCH
 #  include <stdio.h>
@@ -186,10 +186,8 @@ const unsigned long FAR * ZEXPORT get_crc_table()
 #define DO8 DO1; DO1; DO1; DO1; DO1; DO1; DO1; DO1
 
 /* ========================================================================= */
-unsigned long ZEXPORT crc32(crc, buf, len)
-    unsigned long crc;
-    const unsigned char FAR *buf;
-    unsigned len;
+unsigned long ZEXPORT crc32(unsigned long crc, const unsigned char FAR *buf,
+		unsigned len)
 {
     if (buf == Z_NULL) return 0UL;
 
diff --git a/zlib/crc32.h b/zlib/crc32.h
index 8053b6117..cc8e8e789 100644
--- a/zlib/crc32.h
+++ b/zlib/crc32.h
@@ -2,6 +2,7 @@
  * Generated automatically by crc32.c
  */
 
+/*@unchecked@*/
 local const unsigned long FAR crc_table[TBLS][256] =
 {
   {
diff --git a/zlib/deflate.h b/zlib/deflate.h
index b95050103..c05affa85 100644
--- a/zlib/deflate.h
+++ b/zlib/deflate.h
@@ -271,7 +271,8 @@ typedef struct internal_state {
 
         /* in trees.c */
 void _tr_init         OF((deflate_state *s))
-	/*@modifies *s @*/;
+	/*@globals internalState @*/
+	/*@modifies *s, internalState @*/;
 int  _tr_tally        OF((deflate_state *s, unsigned dist, unsigned lc))
 	/*@modifies *s @*/;
 void _tr_flush_block  OF((deflate_state *s, charf *buf, ulg stored_len,
@@ -279,8 +280,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) \
diff --git a/zlib/gzio.c b/zlib/gzio.c
index a52dcf17f..eeec8a2e1 100644
--- a/zlib/gzio.c
+++ b/zlib/gzio.c
@@ -5,7 +5,7 @@
  * Compile this file with -DNO_DEFLATE to avoid the compression code.
  */
 
-/* @(#) $Id: gzio.c,v 1.9 2002/03/17 15:46:23 jbj Exp $ */
+/* @(#) $Id: gzio.c,v 1.10 2002/10/07 09:05:07 jbj Exp $ */
 
 #include <stdio.h>
 
@@ -42,11 +42,16 @@ 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 */
+/*@null@*/
     FILE     *file;   /*!< .gz file */
+/*@null@*/
     Byte     *inbuf;  /*!< input buffer */
+/*@null@*/
     Byte     *outbuf; /*!< output buffer */
     uLong    crc;     /*!< crc32 of uncompressed data */
+/*@null@*/
     char     *msg;    /*!< error message */
+/*@null@*/
     char     *path;   /*!< path name for debugging only */
     int      transparent; /*!< 1 if input file is not a .gz file */
     char     mode;    /*!< 'w' or 'r' */
@@ -55,8 +60,8 @@ typedef struct gz_stream {
 
 
 local gzFile gz_open      OF((const char *path, const char *mode, int  fd))
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 local int do_flush        OF((gzFile file, int flush))
 	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
diff --git a/zlib/infback.c b/zlib/infback.c
index 2209f619f..5e8d9cc0d 100644
--- a/zlib/infback.c
+++ b/zlib/infback.c
@@ -16,7 +16,8 @@
 #include "inffast.h"
 
 /* function prototypes */
-local void fixedtables OF((struct inflate_state FAR *state));
+local void fixedtables OF((struct inflate_state FAR *state))
+	/*@modifies state @*/;
 
 /*
    strm provides memory allocation functions in zalloc and zfree, or
@@ -25,12 +26,8 @@ local void fixedtables OF((struct inflate_state FAR *state));
    windowBits is in the range 8..15, and window is a user-supplied
    window and output buffer that is 2**windowBits bytes.
  */
-int ZEXPORT inflateBackInit_(strm, windowBits, window, version, stream_size)
-z_stream FAR *strm;
-int windowBits;
-unsigned char FAR *window;
-const char *version;
-int stream_size;
+int ZEXPORT inflateBackInit_(z_stream FAR *strm, int windowBits,
+		unsigned char FAR *window, const char *version, int stream_size)
 {
     struct inflate_state FAR *state;
 
@@ -68,8 +65,7 @@ int stream_size;
    used for threaded applications, since the rewriting of the tables and virgin
    may not be thread-safe.
  */
-local void fixedtables(state)
-struct inflate_state FAR *state;
+local void fixedtables(struct inflate_state FAR *state)
 {
 #ifdef BUILDFIXED
     static int virgin = 1;
@@ -235,11 +231,8 @@ struct inflate_state FAR *state;
    inflateBack() can also return Z_STREAM_ERROR if the input parameters
    are not correct, i.e. strm is Z_NULL or the state was not initialized.
  */
-int ZEXPORT inflateBack(strm, in, out, opaque)
-z_stream FAR *strm;
-in_func in;
-out_func out;
-void FAR *opaque;
+int ZEXPORT inflateBack(z_stream FAR *strm, in_func in, out_func out,
+		void FAR *opaque)
 {
     struct inflate_state FAR *state;
     unsigned char *next, *put;	/* next input and output */
@@ -598,8 +591,7 @@ void FAR *opaque;
     return ret;
 }
 
-int ZEXPORT inflateBackEnd(strm)
-z_stream FAR *strm;
+int ZEXPORT inflateBackEnd(z_stream FAR *strm)
 {
     struct inflate_state FAR *state;
 
diff --git a/zlib/inffast.c b/zlib/inffast.c
index 3a5e6f1cb..d1db74c44 100644
--- a/zlib/inffast.c
+++ b/zlib/inffast.c
@@ -61,9 +61,7 @@
       requires strm->avail_out >= 258 for each loop to avoid checking for
       output space.
  */
-void inflate_fast(strm, start)
-z_streamp strm;
-unsigned start;		/* inflate()'s starting value for strm->avail_out */
+void inflate_fast(z_streamp strm, unsigned start)
 {
     struct inflate_state FAR *state;
     unsigned char FAR *in;	/* local strm->next_in */
diff --git a/zlib/inffast.h b/zlib/inffast.h
index 977101b3f..75aef97ec 100644
--- a/zlib/inffast.h
+++ b/zlib/inffast.h
@@ -8,4 +8,5 @@
    subject to change. Applications should only use zlib.h.
  */
 
-void inflate_fast OF((z_streamp strm, unsigned start));
+void inflate_fast OF((z_streamp strm, unsigned start))
+	/*@modifies strm @*/;
diff --git a/zlib/inflate.c b/zlib/inflate.c
index 2e9d13490..44f4e78ff 100644
--- a/zlib/inflate.c
+++ b/zlib/inflate.c
@@ -83,16 +83,19 @@
 #endif
 
 /* function prototypes */
-local void fixedtables OF((struct inflate_state FAR *state));
-local int updatewindow OF((z_streamp strm, unsigned out));
+local void fixedtables OF((struct inflate_state FAR *state))
+	/*@modifies state @*/;
+local int updatewindow OF((z_streamp strm, unsigned out))
+	/*@*/;
 #ifdef BUILDFIXED
-   void makefixed OF((void));
+   void makefixed OF((void))
+	/*@*/;
 #endif
 local unsigned syncsearch OF((unsigned *have, unsigned char FAR *buf,
-                              unsigned len));
+                              unsigned len))
+	/*@modifies *have @*/;
 
-int ZEXPORT inflateReset(strm)
-z_streamp strm;
+int ZEXPORT inflateReset(z_streamp strm)
 {
     struct inflate_state FAR *state;
 
@@ -111,11 +114,8 @@ z_streamp strm;
     return Z_OK;
 }
 
-int ZEXPORT inflateInit2_(strm, windowBits, version, stream_size)
-z_streamp strm;
-int windowBits;
-const char *version;
-int stream_size;
+int ZEXPORT inflateInit2_(z_streamp strm, int windowBits, const char *version,
+		int stream_size)
 {
     struct inflate_state FAR *state;
 
@@ -150,10 +150,7 @@ int stream_size;
     return inflateReset(strm);
 }
 
-int ZEXPORT inflateInit_(strm, version, stream_size)
-z_streamp strm;
-const char *version;
-int stream_size;
+int ZEXPORT inflateInit_(z_streamp strm, const char *version, int stream_size)
 {
     return inflateInit2_(strm, DEF_WBITS, version, stream_size);
 }
@@ -168,8 +165,7 @@ int stream_size;
    used for threaded applications, since the rewriting of the tables and virgin
    may not be thread-safe.
  */
-local void fixedtables(state)
-struct inflate_state FAR *state;
+local void fixedtables(struct inflate_state FAR *state)
 {
 #ifdef BUILDFIXED
     static int virgin = 1;
@@ -232,7 +228,7 @@ struct inflate_state FAR *state;
 
     a.out > inffixed.h
  */
-void makefixed()
+void makefixed(void)
 {
     unsigned low, size;
     struct inflate_state state;
@@ -286,9 +282,7 @@ void makefixed()
    output will fall in the output data, making match copies simpler and faster.
    The advantage may be dependent on the size of the processor's data caches.
  */
-local int updatewindow(strm, out)
-z_streamp strm;
-unsigned out;
+local int updatewindow(z_streamp strm, unsigned out)
 {
     struct inflate_state FAR *state;
     unsigned copy, dist;
@@ -513,9 +507,7 @@ unsigned out;
    will return Z_BUF_ERROR if it has not reached the end of the stream.
  */
 
-int ZEXPORT inflate(strm, flush)
-z_streamp strm;
-int flush;
+int ZEXPORT inflate(z_streamp strm, int flush)
 {
     struct inflate_state FAR *state;
     unsigned char *next, *put;	/* next input and output */
@@ -1054,8 +1046,7 @@ int flush;
     return ret;
 }
 
-int ZEXPORT inflateEnd(strm)
-z_streamp strm;
+int ZEXPORT inflateEnd(z_streamp strm)
 {
     struct inflate_state FAR *state;
     if (strm == Z_NULL || strm->state == Z_NULL || strm->zfree == Z_NULL)
@@ -1068,10 +1059,8 @@ z_streamp strm;
     return Z_OK;
 }
 
-int ZEXPORT inflateSetDictionary(strm, dictionary, dictLength)
-z_streamp strm;
-const Bytef *dictionary;
-uInt dictLength;
+int ZEXPORT inflateSetDictionary(z_streamp strm, const Bytef *dictionary,
+		uInt dictLength)
 {
     struct inflate_state FAR *state;
     unsigned long id;
@@ -1113,10 +1102,7 @@ uInt dictLength;
    called again with more data and the *have state.  *have is initialized to
    zero for the first call.
  */
-local unsigned syncsearch(have, buf, len)
-unsigned *have;
-unsigned char FAR *buf;
-unsigned len;
+local unsigned syncsearch(unsigned *have, unsigned char FAR *buf, unsigned len)
 {
     unsigned got;
     unsigned next;
@@ -1136,8 +1122,7 @@ unsigned len;
     return next;
 }
 
-int ZEXPORT inflateSync(strm)
-z_streamp strm;
+int ZEXPORT inflateSync(z_streamp strm)
 {
     unsigned len;		/* number of bytes to look at or looked at */
     unsigned long in, out;	/* temporary to save total_in and total_out */
@@ -1187,8 +1172,7 @@ z_streamp strm;
    block. When decompressing, PPP checks that at the end of input packet,
    inflate is waiting for these length bytes.
  */
-int ZEXPORT inflateSyncPoint(strm)
-z_streamp strm;
+int ZEXPORT inflateSyncPoint(z_streamp strm)
 {
     struct inflate_state FAR *state;
 
@@ -1197,9 +1181,7 @@ z_streamp strm;
     return state->mode == STORED && state->bits == 0;
 }
 
-int ZEXPORT inflateCopy(dest, source)
-z_streamp dest;
-z_streamp source;
+int ZEXPORT inflateCopy(z_streamp dest, z_streamp source)
 {
     struct inflate_state FAR *state;
     struct inflate_state FAR *copy;
diff --git a/zlib/inftrees.c b/zlib/inftrees.c
index 33073c648..3899710a5 100644
--- a/zlib/inftrees.c
+++ b/zlib/inftrees.c
@@ -29,13 +29,8 @@ const char inflate_copyright[] =
    table index bits.  It will differ if the request is greater than the
    longest code or if it is less than the shortest code.
  */
-int inflate_table(type, lens, codes, table, bits, work)
-codetype type;
-unsigned short FAR *lens;
-unsigned codes;
-code * FAR *table;
-unsigned *bits;
-unsigned short FAR *work;
+int inflate_table(codetype type, unsigned short FAR *lens, unsigned codes,
+		code * FAR *table, unsigned *bits, unsigned short FAR *work)
 {
     unsigned len;		/* a code's length in bits */
     unsigned sym;		/* index of code symbols */
diff --git a/zlib/inftrees.h b/zlib/inftrees.h
index e49c1477c..0c4fc3799 100644
--- a/zlib/inftrees.h
+++ b/zlib/inftrees.h
@@ -52,4 +52,5 @@ typedef enum {
 
 extern int inflate_table OF((codetype type, unsigned short FAR *lens,
                              unsigned codes, code * FAR *table, unsigned *bits,
-                             unsigned short FAR *work));
+                             unsigned short FAR *work))
+	/*@*/;
diff --git a/zlib/trees.c b/zlib/trees.c
index 80db721b0..2c1430e08 100644
--- a/zlib/trees.c
+++ b/zlib/trees.c
@@ -34,7 +34,7 @@
  *          Addison-Wesley, 1983. ISBN 0-201-06672-6.
  */
 
-/* @(#) $Id: trees.c,v 1.8 2002/03/17 15:46:23 jbj Exp $ */
+/* @(#) $Id: trees.c,v 1.9 2002/06/22 18:51:58 jbj Exp $ */
 
 /* #define GEN_TREES_H */
 
@@ -98,6 +98,7 @@ local const uch bl_order[BL_CODES]
 #if defined(GEN_TREES_H) || !defined(STDC)
 /* non ANSI compilers may not accept trees.h */
 
+/*@unchecked@*/
 local ct_data static_ltree[L_CODES+2];
 /*!< The static literal tree. Since the bit lengths are imposed, there is no
  * need for the L_CODES extra codes used during heap construction. However
@@ -105,17 +106,20 @@ local ct_data static_ltree[L_CODES+2];
  * below).
  */
 
+/*@unchecked@*/
 local ct_data static_dtree[D_CODES];
 /*!< The static distance tree. (Actually a trivial tree since all codes use
  * 5 bits.)
  */
 
+/*@unchecked@*/
 uch _dist_code[DIST_CODE_LEN];
 /*!< Distance codes. The first 256 values correspond to the distances
  * 3 .. 258, the last 256 values correspond to the top 8 bits of
  * the 15 bit distances.
  */
 
+/*@unchecked@*/
 uch _length_code[MAX_MATCH-MIN_MATCH+1];
 /*!< length code for each normalized match length (0 == MIN_MATCH) */
 
@@ -159,7 +163,8 @@ local static_tree_desc  static_bl_desc =
  */
 
 local void tr_static_init OF((void))
-	/*@*/;
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
 local void init_block     OF((deflate_state *s))
 	/*@modifies *s @*/;
 local void pqdownheap     OF((deflate_state *s, ct_data *tree, int k))
@@ -190,8 +195,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
diff --git a/zlib/trees.h b/zlib/trees.h
index 72facf900..7eab165e8 100644
--- a/zlib/trees.h
+++ b/zlib/trees.h
@@ -1,5 +1,6 @@
 /* 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}},
@@ -61,6 +62,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}},
@@ -70,6 +72,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,
@@ -99,6 +102,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,
@@ -115,11 +119,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/zlib.h b/zlib/zlib.h
index 49d090443..05d5594a3 100644
--- a/zlib/zlib.h
+++ b/zlib/zlib.h
@@ -69,20 +69,26 @@ typedef void   (*free_func)  OF((voidpf opaque, voidpf address))
 struct internal_state;
 
 typedef struct z_stream_s {
+/*@null@*/
     Bytef    *next_in;  /* next input byte */
     uInt     avail_in;  /* number of bytes available at next_in */
     uLong    total_in;  /* total nb of input bytes read so far */
 
+/*@null@*/
     Bytef    *next_out; /* next output byte should be put there */
     uInt     avail_out; /* remaining free space at next_out */
     uLong    total_out; /* total nb of bytes output so far */
 
-/*@observer@*/
+/*@observer@*/ /*@null@*/
     char     *msg;      /* last error message, NULL if no error */
+/*@null@*/
     struct internal_state FAR *state; /* not visible by applications */
 
+/*@null@*/
     alloc_func zalloc;  /* used to allocate the internal state */
+/*@null@*/
     free_func  zfree;   /* used to free the internal state */
+/*@null@*/
     voidpf     opaque;  /* private data object passed to zalloc and zfree */
 
     int     data_type;  /* best guess about the data type: ascii or binary */
@@ -507,7 +513,8 @@ ZEXTERN int ZEXPORT deflateCopy OF((z_streamp dest,
 */
 
 ZEXTERN int ZEXPORT deflateReset OF((z_streamp strm))
-	/*@modifies strm @*/;
+	/*@globals internalState @*/
+	/*@modifies strm, internalState @*/;
 /*
      This function is equivalent to deflateEnd followed by deflateInit,
    but does not free and reallocate all the internal compression state.
@@ -741,7 +748,8 @@ ZEXTERN int ZEXPORT inflateBackEnd(z_stream FAR *strm)
 
 ZEXTERN int ZEXPORT compress OF((Bytef *dest,   uLongf *destLen,
                                  const Bytef *source, uLong sourceLen))
-	/*@modifies *dest, *destLen @*/;
+	/*@globals internalState @*/
+	/*@modifies *dest, *destLen, internalState @*/;
 /*
      Compresses the source buffer into the destination buffer.  sourceLen is
    the byte length of the source buffer. Upon entry, destLen is the total
@@ -758,7 +766,8 @@ ZEXTERN int ZEXPORT compress OF((Bytef *dest,   uLongf *destLen,
 ZEXTERN int ZEXPORT compress2 OF((Bytef *dest,   uLongf *destLen,
                                   const Bytef *source, uLong sourceLen,
                                   int level))
-	/*@modifies *dest, *destLen @*/;
+	/*@globals internalState @*/
+	/*@modifies *dest, *destLen, internalState @*/;
 /*
      Compresses the source buffer into the destination buffer. The level
    parameter has the same meaning as in deflateInit.  sourceLen is the byte
@@ -794,8 +803,8 @@ ZEXTERN int ZEXPORT uncompress OF((Bytef *dest,   uLongf *destLen,
 typedef voidp gzFile;
 
 ZEXTERN gzFile ZEXPORT gzopen  OF((const char *path, const char *mode))
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 /*
      Opens a gzip (.gz) file for reading or writing. The mode parameter
    is as in fopen ("rb" or "wb") but can also include a compression level
@@ -812,8 +821,8 @@ ZEXTERN gzFile ZEXPORT gzopen  OF((const char *path, const char *mode))
    zlib error is Z_MEM_ERROR).  */
 
 ZEXTERN gzFile ZEXPORT gzdopen  OF((int fd, const char *mode))
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 /*
      gzdopen() associates a gzFile with the file descriptor fd.  File
    descriptors are obtained from calls like open, dup, creat, pipe or
@@ -987,7 +996,8 @@ ZEXTERN const char * ZEXPORT gzerror OF((gzFile file, int *errnum))
    compression library.
 */
 
-ZEXTERN uLong ZEXPORT adler32 OF((uLong adler, const Bytef *buf, uInt len))
+ZEXTERN uLong ZEXPORT adler32 OF((uLong adler, /*@null@*/ const Bytef *buf,
+		uInt len))
 	/*@*/;
 
 /*
@@ -1005,7 +1015,8 @@ ZEXTERN uLong ZEXPORT adler32 OF((uLong adler, const Bytef *buf, uInt len))
      if (adler != original_adler) error();
 */
 
-ZEXTERN uLong ZEXPORT crc32   OF((uLong crc, const Bytef *buf, uInt len))
+ZEXTERN uLong ZEXPORT crc32   OF((uLong crc, /*@null@*/ const Bytef *buf,
+		uInt len))
 	/*@*/;
 /*
      Update a running crc with the bytes buf[0..len-1] and return the updated
@@ -1030,7 +1041,8 @@ ZEXTERN uLong ZEXPORT crc32   OF((uLong crc, const Bytef *buf, uInt len))
  */
 ZEXTERN int ZEXPORT deflateInit_ OF((z_streamp strm, int level,
                                      const char *version, int stream_size))
-	/*@modifies strm @*/;
+	/*@globals internalState @*/
+	/*@modifies strm, internalState @*/;
 ZEXTERN int ZEXPORT inflateInit_ OF((z_streamp strm,
                                      const char *version, int stream_size))
 	/*@modifies strm @*/;
@@ -1038,7 +1050,8 @@ ZEXTERN int ZEXPORT deflateInit2_ OF((z_streamp strm, int  level, int  method,
                                       int windowBits, int memLevel,
                                       int strategy, const char *version,
                                       int stream_size))
-	/*@modifies strm @*/;
+	/*@globals internalState @*/
+	/*@modifies strm, internalState @*/;
 ZEXTERN int ZEXPORT inflateInit2_ OF((z_streamp strm, int  windowBits,
                                       const char *version, int stream_size))
 	/*@modifies strm @*/;
diff --git a/zlib/zutil.h b/zlib/zutil.h
index 00740fb76..0a6c0c924 100644
--- a/zlib/zutil.h
+++ b/zlib/zutil.h
@@ -8,7 +8,7 @@
    subject to change. Applications should only use zlib.h.
  */
 
-/* @(#) $Id: zutil.h,v 1.7 2002/03/17 15:46:23 jbj Exp $ */
+/* @(#) $Id: zutil.h,v 1.8 2002/10/07 09:05:07 jbj Exp $ */
 
 #ifndef _Z_UTIL_H
 #define _Z_UTIL_H
@@ -37,6 +37,7 @@ typedef unsigned short ush;
 typedef ush FAR ushf;
 typedef unsigned long  ulg;
 
+/*@unchecked@*/
 extern const char *z_errmsg[10]; /* indexed by 2-zlib_error */
 /* (size given to avoid silly warnings with Visual C++) */