Add boundsread annotations throughout, enable +bounds checking.

Start narrowing the scope of bounds annotations by adding more annotations.

CVS patchset: 5537
CVS date: 2002/07/02 23:54:35

14 files changed, 133 insertions, 94 deletions

diff --git a/lib/.lclintrc b/lib/.lclintrc
index 5f94e31c4..b591159c8 100644
--- a/lib/.lclintrc
+++ b/lib/.lclintrc
@@ -13,6 +13,7 @@
 +strict			# lclint level
 
 # --- in progress
++bounds
 +slovak-fcns
 -redecl
 
diff --git a/lib/cpio.c b/lib/cpio.c
index f5e2733f7..8585b94de 100644
--- a/lib/cpio.c
+++ b/lib/cpio.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup payload
  * \file lib/cpio.c
  *  Handle cpio payloads within rpm packages.
@@ -55,7 +54,9 @@ static int strntoul(const char *str, /*@out@*/char **endptr, int base, int num)
 	if ( (end - phys) != sizeof(phys) ) return CPIOERR_BAD_HEADER;
 #define SET_NUM_FIELD(phys, val, space) \
 	sprintf(space, "%8.8lx", (unsigned long) (val)); \
-	memcpy(phys, space, 8);
+	/*@-boundsread@*/ \
+	memcpy(phys, space, 8) \
+	/*@=boundsread@*/
 
 int cpioTrailerWrite(FSM_t fsm)
 {
@@ -249,4 +250,3 @@ const char *const cpioStrerror(int rc)
     /*@=branchstate@*/
     return msg;
 }
-/*@=boundsread@*/
diff --git a/lib/depends.c b/lib/depends.c
index 51fdc419e..fc5ac4027 100644
--- a/lib/depends.c
+++ b/lib/depends.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts
  * \file lib/depends.c
  */
@@ -65,7 +64,8 @@ int rpmFLAGS = RPMSENSE_EQUAL;
  * @param b		2nd instance address
  * @return		result of comparison
  */
-static int intcmp(const void * a, const void * b)	/*@*/
+static int intcmp(const void * a, const void * b)
+	/*@requires maxRead(a) == 0 /\ maxRead(b) == 0 @*/
 {
     const int * aptr = a;
     const int * bptr = b;
@@ -253,6 +253,7 @@ int rpmtsAddInstallElement(rpmts ts, Header h,
 	    goto exit;
     }
 
+/*@-boundsread@*/
     {	rpmdbMatchIterator mi;
 	Header h2;
 
@@ -276,6 +277,7 @@ int rpmtsAddInstallElement(rpmts ts, Header h,
 	}
 	mi = rpmdbFreeIterator(mi);
     }
+/*@=boundsread@*/
 
     obsoletes = rpmdsLink(rpmteDS(p, RPMTAG_OBSOLETENAME), "Obsoletes");
     obsoletes = rpmdsInit(obsoletes);
@@ -319,21 +321,6 @@ exit:
     return ec;
 }
 
-#ifdef	DYING
-void rpmtsAvailablePackage(rpmts ts, Header h, fnpyKey key)
-{
-    int scareMem = 0;
-    rpmds provides = rpmdsNew(h, RPMTAG_PROVIDENAME, scareMem);
-    rpmfi fi = rpmfiNew(ts, NULL, h, RPMTAG_BASENAMES, scareMem);
-
-    /* XXX FIXME: return code RPMAL_NOMATCH is error */
-    (void) rpmalAdd(&ts->availablePackages, RPMAL_NOMATCH, key,
-		provides, fi);
-    fi = rpmfiFree(fi, 1);
-    provides = rpmdsFree(provides);
-}
-#endif
-
 int rpmtsAddEraseElement(rpmts ts, Header h, int dboffset)
 {
     return removePackage(ts, h, dboffset, RPMAL_NOMATCH);
@@ -427,10 +414,12 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
 	/*@-observertrans -mayaliasunique@*/
 	while ((start = strstr(rcProvidesString, Name))) {
 	/*@=observertrans =mayaliasunique@*/
+/*@-boundsread@*/
 	    if (xisspace(start[i]) || start[i] == '\0' || start[i] == ',') {
 		rpmdsNotify(dep, _("(rpmrc provides)"), rc);
 		goto exit;
 	    }
+/*@=boundsread@*/
 	    rcProvidesString = start + 1;
 	}
     }
