Splint fiddles.

CVS patchset: 6736
CVS date: 2003/04/09 21:46:31

7 files changed, 178 insertions, 153 deletions

diff --git a/rpmio/digest.c b/rpmio/digest.c
index 1cca844c4..5268b9e13 100644
--- a/rpmio/digest.c
+++ b/rpmio/digest.c
@@ -54,28 +54,28 @@ rpmDigestInit(pgpHashAlgo hashalgo, rpmDigestFlags flags)
     case PGPHASHALGO_MD5:
 	ctx->digestlen = 16;
 	ctx->datalen = 64;
-	/*@-sizeoftype@*/ /* FIX: union, not void pointer */
+/*@-sizeoftype@*/ /* FIX: union, not void pointer */
 	ctx->paramlen = sizeof(md5Param);
-	/*@=sizeoftype@*/
+/*@=sizeoftype@*/
 	ctx->param = xcalloc(1, ctx->paramlen);
-	/*@-type@*/ /* FIX: cast? */
+/*@-type@*/ /* FIX: cast? */
 	ctx->Reset = (void *) md5Reset;
 	ctx->Update = (void *) md5Update;
 	ctx->Digest = (void *) md5Digest;
-	/*@=type@*/
+/*@=type@*/
 	break;
     case PGPHASHALGO_SHA1:
 	ctx->digestlen = 20;
 	ctx->datalen = 64;
-	/*@-sizeoftype@*/ /* FIX: union, not void pointer */
+/*@-sizeoftype@*/ /* FIX: union, not void pointer */
 	ctx->paramlen = sizeof(sha1Param);
-	/*@=sizeoftype@*/
+/*@=sizeoftype@*/
 	ctx->param = xcalloc(1, ctx->paramlen);
-	/*@-type@*/ /* FIX: cast? */
+/*@-type@*/ /* FIX: cast? */
 	ctx->Reset = (void *) sha1Reset;
 	ctx->Update = (void *) sha1Update;
 	ctx->Digest = (void *) sha1Digest;
-	/*@=type@*/
+/*@=type@*/
 	break;
     case PGPHASHALGO_RIPEMD160:
     case PGPHASHALGO_MD2:
