lclint fiddles to annotate globals.

CVS patchset: 5106
CVS date: 2001/10/15 03:22:10

16 files changed, 513 insertions, 104 deletions

diff --git a/rpmio/digest.c b/rpmio/digest.c
index 6fcf1f512..17cb96cbd 100644
--- a/rpmio/digest.c
+++ b/rpmio/digest.c
@@ -80,8 +80,10 @@ DPRINTF((stderr, "*** Update(%p,%p,%d) param %p \"%s\"\n", ctx, data, len, ctx->
     (void) (*ctx->Update) (ctx->param, data, len);
 }
 
+/*@unchecked@*/
 static int _ie = 0x44332211;
 /*@-redef@*/
+/*@unchecked@*/
 static union _dendian {
 /*@unused@*/ int i;
     char b[4];
diff --git a/rpmio/macro.c b/rpmio/macro.c
index 1db21cc8f..075cb1a0e 100644
--- a/rpmio/macro.c
+++ b/rpmio/macro.c
@@ -55,8 +55,15 @@ typedef	FILE * FD_t;
 /*@access MacroContext@*/
 /*@access MacroEntry@*/
 
-struct MacroContext_s rpmGlobalMacroContext;
-struct MacroContext_s rpmCLIMacroContext;
+static struct MacroContext_s rpmGlobalMacroContext_s;
+/*@-compmempass@*/
+MacroContext rpmGlobalMacroContext = &rpmGlobalMacroContext_s;
+/*@=compmempass@*/
+
+static struct MacroContext_s rpmCLIMacroContext_s;
+/*@-compmempass@*/
+MacroContext rpmCLIMacroContext = &rpmCLIMacroContext_s;
+/*@=compmempass@*/
 
 /**
  * Macro expansion state.
@@ -75,17 +82,25 @@ typedef /*@abstract@*/ struct MacroBuf_s {
 #define SAVECHAR(_mb, _c) { *(_mb)->t = (_c), (_mb)->t++, (_mb)->nb--; }
 
 static int expandMacro(MacroBuf mb)
-	/*@modifies mb @*/;
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
+	/*@modifies mb, fileSystem @*/;
 
 /*@-exportlocal -exportheadervar@*/
+
 #define	MAX_MACRO_DEPTH	16
+/*@unchecked@*/
 int max_macro_depth = MAX_MACRO_DEPTH;
 
 #ifdef	DEBUG_MACROS
+/*@unchecked@*/
 int print_macro_trace = 0;
+/*@unchecked@*/
 int print_expand_trace = 0;
 #else
+/*@unchecked@*/
 int print_macro_trace = 0;
+/*@unchecked@*/
 int print_expand_trace = 0;
 #endif
 /*@=exportlocal =exportheadervar@*/
@@ -182,7 +197,7 @@ rpmDumpMacroTable(MacroContext mc, FILE * fp)
     int nempty = 0;
     int nactive = 0;
 
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
     if (fp == NULL) fp = stderr;
     
     fprintf(fp, "========================\n");
@@ -218,13 +233,14 @@ rpmDumpMacroTable(MacroContext mc, FILE * fp)
  */
 /*@dependent@*/ /*@null@*/ static MacroEntry *
 findEntry(MacroContext mc, const char * name, size_t namelen)
-	/*@*/
+	/*@globals rpmGlobalMacroContext @*/
+	/*@modifies rpmGlobalMacroContext @*/
 {
     MacroEntry key, *ret;
     struct MacroEntry_s keybuf;
     char namebuf[1024];
 
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
     if (mc->macroTable == NULL || mc->firstFree == 0)
 	return NULL;
 
@@ -437,7 +453,9 @@ printExpansion(MacroBuf mb, const char * t, const char * te)
  */
 static int
 expandT(MacroBuf mb, const char * f, size_t flen)
-	/*@modifies mb @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
+	/*@modifies mb, fileSystem @*/
 {
     char *sbuf;
     const char *s = mb->s;
@@ -464,7 +482,9 @@ expandT(MacroBuf mb, const char * f, size_t flen)
  */
 static int
 expandS(MacroBuf mb, char * tbuf, size_t tbuflen)
-	/*@modifies mb, *tbuf @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
+	/*@modifies mb, *tbuf, fileSystem @*/
 {
     const char *t = mb->t;
     size_t nb = mb->nb;
@@ -488,7 +508,9 @@ expandS(MacroBuf mb, char * tbuf, size_t tbuflen)
  */
 static int
 expandU(MacroBuf mb, char * u, size_t ulen)
-	/*@modifies mb, *u @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
+	/*@modifies mb, *u, fileSystem @*/
 {
     const char *s = mb->s;
     char *t = mb->t;
@@ -526,6 +548,8 @@ expandU(MacroBuf mb, char * u, size_t ulen)
  */
 static int
 doShellEscape(MacroBuf mb, const char * cmd, size_t clen)
+	/*@globals rpmGlobalMacroContext,
+		fileSystem @*/
 	/*@modifies mb, fileSystem @*/
 {
     char pcmd[BUFSIZ];
@@ -563,6 +587,7 @@ doShellEscape(MacroBuf mb, const char * cmd, size_t clen)
  */
 /*@dependent@*/ static const char *
 doDefine(MacroBuf mb, const char * se, int level, int expandbody)
+	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies mb @*/
 {
     const char *s = se;
@@ -632,10 +657,12 @@ doDefine(MacroBuf mb, const char * se, int level, int expandbody)
 	/*@-retalias@*/ return se; /*@=retalias@*/
     }
 
+/*@-modfilesys@*/
     if (expandbody && expandU(mb, b, (&buf[sizeof(buf)] - b))) {
 	rpmError(RPMERR_BADSPEC, _("Macro %%%s failed to expand\n"), n);
 	/*@-retalias@*/ return se; /*@=retalias@*/
     }
+/*@=modfilesys@*/
 
     addMacro(mb->mc, n, o, b, (level - 1));
 
@@ -650,6 +677,7 @@ doDefine(MacroBuf mb, const char * se, int level, int expandbody)
  */
 /*@dependent@*/ static const char *
 doUndefine(MacroContext mc, const char * se)
+	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies mc @*/
 {
     const char *s = se;
@@ -802,6 +830,7 @@ freeArgs(MacroBuf mb)
  */
 /*@dependent@*/ static const char *
 grabArgs(MacroBuf mb, const MacroEntry me, const char * se, char lastc)
+	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies mb @*/
 {
     char buf[BUFSIZ], *b, *be;
@@ -944,6 +973,8 @@ grabArgs(MacroBuf mb, const MacroEntry me, const char * se, char lastc)
  */
 static void
 doOutput(MacroBuf mb, int waserror, const char * msg, size_t msglen)
+	/*@globals rpmGlobalMacroContext,
+		fileSystem @*/
 	/*@modifies mb, fileSystem @*/
 {
     char buf[BUFSIZ];
@@ -969,7 +1000,9 @@ doOutput(MacroBuf mb, int waserror, const char * msg, size_t msglen)
 static void
 doFoo(MacroBuf mb, int negate, const char * f, size_t fn,
 		const char * g, size_t glen)
-	/*@modifies mb @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies mb, fileSystem, internalState @*/
 {
     char buf[BUFSIZ], *b = NULL, *be;
     int c;
@@ -1063,7 +1096,9 @@ doFoo(MacroBuf mb, int negate, const char * f, size_t fn,
  */
 static int
 expandMacro(MacroBuf mb)
-	/*@modifies mb @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem @*/
+	/*@modifies mb, rpmGlobalMacroContext, fileSystem @*/
 {
     MacroEntry *mep;
     MacroEntry me;
@@ -1272,7 +1307,9 @@ expandMacro(MacroBuf mb)
 	    STREQ("S", f, fn) ||
 	    STREQ("P", f, fn) ||
 	    STREQ("F", f, fn)) {
+		/*@-internalglobs@*/ /* FIX: verbose may be set */
 		doFoo(mb, negate, f, fn, g, gn);
+		/*@=internalglobs@*/
 		s = se;
 		continue;
 	}
@@ -1386,7 +1423,7 @@ expandMacros(void * spec, MacroContext mc, char * s, size_t slen)
 
     if (s == NULL || slen == 0)
 	return 0;
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
 
     tbuf = alloca(slen + 1);
     memset(tbuf, 0, (slen + 1));
@@ -1422,7 +1459,7 @@ addMacro(MacroContext mc,
 {
     MacroEntry * mep;
 
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
 
     /* If new name, expand macro table */
     if ((mep = findEntry(mc, n, 0)) == NULL) {
@@ -1447,7 +1484,7 @@ delMacro(MacroContext mc, const char * n)
 {
     MacroEntry * mep;
 
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
     /* If name exists, pop entry */
     if ((mep = findEntry(mc, n, 0)) != NULL) {
 	popMacro(mep);
@@ -1465,7 +1502,7 @@ rpmDefineMacro(MacroContext mc, const char * macro, int level)
     memset(mb, 0, sizeof(*mb));
     /* XXX just enough to get by */
     /*@-temptrans -assignexpose@*/
-    mb->mc = (mc ? mc : &rpmGlobalMacroContext);
+    mb->mc = (mc ? mc : rpmGlobalMacroContext);
     /*@=temptrans =assignexpose@*/
     (void)doDefine(mb, macro, level, 0);
     return 0;
@@ -1475,7 +1512,7 @@ void
 rpmLoadMacros(MacroContext mc, int level)
 {
 
-    if (mc == NULL || mc == &rpmGlobalMacroContext)
+    if (mc == NULL || mc == rpmGlobalMacroContext)
 	return;
 
     if (mc->macroTable != NULL) {
@@ -1499,7 +1536,7 @@ rpmInitMacros(MacroContext mc, const char *macrofiles)
 
     if (macrofiles == NULL)
 	return;
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
 
     for (mfile = m = xstrdup(macrofiles); mfile && *mfile != '\0'; mfile = me) {
 	FD_t fd;
@@ -1553,7 +1590,7 @@ rpmInitMacros(MacroContext mc, const char *macrofiles)
     m = _free(m);
 
     /* Reload cmdline macros */
-    rpmLoadMacros(&rpmCLIMacroContext, RMIL_CMDLINE);
+    rpmLoadMacros(rpmCLIMacroContext, RMIL_CMDLINE);
 }
 
 /*@-globstate@*/
@@ -1561,7 +1598,7 @@ void
 rpmFreeMacros(MacroContext mc)
 {
     
-    if (mc == NULL) mc = &rpmGlobalMacroContext;
+    if (mc == NULL) mc = rpmGlobalMacroContext;
 
     if (mc->macroTable != NULL) {
 	int i;
@@ -1635,6 +1672,7 @@ int isCompressed(const char * file, rpmCompressedMagic * compressed)
 
 /* =============================================================== */
 
+/*@-modfilesys@*/
 char * 
 rpmExpand(const char *arg, ...)
 {
@@ -1656,6 +1694,7 @@ rpmExpand(const char *arg, ...)
     (void) expandMacros(NULL, NULL, buf, sizeof(buf));
     return xstrdup(buf);
 }
+/*@=modfilesys@*/
 
 int
 rpmExpandNumeric(const char *arg)
@@ -1789,7 +1828,9 @@ rpmGetPath(const char *path, ...)
 	*te = '\0';
     }
     va_end(ap);
+/*@-modfilesys@*/
     (void) expandMacros(NULL, NULL, buf, sizeof(buf));
+/*@=modfilesys@*/
 
     (void) rpmCleanPath(buf);
     return xstrdup(buf);	/* XXX xstrdup has side effects. */
diff --git a/rpmio/rpmio.c b/rpmio/rpmio.c
index 23fec6c03..87fd7b78a 100644
--- a/rpmio/rpmio.c
+++ b/rpmio/rpmio.c
@@ -22,6 +22,7 @@
 #endif
 
 #if !defined(HAVE_HERRNO) && defined(__hpux) /* XXX HP-UX w/o -D_XOPEN_SOURCE needs */
+/*@unchecked@*/
 extern int h_errno;
 #endif
 
@@ -34,6 +35,7 @@ extern int h_errno;
 
 #if !defined(HAVE_INET_ATON)
 static int inet_aton(const char *cp, struct in_addr *inp)
+	/*@modifies *inp @*/
 {
     long addr;
 
@@ -76,6 +78,9 @@ static int inet_aton(const char *cp, struct in_addr *inp)
 
 #define	fdGetFILE(_fd)	((FILE *)fdGetFp(_fd))
 
+/**
+ */
+/*@unchecked@*/
 #if _USE_LIBIO
 int noLibio = 0;
 #else
@@ -83,10 +88,25 @@ int noLibio = 1;
 #endif
 
 #define TIMEOUT_SECS 60
+
+/**
+ */
+/*@unchecked@*/
 static int ftpTimeoutSecs = TIMEOUT_SECS;
+
+/**
+ */
+/*@unchecked@*/
 static int httpTimeoutSecs = TIMEOUT_SECS;
 
+/**
+ */
+/*@unchecked@*/
 int _ftp_debug = 0;
+
+/**
+ */
+/*@unchecked@*/
 int _rpmio_debug = 0;
 
 /**
@@ -104,8 +124,9 @@ _free(/*@only@*/ /*@null@*/ /*@out@*/ const void * p)
 
 /* =============================================================== */
 
+/*@-modfilesys@*/
 static /*@observer@*/ const char * fdbg(/*@null@*/ FD_t fd)
-	/*@modifies fileSystem @*/
+	/*@*/
 {
     static char buf[BUFSIZ];
     char *be = buf;
@@ -164,6 +185,7 @@ static /*@observer@*/ const char * fdbg(/*@null@*/ FD_t fd)
     }
     return buf;
 }
+/*@=modfilesys@*/
 
 /* =============================================================== */
 off_t fdSize(FD_t fd)
@@ -200,7 +222,9 @@ FD_t fdDup(int fdno)
 	return NULL;
     fd = fdNew("open (fdDup)");
     fdSetFdno(fd, nfdno);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> fdDup(%d) fd %p %s\n", fdno, (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
     /*@-refcounttrans@*/ return fd; /*@=refcounttrans@*/
 }
 
@@ -224,7 +248,9 @@ FILE *fdFdopen(void * cookie, const char *fmode)
     fdno = fdFileno(fd);
     if (fdno < 0) return NULL;
     fp = fdopen(fdno, fmode);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> fdFdopen(%p,\"%s\") fdno %d -> fp %p fdno %d\n", cookie, fmode, fdno, fp, fileno(fp)));
+/*@=modfilesys@*/
     fd = fdFree(fd, "open (fdFdopen)");
     return fp;
 }
@@ -237,9 +263,11 @@ DBGIO(fd, (stderr, "==> fdFdopen(%p,\"%s\") fdno %d -> fp %p fdno %d\n", cookie,
 #endif
 
 /* =============================================================== */
+/*@-modfilesys@*/
+/*@-mustmod@*/ /* FIX: cookie is modified */
 static inline /*@null@*/ FD_t XfdLink(void * cookie, const char * msg,
 		const char * file, unsigned line)
-	/*@modifies internalState @*/
+	/*@modifies *cookie @*/
 {
     FD_t fd;
 if (cookie == NULL)
@@ -253,7 +281,10 @@ DBGREFS(fd, (stderr, "--> fd  %p ++ %d %s at %s:%u %s\n", fd, fd->nrefs, msg, fi
     }
     return fd;
 }
+/*@=mustmod@*/
+/*@=modfilesys@*/
 
+/*@-modfilesys@*/
 static inline /*@null@*/ FD_t XfdFree( /*@killref@*/ FD_t fd, const char *msg,
 		const char *file, unsigned line)
 	/*@modifies fd @*/
@@ -271,6 +302,7 @@ DBGREFS(fd, (stderr, "--> fd  %p -- %d %s at %s:%u %s\n", fd, fd->nrefs, msg, fi
     }
     return NULL;
 }
+/*@=modfilesys@*/
 
 static inline /*@null@*/ FD_t XfdNew(const char * msg,
 		const char * file, unsigned line)
@@ -327,7 +359,9 @@ ssize_t fdRead(void * cookie, /*@out@*/ char * buf, size_t count)
 
     if (fd->digest && rc > 0) rpmDigestUpdate(fd->digest, buf, rc);
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tfdRead(%p,%p,%ld) rc %ld %s\n", cookie, buf, (long)count, (long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     return rc;
 }
@@ -362,13 +396,16 @@ ssize_t fdWrite(void * cookie, const char * buf, size_t count)
 	if (ec == -1)	fd->syserrno = errno;
     }
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tfdWrite(%p,%p,%ld) rc %ld %s\n", cookie, buf, (long)count, (long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     return rc;
 }
 
 static inline int fdSeek(void * cookie, _libio_pos_t pos, int whence)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
 #ifdef USE_COOKIE_SEEK_POINTER
     _IO_off64_t p = *pos;
@@ -383,7 +420,9 @@ static inline int fdSeek(void * cookie, _libio_pos_t pos, int whence)
     rc = lseek(fdFileno(fd), p, whence);
     fdstat_exit(fd, FDSTAT_SEEK, rc);
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tfdSeek(%p,%ld,%d) rc %lx %s\n", cookie, (long)p, whence, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     return rc;
 }
@@ -406,7 +445,9 @@ int fdClose( /*@only@*/ void * cookie)
     rc = ((fdno >= 0) ? close(fdno) : -2);
     fdstat_exit(fd, FDSTAT_CLOSE, rc);
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tfdClose(%p) rc %lx %s\n", (fd ? fd : NULL), (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     fd = fdFree(fd, "open (fdClose)");
     return rc;
@@ -424,7 +465,9 @@ DBGIO(fd, (stderr, "==>\tfdClose(%p) rc %lx %s\n", (fd ? fd : NULL), (unsigned l
     fd = fdNew("open (fdOpen)");
     fdSetFdno(fd, fdno);
     fd->flags = flags;
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tfdOpen(\"%s\",%x,0%o) %s\n", path, (unsigned)flags, (unsigned)mode, fdbg(fd)));
+/*@=modfilesys@*/
     /*@-refcounttrans@*/ return fd; /*@=refcounttrans@*/
 }
 
@@ -649,12 +692,14 @@ const char *urlStrerror(const char *url)
 #if !defined(USE_ALT_DNS) || !USE_ALT_DNS 
 static int mygethostbyname(const char * host,
 		/*@out@*/ struct in_addr * address)
-	/*@modifies *address, fileSystem @*/
+	/*@modifies *address @*/
 {
     struct hostent * hostinfo;
 
     /*@-unrecog -multithreaded @*/
+    /*@-globs@*/ /* FIX: h_errno access */
     hostinfo = gethostbyname(host);
+    /*@=globs@*/
     /*@=unrecog =multithreaded @*/
     if (!hostinfo) return 1;
 
@@ -667,7 +712,7 @@ static int mygethostbyname(const char * host,
 
 /*@-compdef@*/	/* FIX: address->s_addr undefined. */
 static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
-	/*@modifies *address, fileSystem @*/
+	/*@modifies *address @*/
 {
     if (xisdigit(host[0])) {
 	/*@-unrecog -moduncon @*/
@@ -675,10 +720,12 @@ static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
 	    return FTPERR_BAD_HOST_ADDR;
 	/*@=unrecog =moduncon @*/
     } else {
+	/*@-globs@*/ /* FIX: h_errno access */
 	if (mygethostbyname(host, address)) {
 	    errno = /*@-unrecog@*/ h_errno /*@=unrecog@*/;
 	    return FTPERR_BAD_HOSTNAME;
 	}
+	/*@=globs@*/
     }
     
     return 0;
@@ -686,6 +733,7 @@ static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
 /*@=compdef@*/
 
 static int tcpConnect(FD_t ctrl, const char * host, int port)
+	/*@globals fileSystem @*/
 	/*@modifies ctrl, fileSystem @*/
 {
     struct sockaddr_in sin;
@@ -706,10 +754,12 @@ static int tcpConnect(FD_t ctrl, const char * host, int port)
 	break;
     }
 
+    /*@-internalglobs@*/
     if (connect(fdno, (struct sockaddr *) &sin, sizeof(sin))) {
 	rc = FTPERR_FAILED_CONNECT;
 	break;
     }
+    /*@=internalglobs@*/
   } while (0);
 
     if (rc < 0)
@@ -717,9 +767,9 @@ static int tcpConnect(FD_t ctrl, const char * host, int port)
 
 if (_ftp_debug)
 fprintf(stderr,"++ connect %s:%d on fdno %d\n",
-/*@-unrecog -moduncon @*/
+/*@-unrecog -moduncon -evalorderuncon @*/
 inet_ntoa(sin.sin_addr)
-/*@=unrecog =moduncon @*/ ,
+/*@=unrecog =moduncon =evalorderuncon @*/ ,
 (int)ntohs(sin.sin_port), fdno);
 
     fdSetFdno(ctrl, (fdno >= 0 ? fdno : -1));
@@ -736,6 +786,7 @@ errxit:
 
 static int checkResponse(void * uu, FD_t ctrl,
 		/*@out@*/ int *ecp, /*@out@*/ char ** str)
+	/*@globals fileSystem @*/
 	/*@modifies ctrl, *ecp, *str, fileSystem @*/
 {
     urlinfo u = uu;
@@ -897,6 +948,7 @@ fprintf(stderr, "<- %s\n", s);
 }
 
 static int ftpCheckResponse(urlinfo u, /*@out@*/ char ** str)
+	/*@globals fileSystem @*/
 	/*@modifies u, *str, fileSystem @*/
 {
     int ec = 0;
@@ -922,6 +974,7 @@ static int ftpCheckResponse(urlinfo u, /*@out@*/ char ** str)
 }
 
 static int ftpCommand(urlinfo u, char ** str, ...)
+	/*@globals fileSystem @*/
 	/*@modifies u, *str, fileSystem @*/
 {
     va_list ap;
@@ -959,6 +1012,7 @@ fprintf(stderr, "-> %s", t);
 }
 
 static int ftpLogin(urlinfo u)
+	/*@globals fileSystem @*/
 	/*@modifies u, fileSystem @*/
 {
     const char * host;
@@ -1134,13 +1188,16 @@ int ftpReq(FD_t data, const char * ftpCmd, const char * ftpArg)
     /* XXX setsockopt SO_KEEPALIVE */
     /* XXX setsockopt SO_TOS IPTOS_THROUGHPUT */
 
+    /*@-internalglobs@*/
     while (connect(fdFileno(data), (struct sockaddr *) &dataAddress, 
-	        sizeof(dataAddress)) < 0) {
+	        sizeof(dataAddress)) < 0)
+    {
 	if (errno == EINTR)
 	    continue;
 	rc = FTPERR_FAILED_DATA_CONNECT;
 	goto errxit;
     }
+    /*@=internalglobs@*/
 
 if (_ftp_debug)
 fprintf(stderr, "-> %s", cmd);
@@ -1167,8 +1224,11 @@ errxit:
     return rc;
 }
 
+/*@unchecked@*/
 /*@null@*/ static rpmCallbackFunction	urlNotify = NULL;
+/*@unchecked@*/
 /*@null@*/ static void *	urlNotifyData = NULL;
+/*@unchecked@*/
 static int			urlNotifyCount = -1;
 
 void urlSetCallback(rpmCallbackFunction notify, void *notifyData, int notifyCount) {
@@ -1218,8 +1278,10 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 	}
     }
 
+/*@-modfilesys@*/
     DBGIO(sfd, (stderr, "++ copied %d bytes: %s\n", itemsCopied,
 	ftpStrerror(rc)));
+/*@=modfilesys@*/
 
     if (urlNotify) {
 	(void)(*urlNotify) (NULL, RPMCALLBACK_INST_OPEN_FILE,
@@ -1230,6 +1292,7 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 }
 
 static int urlConnect(const char * url, /*@out@*/ urlinfo * uret)
+	/*@globals fileSystem @*/
 	/*@modifies *uret, fileSystem @*/
 {
     urlinfo u;
@@ -1316,6 +1379,7 @@ 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 @*/
 {
     static unsigned char ipbuf[3] = { IAC, IP, IAC };
@@ -1333,7 +1397,9 @@ static int ftpAbort(urlinfo u, FD_t data)
     }
     ctrl = u->ctrl;
 
+/*@-modfilesys@*/
     DBGIO(0, (stderr, "-> ABOR\n"));
+/*@=modfilesys@*/
 
 /*@-usereleased -compdef@*/
     if (send(fdFileno(ctrl), ipbuf, sizeof(ipbuf), MSG_OOB) != sizeof(ipbuf)) {
@@ -1376,6 +1442,7 @@ static int ftpAbort(urlinfo u, FD_t data)
 }
 
 static int ftpFileDone(urlinfo u, FD_t data)
+	/*@globals fileSystem @*/
 	/*@modifies u, data, fileSystem @*/
 {
     int rc = 0;
@@ -1393,6 +1460,7 @@ static int ftpFileDone(urlinfo u, FD_t data)
 }
 
 static int httpResp(urlinfo u, FD_t ctrl, /*@out@*/ char ** str)
+	/*@globals fileSystem @*/
 	/*@modifies ctrl, *str, fileSystem @*/
 {
     int ec = 0;
@@ -1416,6 +1484,7 @@ 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 @*/
 {
     urlinfo u = ctrl->url;
@@ -1531,7 +1600,8 @@ void * ufdGetUrlinfo(FD_t fd)
 
 /* =============================================================== */
 static ssize_t ufdRead(void * cookie, /*@out@*/ char * buf, size_t count)
-	/*@modifies internalState, *buf, fileSystem @*/
+	/*@globals fileSystem @*/
+	/*@modifies *buf, fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     int bytesRead;
@@ -1594,7 +1664,8 @@ fprintf(stderr, "*** read: rc %d errno %d %s \"%s\"\n", rc, errno, strerror(errn
 }
 
 static ssize_t ufdWrite(void * cookie, const char * buf, size_t count)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     int bytesWritten;
@@ -1658,7 +1729,8 @@ fprintf(stderr, "*** write: rc %d errno %d %s \"%s\"\n", rc, errno, strerror(err
 }
 
 static inline int ufdSeek(void * cookie, _libio_pos_t pos, int whence)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
 
@@ -1794,7 +1866,7 @@ fprintf(stderr, "-> \r\n");
 /*@-nullstate@*/	/* FIX: u->{ctrl,data}->url undef after XurlLink. */
 /*@null@*/ FD_t ftpOpen(const char *url, /*@unused@*/ int flags,
 		/*@unused@*/ mode_t mode, /*@out@*/ urlinfo *uret)
-	/*@modifies *uret, fileSystem @*/
+	/*@modifies *uret @*/
 {
     urlinfo u = NULL;
     FD_t fd = NULL;
@@ -1832,7 +1904,7 @@ 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, fileSystem @*/
+	/*@modifies *uret @*/
 {
     urlinfo u = NULL;
     FD_t fd = NULL;
@@ -1873,6 +1945,7 @@ exit:
 /*@=nullstate@*/
 
 static /*@null@*/ FD_t ufdOpen(const char * url, int flags, mode_t mode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     FD_t fd = NULL;
@@ -1953,7 +2026,9 @@ fprintf(stderr, "*** ufdOpen(%s,0x%x,0%o)\n", url, (unsigned)flags, (unsigned)mo
 	(void) ufdClose(fd);
 	return NULL;
     }
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tufdOpen(\"%s\",%x,0%o) %s\n", url, (unsigned)flags, (unsigned)mode, fdbg(fd)));
+/*@=modfilesys@*/
     return fd;
 }
 
@@ -1992,6 +2067,7 @@ static inline /*@dependent@*/ /*@null@*/ void * gzdFileno(FD_t fd)
 }
 
 static /*@null@*/ FD_t gzdOpen(const char * path, const char * fmode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     FD_t fd;
@@ -2001,12 +2077,16 @@ static /*@null@*/ FD_t gzdOpen(const char * path, const char * fmode)
     fd = fdNew("open (gzdOpen)");
     fdPop(fd); fdPush(fd, gzdio, gzfile, -1);
     
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdOpen(\"%s\", \"%s\") fd %p %s\n", path, fmode, (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
     return fdLink(fd, "gzdOpen");
 }
 
+/*@-globuse@*/
 static /*@null@*/ FD_t gzdFdopen(void * cookie, const char *fmode)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     int fdno;
@@ -2023,17 +2103,22 @@ static /*@null@*/ FD_t gzdFdopen(void * cookie, const char *fmode)
 
     return fdLink(fd, "gzdFdopen");
 }
+/*@=globuse@*/
 
+/*@-globuse@*/
 static int gzdFlush(FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     return gzflush(gzdFileno(fd), Z_SYNC_FLUSH);	/* XXX W2DO? */
 }
+/*@=globuse@*/
 
 /* =============================================================== */
 /*@-mustmod@*/		/* LCL: *buf is modified */
 static ssize_t gzdRead(void * cookie, /*@out@*/ char * buf, size_t count)
-	/*@modifies internalState, *buf, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *buf, fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     gzFile *gzfile;
@@ -2044,7 +2129,9 @@ static ssize_t gzdRead(void * cookie, /*@out@*/ char * buf, size_t count)
     fdstat_enter(fd, FDSTAT_READ);
     rc = gzread(gzfile, buf, count);
     /*@-compdef@*/
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdRead(%p,%p,%u) rc %lx %s\n", cookie, buf, (unsigned)count, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
     /*@=compdef@*/
     if (rc < 0) {
 	int zerror = 0;
@@ -2064,7 +2151,8 @@ DBGIO(fd, (stderr, "==>\tgzdRead(%p,%p,%u) rc %lx %s\n", cookie, buf, (unsigned)
 /*@=mustmod@*/
 
 static ssize_t gzdWrite(void * cookie, const char * buf, size_t count)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     gzFile *gzfile;
@@ -2077,7 +2165,9 @@ static ssize_t gzdWrite(void * cookie, const char * buf, size_t count)
     gzfile = gzdFileno(fd);
     fdstat_enter(fd, FDSTAT_WRITE);
     rc = gzwrite(gzfile, (void *)buf, count);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdWrite(%p,%p,%u) rc %lx %s\n", cookie, buf, (unsigned)count, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
     if (rc < 0) {
 	int zerror = 0;
 	fd->errcookie = gzerror(gzfile, &zerror);
@@ -2093,7 +2183,8 @@ DBGIO(fd, (stderr, "==>\tgzdWrite(%p,%p,%u) rc %lx %s\n", cookie, buf, (unsigned
 
 /* XXX zlib-1.0.4 has not */
 static inline int gzdSeek(void * cookie, _libio_pos_t pos, int whence)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
 #ifdef USE_COOKIE_SEEK_POINTER
     _IO_off64_t p = *pos;
@@ -2110,7 +2201,9 @@ static inline int gzdSeek(void * cookie, _libio_pos_t pos, int whence)
     gzfile = gzdFileno(fd);
     fdstat_enter(fd, FDSTAT_SEEK);
     rc = gzseek(gzfile, p, whence);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdSeek(%p,%ld,%d) rc %lx %s\n", cookie, (long)p, whence, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
     if (rc < 0) {
 	int zerror = 0;
 	fd->errcookie = gzerror(gzfile, &zerror);
@@ -2128,7 +2221,8 @@ DBGIO(fd, (stderr, "==>\tgzdSeek(%p,%ld,%d) rc %lx %s\n", cookie, (long)p, whenc
 }
 
 static int gzdClose( /*@only@*/ void * cookie)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     gzFile *gzfile;
@@ -2143,7 +2237,9 @@ static int gzdClose( /*@only@*/ void * cookie)
     /* XXX TODO: preserve fd if errors */
 
     if (fd) {
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdClose(%p) zerror %d %s\n", cookie, rc, fdbg(fd)));
+/*@=modfilesys@*/
 	if (rc < 0) {
 	    fd->errcookie = gzerror(gzfile, &rc);
 	    if (rc == Z_ERRNO) {
@@ -2155,7 +2251,9 @@ DBGIO(fd, (stderr, "==>\tgzdClose(%p) zerror %d %s\n", cookie, rc, fdbg(fd)));
 	}
     }
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tgzdClose(%p) rc %lx %s\n", cookie, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     if (_rpmio_debug || rpmIsDebug()) fdstat_print(fd, "GZDIO", stderr);
     if (rc == 0)
@@ -2208,7 +2306,9 @@ static inline /*@dependent@*/ void * bzdFileno(FD_t fd)
     return rc;
 }
 
+/*@-globuse@*/
 static /*@null@*/ FD_t bzdOpen(const char * path, const char * mode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     FD_t fd;
@@ -2219,9 +2319,12 @@ static /*@null@*/ FD_t bzdOpen(const char * path, const char * mode)
     fdPop(fd); fdPush(fd, bzdio, bzfile, -1);
     return fdLink(fd, "bzdOpen");
 }
+/*@=globuse@*/
 
+/*@-globuse@*/
 static /*@null@*/ FD_t bzdFdopen(void * cookie, const char * fmode)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     int fdno;
@@ -2238,17 +2341,23 @@ static /*@null@*/ FD_t bzdFdopen(void * cookie, const char * fmode)
 
     return fdLink(fd, "bzdFdopen");
 }
+/*@=globuse@*/
 
+/*@-globuse@*/
 static int bzdFlush(FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     return bzflush(bzdFileno(fd));
 }
+/*@=globuse@*/
 
 /* =============================================================== */
+/*@-globuse@*/
 /*@-mustmod@*/		/* LCL: *buf is modified */
 static ssize_t bzdRead(void * cookie, /*@out@*/ char * buf, size_t count)
-	/*@modifies internalState, *buf, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *buf, fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     BZFILE *bzfile;
@@ -2274,9 +2383,12 @@ static ssize_t bzdRead(void * cookie, /*@out@*/ char * buf, size_t count)
     return rc;
 }
 /*@=mustmod@*/
+/*@=globuse@*/
 
+/*@-globuse@*/
 static ssize_t bzdWrite(void * cookie, const char * buf, size_t count)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     BZFILE *bzfile;
@@ -2297,6 +2409,7 @@ static ssize_t bzdWrite(void * cookie, const char * buf, size_t count)
     }
     return rc;
 }
+/*@=globuse@*/
 
 static inline int bzdSeek(void * cookie, /*@unused@*/ _libio_pos_t pos,
 			/*@unused@*/ int whence)
@@ -2309,7 +2422,8 @@ static inline int bzdSeek(void * cookie, /*@unused@*/ _libio_pos_t pos,
 }
 
 static int bzdClose( /*@only@*/ void * cookie)
-	/*@modifies internalState, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     FD_t fd = c2f(cookie);
     BZFILE *bzfile;
@@ -2333,7 +2447,9 @@ static int bzdClose( /*@only@*/ void * cookie)
 	}
     }
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==>\tbzdClose(%p) rc %lx %s\n", cookie, (unsigned long)rc, fdbg(fd)));
+/*@=modfilesys@*/
 
     if (_rpmio_debug || rpmIsDebug()) fdstat_print(fd, "BZDIO", stderr);
     if (rc == 0)
@@ -2396,7 +2512,9 @@ size_t Fread(void *buf, size_t size, size_t nmemb, FD_t fd) {
 #ifdef __LCLINT__
     *(char *)buf = '\0';
 #endif
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fread(%p,%u,%u,%p) %s\n", buf, (unsigned)size, (unsigned)nmemb, (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
 
     if (fdGetIo(fd) == fpio) {
 	/*@+voidabstract -nullpass@*/
@@ -2419,7 +2537,9 @@ size_t Fwrite(const void *buf, size_t size, size_t nmemb, FD_t fd)
     int rc;
 
     FDSANE(fd);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fwrite(%p,%u,%u,%p) %s\n", buf, (unsigned)size, (unsigned)nmemb, (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
 
     if (fdGetIo(fd) == fpio) {
 	/*@+voidabstract -nullpass@*/
@@ -2448,7 +2568,9 @@ int Fseek(FD_t fd, _libio_off_t offset, int whence) {
     long int rc;
 
     FDSANE(fd);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fseek(%p,%ld,%d) %s\n", fd, (long)offset, whence, fdbg(fd)));
+/*@=modfilesys@*/
 
     if (fdGetIo(fd) == fpio) {
 	FILE *fp;
@@ -2473,7 +2595,9 @@ int Fclose(FD_t fd)
     int rc = 0, ec = 0;
 
     FDSANE(fd);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fclose(%p) %s\n", (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
 
     fd = fdLink(fd, "Fclose");
     while (fd->nfps >= 0) {
@@ -2644,11 +2768,15 @@ fprintf(stderr, "*** Fdopen(%p,%s) %s\n", fd, fmode, fdbg(fd));
 	    iof = fdio;
 	} else if (!strcmp(end, "gzdio")) {
 	    iof = gzdio;
+	    /*@-internalglobs@*/
 	    fd = gzdFdopen(fd, zstdio);
+	    /*@=internalglobs@*/
 #if HAVE_BZLIB_H
 	} else if (!strcmp(end, "bzdio")) {
 	    iof = bzdio;
+	    /*@-internalglobs@*/
 	    fd = bzdFdopen(fd, zstdio);
+	    /*@=internalglobs@*/
 #endif
 	} else if (!strcmp(end, "ufdio")) {
 	    iof = ufdio;
@@ -2678,7 +2806,9 @@ fprintf(stderr, "*** Fdopen fpio fp %p\n", (void *)fp);
 	    {};
 	if (*end == '\0') {
 	    iof = gzdio;
+	    /*@-internalglobs@*/
 	    fd = gzdFdopen(fd, zstdio);
+	    /*@=internalglobs@*/
 	}
     }
     if (iof == NULL)
@@ -2694,7 +2824,9 @@ fprintf(stderr, "*** Fdopen fpio fp %p\n", (void *)fp);
 	    ciof.seek = iof->seek;
 	    ciof.close = iof->close;
 	    fp = fopencookie(fd, stdio, ciof);
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> fopencookie(%p,\"%s\",*%p) returns fp %p\n", fd, stdio, iof, fp));
+/*@=modfilesys@*/
 	}
 #endif
 
@@ -2709,7 +2841,9 @@ DBGIO(fd, (stderr, "==> fopencookie(%p,\"%s\",*%p) returns fp %p\n", fd, stdio,
 	}
     }
 
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fdopen(%p,\"%s\") returns fd %p %s\n", ofd, fmode, (fd ? fd : NULL), fdbg(fd)));
+/*@=modfilesys@*/
     /*@-refcounttrans -retalias@*/ return fd; /*@=refcounttrans =retalias@*/
 }
 
@@ -2835,7 +2969,9 @@ int Ferror(FD_t fd)
 	if (rc == 0 && ec)
 	    rc = ec;
     }
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Ferror(%p) rc %d %s\n", fd, rc, fdbg(fd)));
+/*@=modfilesys@*/
     return rc;
 }
 
@@ -2846,7 +2982,9 @@ int Fileno(FD_t fd)
     for (i = fd->nfps ; rc == -1 && i >= 0; i--) {
 	rc = fd->fps[i].fdno;
     }
+/*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fileno(%p) rc %d %s\n", (fd ? fd : NULL), rc, fdbg(fd)));
+/*@=modfilesys@*/
     return rc;
 }
 
diff --git a/rpmio/rpmio.h b/rpmio/rpmio.h
index de9748d5f..84e683e33 100644
--- a/rpmio/rpmio.h
+++ b/rpmio/rpmio.h
@@ -57,58 +57,82 @@ extern "C" {
 
 /**
  */
-typedef ssize_t fdio_read_function_t (void *cookie, char *buf, size_t nbytes);
+typedef ssize_t fdio_read_function_t (void *cookie, char *buf, size_t nbytes)
+	/*@globals fileSystem @*/
+	/*@modifies *cookie, fileSystem @*/;
 
 /**
  */
-typedef ssize_t fdio_write_function_t (void *cookie, const char *buf, size_t nbytes);
+typedef ssize_t fdio_write_function_t (void *cookie, const char *buf, size_t nbytes)
+	/*@globals fileSystem @*/
+	/*@modifies *cookie, fileSystem @*/;
 
 /**
  */
-typedef int fdio_seek_function_t (void *cookie, _libio_pos_t pos, int whence);
+typedef int fdio_seek_function_t (void *cookie, _libio_pos_t pos, int whence)
+	/*@globals fileSystem @*/
+	/*@modifies *cookie, fileSystem @*/;
 
 /**
  */
-typedef int fdio_close_function_t (void *cookie);
+typedef int fdio_close_function_t (void *cookie)
+	/*@globals fileSystem @*/
+	/*@modifies *cookie, fileSystem @*/;
 
 
 /**
  */
 typedef /*@only@*/ /*@null@*/ FD_t fdio_ref_function_t ( /*@only@*/ void * cookie,
-		const char * msg, const char * file, unsigned line);
+		const char * msg, const char * file, unsigned line)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 
 /**
  */
 typedef /*@only@*/ /*@null@*/ FD_t fdio_deref_function_t ( /*@only@*/ FD_t fd,
-		const char * msg, const char * file, unsigned line);
+		const char * msg, const char * file, unsigned line)
+	/*@globals fileSystem @*/
+	/*@modifies fd, fileSystem @*/;
 
 
 /**
  */
 typedef /*@only@*/ /*@null@*/ FD_t fdio_new_function_t (const char * msg,
-		const char * file, unsigned line);
+		const char * file, unsigned line)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 
 
 /**
  */
-typedef int fdio_fileno_function_t (void * cookie);
+typedef int fdio_fileno_function_t (void * cookie)
+	/*@globals fileSystem @*/
+	/*@modifies *cookie, fileSystem @*/;
 
 
 /**
  */
-typedef FD_t fdio_open_function_t (const char * path, int flags, mode_t mode);
+typedef FD_t fdio_open_function_t (const char * path, int flags, mode_t mode)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 
 /**
  */
-typedef FD_t fdio_fopen_function_t (const char * path, const char * fmode);
+typedef FD_t fdio_fopen_function_t (const char * path, const char * fmode)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 
 /**
  */
-typedef void * fdio_ffileno_function_t (FD_t fd);
+typedef void * fdio_ffileno_function_t (FD_t fd)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 
 /**
  */
-typedef int fdio_fflush_function_t (FD_t fd);
+typedef int fdio_fflush_function_t (FD_t fd)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 /*@}*/
 
 
@@ -116,15 +140,55 @@ typedef int fdio_fflush_function_t (FD_t fd);
  * \name RPMRPC Vectors.
  */
 /*@{*/
-typedef int fdio_mkdir_function_t (const char * path, mode_t mode);
-typedef int fdio_chdir_function_t (const char * path);
-typedef int fdio_rmdir_function_t (const char * path);
-typedef int fdio_rename_function_t (const char * oldpath, const char * newpath);
-typedef int fdio_unlink_function_t (const char * path);
+
+/**
+ */
+typedef int fdio_mkdir_function_t (const char * path, mode_t mode)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
+
+/**
+ */
+typedef int fdio_chdir_function_t (const char * path)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
+
+/**
+ */
+typedef int fdio_rmdir_function_t (const char * path)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
+
+/**
+ */
+typedef int fdio_rename_function_t (const char * oldpath, const char * newpath)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
+
+/**
+ */
+typedef int fdio_unlink_function_t (const char * path)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 /*@-typeuse@*/
-typedef int fdio_stat_function_t (const char * path, struct stat * st);
-typedef int fdio_lstat_function_t (const char * path, struct stat * st);
-typedef int fdio_access_function_t (const char * path, int amode);
+
+/**
+ */
+typedef int fdio_stat_function_t (const char * path, /*@out@*/ struct stat * st)
+	/*@globals fileSystem @*/
+	/*@modifies *st, fileSystem @*/;
+
+/**
+ */
+typedef int fdio_lstat_function_t (const char * path, /*@out@*/ struct stat * st)
+	/*@globals fileSystem @*/
+	/*@modifies *st, fileSystem @*/;
+
+/**
+ */
+typedef int fdio_access_function_t (const char * path, int amode)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/;
 /*@=typeuse@*/
 /*@}*/
 
@@ -172,29 +236,34 @@ struct FDIO_s {
  * fread(3) clone.
  */
 size_t Fread(/*@out@*/ void * buf, size_t size, size_t nmemb, FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fd, *buf, fileSystem @*/;
 
 /**
  * fwrite(3) clone.
  */
 size_t Fwrite(const void * buf, size_t size, size_t nmemb, FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /**
  * fseek(3) clone.
  */
 int Fseek(FD_t fd, _libio_off_t offset, int whence)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * fclose(3) clone.
  */
 int Fclose( /*@killref@*/ FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /**
  */
 /*@null@*/ FD_t	Fdopen(FD_t fd, const char * fmode)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /**
@@ -202,6 +271,7 @@ int Fclose( /*@killref@*/ FD_t fd)
  */
 /*@null@*/ FD_t	Fopen(/*@null@*/ const char * path,
 			/*@null@*/ const char * fmode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 
@@ -209,6 +279,7 @@ int Fclose( /*@killref@*/ FD_t fd)
  * fflush(3) clone.
  */
 int Fflush(/*@null@*/ FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /**
@@ -221,24 +292,28 @@ int Ferror(/*@null@*/ FD_t fd)
  * fileno(3) clone.
  */
 int Fileno(FD_t fd)
-	/*@*/;
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem@*/;
 
 /**
  * fcntl(2) clone.
  */
 int Fcntl(FD_t fd, int op, void *lip)
+	/*@globals fileSystem @*/
 	/*@modifies fd, *lip, fileSystem @*/;
 
 /**
  * pread(2) clone.
  */
 ssize_t Pread(FD_t fd, void * buf, size_t count, _libio_off_t offset)
+	/*@globals fileSystem @*/
 	/*@modifies fd, *buf, fileSystem @*/;
 
 /**
  * pwrite(2) clone.
  */
 ssize_t Pwrite(FD_t fd, const void * buf, size_t count, _libio_off_t offset)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /*@}*/
@@ -252,60 +327,70 @@ ssize_t Pwrite(FD_t fd, const void * buf, size_t count, _libio_off_t offset)
  * mkdir(2) clone.
  */
 int Mkdir(const char * path, mode_t mode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * chdir(2) clone.
  */
 int Chdir(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * rmdir(2) clone.
  */
 int Rmdir(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * rename(2) clone.
  */
 int Rename(const char * oldpath, const char * newpath)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * link(2) clone.
  */
 int Link(const char * oldpath, const char * newpath)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * unlink(2) clone.
  */
 int Unlink(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * readlink(2) clone.
  */
 int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
+	/*@globals fileSystem @*/
 	/*@modifies *buf, fileSystem @*/;
 
 /**
  * stat(2) clone.
  */
 int Stat(const char * path, /*@out@*/ struct stat * st)
+	/*@globals fileSystem @*/
 	/*@modifies *st, fileSystem @*/;
 
 /**
  * lstat(2) clone.
  */
 int Lstat(const char * path, /*@out@*/ struct stat * st)
+	/*@globals fileSystem @*/
 	/*@modifies *st, fileSystem @*/;
 
 /**
  * access(2) clone.
  */
 int Access(const char * path, int amode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 
@@ -315,12 +400,14 @@ int Access(const char * path, int amode)
 int Glob(const char * pattern, int flags,
 		int errfunc(const char * epath, int eerrno),
 		/*@out@*/ glob_t * pglob)
+	/*@globals fileSystem @*/
 	/*@modifies *pglob, fileSystem @*/;
 
 /**
  * globfree(3) clone.
  */
 void Globfree( /*@only@*/ glob_t * pglob)
+	/*@globals fileSystem @*/
 	/*@modifies *pglob, fileSystem @*/;
 
 
@@ -328,18 +415,21 @@ void Globfree( /*@only@*/ glob_t * pglob)
  * opendir(3) clone.
  */
 /*@null@*/ DIR * Opendir(const char * name)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
 /**
  * readdir(3) clone.
  */
 /*@null@*/ struct dirent * Readdir(DIR * dir)
+	/*@globals fileSystem @*/
 	/*@modifies *dir, fileSystem @*/;
 
 /**
  * closedir(3) clone.
  */
 int	Closedir(/*@only@*/ DIR * dir)
+	/*@globals fileSystem @*/
 	/*@modifies *dir, fileSystem @*/;
 
 /*@}*/
@@ -353,11 +443,13 @@ int	Closedir(/*@only@*/ DIR * dir)
 /**
  */
 off_t	fdSize(FD_t fd)
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem@*/;
 
 /**
  */
 /*@null@*/ FD_t fdDup(int fdno)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem@*/;
 
 #ifdef UNUSED
@@ -378,24 +470,28 @@ off_t	fdSize(FD_t fd)
 /**
  */
 /*@null@*/ FD_t fdOpen(const char *path, int flags, mode_t mode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 #define	fdOpen(_path, _flags, _mode)	fdio->_open((_path), (_flags), (_mode))
 
 /**
  */
 ssize_t fdRead(void * cookie, /*@out@*/ char * buf, size_t count)
+	/*@globals fileSystem @*/
 	/*@modifies *cookie, *buf, fileSystem @*/;
 #define	fdRead(_fd, _buf, _count)	fdio->read((_fd), (_buf), (_count))
 
 /**
  */
 ssize_t	fdWrite(void * cookie, const char * buf, size_t count)
+	/*@globals fileSystem @*/
 	/*@modifies *cookie, fileSystem @*/;
 #define	fdWrite(_fd, _buf, _count)	fdio->write((_fd), (_buf), (_count))
 
 /**
  */
 int fdClose( /*@only@*/ void * cookie)
+	/*@globals fileSystem @*/
 	/*@modifies *cookie, fileSystem @*/;
 #define	fdCLose(_fd)		fdio->close(_fd)
 
@@ -410,7 +506,8 @@ int fdClose( /*@only@*/ void * cookie)
 /**
  */
 int fdWritable(FD_t fd, int secs)
-	/*@modifies fd @*/;
+	/*@globals fileSystem @*/
+	/*@modifies fd, fileSystem @*/;
 
 /**
  */
@@ -461,17 +558,20 @@ typedef enum ftperrCode_e {
  */
 /*@-exportlocal@*/
 int ufdCopy(FD_t sfd, FD_t tfd)
+	/*@globals fileSystem @*/
 	/*@modifies sfd, tfd, fileSystem @*/;
 /*@=exportlocal@*/
 
 /**
  */
 int ufdGetFile( /*@killref@*/ FD_t sfd, FD_t tfd)
+	/*@globals fileSystem @*/
 	/*@modifies sfd, tfd, fileSystem @*/;
 
 /**
  */
 /*@unused@*/ int timedRead(FD_t fd, /*@out@*/ void * bufptr, int length)
+	/*@globals fileSystem @*/
 	/*@modifies fd, *bufptr, fileSystem @*/;
 #define	timedRead	ufdio->read
 
@@ -479,27 +579,27 @@ int ufdGetFile( /*@killref@*/ FD_t sfd, FD_t tfd)
 /*@-exportlocal@*/
 /**
  */
-/*@observer@*/ extern FDIO_t fdio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t fdio;
 
 /**
  */
-/*@observer@*/ extern FDIO_t fpio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t fpio;
 
 /**
  */
-/*@observer@*/ extern FDIO_t ufdio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t ufdio;
 
 /**
  */
-/*@observer@*/ extern FDIO_t gzdio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t gzdio;
 
 /**
  */
-/*@observer@*/ extern FDIO_t bzdio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t bzdio;
 
 /**
  */
-/*@observer@*/ extern FDIO_t fadio;
+/*@observer@*/ /*@unchecked@*/ extern FDIO_t fadio;
 /*@=exportlocal@*/
 /*@}*/
 
diff --git a/rpmio/rpmio_internal.h b/rpmio/rpmio_internal.h
index ff5be7135..a5c7b0a59 100644
--- a/rpmio/rpmio_internal.h
+++ b/rpmio/rpmio_internal.h
@@ -142,6 +142,7 @@ struct _FD_s {
 #define	FDSANE(fd)	assert(fd && fd->magic == FDMAGIC)
 
 /*@-redecl@*/
+/*@unchecked@*/
 extern int _rpmio_debug;
 /*@=redecl@*/
 
diff --git a/rpmio/rpmlog.c b/rpmio/rpmlog.c
index 24f2964dc..0c389bed9 100644
--- a/rpmio/rpmlog.c
+++ b/rpmio/rpmlog.c
@@ -21,7 +21,9 @@
 
 /*@access rpmlogRec @*/
 
+/*@unchecked@*/
 static int nrecs = 0;
+/*@unchecked@*/
 static /*@only@*/ /*@null@*/ rpmlogRec recs = NULL;
 
 /**
@@ -56,6 +58,7 @@ const char * rpmlogMessage(void)
     return _("(no error)");
 }
 
+/*@-modfilesys@*/
 void rpmlogPrint(FILE *f)
 {
     int i;
@@ -70,6 +73,7 @@ void rpmlogPrint(FILE *f)
 	    fprintf(f, "    %s", rec->message);
     }
 }
+/*@=modfilesys@*/
 
 void rpmlogClose (void)
 {
@@ -89,7 +93,9 @@ void rpmlogOpen (/*@unused@*/ const char *ident, /*@unused@*/ int option,
 {
 }
 
+/*@unchecked@*/
 static int rpmlogMask = RPMLOG_UPTO( RPMLOG_NOTICE );
+/*@unchecked@*/
 static /*@unused@*/ int rpmlogFacility = RPMLOG_USER;
 
 int rpmlogSetMask (int mask)
@@ -100,6 +106,7 @@ int rpmlogSetMask (int mask)
     return omask;
 }
 
+/*@unchecked@*/
 static /*@null@*/ rpmlogCallback _rpmlogCallback = NULL;
 
 rpmlogCallback rpmlogSetCallback(rpmlogCallback cb)
@@ -110,7 +117,8 @@ rpmlogCallback rpmlogSetCallback(rpmlogCallback cb)
 }
 
 /*@-readonlytrans@*/	/* FIX: double indirection. */
-/*@observer@*/ static char *rpmlogMsgPrefix[] = {
+/*@observer@*/ /*@unchecked@*/
+static char *rpmlogMsgPrefix[] = {
     N_("fatal error: "),/*!< RPMLOG_EMERG */
     N_("fatal error: "),/*!< RPMLOG_ALERT */
     N_("fatal error: "),/*!< RPMLOG_CRIT */
@@ -130,6 +138,7 @@ static inline int vsnprintf(char * buf, /*@unused@*/ int nb,
 }
 #endif
 
+/*@-modfilesys@*/
 /*@-compmempass@*/ /* FIX: rpmlogMsgPrefix[] dependent, not unqualified */
 /*@-nullstate@*/ /* FIX: rpmlogMsgPrefix[] may be NULL */
 static void vrpmlog (unsigned code, const char *fmt, va_list ap)
@@ -211,13 +220,16 @@ static void vrpmlog (unsigned code, const char *fmt, va_list ap)
 	exit(EXIT_FAILURE);
 }
 /*@=compmempass =nullstate@*/
+/*@=modfilesys@*/
 
 void rpmlog (int code, const char *fmt, ...)
 {
     va_list ap;
 
     va_start(ap, fmt);
+    /*@-internalglobs@*/ /* FIX: shrug */
     vrpmlog(code, fmt, ap);
+    /*@=internalglobs@*/
     va_end(ap);
 }
 
diff --git a/rpmio/rpmlog.h b/rpmio/rpmlog.h
index dce12e039..b0a426010 100644
--- a/rpmio/rpmlog.h
+++ b/rpmio/rpmlog.h
@@ -184,6 +184,7 @@ void rpmlogPrint(FILE *f)
  */
 /*@unused@*/
 void rpmlogClose (void)
+	/*@globals internalState@*/
 	/*@modifies internalState @*/;
 
 /**
@@ -192,19 +193,21 @@ void rpmlogClose (void)
  */
 /*@unused@*/
 void rpmlogOpen (const char * ident, int option, int facility)
+	/*@globals internalState@*/
 	/*@modifies internalState @*/;
 
 /**
  * Set the log mask level.
  */
 int rpmlogSetMask (int mask)
+	/*@globals internalState@*/
 	/*@modifies internalState @*/;
 
 /**
  * Generate a log message using FMT string and option arguments.
  */
 /*@mayexit@*/ /*@printflike@*/ void rpmlog (int pri, const char *fmt, ...)
-	/*@modifies internalState @*/;
+	/*@*/;
 
 /*@-exportlocal@*/
 /**
@@ -228,6 +231,7 @@ int rpmlogCode(void)	/*@*/;
  * Set rpmlog callback function.
  */
 rpmlogCallback rpmlogSetCallback(rpmlogCallback cb)
+	/*@globals internalState@*/
 	/*@modifies internalState @*/;
 /*@=exportlocal@*/
 
@@ -236,6 +240,7 @@ rpmlogCallback rpmlogSetCallback(rpmlogCallback cb)
  * @deprecated gnorpm needs, use rpmlogSetCallback() instead.
  */
 extern rpmlogCallback rpmErrorSetCallback(rpmlogCallback cb)
+	/*@globals internalState@*/
 	/*@modifies internalState @*/;
 
 /**
diff --git a/rpmio/rpmmacro.h b/rpmio/rpmmacro.h
index 52c29de45..0a5b9753a 100644
--- a/rpmio/rpmmacro.h
+++ b/rpmio/rpmmacro.h
@@ -23,6 +23,14 @@ typedef /*@abstract@*/ struct MacroContext_s {
 } * MacroContext;
 
 /**
+ */
+extern MacroContext rpmGlobalMacroContext;
+
+/**
+ */
+extern MacroContext rpmCLIMacroContext;
+
+/**
  * Markers for sources of macros added throughout rpm.
  */
 #define	RMIL_DEFAULT	-15
@@ -46,6 +54,8 @@ extern "C" {
  */
 void	rpmDumpMacroTable	(/*@null@*/ MacroContext mc,
 					/*@null@*/ FILE * fp)
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
 	/*@modifies *fp, fileSystem @*/;
 
 /**
@@ -61,7 +71,9 @@ void	rpmDumpMacroTable	(/*@null@*/ MacroContext mc,
 int	expandMacros	(/*@null@*/ void * spec, /*@null@*/ MacroContext mc,
 				/*@in@*/ /*@out@*/ char * sbuf,
 				size_t sbuflen)
-	/*@modifies *sbuf, internalState @*/;
+	/*@globals rpmGlobalMacroContext,
+		fileSystem @*/
+	/*@modifies *sbuf, rpmGlobalMacroContext, fileSystem @*/;
 
 /**
  * Add macro to context.
@@ -75,7 +87,8 @@ int	expandMacros	(/*@null@*/ void * spec, /*@null@*/ MacroContext mc,
 void	addMacro	(/*@null@*/ MacroContext mc, const char * n,
 				/*@null@*/ const char * o,
 				/*@null@*/ const char * b, int level)
-	/*@modifies mc, internalState @*/;
+	/*@globals rpmGlobalMacroContext@*/
+	/*@modifies mc, rpmGlobalMacroContext @*/;
 
 /**
  * Delete macro from context.
@@ -83,7 +96,8 @@ void	addMacro	(/*@null@*/ MacroContext mc, const char * n,
  * @param n		macro name
  */
 void	delMacro	(/*@null@*/ MacroContext mc, const char * n)
-	/*@modifies mc, internalState @*/;
+	/*@globals rpmGlobalMacroContext@*/
+	/*@modifies mc, rpmGlobalMacroContext @*/;
 
 /**
  * Define macro in context.
@@ -94,7 +108,8 @@ void	delMacro	(/*@null@*/ MacroContext mc, const char * n)
  */
 int	rpmDefineMacro	(/*@null@*/ MacroContext mc, const char * macro,
 				int level)
-	/*@modifies mc, internalState @*/;
+	/*@globals rpmGlobalMacroContext@*/
+	/*@modifies mc, rpmGlobalMacroContext @*/;
 
 /**
  * Load macros from context into global context.
@@ -102,7 +117,8 @@ int	rpmDefineMacro	(/*@null@*/ MacroContext mc, const char * macro,
  * @param level		macro recursion level (0 is entry API)
  */
 void	rpmLoadMacros	(/*@null@*/ MacroContext mc, int level)
-	/*@modifies mc, internalState @*/;
+	/*@globals rpmGlobalMacroContext@*/
+	/*@modifies mc, rpmGlobalMacroContext @*/;
 
 /**
  * Initialize macro context from set of macrofile(s).
@@ -110,14 +126,17 @@ void	rpmLoadMacros	(/*@null@*/ MacroContext mc, int level)
  * @param macrofiles	colon separated list of macro files (NULL does nothing)
  */
 void	rpmInitMacros	(/*@null@*/ MacroContext mc, const char * macrofiles)
-	/*@modifies mc, internalState, fileSystem @*/;
+	/*@globals rpmGlobalMacroContext, rpmCLIMacroContext,
+		fileSystem @*/
+	/*@modifies mc, rpmGlobalMacroContext, fileSystem @*/;
 
 /**
  * Destroy macro context.
  * @param mc		macro context (NULL uses global context).
  */
 void	rpmFreeMacros	(/*@null@*/ MacroContext mc)
-	/*@modifies mc, internalState @*/;
+	/*@globals rpmGlobalMacroContext@*/
+	/*@modifies mc, rpmGlobalMacroContext @*/;
 
 typedef enum rpmCompressedMagic_e {
     COMPRESSED_NOT		= 0,	/*!< not compressed */
@@ -134,6 +153,7 @@ typedef enum rpmCompressedMagic_e {
  */
 int	isCompressed	(const char * file,
 				/*@out@*/ rpmCompressedMagic * compressed)
+	/*@globals fileSystem@*/
 	/*@modifies *compressed, fileSystem @*/;
 
 /**
@@ -142,7 +162,8 @@ int	isCompressed	(const char * file,
  * @return		macro expansion (malloc'ed)
  */
 char *	rpmExpand	(/*@null@*/ const char * arg, ...)
-	/*@*/;
+	/*@globals rpmGlobalMacroContext @*/
+	/*@modifies rpmGlobalMacroContext @*/;
 
 /**
  * Canonicalize file path.
@@ -159,7 +180,8 @@ char *	rpmExpand	(/*@null@*/ const char * arg, ...)
  */
 /*@-redecl@*/
 const char * rpmGetPath	(/*@null@*/ const char * path, ...)
-	/*@*/;
+	/*@globals rpmGlobalMacroContext @*/
+	/*@modifies rpmGlobalMacroContext @*/;
 /*@=redecl@*/
 
 /**
@@ -176,7 +198,8 @@ const char * rpmGetPath	(/*@null@*/ const char * path, ...)
 const char * rpmGenPath	(/*@null@*/ const char * root,
 			/*@null@*/ const char * mdir,
 			/*@null@*/ const char * file)
-	/*@*/;
+	/*@globals rpmGlobalMacroContext @*/
+	/*@modifies rpmGlobalMacroContext @*/;
 /*@=redecl@*/
 
 /**
@@ -187,7 +210,8 @@ const char * rpmGenPath	(/*@null@*/ const char * root,
  * @return		numeric value
  */
 int	rpmExpandNumeric (const char * arg)
-	/*@*/;
+	/*@globals rpmGlobalMacroContext @*/
+	/*@modifies rpmGlobalMacroContext @*/;
 
 #ifdef __cplusplus
 }
diff --git a/rpmio/rpmmalloc.c b/rpmio/rpmmalloc.c
index 911d97721..f401c4581 100644
--- a/rpmio/rpmmalloc.c
+++ b/rpmio/rpmmalloc.c
@@ -9,6 +9,7 @@
 #define	EXIT_FAILURE	1
 #endif
 
+/*@-modfilesys@*/
 /*@only@*/ void *vmefail(size_t size)
 {
     fprintf(stderr, _("memory alloc (%u bytes) returned NULL.\n"), (unsigned)size);
@@ -16,6 +17,7 @@
     /*@notreached@*/
     return NULL;
 }
+/*@=modfilesys@*/
 
 #if !(HAVE_MCHECK_H && defined(__GNUC__)) && !defined(__LCLINT__)
 
diff --git a/rpmio/rpmmessages.h b/rpmio/rpmmessages.h
index 34768d19a..029f9167d 100644
--- a/rpmio/rpmmessages.h
+++ b/rpmio/rpmmessages.h
@@ -64,6 +64,7 @@ typedef /*@only@*/ /*@null@*/
 		const unsigned long total,
 		/*@null@*/ const void * pkgKey,
 		/*@null@*/ rpmCallbackData data)
+	/*@globals internalState@*/
 	/*@modifies internalState@*/;
 
 /**
diff --git a/rpmio/rpmpgp.c b/rpmio/rpmpgp.c
index 06e5bc25c..d608fd9e8 100644
--- a/rpmio/rpmpgp.c
+++ b/rpmio/rpmpgp.c
@@ -7,11 +7,13 @@
 #include "rpmpgp.h"
 #include "debug.h"
 
+/*@unchecked@*/
 static int _debug = 0;
+/*@unchecked@*/
 static int _print = 0;
+/*@unchecked@*/
 /*@null@*/ static struct pgpSig_s * _dig = NULL;
 
-/*@-readonlytrans@*/
 /* This is the unarmored RPM-GPG-KEY public key. */
 const char * redhatPubKeyDSA = "\
 mQGiBDfqVDgRBADBKr3Bl6PO8BQ0H8sJoD6p9U7Yyl7pjtZqioviPwXP+DCWd4u8\n\
@@ -144,6 +146,7 @@ struct pgpValTbl_s pgpHashTbl[] = {
 };
 
 /*@-exportlocal -exportheadervar@*/
+/*@observer@*/ /*@unchecked@*/
 struct pgpValTbl_s pgpKeyServerPrefsTbl[] = {
     { 0x80,			"No-modify" },
     { -1,			"Unknown key server preference" },
@@ -211,9 +214,9 @@ struct pgpValTbl_s pgpPktTbl[] = {
     { PGPPKT_CONTROL,		"Control (GPG)" },
     { -1,			"Unknown packet tag" },
 };
-/*@=readonlytrans@*/
 
 static void pgpPrtNL(void)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     if (!_print) return;
@@ -221,6 +224,7 @@ static void pgpPrtNL(void)
 }
 
 static void pgpPrtInt(const char *pre, int i)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     if (!_print) return;
@@ -230,6 +234,7 @@ static void pgpPrtInt(const char *pre, int i)
 }
 
 static void pgpPrtStr(const char *pre, const char *s)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     if (!_print) return;
@@ -239,6 +244,7 @@ static void pgpPrtStr(const char *pre, const char *s)
 }
 
 static void pgpPrtHex(const char *pre, const byte *p, unsigned int plen)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     if (!_print) return;
@@ -248,6 +254,7 @@ static void pgpPrtHex(const char *pre, const byte *p, unsigned int plen)
 }
 
 void pgpPrtVal(const char * pre, pgpValTbl vs, byte val)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     if (!_print) return;
@@ -258,7 +265,8 @@ void pgpPrtVal(const char * pre, pgpValTbl vs, byte val)
 
 static void pgpHexSet(const char * pre, int lbits,
 		/*@out@*/ mp32number * mpn, const byte * p)
-	/*@modifies *mpn @*/
+	/*@globals fileSystem @*/
+	/*@modifies *mpn, fileSystem @*/
 {
     unsigned int mbits = pgpMpiBits(p);
     unsigned int nbits = (lbits > mbits ? lbits : mbits);
@@ -278,12 +286,14 @@ if (_debug && _print)
 printf("\t %s ", pre), mp32println(mpn->size, mpn->data);
 }
 
-/*@-varuse -readonlytrans @*/
+/*@-varuse =readonlytrans @*/
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpSigRSA[] = {
     " m**d =",
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpSigDSA[] = {
     "    r =",
     "    s =",
@@ -561,13 +571,15 @@ int pgpPrtPktSig(pgpPkt pkt, const byte *h, unsigned int hlen)
     return 0;
 }
 
-/*@-varuse -readonlytrans @*/
+/*@-varuse =readonlytrans @*/
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpPublicRSA[] = {
     "    n =",
     "    e =",
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpSecretRSA[] = {
     "    d =",
     "    p =",
@@ -576,6 +588,7 @@ static const char * pgpSecretRSA[] = {
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpPublicDSA[] = {
     "    p =",
     "    q =",
@@ -584,11 +597,13 @@ static const char * pgpPublicDSA[] = {
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpSecretDSA[] = {
     "    x =",
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpPublicELGAMAL[] = {
     "    p =",
     "    g =",
@@ -596,6 +611,7 @@ static const char * pgpPublicELGAMAL[] = {
     NULL,
 };
 
+/*@observer@*/ /*@unchecked@*/
 static const char * pgpSecretELGAMAL[] = {
     "    x =",
     NULL,
diff --git a/rpmio/rpmpgp.h b/rpmio/rpmpgp.h
index ddef43ac4..b30e4bc4c 100644
--- a/rpmio/rpmpgp.h
+++ b/rpmio/rpmpgp.h
@@ -21,7 +21,7 @@
  */
 typedef const struct pgpValTbl_s {
     int val;
-    const char * str;
+/*@observer@*/ const char * str;
 } * pgpValTbl;
  
 /**
@@ -59,7 +59,7 @@ typedef enum pgpPkt_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpPktTbl[];
 
 /**
@@ -131,7 +131,7 @@ typedef enum pgpSigType_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpSigTypeTbl[];
 
 /**
@@ -171,7 +171,7 @@ typedef enum pgpPubkeyAlgo_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpPubkeyTbl[];
 
 /**
@@ -214,7 +214,7 @@ typedef enum pgpSymkeyAlgo_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpSymkeyTbl[];
 
 /**
@@ -240,7 +240,7 @@ typedef enum pgpCompressAlgo_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpCompressionTbl[];
 
 /**
@@ -274,7 +274,7 @@ typedef enum pgpHashAlgo_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpHashTbl[];
 
 /**
@@ -441,7 +441,7 @@ typedef enum pgpSubType_e {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern struct pgpValTbl_s pgpSubTypeTbl[];
 
 /**
@@ -841,12 +841,12 @@ typedef struct pgpPktUid_s {
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern const char * redhatPubKeyDSA;
 
 /**
  */
-/*@unused@*/
+/*@observer@*/ /*@unchecked@*/ /*@unused@*/
 extern const char * redhatPubKeyRSA;
 
 /**
@@ -1012,62 +1012,74 @@ const char * pgpValStr(pgpValTbl vs, byte val)
 /**
  */
 void pgpPrtVal(const char * pre, pgpValTbl vs, byte val)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtPktSigV3(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtSubType(const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtPktSigV4(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtPktSig(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtKeyV3(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtKeyV4(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtKey(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtUserID(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtComment(pgpPkt pkt, const byte *h, unsigned int hlen)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /**
  */
 int pgpPrtPkt(const byte *p)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 /*@=exportlocal@*/
 
 /**
  */
 int pgpPrtPkts(const byte *pkts, unsigned int plen, struct pgpSig_s *rpmdig, int printing)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 #ifdef __cplusplus
diff --git a/rpmio/rpmrpc.c b/rpmio/rpmrpc.c
index b52d172d3..bf65e7201 100644
--- a/rpmio/rpmrpc.c
+++ b/rpmio/rpmrpc.c
@@ -17,6 +17,7 @@ extern int _rpmio_debug;
 
 /* =============================================================== */
 static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     int rc;
@@ -32,18 +33,21 @@ static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
 }
 
 static int ftpChdir(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     return ftpCmd("CWD", path, NULL);
 }
 
 static int ftpRmdir(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     return ftpCmd("RMD", path, NULL);
 }
 
 static int ftpRename(const char * oldpath, const char * newpath)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     int rc;
@@ -53,6 +57,7 @@ static int ftpRename(const char * oldpath, const char * newpath)
 }
 
 static int ftpUnlink(const char * path)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     return ftpCmd("DELE", path, NULL);
@@ -252,14 +257,19 @@ int Unlink(const char * path) {
 /*
  * FIXME: this is broken. It depends on mc not crossing border on month!
  */
+/*@unchecked@*/
 static int current_mday;
+/*@unchecked@*/
 static int current_mon;
+/*@unchecked@*/
 static int current_year;
 
 /* Following stuff (parse_ls_lga) is used by ftpfs and extfs */
 #define MAXCOLS		30
 
+/*@unchecked@*/
 static char *columns [MAXCOLS];	/* Points to the string in column n */
+/*@unchecked@*/
 static int   column_ptr [MAXCOLS]; /* Index from 0 to the starting positions of the columns */
 
 static int
@@ -783,7 +793,15 @@ typedef enum {
 	DO_FTP_ACCESS	= 4,
 	DO_FTP_GLOB	= 5
 } ftpSysCall_t;
+
+/**
+ */
+/*@unchecked@*/
 static size_t ftpBufAlloced = 0;
+
+/**
+ */
+/*@unchecked@*/
 static /*@only@*/ char * ftpBuf = NULL;
 	
 #define alloca_strdup(_s)       strcpy(alloca(strlen(_s)+1), (_s))
@@ -791,6 +809,7 @@ 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 @*/
 {
     FD_t fd;
@@ -975,13 +994,15 @@ exit:
 }
 
 static int ftpStat(const char * path, /*@out@*/ struct stat *st)
-	/*@modifies *st @*/
+	/*@globals fileSystem @*/
+	/*@modifies *st, fileSystem @*/
 {
     return ftpNLST(path, DO_FTP_STAT, st, NULL, 0);
 }
 
 static int ftpLstat(const char * path, /*@out@*/ struct stat *st)
-	/*@modifies *st @*/
+	/*@globals fileSystem @*/
+	/*@modifies *st, fileSystem @*/
 {
     int rc;
     rc = ftpNLST(path, DO_FTP_LSTAT, st, NULL, 0);
@@ -991,7 +1012,8 @@ fprintf(stderr, "*** ftpLstat(%s) rc %d\n", path, rc);
 }
 
 static int ftpReadlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
-	/*@modifies *buf @*/
+	/*@globals fileSystem @*/
+	/*@modifies *buf, fileSystem @*/
 {
     return ftpNLST(path, DO_FTP_READLINK, NULL, buf, bufsiz);
 }
@@ -999,6 +1021,7 @@ static int ftpReadlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
 static int ftpGlob(const char * path, int flags,
 		int errfunc(const char * epath, int eerno),
 		/*@out@*/ glob_t * pglob)
+	/*@globals fileSystem @*/
 	/*@modifies *pglob, fileSystem @*/
 {
     int rc;
@@ -1020,8 +1043,10 @@ fprintf(stderr, "*** ftpGlob(%s,0x%x,%p,%p) ftpNLST rc %d\n", path, (unsigned)fl
 static void ftpGlobfree(glob_t * pglob)
 	/*@modifies *pglob @*/
 {
+/*@-modfilesys@*/
 if (_rpmio_debug)
 fprintf(stderr, "*** ftpGlobfree(%p)\n", pglob);
+/*@=modfilesys@*/
     if (pglob->gl_offs == -1) {	/* XXX HACK HACK HACK */
 	free((void *)pglob->gl_pathv);
 	pglob->gl_pathv = NULL;
diff --git a/rpmio/rpmurl.h b/rpmio/rpmurl.h
index cc91d8267..3c81f56a9 100644
--- a/rpmio/rpmurl.h
+++ b/rpmio/rpmurl.h
@@ -51,6 +51,9 @@ typedef /*@abstract@*/ /*@refcounted@*/ struct urlinfo {
 extern "C" {
 #endif
 
+/**
+ */
+/*@unchecked@*/
 extern int url_iobuf_size;
 
 /**
@@ -90,14 +93,16 @@ urlinfo	XurlLink(urlinfo u, const char * msg, const char * file, unsigned line)
 /** @todo Remove debugging entry from the ABI. */
 urlinfo	XurlFree( /*@killref@*/ urlinfo u, const char * msg,
 		const char * file, unsigned line)
-	/*@modifies u @*/;
+	/*@globals fileSystem@*/
+	/*@modifies u, fileSystem @*/;
 #define	urlFree(_u, _msg) XurlFree(_u, _msg, __FILE__, __LINE__)
 
 /**
  * Free cached URL control structures.
  */
 void urlFreeCache(void)
-	/*@modifies internalState @*/;
+	/*@globals fileSystem@*/
+	/*@modifies fileSystem @*/;
 
 /**
  * Return type of URL.
@@ -132,6 +137,7 @@ int urlSplit(const char * url, /*@out@*/ urlinfo * u)
  * @return		0 on success, otherwise FTPERR_* code
  */
 int urlGetFile(const char * url, /*@null@*/ const char * dest)
+	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 #ifdef __cplusplus
diff --git a/rpmio/ugid.c b/rpmio/ugid.c
index 67fbf76e4..d55524bc9 100644
--- a/rpmio/ugid.c
+++ b/rpmio/ugid.c
@@ -41,7 +41,9 @@ int unameToUid(const char * thisUname, uid_t * uid)
 
 	pwent = getpwnam(thisUname);
 	if (pwent == NULL) {
+	    /*@-internalglobs@*/ /* FIX: shrug */
 	    endpwent();
+	    /*@=internalglobs@*/
 	    pwent = getpwnam(thisUname);
 	    if (pwent == NULL) return -1;
 	}
@@ -83,7 +85,9 @@ int gnameToGid(const char * thisGname, gid_t * gid)
 
 	grent = getgrnam(thisGname);
 	if (grent == NULL) {
+	    /*@-internalglobs@*/ /* FIX: shrug */
 	    endgrent();
+	    /*@=internalglobs@*/
 	    grent = getgrnam(thisGname);
 	    if (grent == NULL) return -1;
 	}
diff --git a/rpmio/url.c b/rpmio/url.c
index e838372ce..4553643b6 100644
--- a/rpmio/url.c
+++ b/rpmio/url.c
@@ -28,13 +28,21 @@ int url_iobuf_size = URL_IOBUF_SIZE;
 #define	RPMURL_DEBUG_IO		0x40000000
 #define	RPMURL_DEBUG_REFS	0x20000000
 
+/*@unchecked@*/
 int _url_debug = 0;
 #define	URLDBG(_f, _m, _x)	if ((_url_debug | (_f)) & (_m)) fprintf _x
 
 #define URLDBGIO(_f, _x)	URLDBG((_f), RPMURL_DEBUG_IO, _x)
 #define URLDBGREFS(_f, _x)	URLDBG((_f), RPMURL_DEBUG_REFS, _x)
 
-/*@only@*/ /*@null@*/ static urlinfo *uCache = NULL;
+/**
+ */
+/*@only@*/ /*@null@*/ /*@unchecked@*/
+static urlinfo *uCache = NULL;
+
+/**
+ */
+/*@unchecked@*/
 static int uCount = 0;
 
 /**
@@ -53,7 +61,9 @@ urlinfo XurlLink(urlinfo u, const char *msg, const char *file, unsigned line)
 {
     URLSANE(u);
     u->nrefs++;
+/*@-modfilesys@*/
 URLDBGREFS(0, (stderr, "--> url %p ++ %d %s at %s:%u\n", u, u->nrefs, msg, file, line));
+/*@=modfilesys@*/
     /*@-refcounttrans@*/ return u; /*@=refcounttrans@*/
 }
 
@@ -169,7 +179,10 @@ static int urlStrcmp(/*@null@*/ const char * str1, /*@null@*/ const char * str2)
 }
 
 static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
-	/*@modifies *uret @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem@*/
+	/*@modifies *uret, rpmGlobalMacroContext,
+		fileSystem @*/
 {
     urlinfo u;
     int ucx;
@@ -304,6 +317,9 @@ static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
     return;
 }
 
+/**
+ */
+/*@observer@*/ /*@unchecked@*/
 static struct urlstring {
 /*@observer@*/ /*@null@*/ const char * leadin;
     urltype	ret;
@@ -368,6 +384,7 @@ urltype urlPath(const char * url, const char ** pathp)
  * Split URL into components. The URL can look like
  *	service://user:password@host:port/path
  */
+/*@-modfilesys@*/
 int urlSplit(const char * url, urlinfo *uret)
 {
     urlinfo u;
@@ -454,10 +471,13 @@ int urlSplit(const char * url, urlinfo *uret)
     myurl = _free(myurl);
     if (uret) {
 	*uret = u;
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
 	urlFind(uret, 0);
+/*@=globs@*/
     }
     return 0;
 }
+/*@=modfilesys@*/
 
 int urlGetFile(const char * url, const char * dest)
 {