@@ -456,6 +445,7 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
 
     /* XXX only the installer does not have the database open here. */
     if (rpmtsGetRdb(ts) != NULL) {
+/*@-boundsread@*/
 	if (Name[0] == '/') {
 	    /* depFlags better be 0! */
 
@@ -471,6 +461,7 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
 	    }
 	    mi = rpmdbFreeIterator(mi);
 	}
+/*@=boundsread@*/
 
 	mi = rpmtsInitIterator(ts, RPMTAG_PROVIDENAME, Name, 0);
 	(void) rpmdbPruneIterator(mi,
@@ -503,8 +494,10 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
     /*
      * Search for an unsatisfied dependency.
      */
+/*@-boundsread@*/
     if (!(rpmtsFlags(ts) & RPMTRANS_FLAG_NOSUGGEST) && ts->solve != NULL)
 	xx = (*ts->solve) (ts, dep);
+/*@=boundsread@*/
 
 unsatisfied:
     rc = 1;	/* dependency is unsatisfied */
@@ -800,6 +793,7 @@ static void freeBadDeps(void)
  * @param q	predecessor element (i.e. with Provides: )
  * @return	1 if dependency is to be ignored.
  */
+/*@-boundsread@*/
 static int ignoreDep(const rpmte p, const rpmte q)
 	/*@globals badDeps, badDepsInitialized @*/
 	/*@modifies badDeps, badDepsInitialized @*/
@@ -852,6 +846,7 @@ static int ignoreDep(const rpmte p, const rpmte q)
     return 0;
     /*@=compdef@*/
 }
+/*@=boundsread@*/
 
 /**
  * Recursively mark all nodes with their predecessors.
@@ -1051,8 +1046,10 @@ fprintf(stderr, "addRelation: q %p(%s) from %p[%d:%d]\n", q, rpmteN(q), ts->orde
 
     /* Avoid redundant relations. */
     /* XXX TODO: add control bit. */
+/*@-boundsread@*/
     if (selected[i] != 0)
 	return 0;
+/*@=boundsread@*/
 /*@-boundswrite@*/
     selected[i] = 1;
 /*@=boundswrite@*/
@@ -1816,4 +1813,3 @@ exit:
     /*@=branchstate@*/
     return rc;
 }
-/*@=boundsread@*/
diff --git a/lib/formats.c b/lib/formats.c
index 4259f7177..f4be621a4 100644
--- a/lib/formats.c
+++ b/lib/formats.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup header
  * \file lib/formats.c
  */