@@ -111,6 +111,7 @@ DPRINTF((stderr, "*** Update(%p,%p,%d) param %p \"%s\"\n", ctx, data, len, ctx->
 
 /*@unchecked@*/
 static int _ie = 0x44332211;
+
 /*@-redef@*/
 /*@unchecked@*/
 static union _dendian {
@@ -118,6 +119,7 @@ static union _dendian {
     char b[4];
 } *_endian = (union _dendian *)&_ie;
 /*@=redef@*/
+
 #define        IS_BIG_ENDIAN()         (_endian->b[0] == '\x44')
 #define        IS_LITTLE_ENDIAN()      (_endian->b[0] == '\x11')
 
@@ -134,18 +136,18 @@ rpmDigestFinal(DIGEST_CTX ctx, void ** datap, size_t *lenp, int asAscii)
     digest = xmalloc(ctx->digestlen);
 
 DPRINTF((stderr, "*** Final(%p,%p,%p,%d) param %p digest %p\n", ctx, datap, lenp, asAscii, ctx->param, digest));
-    /*@-noeffectuncon@*/ /* FIX: check rc */
+/*@-noeffectuncon@*/ /* FIX: check rc */
     (void) (*ctx->Digest) (ctx->param, digest);
-    /*@=noeffectuncon@*/
+/*@=noeffectuncon@*/
 
-    /*@-sizeoftype@*/
+/*@-sizeoftype@*/
     if (IS_LITTLE_ENDIAN())
     for (i = 0; i < (ctx->digestlen/sizeof(uint32)); i++)
 	digest[i] = swapu32(digest[i]);
-    /*@=sizeoftype@*/
+/*@=sizeoftype@*/
 
     /* Return final digest. */
-    /*@-branchstate@*/
+/*@-branchstate@*/
     if (!asAscii) {
 	if (lenp) *lenp = ctx->digestlen;
 	if (datap) {
@@ -166,7 +168,7 @@ DPRINTF((stderr, "*** Final(%p,%p,%p,%d) param %p digest %p\n", ctx, datap, lenp
 	    *t = '\0';
 	}
     }
-    /*@=branchstate@*/
+/*@=branchstate@*/
     if (digest) {
 	memset(digest, 0, ctx->digestlen);	/* In case it's sensitive */
 	free(digest);
diff --git a/rpmio/rpmpgp.c b/rpmio/rpmpgp.c
index bcab82342..fbfa5b7d4 100644
--- a/rpmio/rpmpgp.c
+++ b/rpmio/rpmpgp.c
@@ -476,7 +476,6 @@ static int pgpPrtSigParams(/*@unused@*/ pgpTag tag, byte pubkey_algo, byte sigty
     for (i = 0; p < pend; i++, p += pgpMpiLen(p)) {
 	if (pubkey_algo == PGPPUBKEYALGO_RSA) {
 	    if (i >= 1) break;
-	    /*@-mods@*/
 	    if (_dig &&
 	(sigtype == PGPSIGTYPE_BINARY || sigtype == PGPSIGTYPE_TEXT))
 	    {
@@ -490,11 +489,9 @@ fprintf(stderr, "\t  m**d = "),  mp32println(stderr, _dig->c.size, _dig->c.data)
 		    /*@switchbreak@*/ break;
 		}
 	    }
-	    /*@=mods@*/
 	    pgpPrtStr("", pgpSigRSA[i]);
 	} else if (pubkey_algo == PGPPUBKEYALGO_DSA) {
 	    if (i >= 2) break;
-	    /*@-mods@*/
 	    if (_dig &&
 	(sigtype == PGPSIGTYPE_BINARY || sigtype == PGPSIGTYPE_TEXT))
 	    {
@@ -513,7 +510,6 @@ fprintf(stderr, "\t  m**d = "),  mp32println(stderr, _dig->c.size, _dig->c.data)
 		}
 		if (xx) return xx;
 	    }
-	    /*@=mods@*/
 	    pgpPrtStr("", pgpSigDSA[i]);
 	} else {
 	    if (_print)
@@ -527,6 +523,8 @@ fprintf(stderr, "\t  m**d = "),  mp32println(stderr, _dig->c.size, _dig->c.data)
 }
 
 int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
+	/*@globals _digp @*/
+	/*@modifies *_digp @*/
 {
     byte version = h[0];
     byte * p;
@@ -555,7 +553,6 @@ int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
 	pgpPrtHex(" signhash16", v->signhash16, sizeof(v->signhash16));
 	pgpPrtNL();
 
-/*@-mods@*/
 	if (_digp && _digp->pubkey_algo == 0) {
 	    _digp->version = v->version;
 	    _digp->hashlen = v->hashlen;
@@ -567,7 +564,6 @@ int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
 	    _digp->hash_algo = v->hash_algo;
 	    memcpy(_digp->signhash16, v->signhash16, sizeof(_digp->signhash16));
 	}
-/*@=mods@*/
 
 	p = ((byte *)v) + sizeof(*v);
 	rc = pgpPrtSigParams(tag, v->pubkey_algo, v->sigtype, p, h, hlen);
@@ -590,12 +586,10 @@ int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
 
 if (_debug && _print)
 fprintf(stderr, "   hash[%u] -- %s\n", plen, pgpHexStr(p, plen));
-/*@-mods@*/
 	if (_digp && _digp->pubkey_algo == 0) {
 	    _digp->hashlen = sizeof(*v) + plen;
 	    _digp->hash = memcpy(xmalloc(_digp->hashlen), v, _digp->hashlen);
 	}
-/*@=mods@*/
 	(void) pgpPrtSubType(p, plen, v->sigtype);
 	p += plen;
 
@@ -614,7 +608,6 @@ fprintf(stderr, " unhash[%u] -- %s\n", plen, pgpHexStr(p, plen));
 	pgpPrtHex(" signhash16", p, 2);
 	pgpPrtNL();
 
-/*@-mods@*/
 	if (_digp && _digp->pubkey_algo == 0) {
 	    _digp->version = v->version;
 	    _digp->sigtype = v->sigtype;
@@ -622,7 +615,6 @@ fprintf(stderr, " unhash[%u] -- %s\n", plen, pgpHexStr(p, plen));
 	    _digp->hash_algo = v->hash_algo;
 	    memcpy(_digp->signhash16, p, sizeof(_digp->signhash16));
 	}
-/*@=mods@*/
 
 	p += 2;
 	if (p > (h + hlen))
@@ -686,15 +678,14 @@ static const char * pgpSecretELGAMAL[] = {
 
 static const byte * pgpPrtPubkeyParams(byte pubkey_algo,
 		/*@returned@*/ const byte *p, const byte *h, unsigned int hlen)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     int i;
 
     for (i = 0; p < &h[hlen]; i++, p += pgpMpiLen(p)) {
 	if (pubkey_algo == PGPPUBKEYALGO_RSA) {
 	    if (i >= 2) break;
-	    /*@-mods@*/
 	    if (_dig) {
 		switch (i) {
 		case 0:		/* n */
@@ -725,11 +716,9 @@ fprintf(stderr, "\t     e = "),  mp32println(stderr, _dig->rsa_pk.e.size, _dig->
 		    /*@switchbreak@*/ break;
 		}
 	    }
-	    /*@=mods@*/
 	    pgpPrtStr("", pgpPublicRSA[i]);
 	} else if (pubkey_algo == PGPPUBKEYALGO_DSA) {
 	    if (i >= 4) break;
-	    /*@-mods@*/
 	    if (_dig) {
 		switch (i) {
 		case 0:		/* p */
@@ -756,7 +745,6 @@ fprintf(stderr, "\t     y = "),  mp32println(stderr, _dig->y.size, _dig->y.data)
 		    /*@switchbreak@*/ break;
 		}
 	    }
-	    /*@=mods@*/
 	    pgpPrtStr("", pgpPublicDSA[i]);
 	} else if (pubkey_algo == PGPPUBKEYALGO_ELGAMAL_ENCRYPT) {
 	    if (i >= 3) break;
@@ -765,7 +753,6 @@ fprintf(stderr, "\t     y = "),  mp32println(stderr, _dig->y.size, _dig->y.data)
 	    if (_print)
 		fprintf(stderr, "%7d", i);
 	}
-    /*@=mods@*/
 	pgpPrtStr("", pgpMpiStr(p));
 	pgpPrtNL();
     }
@@ -848,6 +835,8 @@ static const byte * pgpPrtSeckeyParams(/*@unused@*/ byte pubkey_algo,
 }
 
 int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
+	/*@globals _digp @*/
+	/*@modifies *_digp @*/
 {
     byte version = *h;
     const byte * p;
@@ -868,13 +857,11 @@ int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
 	    fprintf(stderr, " valid %u days", plen);
 	pgpPrtNL();
 
-/*@-mods@*/
 	if (_digp && _digp->tag == tag) {
 	    _digp->version = v->version;
 	    memcpy(_digp->time, v->time, sizeof(_digp->time));
 	    _digp->pubkey_algo = v->pubkey_algo;
 	}
-/*@=mods@*/
 
 	p = ((byte *)v) + sizeof(*v);
 	p = pgpPrtPubkeyParams(v->pubkey_algo, p, h, hlen);
@@ -889,13 +876,11 @@ int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
 	    fprintf(stderr, " %-24.24s(0x%08x)", ctime(&t), (unsigned)t);
 	pgpPrtNL();
 
-/*@-mods@*/
 	if (_digp && _digp->tag == tag) {
 	    _digp->version = v->version;
 	    memcpy(_digp->time, v->time, sizeof(_digp->time));
 	    _digp->pubkey_algo = v->pubkey_algo;
 	}
-/*@=mods@*/
 
 	p = ((byte *)v) + sizeof(*v);
 	p = pgpPrtPubkeyParams(v->pubkey_algo, p, h, hlen);
@@ -912,18 +897,18 @@ int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
 
 /*@-boundswrite@*/
 int pgpPrtUserID(pgpTag tag, const byte *h, unsigned int hlen)
+	/*@globals _digp @*/
+	/*@modifies *_digp @*/
 {
     pgpPrtVal("", pgpTagTbl, tag);
     if (_print)
 	fprintf(stderr, " \"%.*s\"", (int)hlen, (const char *)h);
     pgpPrtNL();
-/*@-mods@*/
     if (_digp) {
 	char * t;
 	_digp->userid = t = memcpy(xmalloc(hlen+1), h, hlen);
 	t[hlen] = '\0';
     }
-/*@=mods@*/
     return 0;
 }
 /*@=boundswrite@*/
@@ -1062,9 +1047,9 @@ void pgpCleanDig(pgpDig dig)
 	mp32nfree(&dig->c);
 	mp32nfree(&dig->rsahm);
     }
-    /*@-nullstate@*/
+/*@-nullstate@*/
     return;
-    /*@=nullstate@*/
+/*@=nullstate@*/
 }
 /*@=boundswrite@*/
 
@@ -1122,13 +1107,14 @@ pgpDig pgpFreeDig(/*@only@*/ /*@null@*/ pgpDig dig)
 }
 
 int pgpPrtPkts(const byte * pkts, unsigned int pktlen, pgpDig dig, int printing)
+	/*@globals _dig, _digp, _print @*/
+	/*@modifies _dig, _digp, *_digp, _print @*/
 {
     unsigned int val = *pkts;
     const byte *p;
     unsigned int pleft;
     int len;
 
-    /*@-mods@*/
     _print = printing;
     _dig = dig;
     if (dig != NULL && (val & 0x80)) {
@@ -1137,7 +1123,6 @@ int pgpPrtPkts(const byte * pkts, unsigned int pktlen, pgpDig dig, int printing)
 	_digp->tag = tag;
     } else
 	_digp = NULL;
-    /*@=mods@*/
 
     for (p = pkts, pleft = pktlen; p < (pkts + pktlen); p += len, pleft -= len) {
 	len = pgpPrtPkt(p, pleft);
diff --git a/rpmio/rpmpgp.h b/rpmio/rpmpgp.h
index b3102e09b..3c9a097e9 100644
--- a/rpmio/rpmpgp.h
+++ b/rpmio/rpmpgp.h
@@ -1159,8 +1159,8 @@ int pgpPrtSubType(const byte *h, unsigned int hlen, pgpSigType sigtype)
  * @return		0 on success
  */
 int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /**
  * Print/parse an OpenPGP key packet.
@@ -1170,8 +1170,8 @@ int pgpPrtSig(pgpTag tag, const byte *h, unsigned int hlen)
  * @return		0 on success
  */
 int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /**
  * Print/parse an OpenPGP userid packet.
@@ -1181,8 +1181,8 @@ int pgpPrtKey(pgpTag tag, const byte *h, unsigned int hlen)
  * @return		0 on success
  */
 int pgpPrtUserID(pgpTag tag, const byte *h, unsigned int hlen)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /**
  * Print/parse an OpenPGP comment packet.
@@ -1202,8 +1202,8 @@ int pgpPrtComment(pgpTag tag, const byte *h, unsigned int hlen)
  * @return		-1 on error, otherwise this packet length
  */
 int pgpPrtPkt(const byte *pkt, unsigned int pleft)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 /*@=exportlocal@*/
 
 /**
@@ -1215,8 +1215,8 @@ int pgpPrtPkt(const byte *pkt, unsigned int pleft)
  * @return		-1 on error, 0 on success
  */
 int pgpPrtPkts(const byte *pkts, unsigned int pktlen, pgpDig dig, int printing)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies dig, fileSystem, internalState @*/;
 
 /**
  * Parse armored OpenPGP packets from a file.
diff --git a/rpmio/rpmrpc.c b/rpmio/rpmrpc.c
index 9f3be35d7..9ea92713c 100644
--- a/rpmio/rpmrpc.c
+++ b/rpmio/rpmrpc.c
@@ -821,12 +821,13 @@ static /*@only@*/ char * ftpBuf = NULL;
 #define alloca_strdup(_s)       strcpy(alloca(strlen(_s)+1), (_s))
 
 /*@-boundswrite@*/
-/*@-mods@*/
 static int ftpNLST(const char * url, ftpSysCall_t ftpSysCall,
 		/*@out@*/ /*@null@*/ struct stat * st,
 		/*@out@*/ /*@null@*/ char * rlbuf, size_t rlbufsiz)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies *st, *rlbuf, fileSystem, internalState @*/
+	/*@globals ftpBufAlloced, ftpBuf,
+		fileSystem, internalState @*/
+	/*@modifies *st, *rlbuf, ftpBufAlloced, ftpBuf,
+		fileSystem, internalState @*/
 {
     FD_t fd;
     const char * path;
@@ -1011,7 +1012,6 @@ exit:
     (void) ufdClose(fd);
     return rc;
 }
-/*@=mods@*/
 /*@=boundswrite@*/
 
 static const char * statstr(const struct stat * st,
@@ -1035,34 +1035,30 @@ static const char * statstr(const struct stat * st,
 static int ftp_st_ino = 0xdead0000;
 
 static int ftpStat(const char * path, /*@out@*/ struct stat *st)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies *st, fileSystem, internalState @*/
+	/*@globals ftp_st_ino, fileSystem, internalState @*/
+	/*@modifies *st, ftp_st_ino, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
     rc = ftpNLST(path, DO_FTP_STAT, st, NULL, 0);
     /* XXX fts(3) needs/uses st_ino, make something up for now. */
-    /*@-mods@*/
     if (st->st_ino == 0)
 	st->st_ino = ftp_st_ino++;
-    /*@=mods@*/
 if (_ftp_debug)
 fprintf(stderr, "*** ftpStat(%s) rc %d\n%s", path, rc, statstr(st, buf));
     return rc;
 }
 
 static int ftpLstat(const char * path, /*@out@*/ struct stat *st)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies *st, fileSystem, internalState @*/
+	/*@globals ftp_st_ino, fileSystem, internalState @*/
+	/*@modifies *st, ftp_st_ino, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
     rc = ftpNLST(path, DO_FTP_LSTAT, st, NULL, 0);
     /* XXX fts(3) needs/uses st_ino, make something up for now. */
-    /*@-mods@*/
     if (st->st_ino == 0)
 	st->st_ino = ftp_st_ino++;
-    /*@=mods@*/
 if (_ftp_debug)
 fprintf(stderr, "*** ftpLstat(%s) rc %d\n%s\n", path, rc, statstr(st, buf));
     return rc;
@@ -1086,7 +1082,7 @@ struct __dirstream {
     size_t size;		/* Total valid data in the block.  */
     size_t offset;		/* Current offset into the block.  */
     off_t filepos;		/* Position of next entry to read.  */
-#if defined(HAVE_PTHREAD_H) && !defined(__LCLINT__)
+#if defined(HAVE_PTHREAD_H)
     pthread_mutex_t lock;	/* Mutex lock for this structure.  */
 #endif
 };
@@ -1111,7 +1107,6 @@ static int ftpmagicdir = 0x8440291;
 #define	ISFTPMAGIC(_dir) (!memcmp((_dir), &ftpmagicdir, sizeof(ftpmagicdir)))
 
 /*@-boundswrite@*/
-/*@-type@*/ /* FIX: abstract DIR */
 /*@null@*/
 static DIR * ftpOpendir(const char * path)
 	/*@globals fileSystem, internalState @*/
@@ -1263,12 +1258,10 @@ static struct dirent * ftpReaddir(DIR * dir)
     int ac;
     int i;
 
-    /*@+voidabstract@*/
     if (mydir == NULL || !ISFTPMAGIC(mydir) || mydir->data == NULL) {
 	/* XXX TODO: EBADF errno. */
 	return NULL;
     }
-    /*@=voidabstract@*/
 
     dp = (struct dirent *) mydir->data;
     av = (const char **) (dp + 1);
@@ -1284,6 +1277,7 @@ static struct dirent * ftpReaddir(DIR * dir)
     mydir->offset = i;
 
     /* XXX glob(3) uses REAL_DIR_ENTRY(dp) test on d_ino */
+/*@-type@*/
     dp->d_ino = i + 1;		/* W2DO? */
     dp->d_reclen = 0;		/* W2DO? */
 
@@ -1293,16 +1287,14 @@ static struct dirent * ftpReaddir(DIR * dir)
     dp->d_type = dt[i];
 /*@=boundsread@*/
 #endif
+/*@=type@*/
 
     strncpy(dp->d_name, av[i], sizeof(dp->d_name));
-/*@+voidabstract@*/
 if (_ftp_debug)
 fprintf(stderr, "*** ftpReaddir(%p) %p \"%s\"\n", (void *)mydir, dp, dp->d_name);
-/*@=voidabstract@*/
     
     return dp;
 }
-/*@=type@*/
 
 static int ftpClosedir(/*@only@*/ DIR * dir)
 	/*@globals fileSystem @*/
@@ -1310,7 +1302,6 @@ static int ftpClosedir(/*@only@*/ DIR * dir)
 {
     FTPDIR mydir = (FTPDIR)dir;
 
-    /*@+voidabstract@*/
 if (_ftp_debug)
 fprintf(stderr, "*** ftpClosedir(%p)\n", (void *)mydir);
     if (mydir == NULL || !ISFTPMAGIC(mydir)) {
@@ -1318,7 +1309,6 @@ fprintf(stderr, "*** ftpClosedir(%p)\n", (void *)mydir);
 	return -1;
     }
     free((void *)mydir);
-    /*@=voidabstract@*/
     mydir = NULL;
     return 0;
 }
@@ -1393,7 +1383,7 @@ int Readlink(const char * path, char * buf, size_t bufsiz)
 	return -2;
 	/*@notreached@*/ break;
     }
-/*@-compdef@*/
+/*@-compdef@*/ /* FIX: *buf is undefined */
     return readlink(path, buf, bufsiz);
 /*@=compdef@*/
 }
@@ -1490,7 +1480,6 @@ fprintf(stderr, "*** Opendir(%s)\n", path);
     /*@=dependenttrans@*/
 }
 
-/*@+voidabstract@*/
 struct dirent * Readdir(DIR * dir)
 {
 if (_rpmio_debug)
@@ -1508,4 +1497,3 @@ fprintf(stderr, "*** Closedir(%p)\n", (void *)dir);
 	return ftpClosedir(dir);
     return closedir(dir);
 }
-/*@=voidabstract@*/
diff --git a/rpmio/rpmsq.c b/rpmio/rpmsq.c
index 1c2536ced..439f3a7c8 100644
--- a/rpmio/rpmsq.c
+++ b/rpmio/rpmsq.c
@@ -1,4 +1,3 @@
-/*@-unrecog@*/
 /** \ingroup rpmio
  * \file rpmio/rpmsq.c
  */
@@ -6,12 +5,103 @@
 #include "system.h"
 
 #if defined(__LCLINT__)
-struct qelem;
+#define	_BITS_SIGTHREAD_H	/* XXX avoid __sigset_t heartburn. */
+
 /*@-exportheader@*/
+/*@constant int SA_SIGINFO@*/
+extern int sighold(int sig)
+	/*@globals errno, systemState @*/;
+extern int sigignore(int sig)
+	/*@globals errno, systemState @*/;
+extern int sigpause(int sig)
+	/*@globals errno, systemState @*/;
+extern int sigrelse(int sig)
+	/*@globals errno, systemState @*/;
+extern void (*sigset(int sig, void (*disp)(int)))(int)
+	/*@globals errno, systemState @*/;
+
+struct qelem;
 extern	void insque(struct qelem * __elem, struct qelem * __prev)
-	/*@modifies  __elem, prev @*/;
+	/*@modifies  __elem, __prev @*/;
 extern	void remque(struct qelem * __elem)
 	/*@modifies  __elem @*/;
+
+extern pthread_t pthread_self(void)
+	/*@*/;
+extern int pthread_equal(pthread_t t1, pthread_t t2)
+	/*@*/;
+
+extern int pthread_create(/*@out@*/ pthread_t *restrict thread,
+		const pthread_attr_t *restrict attr,
+		void *(*start_routine)(void*), void *restrict arg)
+	/*@modifies *thread @*/;
+extern int pthread_join(pthread_t thread, /*@out@*/ void **value_ptr)
+	/*@modifies *value_ptr @*/;
+
+extern int pthread_setcancelstate(int state, /*@out@*/ int *oldstate)
+	/*@globals internalState @*/
+	/*@modifies *oldstate, internalState @*/;
+extern int pthread_setcanceltype(int type, /*@out@*/ int *oldtype)
+	/*@globals internalState @*/
+	/*@modifies *oldtype, internalState @*/;
+extern void pthread_testcancel(void)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
+extern void pthread_cleanup_pop(int execute)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
+extern void pthread_cleanup_push(void (*routine)(void*), void *arg)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
+extern void _pthread_cleanup_pop(/*@out@*/ struct _pthread_cleanup_buffer *__buffer, int execute)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
+extern void _pthread_cleanup_push(/*@out@*/ struct _pthread_cleanup_buffer *__buffer, void (*routine)(void*), /*@out@*/ void *arg)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
+
+extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr)
+	/*@modifies *attr @*/;
+extern int pthread_mutexattr_init(/*@out@*/ pthread_mutexattr_t *attr)
+	/*@modifies *attr @*/;
+
+int pthread_mutexattr_gettype(const pthread_mutexattr_t *restrict attr,
+		/*@out@*/ int *restrict type)
+	/*@modifies *type @*/;
+int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
+	/*@modifies *attr @*/;
+
+extern int pthread_mutex_destroy(pthread_mutex_t *mutex)
+	/*@modifies *mutex @*/;
+extern int pthread_mutex_init(/*@out@*/ pthread_mutex_t *restrict mutex,
+		const pthread_mutexattr_t *restrict attr)
+	/*@modifies *mutex @*/;
+
+extern int pthread_mutex_lock(pthread_mutex_t *mutex)
+	/*@modifies *mutex @*/;
+extern int pthread_mutex_trylock(pthread_mutex_t *mutex)
+	/*@modifies *mutex @*/;
+extern int pthread_mutex_unlock(pthread_mutex_t *mutex)
+	/*@modifies *mutex @*/;
+
+extern int pthread_cond_destroy(pthread_cond_t *cond)
+	/*@modifies *cond @*/;
+extern int pthread_cond_init(/*@out@*/ pthread_cond_t *restrict cond,
+		const pthread_condattr_t *restrict attr)
+	/*@modifies *cond @*/;
+
+extern int pthread_cond_timedwait(pthread_cond_t *restrict cond,
+		pthread_mutex_t *restrict mutex,
+		const struct timespec *restrict abstime)
+	/*@modifies *cond, *mutex @*/;
+extern int pthread_cond_wait(pthread_cond_t *restrict cond,
+		pthread_mutex_t *restrict mutex)
+	/*@modifies *cond, *mutex @*/;
+extern int pthread_cond_broadcast(pthread_cond_t *cond)
+	/*@modifies *cond @*/;
+extern int pthread_cond_signal(pthread_cond_t *cond)
+	/*@modifies *cond @*/;
+
 /*@=exportheader@*/
 #endif
 
@@ -20,31 +110,33 @@ extern	void remque(struct qelem * __elem)
 #include <sys/wait.h>
 #include <search.h>
 
-#if defined(HAVE_PTHREAD_H) && !defined(__LCLINT__)
+#if defined(HAVE_PTHREAD_H)
 
 #include <pthread.h>
 
 /*@unchecked@*/
+/*@-type@*/
 static pthread_mutex_t rpmsigTbl_lock = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
+/*@=type@*/
 
 #define	DO_LOCK()	pthread_mutex_lock(&rpmsigTbl_lock);
 #define	DO_UNLOCK()	pthread_mutex_unlock(&rpmsigTbl_lock);
 #define	INIT_LOCK()	\
-     {	pthread_mutexattr_t attr; \
-	pthread_mutexattr_init(&attr); \
-	pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE); \
-	pthread_mutex_init (&rpmsigTbl_lock, &attr); \
-	pthread_mutexattr_destroy(&attr); \
+    {	pthread_mutexattr_t attr; \
+	(void) pthread_mutexattr_init(&attr); \
+	(void) pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE); \
+	(void) pthread_mutex_init (&rpmsigTbl_lock, &attr); \
+	(void) pthread_mutexattr_destroy(&attr); \
 	rpmsigTbl_sigchld->active = 0; \
-     }
+    }
 #define	ADD_REF(__tbl)	(__tbl)->active++
 #define	SUB_REF(__tbl)	--(__tbl)->active
 #define	CLEANUP_HANDLER(__handler, __arg, __oldtypeptr) \
-	pthread_setcanceltype (PTHREAD_CANCEL_ASYNCHRONOUS, (__oldtypeptr)); \
+    (void) pthread_setcanceltype (PTHREAD_CANCEL_ASYNCHRONOUS, (__oldtypeptr));\
 	pthread_cleanup_push((__handler), (__arg));
 #define	CLEANUP_RESET(__execute, __oldtype) \
-	pthread_cleanup_pop(__execute); \
-	pthread_setcanceltype ((__oldtype), &(__oldtype));
+    (void) pthread_cleanup_pop(__execute); \
+    (void) pthread_setcanceltype ((__oldtype), &(__oldtype));
 
 #define	SAME_THREAD(_a, _b)	pthread_equal(((pthread_t)_a), ((pthread_t)_b))
 
@@ -82,18 +174,15 @@ static struct rpmsqElem rpmsqRock;
 rpmsq rpmsqQueue = &rpmsqRock;
 /*@=compmempass@*/
 
-/*@-mustmod@*/
-int rpmsqInsert(void * elem, /*@unused@*/ void * prev)
+int rpmsqInsert(void * elem, void * prev)
 {
     rpmsq sq = (rpmsq) elem;
     int ret = -1;
 
     if (sq != NULL) {
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "    Insert(%p): %p\n", ME(), sq);
-/*@=modfilesys@*/
 #endif
 	ret = sighold(SIGCHLD);
 	if (ret == 0) {
@@ -105,20 +194,15 @@ fprintf(stderr, "    Insert(%p): %p\n", ME(), sq);
 	    sq->pipes[0] = sq->pipes[1] = -1;
 /*@=bounds@*/
 
-/*@-unqualifiedtrans@*/
 	    sq->id = ME();
-/*@=unqualifiedtrans@*/
 	    ret = pthread_mutex_init(&sq->mutex, NULL);
 	    ret = pthread_cond_init(&sq->cond, NULL);
-#if !defined(__LCLINT__)	/* XXX FIXME */
-	    insque(elem, (prev ? prev : rpmsqQueue));
-#endif
+	    insque(elem, (prev != NULL ? prev : rpmsqQueue));
 	    ret = sigrelse(SIGCHLD);
 	}
     }
     return ret;
 }
-/*@=mustmod@*/
 
 int rpmsqRemove(void * elem)
 {
@@ -128,10 +212,8 @@ int rpmsqRemove(void * elem)
     if (elem != NULL) {
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "    Remove(%p): %p\n", ME(), sq);
-/*@=modfilesys@*/
 #endif
 	ret = sighold (SIGCHLD);
 	if (ret == 0) {
@@ -183,11 +265,8 @@ static struct rpmsig_s {
 };
 /*@=fullinitblock@*/
 
-/*@-incondefs@*/
 void rpmsqAction(int signum,
 		/*@unused@*/ void * info, /*@unused@*/ void * context)
-	/*@globals rpmsqQueue @*/
-	/*@modifies rpmsqQueue @*/
 {
     int save = errno;
     rpmsig tbl;
@@ -218,9 +297,7 @@ void rpmsqAction(int signum,
 			/*@innercontinue@*/ continue;
 		    sq->reaped = reaped;
 		    sq->status = status;
-#if defined(HAVE_PTHREAD_H) && !defined(__LCLINT__)
 		    (void) pthread_cond_signal(&sq->cond);
-#endif
 		    /*@innerbreak@*/ break;
 		}
 	    }
@@ -232,7 +309,6 @@ void rpmsqAction(int signum,
     }
     errno = save;
 }
-/*@=incondefs@*/
 
 int rpmsqEnable(int signum, /*@null@*/ rpmsqAction_t handler)
 	/*@globals rpmsigTbl @*/
@@ -243,11 +319,9 @@ int rpmsqEnable(int signum, /*@null@*/ rpmsqAction_t handler)
     rpmsig tbl;
     int ret = -1;
 
-    DO_LOCK ();
-#if !defined(__LCLINT__)
+    (void) DO_LOCK ();
     if (rpmsqQueue->id == NULL)
 	rpmsqQueue->id = ME();
-#endif
     for (tbl = rpmsigTbl; tbl->signum >= 0; tbl++) {
 	if (tblsignum != tbl->signum)
 	    continue;
@@ -279,7 +353,7 @@ int rpmsqEnable(int signum, /*@null@*/ rpmsqAction_t handler)
 	ret = tbl->active;
 	break;
     }
-    DO_UNLOCK ();
+    (void) DO_UNLOCK ();
     return ret;
 }
 
@@ -291,10 +365,8 @@ pid_t rpmsqFork(rpmsq sq)
     if (sq->reaper) {
 	xx = rpmsqInsert(sq, NULL);
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "    Enable(%p): %p\n", ME(), sq);
-/*@=modfilesys@*/
 #endif
 	xx = rpmsqEnable(SIGCHLD, NULL);
     }
@@ -323,10 +395,8 @@ fprintf(stderr, "    Enable(%p): %p\n", ME(), sq);
 /*@=bounds@*/
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "     Child(%p): %p child %d\n", ME(), sq, getpid());
-/*@=modfilesys@*/
 #endif
 
     } else {				/* Parent. */
@@ -334,10 +404,8 @@ fprintf(stderr, "     Child(%p): %p child %d\n", ME(), sq, getpid());
 	sq->child = pid;
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "    Parent(%p): %p child %d\n", ME(), sq, sq->child);
-/*@=modfilesys@*/
 #endif
 
     }
