Propagate splint-3.0.1.7 close(2) internalState annotation throughout.

CVS patchset: 5542
CVS date: 2002/07/08 14:21:26

9 files changed, 133 insertions, 96 deletions

diff --git a/rpmio/digest.c b/rpmio/digest.c
index 174672061..8e7c5a2c9 100644
--- a/rpmio/digest.c
+++ b/rpmio/digest.c
@@ -103,7 +103,9 @@ int
 rpmDigestUpdate(DIGEST_CTX ctx, const void * data, size_t len)
 {
 DPRINTF((stderr, "*** Update(%p,%p,%d) param %p \"%s\"\n", ctx, data, len, ctx->param, ((char *)data)));
+/*@-boundsread@*/
     return (*ctx->Update) (ctx->param, data, len);
+/*@=boundsread@*/
 }
 /*@=mustmod@*/
 
diff --git a/rpmio/rpmio.c b/rpmio/rpmio.c
index 3ae20a5cd..e0613dbd3 100644
--- a/rpmio/rpmio.c
+++ b/rpmio/rpmio.c
@@ -410,12 +410,16 @@ ssize_t fdWrite(void * cookie, const char * buf, size_t count)
     if (count == 0) return 0;
 
     fdstat_enter(fd, FDSTAT_WRITE);
+/*@-boundsread@*/
     rc = write(fdno, buf, (count > fd->bytesRemain ? fd->bytesRemain : count));
+/*@=boundsread@*/
     fdstat_exit(fd, FDSTAT_WRITE, rc);
 
     if (fd->wr_chunked) {
 	int ec;
+/*@-boundsread@*/
 	ec = write(fdno, "\r\n", sizeof("\r\n")-1);
+/*@=boundsread@*/
 	if (ec == -1)	fd->syserrno = errno;
     }
 
@@ -769,8 +773,8 @@ static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
 /*@=boundsread@*/
 
 static int tcpConnect(FD_t ctrl, const char * host, int port)
-	/*@globals fileSystem @*/
-	/*@modifies ctrl, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ctrl, fileSystem, internalState @*/
 {
     struct sockaddr_in sin;
     int fdno = -1;
@@ -1054,8 +1058,8 @@ fprintf(stderr, "-> %s", t);
 }
 
 static int ftpLogin(urlinfo u)
-	/*@globals fileSystem @*/
-	/*@modifies u, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies u, fileSystem, internalState @*/
 {
     const char * host;
     const char * user;
@@ -1362,8 +1366,8 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 }
 
 static int urlConnect(const char * url, /*@out@*/ urlinfo * uret)