@@ -21,8 +20,9 @@
  * @return		formatted string
  */
 static /*@only@*/ char * triggertypeFormat(int_32 type, const void * data, 
-	/*@unused@*/ char * formatPrefix, /*@unused@*/ int padding,
-	/*@unused@*/ int element)	/*@*/
+		/*@unused@*/ char * formatPrefix, /*@unused@*/ int padding,
+		/*@unused@*/ int element)
+	/*@requires maxRead(data) >= 0 @*/
 {
     const int_32 * item = data;
     char * val;
@@ -45,26 +45,27 @@ static /*@only@*/ char * triggertypeFormat(int_32 type, const void * data,
  * @param element	(unused)
  * @return		formatted string
  */
-static /*@only@*/ char * permsFormat(int_32 type, const void * data, char * formatPrefix,
-	int padding, /*@unused@*/ int element)
-		/*@modifies formatPrefix @*/
+static /*@only@*/ char * permsFormat(int_32 type, const void * data,
+		char * formatPrefix, int padding, /*@unused@*/ int element)
+	/*@modifies formatPrefix @*/
+	/*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char * buf;
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
 	val = xstrdup(_("(not a number)"));
     } else {
 	val = xmalloc(15 + padding);
+/*@-boundswrite@*/
 	strcat(formatPrefix, "s");
+/*@=boundswrite@*/
 	buf = rpmPermsString(*((int_32 *) data));
 	/*@-formatconst@*/
 	sprintf(val, formatPrefix, buf);
 	/*@=formatconst@*/
 	buf = _free(buf);
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -79,18 +80,19 @@ static /*@only@*/ char * permsFormat(int_32 type, const void * data, char * form
  * @return		formatted string
  */
 static /*@only@*/ char * fflagsFormat(int_32 type, const void * data, 
-	char * formatPrefix, int padding, /*@unused@*/ int element)
-		/*@modifies formatPrefix @*/
+		char * formatPrefix, int padding, /*@unused@*/ int element)
+	/*@modifies formatPrefix @*/
+	/*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char buf[15];
     int anint = *((int_32 *) data);
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
 	val = xstrdup(_("(not a number)"));
     } else {
 	buf[0] = '\0';
+/*@-boundswrite@*/
 	if (anint & RPMFILE_DOC)
 	    strcat(buf, "d");
 	if (anint & RPMFILE_CONFIG)
@@ -107,14 +109,16 @@ static /*@only@*/ char * fflagsFormat(int_32 type, const void * data,
 	    strcat(buf, "l");
 	if (anint & RPMFILE_README)
 	    strcat(buf, "r");
+/*@=boundswrite@*/
 
 	val = xmalloc(5 + padding);
+/*@-boundswrite@*/
 	strcat(formatPrefix, "s");
+/*@=boundswrite@*/
 	/*@-formatconst@*/
 	sprintf(val, formatPrefix, buf);
 	/*@=formatconst@*/
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -223,7 +227,6 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
 {
     char * val;
 
-/*@-boundswrite@*/
     if (type != RPM_BIN_TYPE) {
 	val = xstrdup(_("(not a blob)"));
     } else {
@@ -232,6 +235,7 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
 	int lc;
 	int nt = ((element + 2) / 3) * 4;
 
+/*@-boundswrite@*/
 	/*@-globs@*/
 	/* Add additional bytes necessary for eol string(s). */
 	if (b64encode_chars_per_line > 0 && b64encode_eolstr != NULL) {
@@ -249,8 +253,8 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
 	    t = stpcpy(t, enc);
 	    enc = _free(enc);
 	}
-    }
 /*@=boundswrite@*/
+    }
 
     return val;
 }
@@ -289,33 +293,36 @@ static /*@only@*/ char * pgppktFormat(int_32 type, const void * data,
  * @return		formatted string
  */
 static /*@only@*/ char * depflagsFormat(int_32 type, const void * data, 
-	char * formatPrefix, int padding, /*@unused@*/ int element)
-		/*@modifies formatPrefix @*/
+		char * formatPrefix, int padding, /*@unused@*/ int element)
+	/*@modifies formatPrefix @*/
+	/*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char buf[10];
     int anint = *((int_32 *) data);
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
 	val = xstrdup(_("(not a number)"));
     } else {
 	buf[0] = '\0';
 
+/*@-boundswrite@*/
 	if (anint & RPMSENSE_LESS) 
 	    strcat(buf, "<");
 	if (anint & RPMSENSE_GREATER)
 	    strcat(buf, ">");
 	if (anint & RPMSENSE_EQUAL)
 	    strcat(buf, "=");
+/*@=boundswrite@*/
 
 	val = xmalloc(5 + padding);
+/*@-boundswrite@*/
 	strcat(formatPrefix, "s");
+/*@=boundswrite@*/
 	/*@-formatconst@*/
 	sprintf(val, formatPrefix, buf);
 	/*@=formatconst@*/
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -335,19 +342,21 @@ static int fsnamesTag( /*@unused@*/ Header h, /*@out@*/ int_32 * type,
 	/*@globals fileSystem, internalState @*/
 	/*@modifies *type, *data, *count, *freeData,
 		fileSystem, internalState @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     const char ** list;
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemList(&list, count)) {
 	return 1;
     }
+/*@=boundswrite@*/
 
-/*@-boundswrite@*/
     *type = RPM_STRING_ARRAY_TYPE;
     *((const char ***) data) = list;
 
     *freeData = 0;
-/*@=boundswrite@*/
 
     return 0; 
 }
@@ -362,28 +371,30 @@ static int fsnamesTag( /*@unused@*/ Header h, /*@out@*/ int_32 * type,
  * @return		0 on success
  */
 static int instprefixTag(Header h, /*@null@*/ /*@out@*/ rpmTagType * type,
-	/*@null@*/ /*@out@*/ const void ** data,
-	/*@null@*/ /*@out@*/ int_32 * count,
-	/*@null@*/ /*@out@*/ int * freeData)
-		/*@modifies *type, *data, *freeData @*/
+		/*@null@*/ /*@out@*/ const void ** data,
+		/*@null@*/ /*@out@*/ int_32 * count,
+		/*@null@*/ /*@out@*/ int * freeData)
+	/*@modifies *type, *data, *freeData @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
     rpmTagType ipt;
     char ** array;
 
-/*@-boundswrite@*/
     if (hge(h, RPMTAG_INSTALLPREFIX, type, (void **)data, count)) {
 	if (freeData) *freeData = 0;
 	return 0;
     } else if (hge(h, RPMTAG_INSTPREFIXES, &ipt, (void **) &array, count)) {
+/*@-boundsread@*/
 	if (data) *data = xstrdup(array[0]);
+/*@=boundsread@*/
 	if (freeData) *freeData = 1;
 	if (type) *type = RPM_STRING_TYPE;
 	array = hfd(array, ipt);
 	return 0;
     }
-/*@=boundswrite@*/
 
     return 1;
 }
@@ -404,6 +415,8 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
 		fileSystem, internalState @*/
 	/*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext,
 		fileSystem, internalState @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     const char ** filenames;
@@ -419,11 +432,12 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
 	rpmBuildFileList(h, &filenames, &numFiles);
     }
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemList(NULL, count)) {
 	return 1;
     }
+/*@=boundswrite@*/
 
-/*@-boundswrite@*/
     *type = RPM_INT32_TYPE;
     *freeData = 1;
 
@@ -434,11 +448,12 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
 	return 0;
     }
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemUsage(filenames, filesizes, numFiles, &usages, 0))	
 	return 1;