@@ -393,19 +461,15 @@ static int rpmsqWaitUnregister(rpmsq sq)
 	xx = pthread_mutex_unlock(&sq->mutex);
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "      Wake(%p): %p child %d reaper %d ret %d\n", ME(), sq, sq->child, sq->reaper, ret);
-/*@=modfilesys@*/
 #endif
 
     xx = rpmsqRemove(sq);
     xx = rpmsqEnable(-SIGCHLD, NULL);
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "   Disable(%p): %p\n", ME(), sq);
-/*@=modfilesys@*/
 #endif
 
     return ret;
@@ -415,10 +479,8 @@ pid_t rpmsqWait(rpmsq sq)
 {
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "      Wait(%p): %p child %d reaper %d\n", ME(), sq, sq->child, sq->reaper);
-/*@=modfilesys@*/
 #endif
 
     if (sq->reaper) {
@@ -432,18 +494,14 @@ fprintf(stderr, "      Wait(%p): %p child %d reaper %d\n", ME(), sq, sq->child,
 	sq->reaped = reaped;
 	sq->status = status;
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "   Waitpid(%p): %p child %d reaped %d\n", ME(), sq, sq->child, sq->reaped);
-/*@=modfilesys@*/
 #endif
     }
 
 #ifdef _RPMSQ_DEBUG