-	/*@globals fileSystem @*/
-	/*@modifies *uret, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *uret, fileSystem, internalState @*/
 {
     urlinfo u;
     int rc = 0;
@@ -1451,8 +1455,8 @@ int ftpCmd(const char * cmd, const char * url, const char * arg2)
 #endif
 
 static int ftpAbort(urlinfo u, FD_t data)
-	/*@globals fileSystem @*/
-	/*@modifies u, data, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies u, data, fileSystem, internalState @*/
 {
     static unsigned char ipbuf[3] = { IAC, IP, IAC };
     FD_t ctrl;
@@ -1558,8 +1562,8 @@ fprintf(stderr, "*** httpResp: rc %d ec %d\n", rc, ec);
 }
 
 static int httpReq(FD_t ctrl, const char * httpCmd, const char * httpArg)
-	/*@globals fileSystem @*/
-	/*@modifies ctrl, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ctrl, fileSystem, internalState @*/
 {
     urlinfo u = ctrl->url;
     const char * host;
@@ -1686,6 +1690,8 @@ void * ufdGetUrlinfo(FD_t fd)
 static ssize_t ufdRead(void * cookie, /*@out@*/ char * buf, size_t count)
 	/*@globals fileSystem, internalState @*/
 	/*@modifies *buf, fileSystem, internalState @*/
+        /*@requires maxSet(buf) >= (count - 1) @*/
+        /*@ensures maxRead(buf) == result @*/
 {
     FD_t fd = c2f(cookie);
     int bytesRead;
@@ -2000,7 +2006,8 @@ exit:
 /*@-nullstate@*/	/* FIX: u->{ctrl,data}->url undef after XurlLink. */
 static /*@null@*/ FD_t httpOpen(const char * url, /*@unused@*/ int flags,
 		/*@unused@*/ mode_t mode, /*@out@*/ urlinfo * uret)
-	/*@modifies *uret @*/
+	/*@globals internalState @*/
+	/*@modifies *uret, internalState @*/
 {
     urlinfo u = NULL;
     FD_t fd = NULL;
@@ -2045,8 +2052,8 @@ exit:
 /*@=nullstate@*/
 
 static /*@null@*/ FD_t ufdOpen(const char * url, int flags, mode_t mode)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = NULL;
     const char * cmd;
diff --git a/rpmio/rpmio.h b/rpmio/rpmio.h
index a05e2a50f..3046185b2 100644
--- a/rpmio/rpmio.h
+++ b/rpmio/rpmio.h
@@ -264,8 +264,8 @@ int Fseek(FD_t fd, _libio_off_t offset, int whence)
  * fclose(3) clone.
  */
 int Fclose( /*@killref@*/ FD_t fd)
-	/*@globals fileSystem @*/
-	/*@modifies fd, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fd, fileSystem, internalState @*/;
 
 /**
  */
@@ -278,8 +278,8 @@ int Fclose( /*@killref@*/ FD_t fd)
  */
 /*@null@*/ FD_t	Fopen(/*@null@*/ const char * path,
 			/*@null@*/ const char * fmode)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 
 /**
@@ -321,51 +321,51 @@ int Fcntl(FD_t fd, int op, void *lip)
  * mkdir(2) clone.
  */
 int Mkdir(const char * path, mode_t mode)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * chdir(2) clone.
  */
 int Chdir(const char * path)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * rmdir(2) clone.
  */
 int Rmdir(const char * path)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * rename(2) clone.
  */
 int Rename(const char * oldpath, const char * newpath)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * link(2) clone.
  */
 int Link(const char * oldpath, const char * newpath)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * unlink(2) clone.
  */
 int Unlink(const char * path)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * readlink(2) clone.
  */
 /*@-incondefs@*/
 int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
-	/*@globals errno, fileSystem @*/
-	/*@modifies *buf, errno, fileSystem @*/
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies *buf, errno, fileSystem, internalState @*/
 	/*@requires maxSet(buf) >= (bufsiz - 1) @*/
 	/*@ensures maxRead(buf) <= bufsiz @*/;
 /*@=incondefs@*/
@@ -374,15 +374,15 @@ int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
  * stat(2) clone.
  */
 int Stat(const char * path, /*@out@*/ struct stat * st)
-	/*@globals errno, fileSystem @*/
-	/*@modifies *st, errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies *st, errno, fileSystem, internalState @*/;
 
 /**
  * lstat(2) clone.
  */
 int Lstat(const char * path, /*@out@*/ struct stat * st)
-	/*@globals errno, fileSystem @*/
-	/*@modifies *st, errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies *st, errno, fileSystem, internalState @*/;
 
 /**
  * access(2) clone.
@@ -414,13 +414,13 @@ void Globfree( /*@only@*/ glob_t * pglob)
  */
 /*@null@*/
 DIR * Opendir(const char * path)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * readdir(3) clone.
  */
-/*@null@*/
+/*@dependent@*/ /*@null@*/
 struct dirent * Readdir(DIR * dir)
 	/*@globals errno, fileSystem @*/
 	/*@modifies *dir, errno, fileSystem @*/;
@@ -449,8 +449,8 @@ off_t	fdSize(FD_t fd)
 /**
  */
 /*@null@*/ FD_t fdDup(int fdno)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem@*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 #ifdef UNUSED
 /*@null@*/ FILE *fdFdopen( /*@only@*/ void * cookie, const char * mode);
@@ -470,8 +470,8 @@ off_t	fdSize(FD_t fd)
 /**
  */
 /*@null@*/ FD_t fdOpen(const char *path, int flags, mode_t mode)
-	/*@globals errno, fileSystem @*/
-	/*@modifies errno, fileSystem @*/;
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies errno, fileSystem, internalState @*/;
 #define	fdOpen(_path, _flags, _mode)	fdio->_open((_path), (_flags), (_mode))
 
 /**
@@ -495,8 +495,8 @@ ssize_t	fdWrite(void * cookie, const char * buf, size_t count)
 /**
  */
 int fdClose( /*@only@*/ void * cookie)
-	/*@globals errno, fileSystem, systemState @*/
-	/*@modifies *cookie, errno, fileSystem, systemState @*/;
+	/*@globals errno, fileSystem, systemState, internalState @*/
+	/*@modifies *cookie, errno, fileSystem, systemState, internalState @*/;
 #define	fdCLose(_fd)		fdio->close(_fd)
 
 /**
@@ -562,7 +562,8 @@ typedef enum ftperrCode_e {
 /**
  */
 /*@-redecl@*/
-/*@observer@*/ const char *const ftpStrerror(int errorNumber)	/*@*/;
+/*@observer@*/ const char *const ftpStrerror(int errorNumber)
+	/*@*/;
 /*@=redecl@*/
 
 /**
@@ -575,7 +576,9 @@ typedef enum ftperrCode_e {
  */
 /*@-redecl@*/
 /*@unused@*/
-/*@observer@*/ const char * urlStrerror(const char * url)	/*@*/;
+/*@observer@*/ const char * urlStrerror(const char * url)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
 /*@=redecl@*/
 
 /**
@@ -589,8 +592,8 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 /**
  */
 int ufdGetFile( /*@killref@*/ FD_t sfd, FD_t tfd)
-	/*@globals fileSystem @*/
-	/*@modifies sfd, tfd, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies sfd, tfd, fileSystem, internalState @*/;
 
 /**
  */
diff --git a/rpmio/rpmio_internal.h b/rpmio/rpmio_internal.h
index 34accaa65..a4845aa16 100644
--- a/rpmio/rpmio_internal.h
+++ b/rpmio/rpmio_internal.h
@@ -180,26 +180,26 @@ int fdFgets(FD_t fd, char * buf, size_t len)
  */
 /*@null@*/ FD_t ftpOpen(const char *url, /*@unused@*/ int flags,
                 /*@unused@*/ mode_t mode, /*@out@*/ urlinfo *uret)
-	/*@globals fileSystem @*/
-	/*@modifies *uret, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *uret, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ftpReq(FD_t data, const char * ftpCmd, const char * ftpArg)
-	/*@globals fileSystem @*/
-	/*@modifies data, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies data, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ftpCmd(const char * cmd, const char * url, const char * arg2)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ufdClose( /*@only@*/ void * cookie)
-	/*@globals fileSystem @*/
-	/*@modifies cookie, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies cookie, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
@@ -208,7 +208,9 @@ int ufdClose( /*@only@*/ void * cookie)
 	/*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].io;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -234,9 +236,11 @@ void fdSetIo(FD_t fd, /*@kept@*/ /*@null@*/ FDIO_t io)
 	/*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     /*@+voidabstract@*/
     return ((FILE *)fd->fps[fd->nfps].fp);
     /*@=voidabstract@*/
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -246,7 +250,9 @@ void fdSetIo(FD_t fd, /*@kept@*/ /*@null@*/ FDIO_t io)
 	/*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].fp;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -272,7 +278,9 @@ int fdGetFdno(FD_t fd)
 	/*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].fdno;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -549,16 +557,23 @@ int fdFileno(/*@null@*/ void * cookie)
     FD_t fd;
     if (cookie == NULL) return -2;
     fd = c2f(cookie);
