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

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

46 files changed, 340 insertions, 269 deletions

diff --git a/beecrypt/beecrypt.c b/beecrypt/beecrypt.c
index cdcce31d0..d5a6f24a3 100644
--- a/beecrypt/beecrypt.c
+++ b/beecrypt/beecrypt.c
@@ -172,9 +172,11 @@ const randomGenerator* randomGeneratorGet(int index)
 	if ((index < 0) || (index >= RANDOMGENERATORS))
 		return (const randomGenerator*) 0;
 
+/*@-boundsread@*/
 	/*@-compmempass@*/
 	return randomGeneratorList[index];
 	/*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -291,9 +293,11 @@ const hashFunction* hashFunctionGet(int index)
 	if ((index < 0) || (index >= HASHFUNCTIONS))
 		return (const hashFunction*) 0;
 
+/*@-boundsread@*/
 	/*@-compmempass@*/
 	return hashFunctionList[index];
 	/*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -511,9 +515,11 @@ const keyedHashFunction* keyedHashFunctionGet(int index)
 	if ((index < 0) || (index >= KEYEDHASHFUNCTIONS))
 		return (const keyedHashFunction*) 0;
 
+/*@-boundsread@*/
 	/*@-compmempass@*/
 	return keyedHashFunctionList[index];
 	/*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -752,9 +758,11 @@ const blockCipher* blockCipherGet(int index)
 	if ((index < 0) || (index >= BLOCKCIPHERS))
 		return (const blockCipher*) 0;
 
+/*@-boundsread@*/
 	/*@-compmempass@*/
 	return blockCipherList[index];
 	/*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
diff --git a/beecrypt/blockpad.c b/beecrypt/blockpad.c
index a6637ec34..466e44db5 100644
--- a/beecrypt/blockpad.c
+++ b/beecrypt/blockpad.c
@@ -70,9 +70,9 @@ memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
 /*		tmp->data = (byte*) realloc(tmp->data, tmp->size; */
 	}
 
-	/*@-temptrans@*/
+	/*@-temptrans -compdef @*/
 	return tmp;
-	/*@=temptrans@*/
+	/*@=temptrans =compdef @*/
 }
 /*@=boundsread@*/
 
diff --git a/beecrypt/blockpad.h b/beecrypt/blockpad.h
index 265cc15b2..e0f152daa 100644
--- a/beecrypt/blockpad.h
+++ b/beecrypt/blockpad.h
@@ -51,7 +51,8 @@ memchunk* pkcs5Pad  (int blockbytes, /*@only@*/ /*@null@*/ memchunk* tmp)
  * @return		buffer with pad removed
  */
 BEECRYPTAPI /*@only@*/ /*@null@*/