-/*@-modfilesys@*/
 if (_rpmsq_debug)
 fprintf(stderr, "      Fini(%p): %p child %d status 0x%x\n", ME(), sq, sq->child, sq->status);
-/*@=modfilesys@*/
 #endif
 
     return sq->reaped;
@@ -478,8 +536,8 @@ int rpmsqThreadEqual(void * thread)
  */
 static void
 sigchld_cancel (void *arg)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies fileSystem, internalState @*/
+	/*@globals rpmsigTbl, fileSystem, internalState @*/
+	/*@modifies rpmsigTbl, fileSystem, internalState @*/
 {
     pid_t child = *(pid_t *) arg;
     pid_t result;
@@ -490,29 +548,30 @@ sigchld_cancel (void *arg)
 	result = waitpid(child, NULL, 0);
     } while (result == (pid_t)-1 && errno == EINTR);
 
-    DO_LOCK ();
+    (void) DO_LOCK ();
     if (SUB_REF (rpmsigTbl_sigchld) == 0) {
 	(void) rpmsqEnable(-SIGQUIT, NULL);
 	(void) rpmsqEnable(-SIGINT, NULL);
     }
-    DO_UNLOCK ();
+    (void) DO_UNLOCK ();
 }
 
 /**
  * Execute a command, returning its status.
  */