+/*@=boundswrite@*/
 
     *data = usages;
-/*@=boundswrite@*/
 
     filenames = _free(filenames);
 
@@ -454,11 +469,13 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
  * @retval freeData	address of data-was-malloc'ed indicator
  * @return		0 on success
  */
-/*@-bounds@*/
+/*@-bounds@*/	/* LCL: segfault */
 static int triggercondsTag(Header h, /*@out@*/ rpmTagType * type,
-	/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-	/*@out@*/ int * freeData)
-		/*@modifies *type, *data, *count, *freeData @*/
+		/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+		/*@out@*/ int * freeData)
+	/*@modifies *type, *data, *count, *freeData @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -529,11 +546,12 @@ static int triggercondsTag(Header h, /*@out@*/ rpmTagType * type,
  * @retval freeData	address of data-was-malloc'ed indicator
  * @return		0 on success
  */
-/*@-bounds@*/
 static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
-	/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-	/*@out@*/ int * freeData)
-		/*@modifies *type, *data, *count, *freeData @*/
+		/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+		/*@out@*/ int * freeData)
+	/*@modifies *type, *data, *count, *freeData @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -574,7 +592,6 @@ static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
 
     return 0;
 }
-/*@=bounds@*/
 
 /**
  * Retrieve file paths.
@@ -586,18 +603,18 @@ static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
  * @return		0 on success
  */
 static int filenamesTag(Header h, /*@out@*/ rpmTagType * type,
-	/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-	/*@out@*/ int * freeData)
-		/*@modifies *type, *data, *count, *freeData @*/
+		/*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+		/*@out@*/ int * freeData)
+	/*@modifies *type, *data, *count, *freeData @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     *type = RPM_STRING_ARRAY_TYPE;
 
     rpmBuildFileList(h, (const char ***) data, count);
-/*@-boundswrite@*/
     *freeData = 1;
 
     *freeData = 0;	/* XXX WTFO? */
-/*@=boundswrite@*/
 
     return 0; 
 }
@@ -630,17 +647,17 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
 		/*@out@*/ int * freeData)
 	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     char * dstring = rpmExpand(_macro_i18ndomains, NULL);
     int rc;
 
-/*@-boundswrite@*/
     *type = RPM_STRING_TYPE;
     *data = NULL;
     *count = 0;
     *freeData = 0;