+/*@-boundsread@*/
     return fd->fps[0].fdno;
+/*@=boundsread@*/
 }
 /*@=shadow@*/
 
 /**
+ * Read an entire file into a buffer.
+ * @param fn		file name to read
+ * @retval *bp		(malloc'd) buffer address
+ * @retval *blenp	(malloc'd) buffer length
+ * @return		0 on success
  */
 int rpmioSlurp(const char * fn,
                 /*@out@*/ const unsigned char ** bp, /*@out@*/ ssize_t * blenp)
-        /*@globals fileSystem @*/
-        /*@modifies *bp, *blenp, fileSystem @*/;
+        /*@globals fileSystem, internalState @*/
+        /*@modifies *bp, *blenp, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }
diff --git a/rpmio/rpmmacro.h b/rpmio/rpmmacro.h
index 020a954b0..97eae6a3b 100644
--- a/rpmio/rpmmacro.h
+++ b/rpmio/rpmmacro.h
@@ -137,8 +137,8 @@ void	rpmLoadMacros	(/*@null@*/ MacroContext mc, int level)
  */
 void	rpmInitMacros	(/*@null@*/ MacroContext mc, const char * macrofiles)
 	/*@globals rpmGlobalMacroContext, rpmCLIMacroContext,
-		fileSystem @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem @*/;
+		fileSystem, internalState @*/
+	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /**
  * Destroy macro context.
@@ -163,8 +163,8 @@ typedef enum rpmCompressedMagic_e {
  */
 int	isCompressed	(const char * file,
 				/*@out@*/ rpmCompressedMagic * compressed)