-memchunk* pkcs5Unpad(int blockbytes, /*@returned@*/ /*@null@*/ memchunk* tmp)
+memchunk* pkcs5Unpad(int blockbytes,
+		/*@returned@*/ /*@null@*/ /*@out@*/ memchunk* tmp)
 	/*@modifies tmp */;
 
 /**
diff --git a/beecrypt/endianness.c b/beecrypt/endianness.c
index fe8a383f5..762bc5235 100644
--- a/beecrypt/endianness.c
+++ b/beecrypt/endianness.c
@@ -512,7 +512,9 @@ int readChars(javachar* c, FILE* ifp, int count)
 
 int writeByte(javabyte b, FILE* ofp)
 {
+/*@-boundsread@*/
 	return fwrite(&b, 1, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeShort(javashort s, FILE* ofp)
@@ -520,7 +522,9 @@ int writeShort(javashort s, FILE* ofp)
 	#if !(WORDS_BIGENDIAN)
 	s = swap16(s);
 	#endif
+/*@-boundsread@*/
 	return fwrite(&s, 2, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeInt(javaint i, FILE* ofp)
@@ -528,7 +532,9 @@ int writeInt(javaint i, FILE* ofp)
 	#if !(WORDS_BIGENDIAN)
 	i = swap32(i);
 	#endif
+/*@-boundsread@*/
 	return fwrite(&i, 4, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeLong(javalong l, FILE* ofp)
@@ -536,7 +542,9 @@ int writeLong(javalong l, FILE* ofp)
 	#if !(WORDS_BIGENDIAN)
 	l = swap64(l);
 	#endif
+/*@-boundsread@*/
 	return fwrite(&l, 8, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeChar(javachar c, FILE* ofp)
@@ -544,7 +552,9 @@ int writeChar(javachar c, FILE* ofp)
 	#if !(WORDS_BIGENDIAN)
 	c = swap16(c);
 	#endif
+/*@-boundsread@*/
 	return fwrite(&c, 2, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeInts(const javaint* i, FILE* ofp, int count)
diff --git a/build.c b/build.c
index 4a00cb532..6ed926abb 100644
--- a/build.c
+++ b/build.c
@@ -57,8 +57,8 @@ static int checkSpec(rpmts ts, Header h)
 /**
  */
 static int isSpecFile(const char * specfile)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     char buf[256];
     const char * s;
diff --git a/build/build.c b/build/build.c
index b98fd1935..e5625f96c 100644
--- a/build/build.c
+++ b/build/build.c
@@ -20,9 +20,8 @@ static int _build_debug = 0;
 /**
  */
 static void doRmSource(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     struct Source *p;
     Package pkg;
diff --git a/build/files.c b/build/files.c
index 7876ccbe6..b51152b85 100644
--- a/build/files.c
+++ b/build/files.c
@@ -710,9 +710,12 @@ static int parseForConfig(char * buf, FileList fl)
 
 /**
  */
-static int langCmp(const void * ap, const void * bp)	/*@*/
+static int langCmp(const void * ap, const void * bp)
+	/*@*/
 {
+/*@-boundsread@*/
     return strcmp(*(const char **)ap, *(const char **)bp);
+/*@=boundsread@*/
 }
 
 /**
@@ -1124,10 +1127,9 @@ static int checkHardLinks(FileList fl)
 /*@-bounds@*/
 static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 		rpmfi * cpioList, Header h, int isSrc)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies h, *cpioList, fl->processingFailed, fl->fileList,
-		rpmGlobalMacroContext, fileSystem @*/
+		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int _addDotSlash = !(isSrc || rpmExpandNumeric("%{_noPayloadPrefix}"));
     uint_32 multiLibMask = 0;
@@ -1503,12 +1505,11 @@ static /*@null@*/ FileListRec freeFileList(/*@only@*/ FileListRec fileList,
 /*@-boundswrite@*/
 static int addFile(FileList fl, const char * diskURL,
 		/*@null@*/ struct stat * statp)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies *statp, *fl, fl->processingFailed,
 		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
 		fl->totalFileSize, fl->fileCount, fl->inFtw, fl->isDir,
-		rpmGlobalMacroContext, fileSystem @*/
+		rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     const char *fileURL = diskURL;
     struct stat statbuf;
@@ -1727,12 +1728,11 @@ static int addFile(FileList fl, const char * diskURL,
 /*@-boundswrite@*/
 static int processBinaryFile(/*@unused@*/ Package pkg, FileList fl,
 		const char * fileURL)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies *fl, fl->processingFailed,
 		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
 		fl->totalFileSize, fl->fileCount, fl->inFtw, fl->isDir,
-		rpmGlobalMacroContext, fileSystem @*/
+		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int doGlob;
     const char *diskURL = NULL;
diff --git a/build/myftw.c b/build/myftw.c
index a55b06781..7c3c71733 100644
--- a/build/myftw.c
+++ b/build/myftw.c
@@ -58,8 +58,8 @@ myftw_dir (DIR **dirs, int level, int descriptors,
 	   char *dir, size_t len, 
 	   myftwFunc func,
 	   void *fl)
-	/*@globals errno, fileSystem @*/
-	/*@modifies *dirs, *dir, errno, fileSystem @*/
+	/*@globals errno, fileSystem, internalState @*/
+	/*@modifies *dirs, *dir, errno, fileSystem, internalState @*/
 {
   int got;
   struct dirent *entry;
diff --git a/build/myftw.h b/build/myftw.h
index f4e720987..2330de100 100644
--- a/build/myftw.h
+++ b/build/myftw.h
@@ -22,8 +22,8 @@ typedef int (*myftwFunc) (void *fl, const char *name, struct stat *statp)
 	/*@*/;
 
 int myftw (const char *dir, int descriptors, myftwFunc func, void *fl)
-	/*@globals fileSystem @*/
-	/*@modifies *fl, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *fl, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }
diff --git a/build/pack.c b/build/pack.c
index 314edc76a..61a822317 100644
--- a/build/pack.c
+++ b/build/pack.c
@@ -55,9 +55,9 @@ static inline int genSourceRpmName(Spec spec)
  */
 static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
 		const char * fmodeMacro)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies fdo, csa, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies fdo, csa, rpmGlobalMacroContext,
+		fileSystem, internalState @*/
 {
     rpmts ts = rpmtsCreate();
     rpmfi fi = csa->cpioList;
@@ -104,8 +104,8 @@ static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
 /**
  */
 static int cpio_copy(FD_t fdo, CSA_t csa)
-	/*@globals fileSystem@*/
-	/*@modifies fdo, csa, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fdo, csa, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     size_t nb;
@@ -130,9 +130,8 @@ static int cpio_copy(FD_t fdo, CSA_t csa)
  */
 static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
 		const char * file, /*@only@*/ StringBuf sb)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     const char * fn = buf;
@@ -168,9 +167,8 @@ static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
 /**
  */
 static int addFileToTag(Spec spec, const char * file, Header h, int tag)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     StringBuf sb = newStringBuf();
@@ -193,9 +191,8 @@ static int addFileToTag(Spec spec, const char * file, Header h, int tag)
 /**
  */
 static int addFileToArrayTag(Spec spec, const char *file, Header h, int tag)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     StringBuf sb = newStringBuf();
     char *s;
@@ -213,9 +210,9 @@ static int addFileToArrayTag(Spec spec, const char *file, Header h, int tag)
 /**
  */
 static int processScriptFiles(Spec spec, Package pkg)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies pkg->header, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies pkg->header, rpmGlobalMacroContext,
+		fileSystem, internalState @*/
 {
     struct TriggerFileEntry *p;
     
diff --git a/build/parsePreamble.c b/build/parsePreamble.c
index 259cb9554..9186a7537 100644
--- a/build/parsePreamble.c
+++ b/build/parsePreamble.c
@@ -353,9 +353,8 @@ static void fillOutMainPackage(Header h)
  */
 /*@-boundswrite@*/
 static int readIcon(Header h, const char * file)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     const char *fn = NULL;
     char *icon;
@@ -459,14 +458,13 @@ extern int noLang;
 /*@-boundswrite@*/
 static int handlePreambleTag(Spec spec, Package pkg, int tag, const char *macro,
 			     const char *lang)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->macros, spec->st, spec->buildRootURL,
 		spec->sources, spec->numSources, spec->noSource,
 		spec->buildRestrictions, spec->BANames, spec->BACount,
 		spec->line, spec->gotBuildRootURL,
 		pkg->header, pkg->autoProv, pkg->autoReq, pkg->icon,
-		rpmGlobalMacroContext, fileSystem @*/
+		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
diff --git a/build/parsePrep.c b/build/parsePrep.c
index a6d9f4113..7b3172494 100644
--- a/build/parsePrep.c
+++ b/build/parsePrep.c
@@ -36,8 +36,8 @@
  * @return		0 on success
  */
 static int checkOwners(const char * urlfn)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     struct stat sb;
 
@@ -67,9 +67,8 @@ static int checkOwners(const char * urlfn)
 /*@-boundswrite@*/
 /*@observer@*/ static char *doPatch(Spec spec, int c, int strip, const char *db,
 		     int reverse, int removeEmpties)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -162,9 +161,8 @@ static int checkOwners(const char * urlfn)
  */
 /*@-boundswrite@*/
 /*@observer@*/ static const char *doUntar(Spec spec, int c, int quietly)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -281,10 +279,9 @@ static int checkOwners(const char * urlfn)
  * @return		0 on success
  */
 static int doSetupMacro(Spec spec, char *line)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->buildSubdir, spec->macros, spec->prep,
-		rpmGlobalMacroContext, fileSystem @*/
+		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     StringBuf before;
@@ -441,8 +438,9 @@ static int doSetupMacro(Spec spec, char *line)
 /*@-boundswrite@*/
 static int doPatchMacro(Spec spec, char *line)
 	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
-	/*@modifies spec->prep, rpmGlobalMacroContext, fileSystem @*/
+		fileSystem, internalState @*/
+	/*@modifies spec->prep, rpmGlobalMacroContext,
+		fileSystem, internalState  @*/
 {
     char *opt_b;
     int opt_P, opt_p, opt_R, opt_E;
diff --git a/build/rpmbuild.h b/build/rpmbuild.h
index 769a9b729..2f42550fc 100644
--- a/build/rpmbuild.h
+++ b/build/rpmbuild.h
@@ -153,19 +153,18 @@ extern /*@observer@*/ int_32 * const getBuildTime(void)	/*@*/;
  * @return		0 on success, 1 on EOF, <0 on error
  */
 int readLine(Spec spec, int strip)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Stop reading from spec file, freeing resources.
  * @param spec		spec file control structure
  */
 void closeSpec(/*@partial@*/ Spec spec)
-	/*@globals fileSystem@*/
-	/*@modifies spec->fileStack, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies spec->fileStack, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Truncate comment lines.
@@ -208,12 +207,11 @@ void addChangelogEntry(Header h, time_t time, const char * name,
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->build, spec->install, spec->clean, spec->macros,
 		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse %%changelog section of a spec file.
@@ -221,12 +219,11 @@ int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parseChangelog(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
 		spec->packages->header,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse %%description section of a spec file.
@@ -234,13 +231,12 @@ int parseChangelog(Spec spec)
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parseDescription(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->packages,
 		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
 		spec->st,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Parse %%files section of a spec file.
@@ -248,12 +244,11 @@ int parseDescription(Spec spec)
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parseFiles(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->packages,
 		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse tags from preamble of a spec file.
@@ -280,12 +275,11 @@ int parsePreamble(Spec spec, int initialPackage)
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parsePrep(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->prep, spec->buildSubdir, spec->macros,
 		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse dependency relations from spec file and/or autogenerated output buffer.
@@ -309,12 +303,11 @@ int parseRCPOT(Spec spec, Package pkg, const char * field, int tag, int index,
  * @return		>= 0 next rpmParseState, < 0 on error
  */
 int parseScript(Spec spec, int parsePart)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem@*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->packages,
 		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
 		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Evaluate boolean expression.
@@ -444,12 +437,11 @@ void initSourceHeader(Spec spec)
  * @return		0 on success
  */
 int processSourceFiles(Spec spec)
-	/*@globals rpmGlobalMacroContext,
-		fileSystem @*/
+	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies spec->sourceHeader, spec->sourceCpioList,
 		spec->buildRestrictions, spec->BANames,
 		spec->packages->header,
-		rpmGlobalMacroContext, fileSystem @*/;
+		rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse spec file into spec control structure.
diff --git a/build/rpmspec.h b/build/rpmspec.h
index fa2877562..9145a64ba 100644
--- a/build/rpmspec.h
+++ b/build/rpmspec.h
@@ -192,8 +192,8 @@ extern "C" {
  * @return		NULL always
  */
 /*@null@*/ Spec freeSpec(/*@only@*/ /*@null@*/ Spec spec)
-	/*@globals fileSystem @*/
-	/*@modifies spec, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies spec, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * @param spec		spec file control structure
@@ -201,8 +201,8 @@ extern "C" {
  */
 /*@-declundef@*/
 extern /*@null@*/ Spec (*freeSpecVec) (Spec spec)	/* XXX FIXME */
-	/*@globals fileSystem @*/
-	/*@modifies spec, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies spec, fileSystem, internalState @*/;
 /*@=declundef@*/
 
 /** \ingroup rpmbuild
diff --git a/lib/cpio.h b/lib/cpio.h
index 9e04d0985..7cbb61b66 100644
--- a/lib/cpio.h
+++ b/lib/cpio.h
@@ -101,8 +101,8 @@ extern "C" {
  * @return		0 on success
  */
 int cpioTrailerWrite(FSM_t fsm)
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 /**
  * Write cpio header.
@@ -111,8 +111,8 @@ int cpioTrailerWrite(FSM_t fsm)
  * @return		0 on success
  */
 int cpioHeaderWrite(FSM_t fsm, struct stat * st)
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 /**
  * Read cpio header.
@@ -121,15 +121,16 @@ int cpioHeaderWrite(FSM_t fsm, struct stat * st)
  * @return		0 on success
  */
 int cpioHeaderRead(FSM_t fsm, struct stat * st)
-	/*@globals fileSystem@*/
-	/*@modifies fsm, *st, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, *st, fileSystem, internalState @*/;
 
 /** \ingroup payload
  * Return formatted error message on payload handling failure.
  * @param rc		error code
  * @return		formatted error string
  */
-/*@observer@*/ const char *const cpioStrerror(int rc)		/*@*/;
+/*@observer@*/ const char *const cpioStrerror(int rc)
+	/*@*/;
 
 #ifdef __cplusplus
 }
diff --git a/lib/depends.c b/lib/depends.c
index 4f3a9f10c..b838307c9 100644
--- a/lib/depends.c
+++ b/lib/depends.c
@@ -334,8 +334,8 @@ int rpmtsAddEraseElement(rpmts ts, Header h, int dboffset)
  * @return		0 if satisfied, 1 if not satisfied, 2 if error
  */
 static int unsatisfiedDepend(rpmts ts, rpmds dep)
-	/*@globals _cacheDependsRC, fileSystem @*/
-	/*@modifies ts, _cacheDependsRC, fileSystem @*/
+	/*@globals _cacheDependsRC, fileSystem, internalState @*/
+	/*@modifies ts, _cacheDependsRC, fileSystem, internalState @*/
 {
     DBT * key = alloca(sizeof(*key));
     DBT * data = alloca(sizeof(*data));
@@ -556,8 +556,8 @@ exit:
 static int checkPackageDeps(rpmts ts, const char * pkgNEVR,
 		/*@null@*/ rpmds requires, /*@null@*/ rpmds conflicts,
 		/*@null@*/ const char * depName, uint_32 multiLib, int adding)
-	/*@globals fileSystem @*/
-	/*@modifies ts, requires, conflicts, fileSystem */
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, requires, conflicts, fileSystem, internalState */
 {
     const char * Name;
     int_32 Flags;
@@ -657,8 +657,8 @@ static int checkPackageDeps(rpmts ts, const char * pkgNEVR,
  */
 static int checkPackageSet(rpmts ts, const char * dep,
 		/*@only@*/ /*@null@*/ rpmdbMatchIterator mi, int adding)
-	/*@globals fileSystem @*/
-	/*@modifies ts, mi, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, mi, fileSystem, internalState @*/
 {
     int scareMem = 1;
     Header h;
@@ -696,8 +696,8 @@ static int checkPackageSet(rpmts ts, const char * dep,
  * @return		0 no problems found
  */
 static int checkDependentPackages(rpmts ts, const char * dep)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fileSystem, internalState @*/
 {
     rpmdbMatchIterator mi;
     mi = rpmtsInitIterator(ts, RPMTAG_REQUIRENAME, dep, 0);
@@ -711,8 +711,8 @@ static int checkDependentPackages(rpmts ts, const char * dep)
  * @return		0 no problems found
  */
 static int checkDependentConflicts(rpmts ts, const char * dep)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fileSystem, internalState @*/
 {
     int rc = 0;
 
diff --git a/lib/fsm.c b/lib/fsm.c
index db694dab8..a1f890783 100644
--- a/lib/fsm.c
+++ b/lib/fsm.c
@@ -384,8 +384,8 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
 	/*@uses fsm->links, fsm->ix, fsm->sb, fsm->goal, fsm->nsuffix @*/
 	/*@defines fsm->li @*/
 	/*@releases fsm->path @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     struct stat * st = &fsm->sb;
     int rc = 0;
@@ -736,8 +736,8 @@ int fsmMapAttrs(FSM_t fsm)
  */
 static int expandRegular(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->sb @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const struct stat * st = &fsm->sb;
     int left = st->st_size;
@@ -803,8 +803,8 @@ exit:
  */
 static int writeFile(/*@special@*/ FSM_t fsm, int writeData)
 	/*@uses fsm->path, fsm->opath, fsm->sb, fsm->osb, fsm->cfd @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * opath = fsm->opath;
@@ -951,8 +951,8 @@ exit:
  */
 static int writeLinkedFile(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->nsuffix, fsm->ix, fsm->li, fsm->failedFile @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * nsuffix = fsm->nsuffix;
@@ -999,8 +999,8 @@ static int writeLinkedFile(/*@special@*/ FSM_t fsm)
 /*@-boundsread@*/
 static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->opath, fsm->nsuffix, fsm->ix, fsm->li @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * opath = fsm->opath;
@@ -1064,8 +1064,8 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 static int fsmCommitLinks(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->nsuffix, fsm->ix, fsm->sb,
 		fsm->li, fsm->links @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * nsuffix = fsm->nsuffix;
@@ -1110,8 +1110,8 @@ static int fsmCommitLinks(/*@special@*/ FSM_t fsm)
  */
 static int fsmRmdirs(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->dnlx, fsm->ldn, fsm->rdbuf, fsm->iter @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     void * dnli = dnlInitIterator(fsm, 1);
@@ -1167,8 +1167,8 @@ static int fsmMkdirs(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->sb, fsm->osb, fsm->rdbuf, fsm->iter,
 		fsm->ldn, fsm->ldnlen, fsm->ldnalloc @*/
 	/*@defines fsm->dnlx, fsm->ldn @*/
-	/*@globals fileSystem@*/
-	/*@modifies fsm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/
 {
     struct stat * st = &fsm->sb;
     struct stat * ost = &fsm->osb;
diff --git a/lib/fsm.h b/lib/fsm.h
index d093ca93a..8cd4f0b8c 100644
--- a/lib/fsm.h
+++ b/lib/fsm.h
@@ -244,8 +244,9 @@ int fsmSetup(FSM_t fsm, fileStage goal,
 		FD_t cfd,
 		/*@out@*/ unsigned int * archiveSize,
 		/*@out@*/ const char ** failedFile)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, ts, fi, *archiveSize, *failedFile, fileSystem  @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, ts, fi, *archiveSize, *failedFile,
+		fileSystem, internalState @*/;
 
 /**
  * Clean file state machine.
@@ -253,8 +254,8 @@ int fsmSetup(FSM_t fsm, fileStage goal,
  * @return		0 on success
  */
 int fsmTeardown(FSM_t fsm)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 /*@-exportlocal@*/
 /**
@@ -295,8 +296,8 @@ int fsmMapAttrs(FSM_t fsm)
  * @return		0 on success
  */
 int fsmStage(/*@partial@*/ FSM_t fsm, fileStage stage)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }
diff --git a/lib/misc.c b/lib/misc.c
index 839dcb18b..c879fea90 100644
--- a/lib/misc.c
+++ b/lib/misc.c
@@ -122,8 +122,8 @@ int dosetenv(const char * name, const char * value, int overwrite)
 }
 
 static int rpmMkpath(const char * path, mode_t mode, uid_t uid, gid_t gid)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     char * d, * de;
     int created = 0;
diff --git a/lib/misc.h b/lib/misc.h
index ce603501b..ed93b9905 100644
--- a/lib/misc.h
+++ b/lib/misc.h
@@ -18,8 +18,8 @@ extern "C" {
  * @return		rpmRC return code
  */
 rpmRC rpmMkdirPath (const char * dpath, const char * dname)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /**
  * Split string into fields separated by a character.
diff --git a/lib/psm.c b/lib/psm.c
index bd7326058..79bd853a0 100644
--- a/lib/psm.c
+++ b/lib/psm.c
@@ -355,8 +355,8 @@ static int mergeFiles(rpmfi fi, Header h, Header newH)
  */
 /*@-bounds@*/
 static int markReplacedFiles(const PSM_t psm)
-	/*@globals fileSystem@*/
-	/*@modifies psm, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies psm, fileSystem, internalState @*/
 {
     const rpmts ts = psm->ts;
     rpmfi fi = psm->fi;
diff --git a/lib/rpmchecksig.c b/lib/rpmchecksig.c
index 3efa16b93..4594b0f43 100644
--- a/lib/rpmchecksig.c
+++ b/lib/rpmchecksig.c
@@ -348,7 +348,7 @@ static int rpmImportPubkey(const rpmts ts,
 		/*@unused@*/ QVA_t qva,
 		/*@null@*/ const char ** argv)
 	/*@globals RPMVERSION, fileSystem, internalState @*/
-	/*@modifies fileSystem, internalState @*/
+	/*@modifies ts, fileSystem, internalState @*/
 {
     const char * fn;
     int res = 0;
diff --git a/lib/rpmcli.h b/lib/rpmcli.h
index d6237e733..7643a7685 100644
--- a/lib/rpmcli.h
+++ b/lib/rpmcli.h
@@ -372,8 +372,8 @@ int rpmcliQuery(rpmts ts, QVA_t qva, /*@null@*/ const char ** argv)
 /*@-incondefs@*/
 int rpmVerifyFile(const rpmts ts, rpmfi fi,
 		/*@out@*/ rpmVerifyAttrs * res, rpmVerifyAttrs omitMask)
-	/*@globals fileSystem @*/
-	/*@modifies fi, *res, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fi, *res, fileSystem, internalState @*/
 	/*@requires maxSet(res) >= 0 @*/;
 /*@=incondefs@*/
 
@@ -575,8 +575,8 @@ typedef /*@abstract@*/ struct IDTindex_s {
  * @return 		id index
  */
 /*@only@*/ /*@null@*/ IDTX IDTXload(rpmts ts, rpmTag tag)
-	/*@globals fileSystem@*/
-	/*@modifies ts, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fileSystem, internalState  @*/;
 
 /**
  * Load tag (instance,value) pairs from packages, and return sorted id index.
diff --git a/lib/rpmds.c b/lib/rpmds.c
index 3dcd5c3ba..eb141315e 100644
--- a/lib/rpmds.c
+++ b/lib/rpmds.c
@@ -271,7 +271,9 @@ rpmds rpmdsThis(Header h, rpmTag tagN, int_32 Flags)
     EVR[0] = t;
     if (ep) {
 	sprintf(t, "%d:", *ep);
+/*@-compdef@*/
 	t += strlen(t);
+/*@=compdef@*/
     }
     t = stpcpy( stpcpy( stpcpy( t, v), "-"), r);
 /*@=boundswrite@*/
diff --git a/lib/rpmts.c b/lib/rpmts.c
index 6c69a84ac..d59f16c70 100644
--- a/lib/rpmts.c
+++ b/lib/rpmts.c
@@ -25,7 +25,6 @@
 /* portability fiddles */
 #if STATFS_IN_SYS_STATVFS
 /*@-incondefs@*/
-# include <sys/statvfs.h>
 #if defined(__LCLINT__)
 /*@-declundef -exportheader -protoparammatch @*/ /* LCL: missing annotation */
 extern int statvfs (const char * file, /*@out@*/ struct statvfs * buf)
@@ -33,6 +32,8 @@ extern int statvfs (const char * file, /*@out@*/ struct statvfs * buf)
 	/*@modifies *buf, fileSystem @*/;
 /*@=declundef =exportheader =protoparammatch @*/
 /*@=incondefs@*/
+#else
+# include <sys/statvfs.h>
 #endif
 #else
 # if STATFS_IN_SYS_VFS
diff --git a/lib/rpmts.h b/lib/rpmts.h
index 2467dc938..b557bb18a 100644
--- a/lib/rpmts.h
+++ b/lib/rpmts.h
@@ -263,8 +263,8 @@ int rpmtsOpenDB(rpmts ts, int dbmode)
 /*@only@*/ /*@null@*/
 rpmdbMatchIterator rpmtsInitIterator(const rpmts ts, int rpmtag,
 			/*@null@*/ const void * keyp, size_t keylen)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fileSystem, internalState @*/;
 
 /**
  * Attempt to solve a needed dependency.
diff --git a/lib/signature.c b/lib/signature.c
index ce20cd293..e2daeb2d4 100644
--- a/lib/signature.c
+++ b/lib/signature.c
@@ -272,8 +272,10 @@ Header rpmFreeSignature(Header h)
  */
 static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
 		/*@out@*/ int_32 * pktlen, /*@null@*/ const char * passPhrase)
-	/*@globals errno, rpmGlobalMacroContext, fileSystem @*/
-	/*@modifies errno, *pkt, *pktlen, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals errno, rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies errno, *pkt, *pktlen, rpmGlobalMacroContext,
+		fileSystem, internalState @*/
 {
     char * sigfile = alloca(1024);
     int pid, status;
@@ -291,7 +293,9 @@ static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
     addMacro(NULL, "__signature_filename", NULL, sigfile, -1);
 
     inpipe[0] = inpipe[1] = 0;
+/*@-boundsread@*/
     (void) pipe(inpipe);
+/*@=boundsread@*/
 
     if (!(pid = fork())) {
 	const char *pgp_path = rpmExpand("%{?_pgp_path}", NULL);
@@ -402,8 +406,10 @@ static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
  */
 static int makeGPGSignature(const char * file, /*@out@*/ byte ** pkt,
 		/*@out@*/ int_32 * pktlen, /*@null@*/ const char * passPhrase)
-	/*@globals rpmGlobalMacroContext, fileSystem @*/
-	/*@modifies *pkt, *pktlen, rpmGlobalMacroContext, fileSystem @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies *pkt, *pktlen, rpmGlobalMacroContext,
+		fileSystem, internalState @*/
 {
     char * sigfile = alloca(1024);
     int pid, status;
@@ -422,7 +428,9 @@ static int makeGPGSignature(const char * file, /*@out@*/ byte ** pkt,
     addMacro(NULL, "__signature_filename", NULL, sigfile, -1);
 
     inpipe[0] = inpipe[1] = 0;
+/*@-boundsread@*/
     (void) pipe(inpipe);
+/*@=boundsread@*/
 
     if (!(pid = fork())) {
 	const char *gpg_path = rpmExpand("%{?_gpg_path}", NULL);
@@ -682,7 +690,9 @@ static int checkPassPhrase(const char * passPhrase, const int sigTag)
     int xx;
 
     passPhrasePipe[0] = passPhrasePipe[1] = 0;
+/*@-boundsread@*/
     xx = pipe(passPhrasePipe);
+/*@=boundsread@*/
     if (!(pid = fork())) {
 	const char * cmd;
 	char *const *av;
@@ -824,7 +834,9 @@ char * rpmGetPassPhrase(const char * prompt, const int sigTag)
 	/*@notreached@*/ break;
     }
 
+/*@-moduncon -nullpass @*/
     pass = /*@-unrecog@*/ getpass( (prompt ? prompt : "") ) /*@=unrecog@*/ ;
+/*@=moduncon -nullpass @*/
 
     if (checkPassPhrase(pass, sigTag))
 	return NULL;
diff --git a/lib/signature.h b/lib/signature.h
index 8b78cadb0..6a99d6cb9 100644
--- a/lib/signature.h
+++ b/lib/signature.h
@@ -105,7 +105,8 @@ int rpmLookupSignatureType(int action)
  * @param sigTag	signature type/tag
  * @return		pass phrase
  */
-/*@null@*/ char * rpmGetPassPhrase(/*@null@*/ const char * prompt,
+/*@dependent@*/ /*@null@*/
+char * rpmGetPassPhrase(/*@null@*/ const char * prompt,
 		const int sigTag)
 	/*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
 	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/;
diff --git a/lib/transaction.c b/lib/transaction.c
index 6ae79dead..a5684dda4 100644
--- a/lib/transaction.c
+++ b/lib/transaction.c
@@ -85,8 +85,8 @@ static int sharedCmp(const void * one, const void * two)
 /*@-boundsread@*/
 static fileAction decideFileFate(const rpmts ts,
 		const rpmfi ofi, rpmfi nfi)
-	/*@globals fileSystem @*/
-	/*@modifies nfi, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies nfi, fileSystem, internalState @*/
 {
     const char * fn = rpmfiFN(nfi);
     int newFlags = rpmfiFFlags(nfi);
@@ -222,8 +222,8 @@ static int handleInstInstalledFiles(const rpmts ts,
 		rpmte p, rpmfi fi,
 		sharedFileInfo shared,
 		int sharedCount, int reportConflicts)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fi, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fi, fileSystem, internalState @*/
 {
     const char * altNEVR = NULL;
     rpmfi otherFi = NULL;
@@ -311,8 +311,8 @@ static int handleInstInstalledFiles(const rpmts ts,
 /* XXX only ts->rpmdb modified */
 static int handleRmvdInstalledFiles(const rpmts ts, rpmfi fi,
 		sharedFileInfo shared, int sharedCount)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fi, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fi, fileSystem, internalState @*/
 {
     HGE_t hge = fi->hge;
     Header h;
@@ -502,8 +502,8 @@ bingoFps->baseName);
 /* XXX only ts->{probs,di} modified */
 static void handleOverlappedFiles(const rpmts ts,
 		const rpmte p, rpmfi fi)
-	/*@globals fileSystem @*/
-	/*@modifies ts, fi, fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies ts, fi, fileSystem, internalState @*/
 {
     uint_32 fixupSize = 0;
     rpmps ps;
diff --git a/popt/popt.c b/popt/popt.c
index d2dffa715..d4b2dc2f3 100644
--- a/popt/popt.c
+++ b/popt/popt.c
@@ -355,7 +355,8 @@ static int handleAlias(/*@special@*/ poptContext con,
 
 /*@-bounds -boundswrite @*/
 static int execCommand(poptContext con)
-    /*@*/
+	/*@globals internalState @*/
+	/*@modifies internalState @*/
 {
     poptItem item = con->doExec;
     const char ** argv;
diff --git a/popt/popt.h b/popt/popt.h
index c756061dc..fad30bc82 100644
--- a/popt/popt.h
+++ b/popt/popt.h
@@ -241,8 +241,8 @@ void poptResetContext(/*@null@*/poptContext con)
  * @return		next option val, -1 on last item, POPT_ERROR_* on error
  */
 int poptGetNextOpt(/*@null@*/poptContext con)
-	/*@globals fileSystem@*/
-	/*@modifies con, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies con, fileSystem, internalState @*/;
 
 /*@-redecl@*/
 /** \ingroup popt
@@ -334,9 +334,9 @@ int poptAddItem(poptContext con, poptItem newItem, int flags)
  * @return		0 on success, POPT_ERROR_ERRNO on failure
  */
 int poptReadConfigFile(poptContext con, const char * fn)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem,
-		con->execs, con->numExecs @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies con->execs, con->numExecs,
+		fileSystem, internalState @*/;
 
 /** \ingroup popt
  * Read default configuration from /etc/popt and $HOME/.popt.
@@ -345,9 +345,9 @@ int poptReadConfigFile(poptContext con, const char * fn)
  * @return		0 on success, POPT_ERROR_ERRNO on failure
  */
 int poptReadDefaultConfig(poptContext con, /*@unused@*/ int useEnv)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem,
-		con->execs, con->numExecs @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies con->execs, con->numExecs,
+		fileSystem, internalState @*/;
 
 /** \ingroup popt
  * Duplicate an argument array.
diff --git a/popt/test1.c b/popt/test1.c
index 8d84144df..a41ee09a0 100644
--- a/popt/test1.c
+++ b/popt/test1.c
@@ -175,8 +175,8 @@ static void resetVars(void)
 }
 
 int main(int argc, const char ** argv)
-	/*@globals pass2, fileSystem @*/
-	/*@modifies pass2, fileSystem @*/
+	/*@globals pass2, fileSystem, internalState @*/
+	/*@modifies pass2, fileSystem, internalState @*/
 {
     int rc;
     int ec = 0;
diff --git a/rpmdb/fprint.c b/rpmdb/fprint.c
index 250898dc4..2244a91e5 100644
--- a/rpmdb/fprint.c
+++ b/rpmdb/fprint.c
@@ -42,7 +42,9 @@ static /*@null@*/ const struct fprintCacheEntry_s * cacheContainsDirectory(
 
     if (htGetEntry(cache->ht, dirName, &data, NULL, NULL))
 	return NULL;
+/*@-boundsread@*/
     return data[0];
+/*@=boundsread@*/
 }
 
 /**
diff --git a/rpmdb/header.c b/rpmdb/header.c
index 35a9021f7..bd4428710 100644
--- a/rpmdb/header.c
+++ b/rpmdb/header.c
@@ -1669,6 +1669,7 @@ int headerGetEntry(Header h, int_32 tag,
 			/*@null@*/ /*@out@*/ void ** p,
 			/*@null@*/ /*@out@*/ hCNT_t c)
 	/*@modifies *type, *p, *c @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     return intGetEntry(h, tag, type, (hPTR_t *)p, c, 0);
 }
@@ -1691,6 +1692,7 @@ int headerGetEntryMinMemory(Header h, int_32 tag,
 			/*@null@*/ /*@out@*/ hPTR_t * p,
 			/*@null@*/ /*@out@*/ hCNT_t c)
 	/*@modifies *type, *p, *c @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     return intGetEntry(h, tag, type, p, c, 1);
 }
@@ -2678,11 +2680,13 @@ static char * formatValue(sprintfTag tag, Header h,
 	}
 /*@=boundswrite@*/
     } else {
+/*@-boundswrite@*/
 	if (!headerGetEntry(h, tag->tag, &type, (void **)&data, &count)) {
 	    count = 1;
 	    type = RPM_STRING_TYPE;	
 	    data = "(none)";
 	}
+/*@=boundswrite@*/
 
 	datafree = 1;
     }
@@ -2952,9 +2956,11 @@ static char * singleSprintf(Header h, sprintfToken token,
 		     continue;
 /*@=boundswrite@*/
 	    } else {
+/*@-boundswrite@*/
 		if (!headerGetEntry(h, token->u.array.format[i].u.tag.tag, 
 				    &type, NULL, &numElements))
 		    continue;
+/*@=boundswrite@*/
 	    } 
 	    /*@loopbreak@*/ break;
 	}
@@ -3297,9 +3303,11 @@ void headerCopyTags(Header headerFrom, Header headerTo, hTAG_t tagstocopy)
 	int_32 count;
 	if (headerIsEntry(headerTo, *p))
 	    continue;
+/*@-boundswrite@*/
 	if (!headerGetEntryMinMemory(headerFrom, *p, &type,
 				(hPTR_t *) &s, &count))
 	    continue;
+/*@=boundswrite@*/
 	(void) headerAddEntry(headerTo, *p, type, s, count);
 	s = headerFreeData(s, type);
     }
diff --git a/rpmdb/legacy.c b/rpmdb/legacy.c
index 64033c0e4..2c1fd3f61 100644
--- a/rpmdb/legacy.c
+++ b/rpmdb/legacy.c
@@ -244,6 +244,7 @@ exit:
 int _noDirTokens = 0;
 /*@=exportheadervar@*/
 
+/*@-boundsread@*/
 static int dncmp(const void * a, const void * b)
 	/*@*/
 {
@@ -251,6 +252,7 @@ static int dncmp(const void * a, const void * b)
     const char *const * second = b;
     return strcmp(*first, *second);
 }
+/*@=boundsread@*/
 
 /*@-bounds@*/
 void compressFilelist(Header h)
diff --git a/rpmdb/legacy.h b/rpmdb/legacy.h
index 69ade41cf..d9b933187 100644
--- a/rpmdb/legacy.h
+++ b/rpmdb/legacy.h
@@ -27,8 +27,8 @@ extern "C" {
  */
 int domd5(const char * fn, /*@out@*/ unsigned char * digest, int asAscii,
 		/*@null@*/ /*@out@*/ size_t *fsizep)
-	/*@globals fileSystem @*/
-	/*@modifies digest, *fsizep, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies digest, *fsizep, fileSystem, internalState @*/;
 
 /**
  * Convert absolute path tag to (dirname,basename,dirindex) tags.
diff --git a/rpmdb/rpmdb.c b/rpmdb/rpmdb.c
index e37a4da82..6175d0cd6 100644
--- a/rpmdb/rpmdb.c
+++ b/rpmdb/rpmdb.c
@@ -3020,8 +3020,8 @@ if (key->size == 0) key->size++;	/* XXX "/" fixup. */
  * @return		1 if file exists, 0 if not
  */
 static int rpmioFileExists(const char * urlfn)
-        /*@globals fileSystem @*/
-        /*@modifies fileSystem @*/
+        /*@globals fileSystem, internalState @*/
+        /*@modifies fileSystem, internalState @*/
 {
     const char *fn;
     int urltype = urlPath(urlfn, &fn);
@@ -3054,8 +3054,8 @@ static int rpmioFileExists(const char * urlfn)
 
 static int rpmdbRemoveDatabase(const char * prefix,
 		const char * dbpath, int _dbapi)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 { 
     int i;
     char * filename;
@@ -3109,8 +3109,8 @@ static int rpmdbRemoveDatabase(const char * prefix,
 static int rpmdbMoveDatabase(const char * prefix,
 		const char * olddbpath, int _olddbapi,
 		const char * newdbpath, int _newdbapi)
-	/*@globals fileSystem @*/
-	/*@modifies fileSystem @*/
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
 {
     int i;
     char * ofilename, * nfilename;
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) {