-/*@=boundswrite@*/
 
     if (dstring && *dstring) {
 	char *domain, *de;
@@ -679,14 +696,12 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
 	    unsetenv(language);
 /*@i@*/	++_nl_msg_cat_cntr;
 
-/*@-boundswrite@*/
 	if (domain && msgid) {
 	    *data = /*@-unrecog@*/ dgettext(domain, msgid) /*@=unrecog@*/;
 	    *data = xstrdup(*data);	/* XXX xstrdup has side effects. */
 	    *count = 1;
 	    *freeData = 1;
 	}
-/*@=boundswrite@*/
 	dstring = _free(dstring);
 	if (*data)
 	    return 0;
@@ -696,7 +711,6 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
 
     rc = hge(h, tag, type, (void **)data, count);
 
-/*@-boundswrite@*/
     if (rc && (*data) != NULL) {
 	*data = xstrdup(*data);
 	*freeData = 1;
@@ -706,7 +720,6 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
     *freeData = 0;
     *data = NULL;
     *count = 0;
-/*@=boundswrite@*/
     return 1;
 }
 
@@ -724,6 +737,8 @@ static int summaryTag(Header h, /*@out@*/ rpmTagType * type,
 		/*@out@*/ int * freeData)
 	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_SUMMARY, type, data, count, freeData);
 }
@@ -742,6 +757,8 @@ static int descriptionTag(Header h, /*@out@*/ rpmTagType * type,
 		/*@out@*/ int * freeData)
 	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_DESCRIPTION, type, data, count, freeData);
 }
@@ -760,6 +777,8 @@ static int groupTag(Header h, /*@out@*/ rpmTagType * type,
 		/*@out@*/ int * freeData)
 	/*@globals rpmGlobalMacroContext @*/
 	/*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+	/*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+		/\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_GROUP, type, data, count, freeData);
 }
@@ -788,4 +807,3 @@ const struct headerSprintfExtension_s rpmHeaderFormats[] = {
     { HEADER_EXT_MORE, NULL, { (void *) headerDefaultFormats } }
 } ;
 /*@=type@*/
-/*@=boundsread@*/
diff --git a/lib/fs.c b/lib/fs.c
index 0a5fcbbe1..9976f14a3 100644
--- a/lib/fs.c
+++ b/lib/fs.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /*@-mods@*/
 /**
  * \file lib/fs.c
@@ -174,7 +173,9 @@ static int getFilesystemList(void)
 	    /*@-modunconnomods -moduncon @*/
 	    our_mntent * itemptr = getmntent(mtab);
 	    if (!itemptr) break;
+/*@-boundsread@*/
 	    item = *itemptr;	/* structure assignment */
+/*@=boundsread@*/
 	    mntdir = item.our_mntdir;
 #if defined(MNTOPT_RO)
 	    /*@-compdef@*/
@@ -270,10 +271,12 @@ int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes, int numFiles
     sourceDir = rpmGetPath("%{_sourcedir}", NULL);
 
     maxLen = strlen(sourceDir);
+/*@-boundsread@*/
     for (i = 0; i < numFiles; i++) {
 	len = strlen(fileList[i]);
 	if (maxLen < len) maxLen = len;
     }
+/*@=boundsread@*/
     
 /*@-boundswrite@*/
     buf = alloca(maxLen + 1);
@@ -355,4 +358,3 @@ int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes, int numFiles
 }
 /*@=usereleased =onlytrans@*/
 /*@=mods@*/
-/*@=boundsread@*/
diff --git a/lib/fsm.c b/lib/fsm.c
index 9b419222f..f4fe24b4f 100644
--- a/lib/fsm.c
+++ b/lib/fsm.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup payload
  * \file lib/fsm.c
  * File state machine to handle a payload from a package.
@@ -161,6 +160,7 @@ static int mapNextIterator(/*@null@*/ void * a)
 
 /** \ingroup payload
  */