-/*@-bounds@*/
 int
 rpmsqExecve (const char ** argv)
+	/*@globals rpmsigTbl @*/
+	/*@modifies rpmsigTbl @*/
 {
     int oldtype;
     int status = -1;
-    pid_t pid;
+    pid_t pid = 0;
     pid_t result;
     sigset_t newMask, oldMask;
     rpmsq sq = memset(alloca(sizeof(*sq)), 0, sizeof(*sq));
 
-    DO_LOCK ();
+    (void) DO_LOCK ();
     if (ADD_REF (rpmsigTbl_sigchld) == 0) {
 	if (rpmsqEnable(SIGINT, NULL) < 0) {
 	    SUB_REF (rpmsigTbl_sigchld);
@@ -523,12 +582,12 @@ rpmsqExecve (const char ** argv)
 	    goto out_restore_sigint;
 	}
     }
-    DO_UNLOCK ();
+    (void) DO_UNLOCK ();
 
     (void) sigemptyset (&newMask);
     (void) sigaddset (&newMask, SIGCHLD);
     if (sigprocmask (SIG_BLOCK, &newMask, &oldMask) < 0) {
-	DO_LOCK ();
+	(void) DO_LOCK ();
 	if (SUB_REF (rpmsigTbl_sigchld) == 0)
 	    goto out_restore_sigquit_and_sigint;
 	goto out;
@@ -561,7 +620,7 @@ rpmsqExecve (const char ** argv)
 
     CLEANUP_RESET(0, oldtype);
 
-    DO_LOCK ();
+    (void) DO_LOCK ();
     if ((SUB_REF (rpmsigTbl_sigchld) == 0 &&
         (rpmsqEnable(-SIGINT, NULL) < 0 || rpmsqEnable (-SIGQUIT, NULL) < 0))
       || sigprocmask (SIG_SETMASK, &oldMask, NULL) != 0)
@@ -575,8 +634,6 @@ out_restore_sigquit_and_sigint:
 out_restore_sigint:
     (void) rpmsqEnable(-SIGINT, NULL);
 out:
-    DO_UNLOCK ();
+    (void) DO_UNLOCK ();
     return status;
 }
-/*@=bounds@*/
-/*@=unrecog@*/
diff --git a/rpmio/rpmsq.h b/rpmio/rpmsq.h
index 3ad5eb182..4223e42aa 100644
--- a/rpmio/rpmsq.h
+++ b/rpmio/rpmsq.h
@@ -43,6 +43,7 @@ struct rpmsqElem {
     rpmtime_t ms_scriptlets;	/*!< Accumulated script duration (msecs). */
     int reaper;			/*!< Register SIGCHLD handler? */
     int pipes[2];		/*!< Parent/child interlock. */
+/*@shared@*/
     void * id;			/*!< Blocking thread id (pthread_t). */
     pthread_mutex_t mutex;	/*!< Signal delivery to thread condvar. */
     pthread_cond_t cond;
@@ -68,7 +69,8 @@ extern sigset_t rpmsqCaught;
  */
 /*@-exportlocal@*/
 int rpmsqInsert(/*@null@*/ void * elem, /*@null@*/ void * prev)
-	/*@modifies elem @*/;
+	/*@globals systemState @*/
+	/*@modifies elem, prev, systemState @*/;
 /*@=exportlocal@*/
 
 /**
@@ -90,8 +92,8 @@ int rpmsqRemove(/*@null@*/ void * elem)
  */
 /*@-exportlocal@*/
 void rpmsqAction(int signum, void * info, void * context)
-	/*@globals rpmsqCaught, errno, fileSystem @*/
-	/*@modifies rpmsqCaught, errno, fileSystem @*/;
+	/*@globals rpmsqCaught, rpmsqQueue, errno, fileSystem @*/
+	/*@modifies rpmsqCaught, rpmsqQueue, errno, fileSystem @*/;
 /*@=exportlocal@*/
 
 /**
@@ -101,8 +103,8 @@ void rpmsqAction(int signum, void * info, void * context)
  * @return		no. of refs, -1 on error
  */
 int rpmsqEnable(int signum, /*@null@*/ rpmsqAction_t handler)
-	/*@globals rpmsqCaught, fileSystem, internalState @*/
-	/*@modifies rpmsqCaught, fileSystem, internalState @*/;
+	/*@globals rpmsqCaught, rpmsqQueue, fileSystem, internalState @*/
+	/*@modifies rpmsqCaught, rpmsqQueue, fileSystem, internalState @*/;
 
 /**
  * Fork a child process.
diff --git a/rpmio/rpmsw.c b/rpmio/rpmsw.c
index f8b2fc9dc..53347822d 100644
--- a/rpmio/rpmsw.c
+++ b/rpmio/rpmsw.c
@@ -79,10 +79,8 @@ static int rpmsw_initialized = 0;
 
 rpmsw rpmswNow(rpmsw sw)
 {
-/*@-noeffect@*/
     if (!rpmsw_initialized)
 	(void) rpmswInit();
-/*@=noeffect@*/
     if (sw == NULL)
 	return NULL;
     switch (rpmsw_type) {
@@ -144,7 +142,6 @@ rpmtime_t rpmswDiff(rpmsw end, rpmsw begin)
 }
 
 #if defined(HP_TIMING_NOW)
-/*@-type@*/
 static rpmtime_t rpmswCalibrate(void)
 	/*@globals internalState @*/
 	/*@modifies internalState @*/
@@ -161,9 +158,7 @@ static rpmtime_t rpmswCalibrate(void)
     req.tv_sec = 0;
     req.tv_nsec = 20 * 1000 * 1000;
     for (i = 0; i < 100; i++) {
-/*@-compdef@*/
 	rc = nanosleep(&req, &rem);
-/*@=compdef@*/
 	if (rc == 0)
 	    break;
 	if (rem.tv_sec == 0 && rem.tv_nsec == 0)
@@ -176,7 +171,6 @@ static rpmtime_t rpmswCalibrate(void)
 
     return ticks;
 }
-/*@=type@*/
 #endif
 
 rpmtime_t rpmswInit(void)
@@ -244,7 +238,6 @@ rpmtime_t rpmswInit(void)
     return rpmsw_overhead;
 }
 
-/*@-mods@*/
 int rpmswEnter(rpmop op, ssize_t rc)
 {
     if (op == NULL)
@@ -300,5 +293,3 @@ rpmtime_t rpmswSub(rpmop to, rpmop from)
     }
     return usecs;
 }
-
-/*@=mods@*/