Explicit branchstate annotations.

CVS patchset: 5113
CVS date: 2001/10/15 17:53:34

30 files changed, 287 insertions, 91 deletions

diff --git a/lib/Makefile.am b/lib/Makefile.am
index ff8fc39b9..183806bbe 100644
--- a/lib/Makefile.am
+++ b/lib/Makefile.am
@@ -68,14 +68,14 @@ getdate.c: getdate.y
 	 { echo "/*@-globstate -statictrans -unqualifiedtrans -noparams @*/";\
 	   echo "/*@-retvalint -usedef -varuse -nullderef -nullassign @*/";\
 	   echo "/*@-readonlytrans -modunconnomods -compdef @*/";\
-	   echo "/*@-globs -evalorderuncon @*/";\
+	   echo "/*@-globs -evalorderuncon -modobserveruncon -modnomods @*/";\
 	   sed	-e 's,y.tab.c,getdate.c,' y.tab.c \
 		-e 's,^YYSTYPE ,static &,' \
 		-e 's,^short ,static &,' \
 		-e 's,^const short ,static &,' \
 		-e 's,^int yydebug,/*@unused@*/ static &,' \
 		-e 's,^int ,static &,' ;\
-	   echo "/*@=globs =evalorderuncon @*/";\
+	   echo "/*@=globs =evalorderuncon =modobserveruncon =modnomods @*/";\
 	   echo "/*@=readonlytrans =modunconnomods =compdef @*/";\
 	   echo "/*@=retvalint =usedef =varuse =nullderef =nullassign @*/";\
 	   echo "/*@=globstate =statictrans =unqualifiedtrans =noparams @*/";\
diff --git a/lib/cpio.c b/lib/cpio.c
index b7a022cfc..8c5c2f1a0 100644
--- a/lib/cpio.c
+++ b/lib/cpio.c
@@ -181,6 +181,7 @@ const char *const cpioStrerror(int rc)
     int l, myerrno = errno;
 
     strcpy(msg, "cpio: ");
+    /*@-branchstate@*/
     switch (rc) {
     default:
 	s = msg + strlen(msg);
@@ -216,17 +217,20 @@ const char *const cpioStrerror(int rc)
     case CPIOERR_INTERNAL:	s = _("Internal error");	break;
     case CPIOERR_UNMAPPED_FILE:	s = _("Archive file not in header"); break;
     }
+    /*@=branchstate@*/
 
     l = sizeof(msg) - strlen(msg) - 1;
     if (s != NULL) {
 	if (l > 0) strncat(msg, s, l);
 	l -= strlen(s);
     }
+    /*@-branchstate@*/
     if ((rc & CPIOERR_CHECK_ERRNO) && myerrno) {
 	s = _(" failed - ");
 	if (l > 0) strncat(msg, s, l);
 	l -= strlen(s);
 	if (l > 0) strncat(msg, strerror(myerrno), l);
     }
+    /*@=branchstate@*/
     return msg;
 }