+/*@-boundsread@*/
 static int cpioStrCmp(const void * a, const void * b)
 	/*@*/
 {
@@ -177,6 +177,7 @@ static int cpioStrCmp(const void * a, const void * b)
 
     return strcmp(afn, bfn);
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Locate archive path in file info.
@@ -184,6 +185,7 @@ static int cpioStrCmp(const void * a, const void * b)
  * @param fsmPath	archive path
  * @return		index into file info, -1 if archive path was not found
  */
+/*@-boundsread@*/
 static int mapFind(/*@null@*/ FSMI_t iter, const char * fsmPath)
 	/*@modifies iter @*/
 {
@@ -207,6 +209,7 @@ static int mapFind(/*@null@*/ FSMI_t iter, const char * fsmPath)
     }
     return ix;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Directory name iterator.
@@ -256,6 +259,7 @@ static inline int dnlIndex(const DNLI_t dnli)
  * @param reverse	traverse directory names in reverse order?
  * @return		directory name iterator
  */
+/*@-boundsread@*/
 /*@-usereleased@*/
 static /*@only@*/ void * dnlInitIterator(/*@special@*/ const FSM_t fsm,
 		int reverse)
@@ -338,12 +342,14 @@ static /*@only@*/ void * dnlInitIterator(/*@special@*/ const FSM_t fsm,
     return dnli;
 }
 /*@=usereleased@*/
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Return next directory name (from file info).
  * @param dnli		directory name iterator
  * @return		next directory name
  */
+/*@-boundsread@*/
 static /*@observer@*/ const char * dnlNextIterator(/*@null@*/ DNLI_t dnli)
 	/*@modifies dnli @*/
 {
@@ -366,12 +372,14 @@ static /*@observer@*/ const char * dnlNextIterator(/*@null@*/ DNLI_t dnli)
     }
     return dn;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Save hard link in chain.
  * @param fsm		file state machine data
  * @return		Is chain only partially filled?
  */
+/*@-boundsread@*/
 static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
 	/*@uses fsm->links, fsm->ix, fsm->sb, fsm->goal, fsm->nsuffix @*/
 	/*@defines fsm->li @*/
@@ -460,6 +468,7 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
     rc = fsmStage(fsm, FSM_MAP);
     return rc;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Destroy set of hard links.
@@ -588,6 +597,7 @@ int fsmMapPath(FSM_t fsm)
     i = fsm->ix;
     if (fi && i >= 0 && i < fi->fc) {
 
+/*@-boundsread@*/
 	fsm->astriplen = fi->astriplen;
 	fsm->action = (fi->actions ? fi->actions[i] : fi->action);
 	fsm->fflags = (fi->fflags ? fi->fflags[i] : fi->flags);
@@ -596,6 +606,7 @@ int fsmMapPath(FSM_t fsm)
 	/* src rpms have simple base name in payload. */
 	fsm->dirName = fi->dnl[fi->dil[i]];
 	fsm->baseName = fi->bnl[i];
+/*@=boundsread@*/
 
 /*@-boundswrite@*/
 	switch (fsm->action) {
@@ -985,6 +996,7 @@ static int writeLinkedFile(/*@special@*/ FSM_t fsm)
  * @param fsm		file state machine data
  * @return		0 on success
  */
+/*@-boundsread@*/
 static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 	/*@uses fsm->path, fsm->opath, fsm->nsuffix, fsm->ix, fsm->li @*/
 	/*@globals fileSystem@*/
@@ -1042,6 +1054,7 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
     fsm->opath = opath;
     return ec;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Commit hard linked file set atomically.
@@ -1296,6 +1309,7 @@ static int fsmStat(FSM_t fsm)
 	((_x)[sizeof("/dev/log")-1] == '\0' || \
 	 (_x)[sizeof("/dev/log")-1] == ';'))
 
+/*@-boundsread@*/
 /*@-compmempass@*/
 int fsmStage(FSM_t fsm, fileStage stage)
 {
@@ -2253,6 +2267,7 @@ if (!(fsm->mapFlags & CPIO_ALL_HARDLINKS)) break;
     return rc;
 }
 /*@=compmempass@*/
+/*@=boundsread@*/
 
 /*@obserever@*/ const char *const fileActionString(fileAction a)
 {
@@ -2338,4 +2353,3 @@ if (!(fsm->mapFlags & CPIO_ALL_HARDLINKS)) break;
     }
     /*@noteached@*/
 }
-/*@=boundsread@*/
diff --git a/lib/misc.c b/lib/misc.c
index b9231c6ac..21f196d6c 100644
--- a/lib/misc.c
+++ b/lib/misc.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /**
  * \file lib/misc.c
  */
@@ -462,4 +461,3 @@ int rpmHeaderGetEntry(Header h, int_32 tag, int_32 *type,
     }
     /*@notreached@*/
 }