-	/*@globals fileSystem@*/
-	/*@modifies *compressed, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *compressed, fileSystem, internalState @*/;
 
 /**
  * Return (malloc'ed) concatenated macro expansion(s).
diff --git a/rpmio/rpmpgp.h b/rpmio/rpmpgp.h
index 3e4886903..98fa3e286 100644
--- a/rpmio/rpmpgp.h
+++ b/rpmio/rpmpgp.h
@@ -1074,6 +1074,7 @@ int pgpLen(const byte *s, /*@out@*/ unsigned int *lenp)
  */
 /*@unused@*/ static inline
 unsigned int pgpMpiBits(const byte *p)
+	/*@requires maxRead(p) >= 1 @*/
 	/*@*/
 {
     return ((p[0] << 8) | p[1]);
@@ -1086,6 +1087,7 @@ unsigned int pgpMpiBits(const byte *p)
  */
 /*@unused@*/ static inline
 unsigned int pgpMpiLen(const byte *p)
+	/*@requires maxRead(p) >= 1 @*/
 	/*@*/
 {
     return (2 + ((pgpMpiBits(p)+7)>>3));
@@ -1140,6 +1142,7 @@ char * pgpHexStr(const byte *p, unsigned int plen)
  */
 /*@unused@*/ static inline /*@observer@*/
 const char * pgpMpiStr(const byte *p)
+	/*@requires maxRead(p) >= 3 @*/
 	/*@*/
 {
     static char prbuf[2048];
@@ -1282,8 +1285,8 @@ int pgpPrtPkts(const byte *pkts, unsigned int plen, struct pgpDig_s *dig, int pr
  */
 pgpArmor pgpReadPkts(const char * fn,
 		/*@out@*/ const byte ** pkt, /*@out@*/ size_t * pktlen)
-	/*@globals fileSystem @*/
-	/*@modifies *pkt, *pktlen, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *pkt, *pktlen, fileSystem, internalState @*/;
 
 /**
  * Create a container for parsed OpenPGP packates.
diff --git a/rpmio/rpmrpc.c b/rpmio/rpmrpc.c
index 0eeca5ab8..81544156e 100644
--- a/rpmio/rpmrpc.c
+++ b/rpmio/rpmrpc.c
@@ -18,8 +18,8 @@
 
 /* =============================================================== */
 static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     int rc;
     if ((rc = ftpCmd("MKD", path, NULL)) != 0)
@@ -34,22 +34,22 @@ static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
 }
 
 static int ftpChdir(const char * path)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("CWD", path, NULL);
 }
 
 static int ftpRmdir(const char * path)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("RMD", path, NULL);
 }
 
 static int ftpRename(const char * oldpath, const char * newpath)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     int rc;
     if ((rc = ftpCmd("RNFR", oldpath, NULL)) != 0)
@@ -58,8 +58,8 @@ static int ftpRename(const char * oldpath, const char * newpath)
 }
 
 static int ftpUnlink(const char * path)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("DELE", path, NULL);
 }
@@ -825,8 +825,8 @@ static /*@only@*/ char * ftpBuf = NULL;
 static int ftpNLST(const char * url, ftpSysCall_t ftpSysCall,
 		/*@out@*/ /*@null@*/ struct stat * st,
 		/*@out@*/ /*@null@*/ char * rlbuf, size_t rlbufsiz)
-	/*@globals fileSystem @*/
-	/*@modifies *st, *rlbuf, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *st, *rlbuf, fileSystem, internalState @*/
 {
     FD_t fd;
     const char * path;
@@ -1034,8 +1034,8 @@ 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 @*/
-	/*@modifies *st, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *st, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
@@ -1051,8 +1051,8 @@ fprintf(stderr, "*** ftpStat(%s) rc %d\n%s", path, rc, statstr(st, buf));
 }
 
 static int ftpLstat(const char * path, /*@out@*/ struct stat *st)