diff --git a/lib/depends.c b/lib/depends.c
index a69f56665..48d7f0b0c 100644
--- a/lib/depends.c
+++ b/lib/depends.c
@@ -505,7 +505,9 @@ static void parseEVR(char * evr,
 	epoch = evr;
 	*s++ = '\0';
 	version = s;
+	/*@-branchstate@*/
 	if (*epoch == '\0') epoch = "0";
+	/*@=branchstate@*/
     } else {
 	epoch = NULL;	/* XXX disable epoch compare if missing */
 	version = evr;
@@ -688,19 +690,21 @@ int headerMatchesDepFlags(Header h,
     return rpmRangesOverlap(name, pkgEVR, pkgFlags, reqName, reqEVR, reqFlags);
 }
 
-rpmTransactionSet rpmtransCreateSet(rpmdb rpmdb, const char * rootDir)
+rpmTransactionSet rpmtransCreateSet(rpmdb db, const char * rootDir)
 {
     rpmTransactionSet ts;
     int rootLen;
 
+    /*@-branchstate@*/
     if (!rootDir) rootDir = "";
+    /*@=branchstate@*/
 
     ts = xcalloc(1, sizeof(*ts));
     ts->filesystemCount = 0;
     ts->filesystems = NULL;
     ts->di = NULL;
     /*@-assignexpose@*/
-    ts->rpmdb = rpmdb;
+    ts->rpmdb = db;
     /*@=assignexpose@*/
     ts->scriptFd = NULL;
     ts->id = 0;
@@ -823,8 +827,10 @@ int rpmtransAddPackage(rpmTransactionSet ts, Header h, FD_t fd,
     		ts->addedPackages.list;
     ts->order[ts->orderCount++].u.addedIndex = alNum;
 
+    /*@-branchstate@*/
     if (!upgrade || ts->rpmdb == NULL)
 	return 0;
+    /*@=branchstate@*/
 
     /* XXX binary rpms always have RPMTAG_SOURCERPM, source rpms do not */
     if (headerIsEntry(h, RPMTAG_SOURCEPACKAGE))
@@ -837,6 +843,7 @@ int rpmtransAddPackage(rpmTransactionSet ts, Header h, FD_t fd,
 
 	mi = rpmdbInitIterator(ts->rpmdb, RPMTAG_NAME, name, 0);
 	while((h2 = rpmdbNextIterator(mi)) != NULL) {
+	    /*@-branchstate@*/
 	    if (rpmVersionCompare(h, h2))
 		(void) removePackage(ts, rpmdbGetIteratorOffset(mi), alNum);
 	    else {
@@ -851,6 +858,7 @@ int rpmtransAddPackage(rpmTransactionSet ts, Header h, FD_t fd,
 		    ts->addedPackages.list[alNum].multiLib = multiLibMask;
 		}
 	    }
+	    /*@=branchstate@*/
 	}
 	mi = rpmdbFreeIterator(mi);
     }
@@ -884,12 +892,14 @@ int rpmtransAddPackage(rpmTransactionSet ts, Header h, FD_t fd,
 		 * Rpm prior to 3.0.3 does not have versioned obsoletes.
 		 * If no obsoletes version info is available, match all names.
 		 */
+		/*@-branchstate@*/
 		if (obsoletesEVR == NULL ||
 		    headerMatchesDepFlags(h2,
 			obsoletes[j], obsoletesEVR[j], obsoletesFlags[j]))
 		{
 		    (void) removePackage(ts, rpmdbGetIteratorOffset(mi), alNum);
 		}
+		/*@=branchstate@*/
 	    }
 	    mi = rpmdbFreeIterator(mi);
 	  }
@@ -1133,11 +1143,13 @@ alAllSatisfiesDepend(const availableList al,
 	    /*@switchbreak@*/ break;
 	}
 
+	/*@-branchstate@*/
 	if (rc) {
 	    ret = xrealloc(ret, (found + 2) * sizeof(*ret));
 	    if (ret)	/* can't happen */
 		ret[found++] = p;
 	}
+	/*@=branchstate@*/
     }
 
     if (ret)
@@ -1677,6 +1689,7 @@ static int ignoreDep(const struct availablePackage * p,
  */
 static void markLoop(/*@special@*/ struct tsortInfo * tsi,
 		struct availablePackage * q)
+	/*@globals internalState @*/
 	/*@uses tsi @*/
 	/*@modifies internalState @*/
 {
@@ -1755,6 +1768,7 @@ zapRelation(struct availablePackage * q, struct availablePackage * p,
 	/*
 	 * Attempt to unravel a dependency loop by eliminating Requires's.
 	 */
+	/*@-branchstate@*/
 	if (zap && !(p->requireFlags[j] & RPMSENSE_PREREQ)) {
 	    rpmMessage(RPMMESS_DEBUG,
 			_("removing %s-%s-%s \"%s\" from tsort relations.\n"),
@@ -1769,6 +1783,7 @@ zapRelation(struct availablePackage * q, struct availablePackage * p,
 	    if (zap)
 		zap--;
 	}
+	/*@=branchstate@*/
 	/* XXX Note: the loop traverses "not found", get out now! */
 	break;
     }
@@ -2047,6 +2062,7 @@ rescan:
 
 	/* T11. Print all dependency loops. */
 	if ((r = ts->addedPackages.list) != NULL)
+	/*@-branchstate@*/
 	for (i = 0; i < npkgs; i++, r++) {
 	    int printed;
 
@@ -2093,6 +2109,7 @@ rescan:
 		p->tsi.tsi_reqx = 0;
 	    }
 	}
+	/*@=branchstate@*/
 
 	/* If a relation was eliminated, then continue sorting. */
 	/* XXX TODO: add control bit. */
@@ -2251,6 +2268,7 @@ int rpmdepCheck(rpmTransactionSet ts,
     /*
      * Look at the removed packages and make sure they aren't critical.
      */
+    /*@-branchstate@*/
     if (ts->numRemovedPackages > 0) {
       mi = rpmdbInitIterator(ts->rpmdb, RPMDBI_PACKAGES, NULL, 0);
       (void) rpmdbAppendIterator(mi,
@@ -2330,6 +2348,7 @@ int rpmdepCheck(rpmTransactionSet ts,
       }
       mi = rpmdbFreeIterator(mi);
     }
+    /*@=branchstate@*/
 
     if (ps->num) {
 	*conflicts = ps->problems;
@@ -2342,7 +2361,9 @@ exit:
     mi = rpmdbFreeIterator(mi);
     ps->problems = _free(ps->problems);
     ps = _free(ps);
+    /*@-branchstate@*/
     if (_cacheDependsRC)
 	(void) rpmdbCloseDBI(ts->rpmdb, RPMDBI_DEPENDS);
+    /*@=branchstate@*/
     return rc;
 }
diff --git a/lib/fs.c b/lib/fs.c
index ea176530d..8f1737888 100644
--- a/lib/fs.c
+++ b/lib/fs.c
@@ -337,10 +337,12 @@ int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes, int numFiles
 
     sourceDir = _free(sourceDir);
 
+    /*@-branchstate@*/
     if (usagesPtr)
 	*usagesPtr = usages;
     else
 	usages = _free(usages);
+    /*@=branchstate@*/
 
     return 0;
 }
diff --git a/lib/fsm.c b/lib/fsm.c
index 50eab6526..0bfcd6754 100644
--- a/lib/fsm.c
+++ b/lib/fsm.c
@@ -357,12 +357,15 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
     int j;
 
     /* Find hard link set. */
+    /*@-branchstate@*/
     for (fsm->li = fsm->links; fsm->li; fsm->li = fsm->li->next) {
 	if (fsm->li->sb.st_ino == st->st_ino && fsm->li->sb.st_dev == st->st_dev)
 	    break;
     }
+    /*@=branchstate@*/
 
     /* New hard link encountered, add new link to set. */
+    /*@-branchstate@*/
     if (fsm->li == NULL) {
 	fsm->li = xcalloc(1, sizeof(*fsm->li));
 	fsm->li->next = NULL;
@@ -385,6 +388,7 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
 	/*@=kepttrans@*/
 	fsm->links = fsm->li;
     }
+    /*@=branchstate@*/
 
     if (fsm->goal == FSM_PKGBUILD) --fsm->li->linksLeft;
     fsm->li->filex[fsm->li->linksLeft] = fsm->ix;
@@ -451,11 +455,13 @@ FSM_t freeFSM(FSM_t fsm)
 {
     if (fsm) {
 	fsm->path = _free(fsm->path);
+	/*@-branchstate@*/
 	while ((fsm->li = fsm->links) != NULL) {
 	    fsm->links = fsm->li->next;
 	    fsm->li->next = NULL;
 	    fsm->li = freeHardLink(fsm->li);
 	}
+	/*@=branchstate@*/
 	fsm->dnlx = _free(fsm->dnlx);
 	fsm->ldn = _free(fsm->ldn);
 	fsm->iter = mapFreeIterator(fsm->iter);
@@ -673,6 +679,7 @@ int fsmMapAttrs(FSM_t fsm)
  */
 static int expandRegular(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->sb @*/
+	/*@globals fileSystem@*/
 	/*@modifies fsm, fileSystem @*/
 {
     const char * fmd5sum;
@@ -736,6 +743,7 @@ 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 @*/
 {
     const char * path = fsm->path;
@@ -749,6 +757,7 @@ static int writeFile(/*@special@*/ FSM_t fsm, int writeData)
 
     st->st_size = (writeData ? ost->st_size : 0);
 
+    /*@-branchstate@*/
     if (S_ISDIR(st->st_mode)) {
 	st->st_size = 0;
     } else if (S_ISLNK(st->st_mode)) {
@@ -762,6 +771,7 @@ static int writeFile(/*@special@*/ FSM_t fsm, int writeData)
 	st->st_size = fsm->rdnb;
 	symbuf = alloca_strdup(fsm->rdbuf);	/* XXX save readlink return. */
     }
+    /*@=branchstate@*/
 
     if (fsm->mapFlags & CPIO_MAP_ABSOLUTE) {
 	int nb = strlen(fsm->dirName) + strlen(fsm->baseName) + sizeof(".");
@@ -871,6 +881,7 @@ exit:
  */
 static int writeLinkedFile(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->nsuffix, fsm->ix, fsm->li, fsm->failedFile @*/
+	/*@globals fileSystem@*/
 	/*@modifies fsm, fileSystem @*/
 {
     const char * path = fsm->path;
@@ -915,6 +926,7 @@ static int writeLinkedFile(/*@special@*/ FSM_t fsm)
  */
 static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->opath, fsm->nsuffix, fsm->ix, fsm->li @*/
+	/*@globals fileSystem@*/
 	/*@modifies fsm, fileSystem @*/
 {
     const char * path = fsm->path;
@@ -934,6 +946,7 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
     rc = fsmStage(fsm, FSM_MAP);
     fsm->opath = fsm->path;
     fsm->path = NULL;
+    /*@-branchstate@*/
     for (i = 0; i < fsm->li->nlink; i++) {
 	if (fsm->li->filex[i] < 0) continue;
 	if (i == fsm->li->createdPath) continue;
@@ -954,6 +967,7 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 
 	fsm->li->linksLeft--;
     }
+    /*@=branchstate@*/
     fsm->path = _free(fsm->path);
     fsm->opath = _free(fsm->opath);
 
@@ -972,6 +986,7 @@ 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 @*/
 {
     const char * path = fsm->path;
@@ -985,10 +1000,12 @@ static int fsmCommitLinks(/*@special@*/ FSM_t fsm)
     fsm->nsuffix = NULL;
     fsm->ix = -1;
 
+    /*@-branchstate@*/
     for (fsm->li = fsm->links; fsm->li; fsm->li = fsm->li->next) {
 	if (fsm->li->sb.st_ino == st->st_ino && fsm->li->sb.st_dev == st->st_dev)
 	    break;
     }
+    /*@=branchstate@*/
 
     for (i = 0; i < fsm->li->nlink; i++) {
 	if (fsm->li->filex[i] < 0) continue;
@@ -1012,6 +1029,7 @@ 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 @*/
 {
     const char * path = fsm->path;
@@ -1066,6 +1084,7 @@ 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 @*/
 {
     struct stat * st = &fsm->sb;
@@ -1237,6 +1256,7 @@ int fsmStage(FSM_t fsm, fileStage stage)
     }
 #undef	_fafilter
 
+    /*@-branchstate@*/
     switch (stage) {
     case FSM_UNKNOWN:
 	break;
@@ -2103,6 +2123,7 @@ if (!(fsm->mapFlags & CPIO_ALL_HARDLINKS)) break;
     default:
 	break;
     }
+    /*@=branchstate@*/
 
     if (!(stage & FSM_INTERNAL)) {
 	fsm->rc = (rc == CPIOERR_HDR_TRAILER ? 0 : rc);
diff --git a/lib/fsm.h b/lib/fsm.h
index 4bcceacb1..e53388f86 100644
--- a/lib/fsm.h
+++ b/lib/fsm.h
@@ -212,6 +212,7 @@ int fsmSetup(FSM_t fsm, fileStage goal,
 		FD_t cfd,
 		/*@out@*/ unsigned int * archiveSize,
 		/*@out@*/ const char ** failedFile)
+	/*@globals fileSystem @*/
 	/*@modifies fsm, *archiveSize, *failedFile, fileSystem  @*/;
 
 /**
@@ -262,6 +263,7 @@ int fsmMapAttrs(FSM_t fsm)
  * @return		0 on success
  */
 int fsmStage(/*@partial@*/ FSM_t fsm, fileStage stage)
+	/*@globals fileSystem @*/
 	/*@modifies fsm, fileSystem @*/;
 
 #ifdef __cplusplus
diff --git a/lib/getdate.c b/lib/getdate.c
index 15ee04193..e0fe26343 100644
--- a/lib/getdate.c
+++ b/lib/getdate.c
@@ -1,7 +1,7 @@
 /*@-globstate -statictrans -unqualifiedtrans -noparams @*/
 /*@-retvalint -usedef -varuse -nullderef -nullassign @*/
 /*@-readonlytrans -modunconnomods -compdef @*/
-/*@-globs -evalorderuncon @*/
+/*@-globs -evalorderuncon -modobserveruncon -modnomods @*/
 #ifndef lint
 static char const 
 yyrcsid[] = "$FreeBSD: src/usr.bin/yacc/skeleton.c,v 1.28 2000/01/17 02:04:06 bde Exp $";
@@ -1594,7 +1594,7 @@ yyabort:
 yyaccept:
     return (0);
 }
-/*@=globs =evalorderuncon @*/
+/*@=globs =evalorderuncon =modobserveruncon =modnomods @*/
 /*@=readonlytrans =modunconnomods =compdef @*/
 /*@=retvalint =usedef =varuse =nullderef =nullassign @*/
 /*@=globstate =statictrans =unqualifiedtrans =noparams @*/
diff --git a/lib/hdrinline.h b/lib/hdrinline.h
index 3a9c58061..883fe04ec 100644
--- a/lib/hdrinline.h
+++ b/lib/hdrinline.h
@@ -178,7 +178,7 @@ unsigned int headerSizeof(/*@null@*/ Header h, enum hMagic magicp)
  */
 /*@unused@*/ static inline
 /*@null@*/ Header headerRead(FD_t fd, enum hMagic magicp)
-	/*@modifies fd, fileSystem @*/
+	/*@modifies fd @*/
 {
     return hdrVec->hdrread(fd, magicp);
 }
@@ -192,7 +192,7 @@ unsigned int headerSizeof(/*@null@*/ Header h, enum hMagic magicp)
  */
 /*@unused@*/ static inline
 int headerWrite(FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
-	/*@modifies fd, h, fileSystem @*/
+	/*@modifies fd, h @*/
 {
     /*@-abstract@*/
     if (h == NULL) return 0;
@@ -406,19 +406,19 @@ int headerRemoveEntry(Header h, int_32 tag)
  *
  * @param h		header
  * @param fmt		format to use
- * @param tags		array of tag name/value pairs
+ * @param tbltags	array of tag name/value pairs
  * @param extensions	chained table of formatting extensions.
  * @retval errmsg	error message (if any)
  * @return		formatted output string (malloc'ed)
  */
 /*@unused@*/ static inline
 /*@only@*/ char * headerSprintf(Header h, const char * fmt,
-		     const struct headerTagTableEntry_s * tags,
+		     const struct headerTagTableEntry_s * tbltags,
 		     const struct headerSprintfExtension_s * extensions,
 		     /*@null@*/ /*@out@*/ errmsg_t * errmsg)
 	/*@modifies *errmsg @*/
 {
-    return (h2hv(h)->hdrsprintf) (h, fmt, tags, extensions, errmsg);
+    return (h2hv(h)->hdrsprintf) (h, fmt, tbltags, extensions, errmsg);
 }
 
 /** \ingroup header
diff --git a/lib/hdrproto.h b/lib/hdrproto.h
index 8adf4422d..ed0844de9 100644
--- a/lib/hdrproto.h
+++ b/lib/hdrproto.h
@@ -100,6 +100,7 @@ unsigned int headerSizeof(/*@null@*/ Header h, enum hMagic magicp)
  * @return		0 on success, 1 on error
  */
 int headerWrite(FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
+	/*@globals fileSystem @*/
 	/*@modifies fd, h, fileSystem @*/;
 
 /** \ingroup header
@@ -117,7 +118,7 @@ int headerWrite(FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
  * @return		header (or NULL on error)
  */
 /*@null@*/ Header headerRead(FD_t fd, enum hMagic magicp)
-	/*@modifies fd, fileSystem @*/;
+	/*@modifies fd @*/;
 
 /** \ingroup header
  * Check if tag is in header.
@@ -271,13 +272,13 @@ int headerRemoveEntry(Header h, int_32 tag)
  *
  * @param h		header
  * @param fmt		format to use
- * @param tags		array of tag name/value pairs
+ * @param tbltags	array of tag name/value pairs
  * @param extensions	chained table of formatting extensions.
  * @retval errmsg	error message (if any)
  * @return		formatted output string (malloc'ed)
  */
 /*@only@*/ char * headerSprintf(Header h, const char * fmt,
-		     const struct headerTagTableEntry_s * tags,
+		     const struct headerTagTableEntry_s * tbltags,
 		     const struct headerSprintfExtension_s * extensions,
 		     /*@null@*/ /*@out@*/ errmsg_t * errmsg)
 	/*@modifies *errmsg @*/;
diff --git a/lib/header.c b/lib/header.c
index 228405402..6cf2f48c8 100644
--- a/lib/header.c
+++ b/lib/header.c
@@ -740,6 +740,7 @@ Header headerCopy(Header h)
     int_32 tag, type, count;
     hPTR_t ptr;
    
+    /*@-branchstate@*/
     for (hi = headerInitIterator(h);
 	headerNextIterator(hi, &tag, &type, &ptr, &count);
 	ptr = headerFreeData((void *)ptr, type))
@@ -747,6 +748,7 @@ Header headerCopy(Header h)
 	if (ptr) (void) headerAddEntry(nh, tag, type, ptr, count);
     }
     hi = headerFreeIterator(hi);
+    /*@=branchstate@*/
 
     return headerReload(nh, HEADER_IMAGE);
 }
@@ -930,13 +932,17 @@ Header headerCopyLoad(const void * uh)
     Header h = NULL;
 
     /* Sanity checks on header intro. */
+    /*@-branchstate@*/
     if (!(hdrchkTags(il) || hdrchkData(dl)) && pvlen < headerMaxbytes) {
 	nuh = memcpy(xmalloc(pvlen), uh, pvlen);
 	if ((h = headerLoad(nuh)) != NULL)
 	    h->flags |= HEADERFLAG_ALLOCATED;
     }
+    /*@=branchstate@*/
+    /*@-branchstate@*/
     if (h == NULL)
 	nuh = _free(nuh);
+    /*@=branchstate@*/
     return h;
 }
 
@@ -1587,7 +1593,9 @@ int headerAddI18NString(Header h, int_32 tag, const char * string, const char *
 
     if (!table)
 	return 0;
+    /*@-branchstate@*/
     if (!lang) lang = "C";
+    /*@=branchstate@*/
 
     {	const char * l = table->data;
 	for (langNum = 0; langNum < table->info.count; langNum++) {
@@ -1701,10 +1709,12 @@ int headerModifyEntry(Header h, int_32 tag, int_32 type, hPTR_t p, int_32 c)
     entry->info.type = type;
     entry->data = grabData(type, p, c, &entry->length);
 
+    /*@-branchstate@*/
     if (ENTRY_IN_REGION(entry)) {
 	entry->info.offset = 0;
     } else
 	oldData = _free(oldData);
+    /*@=branchstate@*/
 
     return 1;
 }
@@ -2278,6 +2288,7 @@ static char * formatValue(sprintfTag tag, Header h,
     headerSprintfExtension ext;
 
     memset(buf, 0, sizeof(buf));
+    /*@-branchstate@*/
     if (tag->ext) {
 	if (getExtension(h, tag->ext, &type, &data, &count, 
 			 extCache + tag->extNum))
@@ -2295,6 +2306,7 @@ static char * formatValue(sprintfTag tag, Header h,
 
 	mayfree = 1;
     }
+    /*@=branchstate@*/
 
     if (tag->arrayCount) {
 	/*@-observertrans -modobserver@*/
@@ -2326,6 +2338,7 @@ static char * formatValue(sprintfTag tag, Header h,
 	}
     }
     
+    /*@-branchstate@*/
     switch (type) {
     case RPM_STRING_ARRAY_TYPE:
 	strarray = (const char **)data;
@@ -2399,6 +2412,7 @@ static char * formatValue(sprintfTag tag, Header h,
 	val = xstrdup(_("(unknown type)"));
 	break;
     }
+    /*@=branchstate@*/
 
     return val;
 }
@@ -2566,13 +2580,13 @@ freeExtensionCache(const headerSprintfExtension extensions,
 }
 
 char * headerSprintf(Header h, const char * fmt, 
-		const struct headerTagTableEntry_s * tabletags,
+		const struct headerTagTableEntry_s * tbltags,
 		const struct headerSprintfExtension_s * extensions,
 		errmsg_t * errmsg)
 {
     /*@-castexpose@*/	/* FIX: legacy API shouldn't change. */
     headerSprintfExtension exts = (headerSprintfExtension) extensions;
-    headerTagTableEntry tags = (headerTagTableEntry) tabletags;
+    headerTagTableEntry tags = (headerTagTableEntry) tbltags;
     /*@=castexpose@*/
     char * fmtString;
     sprintfToken format;
diff --git a/lib/header.h b/lib/header.h
index 87ca03d01..d2fa40ab6 100644
--- a/lib/header.h
+++ b/lib/header.h
@@ -396,7 +396,7 @@ typedef
  */
 typedef
 /*@null@*/ Header (*HDRhdrread) (FD_t fd, enum hMagic magicp)
-	/*@modifies fd, fileSystem @*/;
+	/*@modifies fd @*/;
 
 /** \ingroup header
  * Write (with unload) header to file handle.
@@ -407,6 +407,7 @@ typedef
  */
 typedef
 int (*HDRhdrwrite) (FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
+	/*@globals fileSystem @*/
 	/*@modifies fd, h, fileSystem @*/;
 
 /** \ingroup header
diff --git a/lib/header_internal.h b/lib/header_internal.h
index 7ae69c62b..d6fd351fb 100644
--- a/lib/header_internal.h
+++ b/lib/header_internal.h
@@ -174,6 +174,7 @@ int headerGetRawEntry(Header h, int_32 tag,
 /*@unused@*/
 void headerDump(Header h, FILE *f, int flags,
 		const struct headerTagTableEntry_s * tags)
+	/*@globals fileSystem @*/
 	/*@modifies f, fileSystem @*/;
 #define HEADER_DUMP_INLINE   1
 
diff --git a/lib/manifest.c b/lib/manifest.c
index c1223835d..2ffb6e6c6 100644
--- a/lib/manifest.c
+++ b/lib/manifest.c
@@ -105,8 +105,10 @@ int rpmReadPackageManifest(FD_t fd, int * argcPtr, const char *** argvPtr)
 	appendStringBuf(sb, s);
     }
 
+    /*@-branchstate@*/
     if (s == NULL)		/* XXX always true */
 	s = getStringBuf(sb);
+    /*@=branchstate@*/
 
     if (!(s && *s)) {
 	rc = 1;
@@ -148,12 +150,14 @@ int rpmReadPackageManifest(FD_t fd, int * argcPtr, const char *** argvPtr)
 	*argcPtr = ac;
 
 exit:
+    /*@-branchstate@*/
     if (argvPtr == NULL || (rc != 0 && av)) {
 	if (av)
 	for (i = 0; i < ac; i++)
 	    /*@-unqualifiedtrans@*/av[i] = _free(av[i]); /*@=unqualifiedtrans@*/
 	/*@-dependenttrans@*/ av = _free(av); /*@=dependenttrans@*/
     }
+    /*@=branchstate@*/
     sb = freeStringBuf(sb);
     /*@-nullstate@*/
     return rc;
diff --git a/lib/manifest.h b/lib/manifest.h
index 6ca4429c9..d62d74f6a 100644
--- a/lib/manifest.h
+++ b/lib/manifest.h
@@ -25,6 +25,7 @@ char * rpmPermsString(int mode)
  * @retval argvPtr		args themselves
  */
 int rpmReadPackageManifest(FD_t fd, int * argcPtr, const char *** argvPtr)
+	/*@globals fileSystem @*/
 	/*@modifies fd, *argcPtr, *argvPtr, fileSystem @*/;
 
 #ifdef __cplusplus
diff --git a/lib/misc.c b/lib/misc.c
index ef2b99685..47719197d 100644
--- a/lib/misc.c
+++ b/lib/misc.c
@@ -106,7 +106,9 @@ int rpmfileexists(const char * urlfn)
     int urltype = urlPath(urlfn, &fn);
     struct stat buf;
 
+    /*@-branchstate@*/
     if (*fn == '\0') fn = "/";
+    /*@=branchstate@*/
     switch (urltype) {
     case URL_IS_FTP:	/* XXX WRONG WRONG WRONG */
     case URL_IS_HTTP:	/* XXX WRONG WRONG WRONG */
@@ -152,6 +154,7 @@ 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 @*/
 {
     char * d, * de;
@@ -210,9 +213,12 @@ int makeTempFile(const char * prefix, const char ** fnptr, FD_t * fdptr)
     FD_t fd = NULL;
     int ran;
 
+    /*@-branchstate@*/
     if (!prefix) prefix = "";
+    /*@=branchstate@*/
 
     /* Create the temp directory if it doesn't already exist. */
+    /*@-branchstate@*/
     if (!_initialized) {
 	_initialized = 1;
 	/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
@@ -221,6 +227,7 @@ int makeTempFile(const char * prefix, const char ** fnptr, FD_t * fdptr)
 	if (rpmMkpath(tempfn, 0755, (uid_t) -1, (gid_t) -1))
 	    goto errxit;
     }
+    /*@=branchstate@*/
 
     /* XXX should probably use mkstemp here */
     srand(time(NULL));
@@ -286,10 +293,12 @@ int makeTempFile(const char * prefix, const char ** fnptr, FD_t * fdptr)
 	break;
     }
 
+    /*@-branchstate@*/
     if (fnptr)
 	*fnptr = tempfn;
     else 
 	tempfn = _free(tempfn);
+    /*@=branchstate@*/
     *fdptr = fd;
 
     return 0;
@@ -373,6 +382,7 @@ void compressFilelist(Header h)
 	goto exit;
     }
 
+    /*@-branchstate@*/
     for (i = 0; i < count; i++) {
 	const char ** needle;
 	char savechar;
@@ -399,6 +409,7 @@ void compressFilelist(Header h)
 	*baseName = savechar;
 	baseNames[i] = baseName;
     }
+    /*@=branchstate@*/
 
 exit:
     if (count > 0) {
@@ -458,10 +469,12 @@ static void doBuildFileList(Header h, /*@out@*/ const char *** fileListPtr,
     baseNames = hfd(baseNames, bnt);
     dirNames = hfd(dirNames, dnt);
 
+    /*@-branchstate@*/
     if (fileListPtr)
 	*fileListPtr = fileNames;
     else
 	fileNames = _free(fileNames);
+    /*@=branchstate@*/
     if (fileCountPtr) *fileCountPtr = count;
 }
 
@@ -472,6 +485,7 @@ void expandFilelist(Header h)
     const char ** fileNames = NULL;
     int count = 0;
 
+    /*@-branchstate@*/
     if (!headerIsEntry(h, RPMTAG_OLDFILENAMES)) {
 	doBuildFileList(h, &fileNames, &count, RPMTAG_BASENAMES,
 			RPMTAG_DIRNAMES, RPMTAG_DIRINDEXES);
@@ -481,6 +495,7 @@ void expandFilelist(Header h)
 			fileNames, count);
 	fileNames = _free(fileNames);
     }
+    /*@=branchstate@*/
 
     (void) hre(h, RPMTAG_DIRNAMES);
     (void) hre(h, RPMTAG_BASENAMES);
@@ -603,10 +618,12 @@ fprintf(stderr, "*** rpmGlob argv[%d] \"%s\"\n", argc, argv[argc]);
 if (_debug)
 fprintf(stderr, "*** GLOB maxb %d diskURL %d %*s globURL %p %s\n", (int)maxb, (int)nb, (int)nb, av[j], globURL, globURL);
 	
+	/*@-branchstate@*/
 	if (argc == 0)
 	    argv = xmalloc((gl.gl_pathc+1) * sizeof(*argv));
 	else if (gl.gl_pathc > 0)
 	    argv = xrealloc(argv, (argc+gl.gl_pathc+1) * sizeof(*argv));
+	/*@=branchstate@*/
 	for (i = 0; i < gl.gl_pathc; i++) {
 	    const char * globFile = &(gl.gl_pathv[i][0]);
 	    if (globRoot > globURL && globRoot[-1] == '/')
diff --git a/lib/package.c b/lib/package.c
index 3ae46c073..42be6dc1b 100644
--- a/lib/package.c
+++ b/lib/package.c
@@ -190,6 +190,7 @@ static rpmRC readPackageHeaders(FD_t fd,
 	 * careful. This fixup makes queries give the new values though,
 	 * which is quite handy.
 	 */
+	/*@-branchstate@*/
 	if (headerGetEntry(*hdr, RPMTAG_DEFAULTPREFIX, NULL,
 			   (void **) &defaultPrefix, NULL))
 	{
@@ -198,6 +199,7 @@ static rpmRC readPackageHeaders(FD_t fd,
 	    (void) headerAddEntry(*hdr, RPMTAG_PREFIXES, RPM_STRING_ARRAY_TYPE,
 			   &defaultPrefix, 1); 
 	}
+	/*@=branchstate@*/
 
 	/*
 	 * The file list was moved to a more compressed format which not
diff --git a/lib/poptI.c b/lib/poptI.c
index ab5453cdc..8d99f1dbf 100644
--- a/lib/poptI.c
+++ b/lib/poptI.c
@@ -35,10 +35,12 @@ static void installArgCallback( /*@unused@*/ poptContext con,
 		/*@unused@*/ enum poptCallbackReason reason,
 		const struct poptOption * opt, const char * arg,
 		/*@unused@*/ const void * data)
+	/*@globals rpmIArgs */
 	/*@modifies rpmIArgs */
 {
     struct rpmInstallArguments_s * ia = &rpmIArgs;
 
+    /*@-branchstate@*/
     switch (opt->val) {
     case POPT_EXCLUDEPATH:
 	if (arg == NULL || *arg != '/') 
@@ -80,6 +82,7 @@ static void installArgCallback( /*@unused@*/ poptContext con,
 	ia->rbtid = tid;
       }	break;
     }
+    /*@=branchstate@*/
 }
 
 /**
diff --git a/lib/poptK.c b/lib/poptK.c
index ba8f6e2a8..942cb6098 100644
--- a/lib/poptK.c
+++ b/lib/poptK.c
@@ -21,6 +21,7 @@ static void signArgCallback( /*@unused@*/ poptContext con,
 		/*@unused@*/ enum poptCallbackReason reason,
 		const struct poptOption * opt, /*@unused@*/ const char * arg,
 		/*@unused@*/ const void * data)
+	/*@globals rpmKArgs @*/
 	/*@modifies rpmKArgs @*/
 {
     struct rpmSignArguments_s * rka = &rpmKArgs;
diff --git a/lib/poptQV.c b/lib/poptQV.c
index 9fa8bca57..d8f07746f 100644
--- a/lib/poptQV.c
+++ b/lib/poptQV.c
@@ -28,6 +28,7 @@ static void rpmQVSourceArgCallback( /*@unused@*/ poptContext con,
 		/*@unused@*/ enum poptCallbackReason reason,
 		const struct poptOption * opt, /*@unused@*/ const char * arg, 
 		/*@unused@*/ const void * data)
+	/*@globals rpmQVArgs @*/
 	/*@modifies rpmQVArgs @*/
 {
     QVA_t qva = &rpmQVArgs;
@@ -106,6 +107,7 @@ static void queryArgCallback(/*@unused@*/poptContext con,
 		/*@unused@*/enum poptCallbackReason reason,
 		const struct poptOption * opt, const char * arg, 
 		/*@unused@*/ const void * data)
+	/*@globals rpmQVArgs @*/
 	/*@modifies rpmQVArgs @*/
 {
     QVA_t qva = &rpmQVArgs;
@@ -127,6 +129,7 @@ static void queryArgCallback(/*@unused@*/poptContext con,
     case POPT_QUERYFORMAT:
 	if (arg) {
 	    char * qf = (char *)qva->qva_queryFormat;
+	    /*@-branchstate@*/
 	    if (qf) {
 		int len = strlen(qf) + strlen(arg) + 1;
 		qf = xrealloc(qf, len);
@@ -135,6 +138,7 @@ static void queryArgCallback(/*@unused@*/poptContext con,
 		qf = xmalloc(strlen(arg) + 1);
 		strcpy(qf, arg);
 	    }
+	    /*@=branchstate@*/
 	    qva->qva_queryFormat = qf;
 	}
 	break;
diff --git a/lib/psm.c b/lib/psm.c
index d0517552a..7a2ccaf14 100644
--- a/lib/psm.c
+++ b/lib/psm.c
@@ -91,7 +91,9 @@ void loadFi(Header h, TFI_t fi)
     fi->hre = (HRE_t) headerRemoveEntry;
     fi->hfd = hfd = headerFreeData;
 
+    /*@-branchstate@*/
     if (h && fi->h == NULL)	fi->h = headerLink(h);
+    /*@=branchstate@*/
 
     /* Duplicate name-version-release so that headers can be free'd. */
     rc = hge(fi->h, RPMTAG_NAME, NULL, (void **) &fi->name, NULL);
@@ -891,10 +893,12 @@ static int runScript(PSM_t psm, Header h,
 
     if (script) {
 	FD_t fd;
+	/*@-branchstate@*/
 	if (makeTempFile((!ts->chrootDone ? ts->rootDir : "/"), &fn, &fd)) {
 	    if (freePrefixes) free(prefixes);
 	    return 1;
 	}
+	/*@=branchstate@*/
 
 	if (rpmIsDebug() &&
 	    (!strcmp(argv[0], "/bin/sh") || !strcmp(argv[0], "/bin/bash")))
@@ -954,6 +958,7 @@ static int runScript(PSM_t psm, Header h,
 	(void) dup2(pipes[0], STDIN_FILENO);
 	(void) close(pipes[0]);
 
+	/*@-branchstate@*/
 	if (ts->scriptFd != NULL) {
 	    int sfdno = Fileno(ts->scriptFd);
 	    int ofdno = Fileno(out);
@@ -969,17 +974,21 @@ static int runScript(PSM_t psm, Header h,
 		(void) Fclose (ts->scriptFd);
 	    }
 	}
+	/*@=branchstate@*/
 
+	/*@-branchstate@*/
 	{   const char *ipath = rpmExpand("PATH=%{_install_script_path}", NULL);
 	    const char *path = SCRIPT_PATH;
 
 	    if (ipath && ipath[5] != '%')
 		path = ipath;
+
 	    (void) doputenv(path);
 	    /*@-modobserver@*/
 	    ipath = _free(ipath);
 	    /*@=modobserver@*/
 	}
+	/*@=branchstate@*/
 
 	for (i = 0; i < numPrefixes; i++) {
 	    sprintf(prefixBuf, "RPM_INSTALL_PREFIX%d=%s", i, prefixes[i]);
@@ -1034,11 +1043,13 @@ static int runScript(PSM_t psm, Header h,
 
     (void) Fclose(out);	/* XXX dup'd STDOUT_FILENO */
     
+    /*@-branchstate@*/
     if (script) {
 	if (!rpmIsDebug())
 	    (void) unlink(fn);
 	fn = _free(fn);
     }
+    /*@=branchstate@*/
 
     return rc;
 }
@@ -1070,12 +1081,14 @@ static rpmRC runInstScript(PSM_t psm)
     (void) hge(fi->h, psm->progTag, &ptt, (void **) &programArgv, &programArgc);
     (void) hge(fi->h, psm->scriptTag, &stt, (void **) &script, NULL);
 
+    /*@-branchstate@*/
     if (programArgv && ptt == RPM_STRING_TYPE) {
 	argv = alloca(sizeof(char *));
 	*argv = (const char *) programArgv;
     } else {
 	argv = (const char **) programArgv;
     }
+    /*@=branchstate@*/
 
     rc = runScript(psm, fi->h, tag2sln(psm->scriptTag), programArgc, argv,
 		script, psm->scriptArg, -1);
@@ -1348,6 +1361,7 @@ int psmStage(PSM_t psm, pkgStage stage)
     rpmRC rc = psm->rc;
     int saveerrno;
 
+    /*@-branchstate@*/
     switch (stage) {
     case PSM_UNKNOWN:
 	break;
@@ -1965,6 +1979,7 @@ fprintf(stderr, "*** PSM_RDB_LOAD: header #%u not found\n", fi->record);
     default:
 	break;
     }
+    /*@=branchstate@*/
 
     /*@-nullstate@*/	/* FIX: psm->oh and psm->fi->h may be NULL. */
     return rc;
diff --git a/lib/query.c b/lib/query.c
index 683ec443c..cc0da5e89 100644
--- a/lib/query.c
+++ b/lib/query.c
@@ -147,7 +147,7 @@ static int countLinks(int_16 * fileRdevList, int_32 * fileInodeList, int nfiles,
     return nlink;
 }
 
-int showQueryPackage(QVA_t qva, /*@unused@*/rpmdb rpmdb, Header h)
+int showQueryPackage(QVA_t qva, /*@unused@*/rpmdb db, Header h)
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -192,6 +192,7 @@ int showQueryPackage(QVA_t qva, /*@unused@*/rpmdb rpmdb, Header h)
     if (queryFormat) {
 	const char * str = queryHeader(h, queryFormat);
 	nonewline = 1;
+	/*@-branchstate@*/
 	if (str) {
 	    size_t tb = (te - t);
 	    size_t sb = strlen(str);
@@ -205,6 +206,7 @@ int showQueryPackage(QVA_t qva, /*@unused@*/rpmdb rpmdb, Header h)
 	    /*@=usereleased@*/
 	    str = _free(str);
 	}
+	/*@=branchstate@*/
     }
 
     if (!(queryFlags & QUERY_FOR_LIST))
@@ -402,6 +404,7 @@ exit:
  */
 static void
 printNewSpecfile(Spec spec)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     Header h;
@@ -413,6 +416,7 @@ printNewSpecfile(Spec spec)
     if (sl == NULL || st == NULL)
 	return;
 
+    /*@-branchstate@*/
     for (i = 0; i < st->st_ntags; i++) {
 	spectag t = st->st_t + i;
 	const char * tn = tagName(t->t_tag);
@@ -487,6 +491,7 @@ printNewSpecfile(Spec spec)
 	    /*@switchbreak@*/ break;
 	}
     }
+    /*@=branchstate@*/
     msgstr = _free(msgstr);
 
     for (i = 0; i < sl->sl_nlines; i++) {
@@ -556,7 +561,7 @@ int	(*parseSpecVec) (Spec *specp, const char *specFile, const char *rootdir,
 /*@=redecl@*/
 
 int rpmQueryVerify(QVA_t qva, rpmQVSources source, const char * arg,
-	rpmdb rpmdb, QVF_t showPackage)
+	rpmdb db, QVF_t showPackage)
 {
     rpmdbMatchIterator mi = NULL;
     Header h;
@@ -566,6 +571,7 @@ int rpmQueryVerify(QVA_t qva, rpmQVSources source, const char * arg,
     const char ** av = NULL;
     char * end = NULL;
 
+    /*@-branchstate@*/
     switch (source) {
     case RPMQV_RPM:
     {	int ac = 0;
@@ -613,7 +619,7 @@ restart:
 
 	    /* Query a package file. */
 	    if (rpmrc == RPMRC_OK) {
-		retcode = showPackage(qva, rpmdb, h);
+		retcode = showPackage(qva, db, h);
 		h = headerFree(h);
 		continue;
 	    }
@@ -693,7 +699,7 @@ restart:
 
     case RPMQV_ALL:
 	/* RPMDBI_PACKAGES */
-	mi = rpmdbInitIterator(rpmdb, RPMDBI_PACKAGES, NULL, 0);
+	mi = rpmdbInitIterator(db, RPMDBI_PACKAGES, NULL, 0);
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERYINFO, _("no packages\n"));
 	    retcode = 1;
@@ -711,7 +717,7 @@ restart:
 	break;
 
     case RPMQV_GROUP:
-	mi = rpmdbInitIterator(rpmdb, RPMTAG_GROUP, arg, 0);
+	mi = rpmdbInitIterator(db, RPMTAG_GROUP, arg, 0);
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERYINFO,
 		_("group %s does not contain any packages\n"), arg);
@@ -722,7 +728,7 @@ restart:
 	break;
 
     case RPMQV_TRIGGEREDBY:
-	mi = rpmdbInitIterator(rpmdb, RPMTAG_TRIGGERNAME, arg, 0);
+	mi = rpmdbInitIterator(db, RPMTAG_TRIGGERNAME, arg, 0);
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERYINFO, _("no package triggers %s\n"), arg);
 	    retcode = 1;
@@ -732,7 +738,7 @@ restart:
 	break;
 
     case RPMQV_WHATREQUIRES:
-	mi = rpmdbInitIterator(rpmdb, RPMTAG_REQUIRENAME, arg, 0);
+	mi = rpmdbInitIterator(db, RPMTAG_REQUIRENAME, arg, 0);
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERYINFO, _("no package requires %s\n"), arg);
 	    retcode = 1;
@@ -743,7 +749,7 @@ restart:
 
     case RPMQV_WHATPROVIDES:
 	if (arg[0] != '/') {
-	    mi = rpmdbInitIterator(rpmdb, RPMTAG_PROVIDENAME, arg, 0);
+	    mi = rpmdbInitIterator(db, RPMTAG_PROVIDENAME, arg, 0);
 	    if (mi == NULL) {
 		rpmError(RPMERR_QUERYINFO, _("no package provides %s\n"), arg);
 		retcode = 1;
@@ -774,7 +780,7 @@ restart:
 	    fn = xstrdup(arg);
 	(void) rpmCleanPath(fn);
 
-	mi = rpmdbInitIterator(rpmdb, RPMTAG_BASENAMES, fn, 0);
+	mi = rpmdbInitIterator(db, RPMTAG_BASENAMES, fn, 0);
 	if (mi == NULL) {
 	    int myerrno = 0;
 	    if (access(fn, F_OK) != 0)
@@ -817,7 +823,7 @@ restart:
 	}
 	rpmMessage(RPMMESS_DEBUG, _("package record number: %u\n"), recOffset);
 	/* RPMDBI_PACKAGES */
-	mi = rpmdbInitIterator(rpmdb, RPMDBI_PACKAGES, &recOffset, sizeof(recOffset));
+	mi = rpmdbInitIterator(db, RPMDBI_PACKAGES, &recOffset, sizeof(recOffset));
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERY,
 		_("record %u could not be read\n"), recOffset);
@@ -829,7 +835,7 @@ restart:
 
     case RPMQV_PACKAGE:
 	/* XXX HACK to get rpmdbFindByLabel out of the API */
-	mi = rpmdbInitIterator(rpmdb, RPMDBI_LABEL, arg, 0);
+	mi = rpmdbInitIterator(db, RPMDBI_LABEL, arg, 0);
 	if (mi == NULL) {
 	    rpmError(RPMERR_QUERYINFO, _("package %s is not installed\n"), arg);
 	    retcode = 1;
@@ -838,13 +844,14 @@ restart:
 	}
 	break;
     }
+    /*@=branchstate@*/
    
     return retcode;
 }
 
 int rpmQuery(QVA_t qva, rpmQVSources source, const char * arg)
 {
-    rpmdb rpmdb = NULL;
+    rpmdb db = NULL;
     int rc;
 
     switch (source) {
@@ -852,15 +859,15 @@ int rpmQuery(QVA_t qva, rpmQVSources source, const char * arg)
     case RPMQV_SPECFILE:
 	break;
     default:
-	if (rpmdbOpen(qva->qva_prefix, &rpmdb, O_RDONLY, 0644))
+	if (rpmdbOpen(qva->qva_prefix, &db, O_RDONLY, 0644))
 	    return 1;
 	break;
     }
 
-    rc = rpmQueryVerify(qva, source, arg, rpmdb, showQueryPackage);
+    rc = rpmQueryVerify(qva, source, arg, db, showQueryPackage);
 
-    if (rpmdb != NULL)
-	(void) rpmdbClose(rpmdb);
+    if (db != NULL)
+	(void) rpmdbClose(db);
 
     return rc;
 }
diff --git a/lib/rpmchecksig.c b/lib/rpmchecksig.c
index a5ea603ee..8e2a5782e 100644
--- a/lib/rpmchecksig.c
+++ b/lib/rpmchecksig.c
@@ -134,6 +134,7 @@ int rpmReSign(rpmResignFlags flags, char * passPhrase, const char ** argv)
     rpmRC rc;
     
     tmprpm[0] = '\0';
+    /*@-branchstate@*/
     if (argv)
     while ((rpm = *argv++) != NULL) {
 
@@ -228,6 +229,7 @@ int rpmReSign(rpmResignFlags flags, char * passPhrase, const char ** argv)
 	(void) rename(trpm, rpm);
 	tmprpm[0] = '\0';
     }
+    /*@=branchstate@*/
 
     res = 0;
 
@@ -279,6 +281,7 @@ int rpmCheckSig(rpmCheckSigFlags flags, const char ** argv)
 
     memset(dig, 0, sizeof(*dig));
 
+    /*@-branchstate@*/
     while ((pkgfn = *argv++) != NULL) {
 
 	if (manageFile(&fd, &pkgfn, O_RDONLY, 0)) {
@@ -565,6 +568,7 @@ fprintf(stderr, "========================= Red Hat DSA Public Key\n");
 	mp32nfree(&dig->c);
 	mp32nfree(&dig->rsahm);
     }
+    /*@=branchstate@*/
 
     dig->sha1ctx = _free(dig->sha1ctx);
     dig->sha1 = _free(dig->sha1);
diff --git a/lib/rpmcli.h b/lib/rpmcli.h
index 674c3fab3..8061055fe 100644
--- a/lib/rpmcli.h
+++ b/lib/rpmcli.h
@@ -527,12 +527,12 @@ typedef enum rpmResignFlags_e {
 
 /** \ingroup rpmcli
  * Create/modify elements in signature header.
- * @param add		type of signature operation
+ * @param flags		type of signature operation
  * @param passPhrase
  * @param argv		array of package file names (NULL terminated)
  * @return		0 on success
  */
-int rpmReSign(rpmResignFlags add, char * passPhrase,
+int rpmReSign(rpmResignFlags flags, char * passPhrase,
 		/*@null@*/ const char ** argv)
 	/*@globals rpmGlobalMacroContext,
 		fileSystem, internalState @*/
diff --git a/lib/rpminstall.c b/lib/rpminstall.c
index 90ac3a409..33318a0c4 100644
--- a/lib/rpminstall.c
+++ b/lib/rpminstall.c
@@ -31,6 +31,7 @@ static int progressCurrent = 0;
 /**
  */
 static void printHash(const unsigned long amount, const unsigned long total)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     int hashesNeeded;
@@ -74,6 +75,7 @@ void * rpmShowProgress(/*@null@*/ const void * arg,
 			const unsigned long total,
 			/*@null@*/ const void * pkgKey,
 			/*@null@*/ void * data)
+	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/
 {
     /*@-castexpose@*/
@@ -220,6 +222,7 @@ int rpmInstall(const char * rootdir, const char ** fileArgv,
     }
 
     /* Build fully globbed list of arguments in argv[argc]. */
+    /*@-branchstate@*/
     /*@-temptrans@*/
     for (eiu->fnp = fileArgv; *eiu->fnp != NULL; eiu->fnp++) {
     /*@=temptrans@*/
@@ -232,6 +235,7 @@ int rpmInstall(const char * rootdir, const char ** fileArgv,
 	eiu->argc += ac;
 	eiu->argv[eiu->argc] = NULL;
     }
+    /*@=branchstate@*/
     av = _free(av);	ac = 0;
 
 restart:
@@ -496,6 +500,7 @@ restart:
 	    stopInstall = 1;
 	}
 
+	/*@-branchstate@*/
 	if (!stopInstall && conflicts) {
 	    rpmMessage(RPMMESS_ERROR, _("failed dependencies:\n"));
 	    printDepProblems(stderr, conflicts, numConflicts);
@@ -503,6 +508,7 @@ restart:
 	    eiu->numFailed = eiu->numPkgs;
 	    stopInstall = 1;
 	}
+	/*@=branchstate@*/
     }
 
     if (eiu->numRPMS && !(interfaceFlags & INSTALL_NOORDER)) {
@@ -641,6 +647,7 @@ int rpmErase(const char * rootdir, const char ** argv,
 	    stopUninstall = 1;
 	}
 
+	/*@-branchstate@*/
 	if (!stopUninstall && conflicts) {
 	    rpmMessage(RPMMESS_ERROR, _("removing these packages would break "
 			      "dependencies:\n"));
@@ -649,6 +656,7 @@ int rpmErase(const char * rootdir, const char ** argv,
 	    numFailed += numPackages;
 	    stopUninstall = 1;
 	}
+	/*@=branchstate@*/
     }
 
     if (!stopUninstall) {
@@ -767,6 +775,7 @@ IDTX IDTXload(rpmdb db, rpmTag tag)
     HGE_t hge = (HGE_t) headerGetEntry;
     Header h;
 
+    /*@-branchstate@*/
     mi = rpmdbInitIterator(db, tag, NULL, 0);
     while ((h = rpmdbNextIterator(mi)) != NULL) {
 	rpmTagType type = RPM_NULL_TYPE;
@@ -798,6 +807,7 @@ IDTX IDTXload(rpmdb db, rpmTag tag)
 	idtx->nidt++;
     }
     mi = rpmdbFreeIterator(mi);
+    /*@=branchstate@*/
 
     return IDTXsort(idtx);
 }
@@ -841,6 +851,7 @@ IDTX IDTXglob(const char * globstr, rpmTag tag)
 	}
 
 	tidp = NULL;
+	/*@-branchstate@*/
 	if (hge(h, tag, &type, (void **) &tidp, &count) && tidp) {
 
 	    idtx = IDTXgrow(idtx, 1);
@@ -859,6 +870,7 @@ IDTX IDTXglob(const char * globstr, rpmTag tag)
 	    }
 	    idtx->nidt++;
 	}
+	/*@=branchstate@*/
 
 	h = headerFree(h);
 	(void) Fclose(fd);
diff --git a/lib/rpmlead.h b/lib/rpmlead.h
index fe32a074d..a50566fb1 100644
--- a/lib/rpmlead.h
+++ b/lib/rpmlead.h
@@ -19,7 +19,7 @@ extern "C" {
  * @return		0 on success, 1 on error
  */
 int writeLead(FD_t fd, const struct rpmlead *lead)
-	/*@globals fileSystem@*/
+	/*@globals fileSystem @*/
 	/*@modifies fd, fileSystem @*/;
 
 /** \ingroup lead
@@ -29,7 +29,7 @@ int writeLead(FD_t fd, const struct rpmlead *lead)
  * @return		0 on success, 1 on error
  */
 int readLead(FD_t fd, /*@out@*/ struct rpmlead *lead)
-	/*@modifies fd, *lead, fileSystem @*/;
+	/*@modifies fd, *lead @*/;
 
 #ifdef __cplusplus
 }
diff --git a/lib/rpmlib.h b/lib/rpmlib.h
index caa337afa..1f58e0511 100644
--- a/lib/rpmlib.h
+++ b/lib/rpmlib.h
@@ -543,8 +543,8 @@ enum rpm_machtable_e {
  */
 int rpmReadConfigFiles(/*@null@*/ const char * file,
 		/*@null@*/ const char * target)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/;
 
 /** \ingroup rpmrc
  * Read rpmrc (and macro) configuration file(s).
@@ -552,8 +552,8 @@ int rpmReadConfigFiles(/*@null@*/ const char * file,
  * @return		0 on succes
  */
 int rpmReadRC(/*@null@*/ const char * rcfiles)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState  @*/;
 
 /** \ingroup rpmrc
  * Return current arch name and/or number.
@@ -597,8 +597,8 @@ int rpmMachineScore(int type, const char * name)
  * @return		0 always
  */
 int rpmShowRC(FILE * fp)
-	/*@globals fileSystem@*/
-	/*@modifies *fp, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *fp, fileSystem, internalState  @*/;
 
 /** \ingroup rpmrc
  * @deprecated Use addMacro to set _target_* macros.
@@ -608,7 +608,7 @@ int rpmShowRC(FILE * fp)
  * @param osTable
  */
 void rpmSetTables(int archTable, int osTable)
-	/*@globals fileSystem, internalState@*/
+	/*@globals fileSystem, internalState @*/
 	/*@modifies fileSystem, internalState @*/;
 
 /** \ingroup rpmrc
@@ -622,7 +622,7 @@ void rpmSetTables(int archTable, int osTable)
  * @param os		os name (or NULL)
  */
 void rpmSetMachine(/*@null@*/ const char * arch, /*@null@*/ const char * os)
-	/*@globals fileSystem, internalState@*/
+	/*@globals fileSystem, internalState @*/
 	/*@modifies fileSystem, internalState @*/;
 
 /** \ingroup rpmrc
@@ -643,7 +643,7 @@ void rpmGetMachine( /*@null@*/ /*@out@*/ const char **arch,
  * @todo Eliminate from API.
  */
 void rpmFreeRpmrc(void)
-	/*@globals internalState@*/
+	/*@globals internalState @*/
 	/*@modifies internalState @*/;
 
 /*@}*/
@@ -669,51 +669,51 @@ extern int dbiTagsMax;
 
 /** \ingroup rpmdb
  * Open rpm database.
- * @param root		path to top of install tree
+ * @param prefix	path to top of install tree
  * @retval dbp		address of rpm database
  * @param mode		open(2) flags:  O_RDWR or O_RDONLY (O_CREAT also)
  * @param perms		database permissions
  * @return		0 on success
  */
-int rpmdbOpen (/*@null@*/ const char * root, /*@null@*/ /*@out@*/ rpmdb * dbp,
+int rpmdbOpen (/*@null@*/ const char * prefix, /*@null@*/ /*@out@*/ rpmdb * dbp,
 		int mode, int perms)
 	/*@globals fileSystem@*/
 	/*@modifies *dbp, fileSystem @*/;
 
 /** \ingroup rpmdb
  * Initialize database.
- * @param root		path to top of install tree
+ * @param prefix	path to top of install tree
  * @param perms		database permissions
  * @return		0 on success
  */
-int rpmdbInit(/*@null@*/ const char * root, int perms)
+int rpmdbInit(/*@null@*/ const char * prefix, int perms)
 	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /** \ingroup rpmdb
  * Verify database components.
- * @param root		path to top of install tree
+ * @param prefix	path to top of install tree
  * @return		0 on success
  */
-int rpmdbVerify(/*@null@*/ const char * root)
+int rpmdbVerify(/*@null@*/ const char * prefix)
 	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /** \ingroup rpmdb
  * Close all database indices and free rpmdb.
- * @param rpmdb		rpm database
+ * @param db		rpm database
  * @return		0 on success
  */
-int rpmdbClose (/*@only@*/ /*@null@*/ rpmdb rpmdb)
+int rpmdbClose (/*@only@*/ /*@null@*/ rpmdb db)
 	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
 /** \ingroup rpmdb
  * Sync all database indices.
- * @param rpmdb		rpm database
+ * @param db		rpm database
  * @return		0 on success
  */
-int rpmdbSync (/*@null@*/ rpmdb rpmdb)
+int rpmdbSync (/*@null@*/ rpmdb db)
 	/*@globals fileSystem@*/
 	/*@modifies fileSystem @*/;
 
@@ -895,7 +895,7 @@ int rpmdbSetIteratorModified(/*@null@*/ rpmdbMatchIterator mi, int modified)
  */
 /*@only@*/ /*@null@*/ rpmdbMatchIterator rpmdbInitIterator(
 			/*@kept@*/ /*@null@*/ rpmdb db, int rpmtag,
-			/*@null@*/ const void * key, size_t keylen)
+			/*@null@*/ const void * keyp, size_t keylen)
 	/*@globals fileSystem@*/
 	/*@modifies db, fileSystem @*/;
 
@@ -914,18 +914,19 @@ int rpmdbAdd(/*@null@*/ rpmdb db, int iid, Header h)
  * Remove package header from rpm database and indices.
  * @param db		rpm database
  * @param rid		remove transaction id (rid = 0 or -1 to skip)
- * @param offset	location in Packages dbi
+ * @param hdrNum	package instance number in database
  * @return		0 on success
  */
-int rpmdbRemove(/*@null@*/ rpmdb db, /*@unused@*/ int rid, unsigned int offset)
+int rpmdbRemove(/*@null@*/ rpmdb db, /*@unused@*/ int rid, unsigned int hdrNum)
 	/*@globals fileSystem@*/
 	/*@modifies db, fileSystem @*/;
 
 /** \ingroup rpmdb
  * Rebuild database indices from package headers.
- * @param root		path to top of install tree
+ * @param prefix	path to top of install tree
+ * @return		0 on success
  */
-int rpmdbRebuild(/*@null@*/ const char * root)
+int rpmdbRebuild(/*@null@*/ const char * prefix)
 	/*@globals fileSystem @*/
 	/*@modifies fileSystem @*/;
 
@@ -1231,12 +1232,12 @@ typedef /*@abstract@*/ struct rpmTransactionSet_s * rpmTransactionSet;
 
 /** \ingroup rpmtrans
  * Create an empty transaction set.
- * @param rpmdb		rpm database (may be NULL if database is not accessed)
+ * @param db		rpm database (may be NULL if database is not accessed)
  * @param rootdir	path to top of install tree
  * @return		transaction set
  */
 /*@only@*/ rpmTransactionSet rpmtransCreateSet(
-		/*@null@*/ /*@kept@*/ rpmdb rpmdb,
+		/*@null@*/ /*@kept@*/ rpmdb db,
 		/*@null@*/ const char * rootDir)
 	/*@*/;
 
diff --git a/lib/rpmlibprov.c b/lib/rpmlibprov.c
index 0424b6092..f934f6d33 100644
--- a/lib/rpmlibprov.c
+++ b/lib/rpmlibprov.c
@@ -90,20 +90,26 @@ int rpmGetRpmlibProvides(const char *** provNames, int ** provFlags,
         versions[n] = rpmlibProvides[n].featureEVR;
     }
     
+    /*@-branchstate@*/
     if (provNames)
 	*provNames = names;
     else
 	names = _free(names);
+    /*@=branchstate@*/
 
+    /*@-branchstate@*/
     if (provFlags)
 	*provFlags = flags;
     else
 	flags = _free(flags);
+    /*@=branchstate@*/
 
+    /*@-branchstate@*/
     if (provVersions)
 	*provVersions = versions;
     else
 	versions = _free(versions);
+    /*@=branchstate@*/
 
     /*@-compmempass@*/ /* FIX: rpmlibProvides[] reachable */
     return n;
diff --git a/lib/rpmrc.c b/lib/rpmrc.c
index 6a16b6218..e379dd6df 100644
--- a/lib/rpmrc.c
+++ b/lib/rpmrc.c
@@ -1,4 +1,4 @@
-/*@-internalglobs -globs@*/
+/*@-branchstate@*/
 #include "system.h"
 
 #include <stdarg.h>
@@ -17,10 +17,11 @@
 
 /*@access FD_t@*/		/* compared with NULL */
 
-/*@observer@*/ static const char *defrcfiles =
-	LIBRPMRC_FILENAME ":/etc/rpmrc:~/.rpmrc";
+/*@observer@*/ /*@unchecked@*/
+static const char *defrcfiles = LIBRPMRC_FILENAME ":/etc/rpmrc:~/.rpmrc";
 
-/*@observer@*/ const char * macrofiles = MACROFILES;
+/*@observer@*/ /*@checked@*/
+const char * macrofiles = MACROFILES;
 
 typedef /*@owned@*/ const char * cptr_t;
 
@@ -91,6 +92,7 @@ typedef struct tableType_s {
 } * tableType;
 
 /*@-fullinitblock@*/
+/*@unchecked@*/
 static struct tableType_s tables[RPM_MACHTABLE_COUNT] = {
     { "arch", 1, 0 },
     { "os", 1, 0 },
@@ -101,6 +103,7 @@ static struct tableType_s tables[RPM_MACHTABLE_COUNT] = {
 /* this *must* be kept in alphabetical order */
 /* The order of the flags is archSpecific, required, macroize, localize */
 
+/*@unchecked@*/
 static struct rpmOption optionTable[] = {
     { "include",		RPMVAR_INCLUDE,			0, 1,	0, 2 },
     { "macrofiles",		RPMVAR_MACROFILES,		0, 0,	0, 1 },
@@ -108,25 +111,45 @@ static struct rpmOption optionTable[] = {
     { "provides",               RPMVAR_PROVIDES,                0, 0,	0, 0 },
 };
 /*@=fullinitblock@*/
+
+/*@unchecked@*/
 static int optionTableSize = sizeof(optionTable) / sizeof(*optionTable);
 
 #define OS	0
 #define ARCH	1
 
+/*@unchecked@*/
 static cptr_t current[2];
+
+/*@unchecked@*/
 static int currTables[2] = { RPM_MACHTABLE_INSTOS, RPM_MACHTABLE_INSTARCH };
+
+/*@unchecked@*/
 static struct rpmvarValue values[RPMVAR_NUM];
+
+/*@unchecked@*/
 static int defaultsInitialized = 0;
 
 /* prototypes */
 static int doReadRC( /*@killref@*/ FD_t fd, const char * urlfn)
-	/*@modifies fd, fileSystem @*/;
+	/*@globals rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies fd, fileSystem, internalState @*/;
+
 static void rpmSetVarArch(int var, const char * val,
 		/*@null@*/ const char * arch)
+	/*@globals internalState @*/
 	/*@modifies internalState @*/;
+
 static void rebuildCompatTables(int type, const char * name)
+	/*@globals internalState @*/
 	/*@modifies internalState @*/;
 
+static void rpmRebuildTargetVars(/*@null@*/ const char **target, /*@null@*/ const char ** canontarget)
+	/*@globals rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies *canontarget, fileSystem, internalState @*/;
+
 static int optionCompare(const void * a, const void * b)
 	/*@*/
 {
@@ -134,9 +157,6 @@ static int optionCompare(const void * a, const void * b)
 		      ((struct rpmOption *) b)->name);
 }
 
-static void rpmRebuildTargetVars(/*@null@*/ const char **target, /*@null@*/ const char ** canontarget)
-	/*@modifies *canontarget, fileSystem @*/;
-
 static /*@observer@*/ /*@null@*/ machCacheEntry
 machCacheFindEntry(const machCache cache, const char * key)
 	/*@*/
@@ -151,7 +171,8 @@ machCacheFindEntry(const machCache cache, const char * key)
 
 static int machCompatCacheAdd(char * name, const char * fn, int linenum,
 				machCache cache)
-	/*@modifies *name, cache->cache, cache->size @*/
+	/*@globals internalState @*/
+	/*@modifies *name, cache->cache, cache->size, internalState @*/
 {
     machCacheEntry entry = NULL;
     char * chptr;
@@ -301,7 +322,8 @@ static void machFindEquivs(machCache cache, machEquivTable table,
 
 static int addCanon(canonEntry * table, int * tableLen, char * line,
 		    const char * fn, int lineNum)
-	/*@modifies *table, *tableLen, *line @*/
+	/*@globals internalState @*/
+	/*@modifies *table, *tableLen, *line, internalState @*/
 {
     canonEntry t;
     char *s, *s1;
@@ -354,7 +376,8 @@ static int addCanon(canonEntry * table, int * tableLen, char * line,
 
 static int addDefault(defaultEntry * table, int * tableLen, char * line,
 			const char * fn, int lineNum)
-	/*@modifies *table, *tableLen, *line @*/
+	/*@globals internalState @*/
+	/*@modifies *table, *tableLen, *line, internalState @*/
 {
     defaultEntry t;
 
@@ -419,6 +442,7 @@ const char * lookupInDefaultTable(const char * name,
 int rpmReadConfigFiles(const char * file, const char * target)
 {
 
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
     /* Preset target macros */
     /*@-nullstate@*/	/* FIX: target can be NULL */
     rpmRebuildTargetVars(&target, NULL);
@@ -437,12 +461,15 @@ int rpmReadConfigFiles(const char * file, const char * target)
 	cpu = _free(cpu);
 	os = _free(os);
     }
+/*@=globs@*/
 
     return 0;
 }
 
 static void setVarDefault(int var, const char * macroname, const char * val,
 		/*@null@*/ const char * body)
+	/*@globals rpmGlobalMacroContext,
+		internalState @*/
 	/*@modifies internalState @*/
 {
     if (var >= 0) {	/* XXX Dying ... */
@@ -455,6 +482,8 @@ static void setVarDefault(int var, const char * macroname, const char * val,
 }
 
 static void setPathDefault(int var, const char * macroname, const char * subdir)
+	/*@globals rpmGlobalMacroContext,
+		internalState @*/
 	/*@modifies internalState @*/
 {
 
@@ -486,7 +515,8 @@ static void setPathDefault(int var, const char * macroname, const char * subdir)
     }
 }
 
-/*@observer@*/ static const char * prescriptenviron = "\n\
+/*@observer@*/ /*@unchecked@*/
+static const char * prescriptenviron = "\n\
 RPM_SOURCE_DIR=\"%{_sourcedir}\"\n\
 RPM_BUILD_DIR=\"%{_builddir}\"\n\
 RPM_OPT_FLAGS=\"%{optflags}\"\n\
@@ -504,6 +534,8 @@ export RPM_BUILD_ROOT\n}\
 ";
 
 static void setDefaults(void)
+	/*@globals rpmGlobalMacroContext,
+		internalState @*/
 	/*@modifies internalState @*/
 {
 
@@ -540,12 +572,17 @@ static void setDefaults(void)
 }
 
 int rpmReadRC(const char * rcfiles)
+	/*@globals rpmGlobalMacroContext,
+		internalState @*/
+	/*@modifies internalState @*/
 {
     char *myrcfiles, *r, *re;
     int rc;
 
     if (!defaultsInitialized) {
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
 	setDefaults();
+/*@=globs@*/
 	defaultsInitialized = 1;
     }
 
@@ -603,7 +640,9 @@ int rpmReadRC(const char * rcfiles)
 	    rc = 1;
 	    break;
 	} else {
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
 	    rc = doReadRC(fd, fn);
+/*@=globs@*/
 	}
  	if (rc) break;
     }
@@ -616,7 +655,9 @@ int rpmReadRC(const char * rcfiles)
     {	const char *mfpath;
 	if ((mfpath = rpmGetVar(RPMVAR_MACROFILES)) != NULL) {
 	    mfpath = xstrdup(mfpath);
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
 	    rpmInitMacros(NULL, mfpath);
+/*@=globs@*/
 	    mfpath = _free(mfpath);
 	}
     }
@@ -626,7 +667,9 @@ int rpmReadRC(const char * rcfiles)
 
 /*@-usedef@*/	/*@ FIX: se usage inconsistent, W2DO? */
 static int doReadRC( /*@killref@*/ FD_t fd, const char * urlfn)
-	/*@modifies fd, fileSystem @*/
+	/*@globals rpmGlobalMacroContext,
+		fileSystem, internalState @*/
+	/*@modifies fd, fileSystem, internalState @*/
 {
     const char *s;
     char *se, *next;
@@ -930,15 +973,18 @@ static inline unsigned int cpuid_edx(unsigned int op)
 
 }
 
+/*@unchecked@*/
 static sigjmp_buf jenv;
 
 static inline void model3(int _unused)
+	/*@globals internalState @*/
 	/*@modifies internalState @*/
 {
 	siglongjmp(jenv, 1);
 }
 
 static inline int RPMClass(void)
+	/*@globals internalState @*/
 	/*@modifies internalState @*/
 {
 	int cpu;
@@ -1658,8 +1704,10 @@ int rpmShowRC(FILE * fp)
     rpmShowRpmlibProvides(fp);
     fprintf(fp, "\n");
 
+/*@-globs@*/ /* FIX: rpmGlobalMacroContext not in <rpmlib.h> */
     rpmDumpMacroTable(NULL, fp);
+/*@=globs@*/
 
     return 0;
 }
-/*@=internalglobs =globs@*/
+/*@=branchstate@*/
diff --git a/lib/transaction.c b/lib/transaction.c
index 81eec9c2d..64854275e 100644
--- a/lib/transaction.c
+++ b/lib/transaction.c
@@ -1,3 +1,4 @@
+/*@-branchstate@*/
 /** \ingroup rpmtrans
  * \file lib/transaction.c
  */
@@ -23,11 +24,11 @@ extern const char * chroot_prefix;
 /*@-incondefs@*/
 # include <sys/statvfs.h>
 #if defined(__LCLINT__)
-/*@-declundef -exportheader @*/ /* LCL: missing annotation */
+/*@-declundef -exportheader -protoparammatch @*/ /* LCL: missing annotation */
 extern int statvfs (const char * file, /*@out@*/ struct statvfs * buf)
 	/*@globals fileSystem@*/
 	/*@modifies *buf, fileSystem @*/;
-/*@=declundef =exportheader @*/
+/*@=declundef =exportheader =protoparammatch @*/
 /*@=incondefs@*/
 #endif
 #else
@@ -2141,3 +2142,4 @@ assert(alp == fi->ap);
 	return 0;
     /*@=nullstate@*/
 }
+/*@=branchstate@*/
diff --git a/lib/verify.c b/lib/verify.c
index eeecdbbbe..bce334196 100644
--- a/lib/verify.c
+++ b/lib/verify.c
@@ -278,8 +278,8 @@ int rpmVerifyFile(const char * root, Header h, int filenum,
  */
 int rpmVerifyScript(const char * rootDir, Header h, /*@null@*/ FD_t scriptFd)
 {
-    rpmdb rpmdb = NULL;
-    rpmTransactionSet ts = rpmtransCreateSet(rpmdb, rootDir);
+    rpmdb db = NULL;
+    rpmTransactionSet ts = rpmtransCreateSet(db, rootDir);
     TFI_t fi = xcalloc(1, sizeof(*fi));
     struct psm_s psmbuf;
     PSM_t psm = &psmbuf;
@@ -462,11 +462,11 @@ exit:
 
 /**
  * Check installed package dependencies for problems.
- * @param rpmdb		rpm database
+ * @param db		rpm database
  * @param h		header
  * @return		0 no problems, 1 problems found
  */
-static int verifyDependencies(rpmdb rpmdb, Header h)
+static int verifyDependencies(rpmdb db, Header h)
 	/*@globals fileSystem@*/
 	/*@modifies h, fileSystem @*/
 {
@@ -476,12 +476,13 @@ static int verifyDependencies(rpmdb rpmdb, Header h)
     int rc = 0;		/* assume no problems */
     int i;
 
-    ts = rpmtransCreateSet(rpmdb, NULL);
+    ts = rpmtransCreateSet(db, NULL);
     (void) rpmtransAddPackage(ts, h, NULL, NULL, 0, NULL);
 
     (void) rpmdepCheck(ts, &conflicts, &numConflicts);
     ts = rpmtransFree(ts);
 
+    /*@-branchstate@*/
     if (numConflicts) {
 	const char *n, *v, *r;
 	char * t, * te;
@@ -520,10 +521,11 @@ static int verifyDependencies(rpmdb rpmdb, Header h)
 	}
 	rc = 1;
     }
+    /*@=branchstate@*/
     return rc;
 }
 
-int showVerifyPackage(QVA_t qva, rpmdb rpmdb, Header h)
+int showVerifyPackage(QVA_t qva, rpmdb db, Header h)
 {
     const char * prefix = (qva->qva_prefix ? qva->qva_prefix : "");
     int ec = 0;
@@ -540,7 +542,7 @@ int showVerifyPackage(QVA_t qva, rpmdb rpmdb, Header h)
 	}
     }
     if (qva->qva_flags & VERIFY_DEPS) {
-	if ((rc = verifyDependencies(rpmdb, h)) != 0)
+	if ((rc = verifyDependencies(db, h)) != 0)
 	    ec = rc;
     }
     if (qva->qva_flags & VERIFY_FILES) {
@@ -559,7 +561,7 @@ int showVerifyPackage(QVA_t qva, rpmdb rpmdb, Header h)
 
 int rpmVerify(QVA_t qva, rpmQVSources source, const char * arg)
 {
-    rpmdb rpmdb = NULL;
+    rpmdb db = NULL;
     int rc;
 
     switch (source) {
@@ -568,15 +570,15 @@ int rpmVerify(QVA_t qva, rpmQVSources source, const char * arg)
 	    break;
 	/*@fallthrough@*/
     default:
-	if ((rc = rpmdbOpen(qva->qva_prefix, &rpmdb, O_RDONLY, 0644)) != 0)
+	if ((rc = rpmdbOpen(qva->qva_prefix, &db, O_RDONLY, 0644)) != 0)
 	    return 1;
 	break;
     }
 
-    rc = rpmQueryVerify(qva, source, arg, rpmdb, showVerifyPackage);
+    rc = rpmQueryVerify(qva, source, arg, db, showVerifyPackage);
 
-    if (rpmdb != NULL)
-	(void) rpmdbClose(rpmdb);
+    if (db != NULL)
+	(void) rpmdbClose(db);
 
     return rc;
 }