-/*@=boundsread@*/
diff --git a/lib/package.c b/lib/package.c
index 96bee8962..a2d3e116c 100644
--- a/lib/package.c
+++ b/lib/package.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup header
  * \file lib/package.c
  */
@@ -169,8 +168,10 @@ static int rpmtsStashKeyid(rpmts ts)
 
     if (keyids != NULL)
     for (i = 0; i < nkeyids; i++) {
+/*@-boundsread@*/
 	if (keyid == keyids[i])
 	    return 1;
+/*@=boundsread@*/
     }
 
     keyids = xrealloc(keyids, (nkeyids + 1) * sizeof(*keyids));
@@ -216,11 +217,13 @@ int rpmReadPackageFile(rpmts ts, FD_t fd,
 	goto exit;
     }
 
+/*@-boundsread@*/
     if (l->magic[0] != RPMLEAD_MAGIC0 || l->magic[1] != RPMLEAD_MAGIC1
      || l->magic[2] != RPMLEAD_MAGIC2 || l->magic[3] != RPMLEAD_MAGIC3) {
 	rc = RPMRC_NOTFOUND;
 	goto exit;
     }
+/*@=boundsread@*/
 
     switch (l->major) {
     case 1:
@@ -469,4 +472,3 @@ exit:
     sig = rpmFreeSignature(sig);
     return rc;
 }
-/*@=boundsread@*/
diff --git a/lib/poptALL.c b/lib/poptALL.c
index 5e2f7391a..221409db9 100644
--- a/lib/poptALL.c
+++ b/lib/poptALL.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmcli
  * \file lib/poptALL.c
  *  Popt tables for all rpm modes.
@@ -224,10 +223,10 @@ rpmcliInit(int argc, char *const argv[], struct poptOption * optionsTable)
 /*@=globs =mods@*/
 
 #if !defined(__LCLINT__)
-    (void)setlocale(LC_ALL, "" );
+    (void) setlocale(LC_ALL, "" );
 
-    (void)bindtextdomain(PACKAGE, LOCALEDIR);
-    (void)textdomain(PACKAGE);
+    (void) bindtextdomain(PACKAGE, LOCALEDIR);
+    (void) textdomain(PACKAGE);
 #endif
 
     rpmSetVerbosity(RPMMESS_NORMAL);
@@ -280,5 +279,3 @@ rpmcliInit(int argc, char *const argv[], struct poptOption * optionsTable)
     return optCon;
 }
 /*@=globstate@*/
-
-/*@=boundsread@*/
diff --git a/lib/poptI.c b/lib/poptI.c
index 13736dedb..ecf82adc7 100644
--- a/lib/poptI.c
+++ b/lib/poptI.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmcli
  * \file lib/poptI.c
  *  Popt tables for install modes.
@@ -244,4 +243,3 @@ struct poptOption rpmInstallPoptTable[] = {
    POPT_TABLEEND
 };
 /*@=bitwisesigned =compmempass @*/