-	/*@globals fileSystem @*/
-	/*@modifies *st, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *st, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
@@ -1068,8 +1068,8 @@ fprintf(stderr, "*** ftpLstat(%s) rc %d\n%s\n", path, rc, statstr(st, buf));
 }
 
 static int ftpReadlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
-	/*@globals fileSystem @*/
-	/*@modifies *buf, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *buf, fileSystem, internalState @*/
 {
     int rc;
     rc = ftpNLST(path, DO_FTP_READLINK, NULL, buf, bufsiz);
@@ -1098,8 +1098,8 @@ static int ftpmagicdir = 0x8440291;
 /*@-type@*/ /* FIX: abstract DIR */
 /*@null@*/
 static DIR * ftpOpendir(const char * path)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     DIR * dir;
     struct dirent * dp;
@@ -1231,7 +1231,7 @@ fprintf(stderr, "*** ftpOpendir(%s)\n", path);
 }
 /*@=boundswrite@*/
 
-/*@null@*/
+/*@dependent@*/ /*@null@*/
 static struct dirent * ftpReaddir(DIR * dir)
 	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
@@ -1367,7 +1367,9 @@ int Readlink(const char * path, char * buf, size_t bufsiz)
 	return -2;
 	/*@notreached@*/ break;
     }
+/*@-compdef@*/
     return readlink(path, buf, bufsiz);
+/*@=compdef@*/
 }
 
 int Access(const char * path, int amode)
diff --git a/rpmio/rpmurl.h b/rpmio/rpmurl.h
index 0f06eb267..770c610c3 100644
--- a/rpmio/rpmurl.h
+++ b/rpmio/rpmurl.h
@@ -109,21 +109,22 @@ urlinfo	XurlLink(urlinfo u, const char * msg, const char * file, unsigned line)
  * @return		dereferenced instance (NULL if freed)
  */
 /*@unused@*/ urlinfo	urlFree( /*@killref@*/ urlinfo u, const char * msg)
-	/*@modifies u @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies u, fileSystem, internalState @*/;
 
 /** @todo Remove debugging entry from the ABI. */
 urlinfo	XurlFree( /*@killref@*/ urlinfo u, const char * msg,
 		const char * file, unsigned line)
-	/*@globals fileSystem@*/
-	/*@modifies u, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies u, fileSystem, internalState @*/;
 #define	urlFree(_u, _msg) XurlFree(_u, _msg, __FILE__, __LINE__)
 
 /**
  * Free cached URL control structures.
  */
 void urlFreeCache(void)
-	/*@globals _url_cache, _url_count, fileSystem @*/
-	/*@modifies _url_cache, _url_count, fileSystem @*/;
+	/*@globals _url_cache, _url_count, fileSystem, internalState @*/
+	/*@modifies _url_cache, _url_count, fileSystem, internalState @*/;
 
 /**
  * Return type of URL.
@@ -152,7 +153,8 @@ urltype	urlPath(const char * url, /*@out@*/ const char ** pathp)
  * @return		0 on success, -1 on error
  */
 int urlSplit(const char * url, /*@out@*/ urlinfo * uret)
-	/*@modifies *uret @*/;
+	/*@globals internalState @*/
+	/*@modifies *uret, internalState @*/;
 
 /**
  * Copy data from URL to local file.
@@ -161,8 +163,8 @@ int urlSplit(const char * url, /*@out@*/ urlinfo * uret)
  * @return		0 on success, otherwise FTPERR_* code
  */
 int urlGetFile(const char * url, /*@null@*/ const char * dest)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }
diff --git a/rpmio/url.c b/rpmio/url.c
index cbb3ebaf6..685375c44 100644
--- a/rpmio/url.c
+++ b/rpmio/url.c
@@ -193,8 +193,8 @@ static int urlStrcmp(/*@null@*/ const char * str1, /*@null@*/ const char * str2)
 /*@-boundswrite@*/
 /*@-mods@*/
 static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
-	/*@globals rpmGlobalMacroContext, fileSystem@*/
-	/*@modifies *uret, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies *uret, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     urlinfo u;
     int ucx;
@@ -266,8 +266,11 @@ static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
 	    prompt = alloca(strlen(host) + strlen(user) + 256);
 	    sprintf(prompt, _("Password for %s@%s: "), user, host);
 	    u->password = _free(u->password);
+/*@-dependenttrans -moduncon @*/
 	    u->password = /*@-unrecog@*/ getpass(prompt) /*@=unrecog@*/;
-	    u->password = xstrdup(u->password);	/* XXX xstrdup has side effects. */
+/*@=dependenttrans =moduncon @*/
+	    if (u->password)
+		u->password = xstrdup(u->password);
 	}
 
 	if (u->proxyh == NULL) {