-/*@=boundsread@*/
diff --git a/lib/poptQV.c b/lib/poptQV.c
index e0cb20d74..3b5e25fea 100644
--- a/lib/poptQV.c
+++ b/lib/poptQV.c
@@ -1,4 +1,3 @@
-/*@-bounds@*/
 /** \ingroup rpmcli
  * \file lib/poptQV.c
  *  Popt tables for query/verify modes.
@@ -161,7 +160,9 @@ static void queryArgCallback(/*@unused@*/poptContext con,
 	    if (qf) {
 		int len = strlen(qf) + strlen(arg) + 1;
 		qf = xrealloc(qf, len);
+/*@-boundswrite@*/
 		strcat(qf, arg);
+/*@=boundswrite@*/
 	    } else {
 		qf = xmalloc(strlen(arg) + 1);
 		strcpy(qf, arg);
@@ -313,4 +314,3 @@ struct poptOption rpmSignPoptTable[] = {
 
    POPT_TABLEEND
 };
-/*@=bounds@*/
diff --git a/lib/psm.c b/lib/psm.c
index cfc46d763..e90beacba 100644
--- a/lib/psm.c
+++ b/lib/psm.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts payload
  * \file lib/psm.c
  * Package state machine to handle a package from a transaction set.
@@ -68,10 +67,12 @@ int rpmVersionCompare(Header first, Header second)
     else if (!epochOne && epochTwo)
 	return -1;
     else if (epochOne && epochTwo) {
+/*@-boundsread@*/
 	if (*epochOne < *epochTwo)
 	    return -1;
 	else if (*epochOne > *epochTwo)
 	    return 1;
+/*@=boundsread@*/
     }
 
     rc = headerGetEntry(first, RPMTAG_VERSION, NULL, (void **) &one, NULL);
@@ -139,7 +140,9 @@ static int rpmInstallLoadMacros(rpmfi fi, Header h)
 	    continue;
 	switch (type) {
 	case RPM_INT32_TYPE:
+/*@-boundsread@*/
 	    sprintf(numbuf, "%d", *body.i32p);
+/*@=boundsread@*/
 	    addMacro(NULL, tagm->macroname, NULL, numbuf, -1);
 	    /*@switchbreak@*/ break;
 	case RPM_STRING_TYPE:
@@ -1932,4 +1935,3 @@ fprintf(stderr, "*** PSM_RDB_LOAD: header #%u not found\n", fi->record);
     /*@=nullstate@*/
 }
 /*@=nullpass@*/
-/*@=boundsread@*/
diff --git a/lib/rpmlib.h b/lib/rpmlib.h
index 5b1346809..c3b685fd3 100644
--- a/lib/rpmlib.h
+++ b/lib/rpmlib.h
@@ -1011,10 +1011,14 @@ void freeFilesystems(void)
  * @retval num			address of number of file systems (or NULL)
  * @return			0 on success, 1 on error
  */
+/*@-incondefs@*/
 int rpmGetFilesystemList( /*@null@*/ /*@out@*/ const char *** listptr,
 		/*@null@*/ /*@out@*/ int * num)
 	/*@globals fileSystem, internalState @*/
-	/*@modifies *listptr, *num, fileSystem, internalState @*/;
+	/*@modifies *listptr, *num, fileSystem, internalState @*/
+	/*@requires maxSet(listptr) >= 0 /\ maxSet(num) >= 0 @*/
+	/*@ensures maxRead(num) == 0 @*/;
+/*@=incondefs@*/
 
 /**
  * Determine per-file system usage for a list of files.
@@ -1025,13 +1029,18 @@ int rpmGetFilesystemList( /*@null@*/ /*@out@*/ const char *** listptr,
  * @param flags			(unused)
  * @return			0 on success, 1 on error
  */
+/*@-incondefs@*/
 int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes,
 		int numFiles, /*@null@*/ /*@out@*/ uint_32 ** usagesPtr,
 		int flags)
 	/*@globals rpmGlobalMacroContext,
 		fileSystem, internalState @*/
 	/*@modifies *usagesPtr, rpmGlobalMacroContext,
-		fileSystem, internalState @*/;
+		fileSystem, internalState @*/
+	/*@requires maxSet(fileList) >= 0 /\ maxSet(fssizes) == 0
+		/\ maxSet(usagesPtr) >= 0 @*/
+	/*@ensures maxRead(usagesPtr) == 0 @*/;
+/*@=incondefs@*/
 
 /* ==================================================================== */
 /** \name RPMEIU */
diff --git a/lib/transaction.c b/lib/transaction.c
index 3e17e0b96..6ae79dead 100644
--- a/lib/transaction.c
+++ b/lib/transaction.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts
  * \file lib/transaction.c
  */
@@ -83,6 +82,7 @@ static int sharedCmp(const void * one, const void * two)
 
 /**
  */
+/*@-boundsread@*/
 static fileAction decideFileFate(const rpmts ts,
 		const rpmfi ofi, rpmfi nfi)
 	/*@globals fileSystem @*/
@@ -177,9 +177,11 @@ static fileAction decideFileFate(const rpmts ts,
      */
     return save;
 }
+/*@=boundsread@*/
 
 /**
  */
+/*@-boundsread@*/
 static int filecmp(rpmfi afi, rpmfi bfi)
 	/*@*/
 {
@@ -210,6 +212,7 @@ static int filecmp(rpmfi afi, rpmfi bfi)
 
     return 0;
 }
+/*@=boundsread@*/
 
 /**
  */
@@ -1483,4 +1486,3 @@ fi->actions = actions;
 	return 0;
     /*@=nullstate@*/
 }
-/*@=boundsread@*/