Remove splint tags.

23 files changed, 278 insertions, 1237 deletions

diff --git a/build/build.c b/build/build.c
index 697de5164..35162a075 100644
--- a/build/build.c
+++ b/build/build.c
@@ -10,18 +10,11 @@
 
 #include "debug.h"
 
-/*@unchecked@*/
 static int _build_debug = 0;
 
-/*@access StringBuf @*/
-/*@access urlinfo @*/		/* XXX compared with NULL */
-/*@access FD_t @*/
-
 /**
  */
 static void doRmSource(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     struct Source *p;
     Package pkg;
@@ -77,7 +70,6 @@ int doScript(Spec spec, int what, const char *name, StringBuf sb, int test)
     int status;
     int rc;
     
-    /*@-branchstate@*/
     switch (what) {
     case RPMBUILD_PREP:
 	name = "%prep";
@@ -129,7 +121,6 @@ int doScript(Spec spec, int what, const char *name, StringBuf sb, int test)
     }
     if (name == NULL)	/* XXX shouldn't happen */
 	name = "???";
-    /*@=branchstate@*/
 
     if ((what != RPMBUILD_RMBUILD) && sb == NULL) {
 	rc = 0;
@@ -153,24 +144,19 @@ int doScript(Spec spec, int what, const char *name, StringBuf sb, int test)
     }
 #endif
 
-    /*@-branchstate@*/
     if (fdGetFp(fd) == NULL)
 	xfd = Fdopen(fd, "w.fpio");
     else
 	xfd = fd;
-    /*@=branchstate@*/
 
-    /*@-type@*/ /* FIX: cast? */
+    /* FIX: cast? */
     if ((fp = fdGetFp(xfd)) == NULL) {
 	rc = RPMERR_SCRIPT;
 	goto exit;
     }
-    /*@=type@*/
     
     (void) urlPath(rootURL, &rootDir);
-    /*@-branchstate@*/
     if (*rootDir == '\0') rootDir = "/";
-    /*@=branchstate@*/
 
     (void) urlPath(scriptName, &buildScript);
 
@@ -199,13 +185,11 @@ int doScript(Spec spec, int what, const char *name, StringBuf sb, int test)
     
 if (_build_debug)
 fprintf(stderr, "*** rootURL %s buildDirURL %s\n", rootURL, buildDirURL);
-/*@-boundsread@*/
     if (buildDirURL && buildDirURL[0] != '/' &&
 	(urlSplit(buildDirURL, &u) != 0)) {
 	rc = RPMERR_SCRIPT;
 	goto exit;
     }
-/*@=boundsread@*/
     if (u != NULL) {
 	switch (u->urltype) {
 	case URL_IS_HTTPS:
@@ -233,12 +217,8 @@ fprintf(stderr, "*** addMacros\n");
     rpmMessage(RPMMESS_NORMAL, _("Executing(%s): %s\n"), name, buildCmd);
     if (!(child = fork())) {
 
-	/*@-mods@*/
 	errno = 0;
-	/*@=mods@*/
-/*@-boundsread@*/
 	(void) execvp(argv[0], (char *const *)argv);
-/*@=boundsread@*/
 
 	rpmError(RPMERR_SCRIPT, _("Exec of %s failed (%s): %s\n"),
 		scriptName, name, strerror(errno));
@@ -300,14 +280,12 @@ int buildSpec(rpmts ts, Spec spec, int what, int test)
 	/* packaging on the first run, and skip RMSOURCE altogether */
 	if (spec->BASpecs != NULL)
 	for (x = 0; x < spec->BACount; x++) {
-/*@-boundsread@*/
 	    if ((rc = buildSpec(ts, spec->BASpecs[x],
 				(what & ~RPMBUILD_RMSOURCE) |
 				(x ? 0 : (what & RPMBUILD_PACKAGESOURCE)),
 				test))) {
 		goto exit;
 	    }
-/*@=boundsread@*/
 	}
     } else {
 	if ((what & RPMBUILD_PREP) &&
diff --git a/build/buildio.h b/build/buildio.h
index f3641fa33..3e45140f6 100644
--- a/build/buildio.h
+++ b/build/buildio.h
@@ -12,12 +12,10 @@
 
 /**
  */
-typedef /*@abstract@*/ struct cpioSourceArchive_s {
+typedef struct cpioSourceArchive_s {
     unsigned int cpioArchiveSize;
     FD_t	cpioFdIn;
-/*@refcounted@*/ /*@relnull@*/
     rpmfi	cpioList;
-/*@only@*/
     struct rpmlead * lead;	/* XXX FIXME: exorcize lead/arch/os */
 } * CSA_t;
 
@@ -34,15 +32,11 @@ extern "C" {
  * @param csa
  * @return		0 on success
  */
-/*@unused@*/ int readRPM(/*@null@*/ const char * fileName,
-		/*@out@*/ Spec * specp,
-		/*@out@*/ struct rpmlead * lead,
-		/*@out@*/ Header * sigs,
-		CSA_t csa)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies *specp, *lead, *sigs, csa, csa->cpioFdIn,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int readRPM(const char * fileName,
+		Spec * specp,
+		struct rpmlead * lead,
+		Header * sigs,
+		CSA_t csa);
 
 /**
  * Write rpm package to file.
@@ -59,16 +53,12 @@ extern "C" {
  * @retval cookie	generated cookie (i.e build host/time)
  * @return		0 on success
  */
-int writeRPM(Header * hdrp, /*@null@*/ unsigned char ** pkgidp,
+int writeRPM(Header * hdrp, unsigned char ** pkgidp,
 		const char * fileName,
 		int type,
 		CSA_t csa,
-		/*@null@*/ char * passPhrase,
-		/*@out@*/ const char ** cookie)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies *hdrp, *pkgidp, *cookie, csa, csa->cpioArchiveSize,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+		char * passPhrase,
+		const char ** cookie);
 
 #ifdef __cplusplus
 }
diff --git a/build/expression.c b/build/expression.c
index dd407d75e..012ee2b4b 100644
--- a/build/expression.c
+++ b/build/expression.c
@@ -41,7 +41,6 @@ typedef struct _value {
 /**
  */
 static Value valueMakeInteger(int i)
-	/*@*/
 {
   Value v;
 
@@ -53,8 +52,7 @@ static Value valueMakeInteger(int i)
 
 /**
  */
-static Value valueMakeString(/*@only@*/ const char *s)
-	/*@*/
+static Value valueMakeString(const char *s)
 {
   Value v;
 
@@ -66,8 +64,7 @@ static Value valueMakeString(/*@only@*/ const char *s)
 
 /**
  */
-static void valueFree( /*@only@*/ Value v)
-	/*@modifies v @*/
+static void valueFree( Value v)
 {
   if (v) {
     if (v->type == VALUE_TYPE_STRING)
@@ -78,7 +75,6 @@ static void valueFree( /*@only@*/ Value v)
 
 #ifdef DEBUG_PARSER
 static void valueDump(const char *msg, Value v, FILE *fp)
-	/*@*/
 {
   if (msg)
     fprintf(fp, "%s ", msg);
@@ -101,12 +97,9 @@ static void valueDump(const char *msg, Value v, FILE *fp)
  * Parser state.
  */
 typedef struct _parseState {
-/*@owned@*/
     char *str;		/*!< expression string */
-/*@dependent@*/
     char *p;		/*!< current position in expression string */
     int nextToken;	/*!< current lookahead token */
-/*@relnull@*/
     Value tokenValue;	/*!< valid when TOK_INTEGER or TOK_STRING */
     Spec spec;		/*!< spec file that we are parsing inside of */
 } *ParseState;
@@ -115,7 +108,6 @@ typedef struct _parseState {
 /**
  * \name Parser tokens
  */
-/*@{*/
 #define TOK_EOF          1
 #define TOK_INTEGER      2
 #define TOK_STRING       3
@@ -135,7 +127,6 @@ typedef struct _parseState {
 #define TOK_NOT         17
 #define TOK_LOGICAL_AND 18
 #define TOK_LOGICAL_OR  19
-/*@}*/
 
 #define	EXPRBUFSIZ	BUFSIZ
 
@@ -169,7 +160,6 @@ ETTE_t exprTokTable[] = {
 };
 
 static const char *prToken(int val)
-	/*@*/
 {
     ETTE_t *et;
     
@@ -184,11 +174,7 @@ static const char *prToken(int val)
 /**
  * @param state		expression parser state
  */
-/*@-boundswrite@*/
 static int rdToken(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   int token;
   Value v = NULL;
@@ -321,28 +307,18 @@ static int rdToken(ParseState state)
 
   return 0;
 }
-/*@=boundswrite@*/
 
-/*@null@*/
-static Value doLogical(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/;
+static Value doLogical(ParseState state);
 
 /**
  * @param state		expression parser state
  */
-/*@null@*/
 static Value doPrimary(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   Value v;
 
   DEBUG(printf("doPrimary()\n"));
 
-  /*@-branchstate@*/
   switch (state->nextToken) {
   case TOK_OPEN_P:
     if (rdToken(state))
@@ -405,9 +381,8 @@ static Value doPrimary(ParseState state)
     break;
   default:
     return NULL;
-    /*@notreached@*/ break;
+    break;
   }
-  /*@=branchstate@*/
 
   DEBUG(valueDump("doPrimary:", v, stdout));
   return v;
@@ -416,11 +391,7 @@ static Value doPrimary(ParseState state)
 /**
  * @param state		expression parser state
  */
-/*@null@*/
 static Value doMultiplyDivide(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   Value v1, v2 = NULL;
 
@@ -430,7 +401,6 @@ static Value doMultiplyDivide(ParseState state)
   if (v1 == NULL)
     return NULL;
 
-  /*@-branchstate@*/
   while (state->nextToken == TOK_MULTIPLY
 	 || state->nextToken == TOK_DIVIDE) {
     int op = state->nextToken;
@@ -462,7 +432,6 @@ static Value doMultiplyDivide(ParseState state)
       return NULL;
     }
   }
-  /*@=branchstate@*/
 
   if (v2) valueFree(v2);
   return v1;
@@ -471,12 +440,7 @@ static Value doMultiplyDivide(ParseState state)
 /**
  * @param state		expression parser state
  */
-/*@-boundswrite@*/
-/*@null@*/
 static Value doAddSubtract(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   Value v1, v2 = NULL;
 
@@ -486,7 +450,6 @@ static Value doAddSubtract(ParseState state)
   if (v1 == NULL)
     return NULL;
 
-  /*@-branchstate@*/
   while (state->nextToken == TOK_ADD || state->nextToken == TOK_MINUS) {
     int op = state->nextToken;
 
@@ -527,21 +490,15 @@ static Value doAddSubtract(ParseState state)
       v1 = valueMakeString(copy);
     }
   }
-  /*@=branchstate@*/
 
   if (v2) valueFree(v2);
   return v1;
 }
-/*@=boundswrite@*/
 
 /**
  * @param state		expression parser state
  */
-/*@null@*/
 static Value doRelational(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   Value v1, v2 = NULL;
 
@@ -551,7 +508,6 @@ static Value doRelational(ParseState state)
   if (v1 == NULL)
     return NULL;
 
-  /*@-branchstate@*/
   while (state->nextToken >= TOK_EQ && state->nextToken <= TOK_GE) {
     int op = state->nextToken;
 
@@ -574,24 +530,24 @@ static Value doRelational(ParseState state)
       switch (op) {
       case TOK_EQ:
 	r = (i1 == i2);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_NEQ:
 	r = (i1 != i2);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_LT:
 	r = (i1 < i2);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_LE:
 	r = (i1 <= i2);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_GT:
 	r = (i1 > i2);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_GE:
 	r = (i1 >= i2);
-	/*@switchbreak@*/ break;
+	break;
       default:
-	/*@switchbreak@*/ break;
+	break;
       }
       valueFree(v1);
       v1 = valueMakeInteger(r);
@@ -602,30 +558,29 @@ static Value doRelational(ParseState state)
       switch (op) {
       case TOK_EQ:
 	r = (strcmp(s1,s2) == 0);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_NEQ:
 	r = (strcmp(s1,s2) != 0);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_LT:
 	r = (strcmp(s1,s2) < 0);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_LE:
 	r = (strcmp(s1,s2) <= 0);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_GT:
 	r = (strcmp(s1,s2) > 0);
-	/*@switchbreak@*/ break;
+	break;
       case TOK_GE:
 	r = (strcmp(s1,s2) >= 0);
-	/*@switchbreak@*/ break;
+	break;
       default:
-	/*@switchbreak@*/ break;
+	break;
       }
       valueFree(v1);
       v1 = valueMakeInteger(r);
     }
   }
-  /*@=branchstate@*/
 
   if (v2) valueFree(v2);
   return v1;
@@ -635,9 +590,6 @@ static Value doRelational(ParseState state)
  * @param state		expression parser state
  */
 static Value doLogical(ParseState state)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies state->nextToken, state->p, state->tokenValue,
-		rpmGlobalMacroContext @*/
 {
   Value v1, v2 = NULL;
 
@@ -647,7 +599,6 @@ static Value doLogical(ParseState state)
   if (v1 == NULL)
     return NULL;
 
-  /*@-branchstate@*/
   while (state->nextToken == TOK_LOGICAL_AND
 	 || state->nextToken == TOK_LOGICAL_OR) {
     int op = state->nextToken;
@@ -679,7 +630,6 @@ static Value doLogical(ParseState state)
       return NULL;
     }
   }
-  /*@=branchstate@*/
 
   if (v2) valueFree(v2);
   return v1;
@@ -721,9 +671,7 @@ int parseExpressionBoolean(Spec spec, const char *expr)
     result = v->data.i != 0;
     break;
   case VALUE_TYPE_STRING:
-/*@-boundsread@*/
     result = v->data.s[0] != '\0';
-/*@=boundsread@*/
     break;
   default:
     break;
@@ -765,7 +713,6 @@ char * parseExpressionString(Spec spec, const char *expr)
 
   DEBUG(valueDump("parseExprString:", v, stdout));
 
-  /*@-branchstate@*/
   switch (v->type) {
   case VALUE_TYPE_INTEGER: {
     char buf[128];
@@ -778,7 +725,6 @@ char * parseExpressionString(Spec spec, const char *expr)
   default:
     break;
   }
-  /*@=branchstate@*/
 
   state.str = _free(state.str);
   valueFree(v);
diff --git a/build/files.c b/build/files.c
index 25adeac07..9aac1dbae 100644
--- a/build/files.c
+++ b/build/files.c
@@ -32,12 +32,6 @@
 #include "misc.h"
 #include "debug.h"
 
-/*@access Header @*/
-/*@access rpmfi @*/
-/*@access rpmte @*/
-/*@access FD_t @*/
-/*@access StringBuf @*/		/* compared with NULL */
-
 #define	SKIPWHITE(_x)	{while(*(_x) && (xisspace(*_x) || *(_x) == ',')) (_x)++;}
 #define	SKIPNONWHITE(_x){while(*(_x) &&!(xisspace(*_x) || *(_x) == ',')) (_x)++;}
 
@@ -73,52 +67,37 @@ typedef struct FileListRec_s {
 #define	fl_size	fl_st.st_size
 #define	fl_mtime fl_st.st_mtime
 
-/*@only@*/
     const char *diskURL;	/* get file from here       */
-/*@only@*/
     const char *fileURL;	/* filename in cpio archive */
-/*@observer@*/
     const char *uname;
-/*@observer@*/
     const char *gname;
     unsigned	flags;
     specdFlags	specdFlags;	/* which attributes have been explicitly specified. */
     unsigned	verifyFlags;
-/*@only@*/
     const char *langs;		/* XXX locales separated with | */
 } * FileListRec;
 
 /**
  */
 typedef struct AttrRec_s {
-/*@null@*/
     const char *ar_fmodestr;
-/*@null@*/
     const char *ar_dmodestr;
-/*@null@*/
     const char *ar_user;
-/*@null@*/
     const char *ar_group;
     mode_t	ar_fmode;
     mode_t	ar_dmode;
 } * AttrRec;
 
-/*@-readonlytrans@*/
-/*@unchecked@*/ /*@observer@*/
 static struct AttrRec_s root_ar = { NULL, NULL, "root", "root", 0, 0 };
-/*@=readonlytrans@*/
 
 /* list of files */
-/*@unchecked@*/ /*@only@*/ /*@null@*/
 static StringBuf check_fileList = NULL;
 
 /**
  * Package file tree walk data.
  */
 typedef struct FileList_s {
-/*@only@*/
     const char * buildRootURL;
-/*@only@*/
     const char * prefix;
 
     int fileCount;
@@ -143,7 +122,6 @@ typedef struct FileList_s {
     specdFlags defSpecdFlags;
     int defVerifyFlags;
     int nLangs;
-/*@only@*/ /*@null@*/
     const char ** currentLangs;
 
     /* Hard coded limit of MAXDOCDIR docdirs.         */
@@ -151,7 +129,6 @@ typedef struct FileList_s {
     const char * docDirs[MAXDOCDIR];
     int docDirCount;
     
-/*@only@*/
     FileListRec fileList;
     int fileListRecsAlloced;
     int fileListRecsUsed;
@@ -159,7 +136,7 @@ typedef struct FileList_s {
 
 /**
  */
-static void nullAttrRec(/*@out@*/ AttrRec ar)	/*@modifies ar @*/
+static void nullAttrRec(AttrRec ar)
 {
     ar->ar_fmodestr = NULL;
     ar->ar_dmodestr = NULL;
@@ -171,22 +148,19 @@ static void nullAttrRec(/*@out@*/ AttrRec ar)	/*@modifies ar @*/
 
 /**
  */
-static void freeAttrRec(AttrRec ar)	/*@modifies ar @*/
+static void freeAttrRec(AttrRec ar)
 {
     ar->ar_fmodestr = _free(ar->ar_fmodestr);
     ar->ar_dmodestr = _free(ar->ar_dmodestr);
     ar->ar_user = _free(ar->ar_user);
     ar->ar_group = _free(ar->ar_group);
     /* XXX doesn't free ar (yet) */
-    /*@-nullstate@*/
     return;
-    /*@=nullstate@*/
 }
 
 /**
  */
-static void dupAttrRec(const AttrRec oar, /*@in@*/ /*@out@*/ AttrRec nar)
-	/*@modifies nar @*/
+static void dupAttrRec(const AttrRec oar, AttrRec nar)
 {
     if (oar == nar)
 	return;
@@ -203,8 +177,6 @@ static void dupAttrRec(const AttrRec oar, /*@in@*/ /*@out@*/ AttrRec nar)
 /**
  */
 static void dumpAttrRec(const char * msg, AttrRec ar)
-	/*@globals fileSystem@*/
-	/*@modifies fileSystem @*/
 {
     if (msg)
 	fprintf(stderr, "%s:\t", msg);
@@ -220,10 +192,7 @@ static void dumpAttrRec(const char * msg, AttrRec ar)
  * @param s
  * @param delim
  */
-/*@-boundswrite@*/
-/*@null@*/
-static char *strtokWithQuotes(/*@null@*/ char *s, char *delim)
-	/*@modifies *s @*/
+static char *strtokWithQuotes(char *s, char *delim)
 {
     static char *olds = NULL;
     char *token;
@@ -258,17 +227,12 @@ static char *strtokWithQuotes(/*@null@*/ char *s, char *delim)
 	olds = s+1;
     }
 
-    /*@-retalias -temptrans @*/
     return token;
-    /*@=retalias =temptrans @*/
 }
-/*@=boundswrite@*/
 
 /**
  */
 static void timeCheck(int tc, Header h)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -281,27 +245,23 @@ static void timeCheck(int tc, Header h)
     x = hge(h, RPMTAG_OLDFILENAMES, &fnt, (void **) &files, &count);
     x = hge(h, RPMTAG_FILEMTIMES, NULL, (void **) &mtime, NULL);
     
-/*@-boundsread@*/
     for (x = 0; x < count; x++) {
 	if ((currentTime - mtime[x]) > tc)
 	    rpmMessage(RPMMESS_WARNING, _("TIMECHECK failure: %s\n"), files[x]);
     }
     files = hfd(files, fnt);
-/*@=boundsread@*/
 }
 
 /**
  */
 typedef struct VFA {
-/*@observer@*/ /*@null@*/ const char * attribute;
+const char * attribute;
     int not;
     int	flag;
 } VFA_t;
 
 /**
  */
-/*@-exportlocal -exportheadervar@*/
-/*@unchecked@*/
 VFA_t verifyAttrs[] = {
     { "md5",	0,	RPMVERIFY_MD5 },
     { "size",	0,	RPMVERIFY_FILESIZE },
@@ -313,7 +273,6 @@ VFA_t verifyAttrs[] = {
     { "rdev",	0,	RPMVERIFY_RDEV },
     { NULL, 0,	0 }
 };
-/*@=exportlocal =exportheadervar@*/
 
 /**
  * Parse %verify and %defverify from file manifest.
@@ -321,11 +280,7 @@ VFA_t verifyAttrs[] = {
  * @param fl		package file tree walk data
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int parseForVerify(char * buf, FileList fl)
-	/*@modifies buf, fl->processingFailed,
-		fl->currentVerifyFlags, fl->defVerifyFlags,
-		fl->currentSpecdFlags, fl->defSpecdFlags @*/
 {
     char *p, *pe, *q;
     const char *name;
@@ -387,9 +342,9 @@ static int parseForVerify(char * buf, FileList fl)
 	{   VFA_t *vfa;
 	    for (vfa = verifyAttrs; vfa->attribute != NULL; vfa++) {
 		if (strcmp(p, vfa->attribute))
-		    /*@innercontinue@*/ continue;
+		    continue;
 		verifyFlags |= vfa->flag;
-		/*@innerbreak@*/ break;
+		break;
 	    }
 	    if (vfa->attribute)
 		continue;
@@ -409,7 +364,6 @@ static int parseForVerify(char * buf, FileList fl)
 
     return 0;
 }
-/*@=boundswrite@*/
 
 #define	isAttrDefault(_ars)	((_ars)[0] == '-' && (_ars)[1] == '\0')
 
@@ -419,10 +373,7 @@ static int parseForVerify(char * buf, FileList fl)
  * @param fl		package file tree walk data
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int parseForDev(char * buf, FileList fl)
-	/*@modifies buf, fl->processingFailed,
-		fl->noGlob, fl->devtype, fl->devmajor, fl->devminor @*/
 {
     const char * name;
     const char * errstr = NULL;
@@ -474,12 +425,10 @@ static int parseForDev(char * buf, FileList fl)
 	{} ;
     if (*pe == '\0') {
 	fl->devmajor = atoi(p);
-	/*@-unsignedcompare @*/	/* LCL: ge is ok */
 	if (!(fl->devmajor >= 0 && fl->devmajor < 256)) {
 	    errstr = "devmajor";
 	    goto exit;
 	}
-	/*@=unsignedcompare @*/
 	pe++;
     } else {
 	errstr = "devmajor";
@@ -513,7 +462,6 @@ exit:
     }
     return rc;
 }
-/*@=boundswrite@*/
 
 /**
  * Parse %attr and %defattr from file manifest.
@@ -521,11 +469,7 @@ exit:
  * @param fl		package file tree walk data
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int parseForAttr(char * buf, FileList fl)
-	/*@modifies buf, fl->processingFailed,
-		fl->cur_ar, fl->def_ar,
-		fl->currentSpecdFlags, fl->defSpecdFlags @*/
 {
     const char *name;
     char *p, *pe, *q;
@@ -646,7 +590,6 @@ static int parseForAttr(char * buf, FileList fl)
     
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  * Parse %config from file manifest.
@@ -654,9 +597,7 @@ static int parseForAttr(char * buf, FileList fl)
  * @param fl		package file tree walk data
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int parseForConfig(char * buf, FileList fl)
-	/*@modifies buf, fl->processingFailed, fl->currentFlags @*/
 {
     char *p, *pe, *q;
     const char *name;
@@ -712,16 +653,12 @@ static int parseForConfig(char * buf, FileList fl)
 
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  */
 static int langCmp(const void * ap, const void * bp)
-	/*@*/
 {
-/*@-boundsread@*/
     return strcmp(*(const char **)ap, *(const char **)bp);
-/*@=boundsread@*/
 }
 
 /**
@@ -730,10 +667,7 @@ static int langCmp(const void * ap, const void * bp)
  * @param fl		package file tree walk data
  * @return		0 on success
  */
-/*@-bounds@*/
 static int parseForLang(char * buf, FileList fl)
-	/*@modifies buf, fl->processingFailed,
-		fl->currentLangs, fl->nLangs @*/
 {
     char *p, *pe, *q;
     const char *name;
@@ -793,7 +727,7 @@ static int parseForLang(char * buf, FileList fl)
 	if (fl->currentLangs != NULL)
 	for (i = 0; i < fl->nLangs; i++) {
 	    if (strncmp(fl->currentLangs[i], p, np))
-		/*@innercontinue@*/ continue;
+		continue;
 	    rpmError(RPMERR_BADSPEC, _("Duplicate locale %.*s in %%lang(%s)\n"),
 		(int)np, p, q);
 	    fl->processingFailed = 1;
@@ -817,14 +751,10 @@ static int parseForLang(char * buf, FileList fl)
 
     return 0;
 }
-/*@=bounds@*/
 
 /**
  */
-/*@-boundswrite@*/
-static int parseForRegexLang(const char * fileName, /*@out@*/ char ** lang)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies *lang, rpmGlobalMacroContext @*/
+static int parseForRegexLang(const char * fileName, char ** lang)
 {
     static int initialized = 0;
     static int hasRegex = 0;
@@ -863,12 +793,9 @@ static int parseForRegexLang(const char * fileName, /*@out@*/ char ** lang)
 	*lang = buf;
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  */
-/*@-exportlocal -exportheadervar@*/
-/*@unchecked@*/
 VFA_t virtualFileAttributes[] = {
 	{ "%dir",	0,	0 },	/* XXX why not RPMFILE_DIR? */
 	{ "%doc",	0,	RPMFILE_DOC },
@@ -889,7 +816,6 @@ VFA_t virtualFileAttributes[] = {
 
 	{ NULL, 0, 0 }
 };
-/*@=exportlocal =exportheadervar@*/
 
 /**
  * Parse simple attributes (e.g. %dir) from file manifest.
@@ -900,15 +826,8 @@ VFA_t virtualFileAttributes[] = {
  * @retval *fileName	file name
  * @return		0 on success
  */
-/*@-boundswrite@*/
-static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
-			  FileList fl, /*@out@*/ const char ** fileName)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies buf, fl->processingFailed, *fileName,
-		fl->currentFlags,
-		fl->docDirs, fl->docDirCount, fl->isDir,
-		fl->passedSpecialDoc, fl->isSpecialDoc,
-		pkg->specialDoc, rpmGlobalMacroContext @*/
+static int parseForSimple(Spec spec, Package pkg, char * buf,
+			  FileList fl, const char ** fileName)
 {
     char *s, *t;
     int res, specialDoc = 0;
@@ -943,7 +862,7 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
     {	VFA_t *vfa;
 	for (vfa = virtualFileAttributes; vfa->attribute != NULL; vfa++) {
 	    if (strcmp(s, vfa->attribute))
-		/*@innercontinue@*/ continue;
+		continue;
 	    if (!vfa->flag) {
 		if (!strcmp(s, "%dir"))
 		    fl->isDir = 1;	/* XXX why not RPMFILE_DIR? */
@@ -954,7 +873,7 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
 		    fl->currentFlags |= vfa->flag;
 	    }
 
-	    /*@innerbreak@*/ break;
+	    break;
 	}
 	/* if we got an attribute, continue with next token */
 	if (vfa->attribute != NULL)
@@ -969,7 +888,6 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
 	    res = 1;
 	}
 
-	/*@-branchstate@*/
 	if (*s != '/') {
 	    if (fl->currentFlags & RPMFILE_DOC) {
 		specialDoc = 1;
@@ -989,7 +907,6 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
 	} else {
 	    *fileName = s;
 	}
-	/*@=branchstate@*/
     }
 
     if (specialDoc) {
@@ -1032,9 +949,7 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
 		appendLineStringBuf(pkg->specialDoc, "rm -rf $DOCDIR");
 		appendLineStringBuf(pkg->specialDoc, RPM_MKDIR_P " $DOCDIR");
 
-		/*@-temptrans@*/
 		*fileName = buf;
-		/*@=temptrans@*/
 		fl->passedSpecialDoc = 1;
 		fl->isSpecialDoc = 1;
 	    }
@@ -1047,11 +962,10 @@ static int parseForSimple(/*@unused@*/Spec spec, Package pkg, char * buf,
 
     return res;
 }
-/*@=boundswrite@*/
 
 /**
  */
-static int compareFileListRecs(const void * ap, const void * bp)	/*@*/
+static int compareFileListRecs(const void * ap, const void * bp)	
 {
     const char *a = ((FileListRec)ap)->fileURL;
     const char *b = ((FileListRec)bp)->fileURL;
@@ -1064,7 +978,7 @@ static int compareFileListRecs(const void * ap, const void * bp)	/*@*/
  * @param fileName	file path
  * @return		1 if doc file, 0 if not
  */
-static int isDoc(FileList fl, const char * fileName)	/*@*/
+static int isDoc(FileList fl, const char * fileName)	
 {
     int x = fl->docDirCount;
     size_t k, l;
@@ -1085,7 +999,6 @@ static int isDoc(FileList fl, const char * fileName)	/*@*/
  * @return		1 if partial hardlink sets can exist, 0 otherwise.
  */
 static int checkHardLinks(FileList fl)
-	/*@*/
 {
     FileListRec ilp, jlp;
     int i, j;
@@ -1098,13 +1011,13 @@ static int checkHardLinks(FileList fl)
 	for (j = i + 1; j < fl->fileListRecsUsed; j++) {
 	    jlp = fl->fileList + j;
 	    if (!S_ISREG(jlp->fl_mode))
-		/*@innercontinue@*/ continue;
+		continue;
 	    if (ilp->fl_nlink != jlp->fl_nlink)
-		/*@innercontinue@*/ continue;
+		continue;
 	    if (ilp->fl_ino != jlp->fl_ino)
-		/*@innercontinue@*/ continue;
+		continue;
 	    if (ilp->fl_dev != jlp->fl_dev)
-		/*@innercontinue@*/ continue;
+		continue;
 	    return 1;
 	}
     }
@@ -1120,12 +1033,8 @@ static int checkHardLinks(FileList fl)
  * @param h
  * @param isSrc
  */
-/*@-bounds@*/
-static void genCpioListAndHeader(/*@partial@*/ FileList fl,
+static void genCpioListAndHeader(FileList fl,
 		rpmfi * fip, Header h, int isSrc)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies h, *fip, fl->processingFailed, fl->fileList,
-		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int _addDotSlash = !(isSrc || rpmExpandNumeric("%{_noPayloadPrefix}"));
     int apathlen = 0;
@@ -1218,7 +1127,6 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 	(void) headerAddOrAppendEntry(h, RPMTAG_OLDFILENAMES, RPM_STRING_ARRAY_TYPE,
 			       &(flp->fileURL), 1);
 
-/*@-sizeoftype@*/
       if (sizeof(flp->fl_size) != sizeof(uint_32)) {
 	uint_32 psize = (uint_32)flp->fl_size;
 	(void) headerAddOrAppendEntry(h, RPMTAG_FILESIZES, RPM_INT32_TYPE,
@@ -1271,7 +1179,6 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 	(void) headerAddOrAppendEntry(h, RPMTAG_FILEINODES, RPM_INT32_TYPE,
 				&(flp->fl_ino), 1);
       }
-/*@=sizeoftype@*/
 
 	(void) headerAddOrAppendEntry(h, RPMTAG_FILELANGS, RPM_STRING_ARRAY_TYPE,
 			       &(flp->langs),  1);
@@ -1350,9 +1257,7 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 
     if (fi == NULL) return;		/* XXX can't happen */
 
-/*@-onlytrans@*/
     fi->te = xcalloc(1, sizeof(*fi->te));
-/*@=onlytrans@*/
     fi->te->type = TR_ADDED;
 
     fi->dnl = _free(fi->dnl);
@@ -1364,11 +1269,10 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
     *d = '\0';
 
     fi->bnl = xmalloc(fi->fc * (sizeof(*fi->bnl) + sizeof(*fi->dil)));
-/*@-dependenttrans@*/ /* FIX: artifact of spoofing headerGetEntry */
+/* FIX: artifact of spoofing headerGetEntry */
     fi->dil = (!scareMem)
 	? xcalloc(sizeof(*fi->dil), fi->fc)
 	: (int *)(fi->bnl + fi->fc);
-/*@=dependenttrans@*/
 
     fi->apath = xmalloc(fi->fc * sizeof(*fi->apath) + apathlen + 1);
     a = (char *)(fi->apath + fi->fc);
@@ -1403,9 +1307,8 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 
 	/* Create disk directory and base name. */
 	fi->dil[i] = i;
-/*@-dependenttrans@*/ /* FIX: artifact of spoofing headerGetEntry */
+/* FIX: artifact of spoofing headerGetEntry */
 	fi->dnl[fi->dil[i]] = d;
-/*@=dependenttrans@*/
 	d = stpcpy(d, flp->diskURL);
 
 	/* Make room for the dirName NUL, find start of baseName. */
@@ -1417,9 +1320,7 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 	d += 2;		/* skip both dirname and basename NUL's */
 
 	/* Create archive path, normally adding "./" */
-	/*@-dependenttrans@*/	/* FIX: xstrdup? nah ... */
 	fi->apath[i] = a;
- 	/*@=dependenttrans@*/
 	if (_addDotSlash)
 	    a = stpcpy(a, "./");
 	a = stpcpy(a, (flp->fileURL + skipLen));
@@ -1436,22 +1337,17 @@ static void genCpioListAndHeader(/*@partial@*/ FileList fl,
 	    fi->fmapflags[i] |= CPIO_FOLLOW_SYMLINKS;
 
     }
-    /*@-branchstate -compdef@*/
     if (fip)
 	*fip = fi;
     else
 	fi = rpmfiFree(fi);
-    /*@=branchstate =compdef@*/
   }
 }
-/*@=bounds@*/
 
 /**
  */
-/*@-boundswrite@*/
-static /*@null@*/ FileListRec freeFileList(/*@only@*/ FileListRec fileList,
+static FileListRec freeFileList(FileListRec fileList,
 			int count)
-	/*@*/
 {
     while (count--) {
 	fileList[count].diskURL = _free(fileList[count].diskURL);
@@ -1461,17 +1357,9 @@ static /*@null@*/ FileListRec freeFileList(/*@only@*/ FileListRec fileList,
     fileList = _free(fileList);
     return NULL;
 }
-/*@=boundswrite@*/
 
 /* forward ref */
-static int recurseDir(FileList fl, const char * diskURL)
-	/*@globals check_fileList, rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies *fl, fl->processingFailed,
-		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
-		fl->totalFileSize, fl->fileCount, fl->inFtw, fl->isDir,
-		check_fileList, rpmGlobalMacroContext,
-		fileSystem, internalState @*/;
+static int recurseDir(FileList fl, const char * diskURL);
 
 /**
  * Add a file to the package manifest.
@@ -1480,16 +1368,8 @@ static int recurseDir(FileList fl, const char * diskURL)
  * @param statp		file stat (possibly NULL)
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int addFile(FileList fl, const char * diskURL,
-		/*@null@*/ struct stat * statp)
-	/*@globals check_fileList, rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies *statp, *fl, fl->processingFailed,
-		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
-		fl->totalFileSize, fl->fileCount,
-		check_fileList, rpmGlobalMacroContext,
-		fileSystem, internalState @*/
+		struct stat * statp)
 {
     const char *fileURL = diskURL;
     struct stat statbuf;
@@ -1518,10 +1398,8 @@ static int addFile(FileList fl, const char * diskURL,
     }
 
     /* XXX make sure '/' can be packaged also */
-    /*@-branchstate@*/
     if (*fileURL == '\0')
 	fileURL = "/";
-    /*@=branchstate@*/
 
     /* If we are using a prefix, validate the file */
     if (!fl->inFtw && fl->prefix) {
@@ -1565,9 +1443,8 @@ static int addFile(FileList fl, const char * diskURL,
     }
 
     if ((! fl->isDir) && S_ISDIR(statp->st_mode)) {
-/*@-nullstate@*/ /* FIX: fl->buildRootURL may be NULL */
+/* FIX: fl->buildRootURL may be NULL */
 	return recurseDir(fl, diskURL);
-/*@=nullstate@*/
     }
 
     fileMode = statp->st_mode;
@@ -1676,7 +1553,6 @@ static int addFile(FileList fl, const char * diskURL,
 
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  * Add directory (and all of its files) to the package manifest.
@@ -1706,11 +1582,11 @@ static int recurseDir(FileList fl, const char * diskURL)
 	case FTS_SLNONE:	/* symbolic link without target */
 	case FTS_DEFAULT:	/* none of the above */
 	    rc = addFile(fl, fts->fts_accpath, fts->fts_statp);
-	    /*@switchbreak@*/ break;
+	    break;
 	case FTS_DOT:		/* dot or dot-dot */
 	case FTS_DP:		/* postorder directory */
 	    rc = 0;
-	    /*@switchbreak@*/ break;
+	    break;
 	case FTS_NS:		/* stat(2) failed */
 	case FTS_DNR:		/* unreadable directory */
 	case FTS_ERR:		/* error; errno is set */
@@ -1720,7 +1596,7 @@ static int recurseDir(FileList fl, const char * diskURL)
 	case FTS_W:		/* whiteout object */
 	default:
 	    rc = RPMERR_BADSPEC;
-	    /*@switchbreak@*/ break;
+	    break;
 	}
 	if (rc)
 	    break;
@@ -1743,13 +1619,6 @@ static int recurseDir(FileList fl, const char * diskURL)
  */
 static int processMetadataFile(Package pkg, FileList fl, const char * fileURL,
 		rpmTag tag)
-	/*@globals check_fileList, rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies pkg->header, *fl, fl->processingFailed,
-		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
-		fl->totalFileSize, fl->fileCount,
-		check_fileList, rpmGlobalMacroContext,
-		fileSystem, internalState @*/
 {
     const char * buildURL = "%{_builddir}/%{?buildsubdir}/";
     const char * fn = NULL;
@@ -1767,13 +1636,12 @@ static int processMetadataFile(Package pkg, FileList fl, const char * fileURL,
     } else
 	fn = rpmGenPath(buildURL, NULL, fn);
 
-/*@-branchstate@*/
     switch (tag) {
     default:
 	rpmError(RPMERR_BADSPEC, _("%s: can't load unknown tag (%d).\n"),
 		fn, tag);
 	goto exit;
-	/*@notreached@*/ break;
+	break;
     case RPMTAG_PUBKEYS:
 	if ((rc = pgpReadPkts(fn, (const byte **)&pkt, (size_t *)&pktlen)) <= 0) {
 	    rpmError(RPMERR_BADSPEC, _("%s: public key read failed.\n"), fn);
@@ -1794,7 +1662,6 @@ static int processMetadataFile(Package pkg, FileList fl, const char * fileURL,
 	pkt = NULL;
 	break;
     }
-/*@=branchstate@*/
 
     xx = headerAddOrAppendEntry(pkg->header, tag,
 		RPM_STRING_ARRAY_TYPE, &apkt, 1);
@@ -1821,13 +1688,8 @@ exit:
  * @param fileURL
  * @return		0 on success
  */
-static int processBinaryFile(/*@unused@*/ Package pkg, FileList fl,
+static int processBinaryFile(Package pkg, FileList fl,
 		const char * fileURL)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies *fl, fl->processingFailed,
-		fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
-		fl->totalFileSize, fl->fileCount,
-		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int quote = 1;	/* XXX permit quoted glob characters. */
     int doGlob;
@@ -1870,14 +1732,11 @@ static int processBinaryFile(/*@unused@*/ Package pkg, FileList fl,
 	    goto exit;
 	}
 
-	/*@-branchstate@*/
 	rc = rpmGlob(diskURL, &argc, &argv);
 	if (rc == 0 && argc >= 1 && !Glob_pattern_p(argv[0], quote)) {
 	    for (i = 0; i < argc; i++) {
 		rc = addFile(fl, argv[i], NULL);
-/*@-boundswrite@*/
 		argv[i] = _free(argv[i]);
-/*@=boundswrite@*/
 	    }
 	    argv = _free(argv);
 	} else {
@@ -1886,7 +1745,6 @@ static int processBinaryFile(/*@unused@*/ Package pkg, FileList fl,
 	    rc = 1;
 	    goto exit;
 	}
-	/*@=branchstate@*/
     } else {
 	rc = addFile(fl, diskURL, NULL);
     }
@@ -1902,14 +1760,8 @@ exit:
 
 /**
  */
-/*@-boundswrite@*/
 static int processPackageFiles(Spec spec, Package pkg,
 			       int installSpecialDoc, int test)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState@*/
-	/*@modifies spec->macros,
-		pkg->cpioList, pkg->fileList, pkg->specialDoc, pkg->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     struct FileList_s fl;
@@ -1947,7 +1799,7 @@ static int processPackageFiles(Spec spec, Package pkg,
 	}
 	ffn = _free(ffn);
 
-	/*@+voidabstract@*/ f = fdGetFp(fd); /*@=voidabstract@*/
+	f = fdGetFp(fd);
 	if (f != NULL)
 	while (fgets(buf, sizeof(buf), f)) {
 	    handleComments(buf);
@@ -2026,9 +1878,7 @@ static int processPackageFiles(Spec spec, Package pkg,
 	if (*s == '\0')
 	    continue;
 	fileName = NULL;
-	/*@-nullpass@*/	/* LCL: buf is NULL ?!? */
 	strcpy(buf, s);
-	/*@=nullpass@*/
 	
 	/* Reset for a new line in %files */
 	fl.isDir = 0;
@@ -2048,16 +1898,13 @@ static int processPackageFiles(Spec spec, Package pkg,
 	if (fl.currentLangs) {
 	    int i;
 	    for (i = 0; i < fl.nLangs; i++)
-		/*@-unqualifiedtrans@*/
 		fl.currentLangs[i] = _free(fl.currentLangs[i]);
-		/*@=unqualifiedtrans@*/
 	    fl.currentLangs = _free(fl.currentLangs);
 	}
   	fl.nLangs = 0;
 
 	dupAttrRec(&fl.def_ar, &fl.cur_ar);
 
-	/*@-nullpass@*/	/* LCL: buf is NULL ?!? */
 	if (parseForVerify(buf, &fl))
 	    continue;
 	if (parseForAttr(buf, &fl))
@@ -2068,34 +1915,23 @@ static int processPackageFiles(Spec spec, Package pkg,
 	    continue;
 	if (parseForLang(buf, &fl))
 	    continue;
-	/*@-nullstate@*/	/* FIX: pkg->fileFile might be NULL */
 	if (parseForSimple(spec, pkg, buf, &fl, &fileName))
-	/*@=nullstate@*/
 	    continue;
-	/*@=nullpass@*/
 	if (fileName == NULL)
 	    continue;
 
-	/*@-branchstate@*/
 	if (fl.isSpecialDoc) {
 	    /* Save this stuff for last */
 	    specialDoc = _free(specialDoc);
 	    specialDoc = xstrdup(fileName);
 	    dupAttrRec(&fl.cur_ar, specialDocAttrRec);
 	} else if (fl.currentFlags & RPMFILE_PUBKEY) {
-/*@-nullstate@*/	/* FIX: pkg->fileFile might be NULL */
 	    (void) processMetadataFile(pkg, &fl, fileName, RPMTAG_PUBKEYS);
-/*@=nullstate@*/
 	} else if (fl.currentFlags & RPMFILE_POLICY) {
-/*@-nullstate@*/	/* FIX: pkg->fileFile might be NULL */
 	    (void) processMetadataFile(pkg, &fl, fileName, RPMTAG_POLICIES);
-/*@=nullstate@*/
 	} else {
-/*@-nullstate@*/	/* FIX: pkg->fileFile might be NULL */
 	    (void) processBinaryFile(pkg, &fl, fileName);
-/*@=nullstate@*/
 	}
-	/*@=branchstate@*/
     }
 
     /* Now process special doc, if there is one */
@@ -2125,9 +1961,7 @@ static int processPackageFiles(Spec spec, Package pkg,
 	if (fl.currentLangs) {
 	    int i;
 	    for (i = 0; i < fl.nLangs; i++)
-		/*@-unqualifiedtrans@*/
 		fl.currentLangs[i] = _free(fl.currentLangs[i]);
-		/*@=unqualifiedtrans@*/
 	    fl.currentLangs = _free(fl.currentLangs);
 	}
   	fl.nLangs = 0;
@@ -2135,9 +1969,7 @@ static int processPackageFiles(Spec spec, Package pkg,
 	dupAttrRec(specialDocAttrRec, &fl.cur_ar);
 	freeAttrRec(specialDocAttrRec);
 
-	/*@-nullstate@*/	/* FIX: pkg->fileFile might be NULL */
 	(void) processBinaryFile(pkg, &fl, specialDoc);
-	/*@=nullstate@*/
 
 	specialDoc = _free(specialDoc);
     }
@@ -2167,9 +1999,7 @@ exit:
     if (fl.currentLangs) {
 	int i;
 	for (i = 0; i < fl.nLangs; i++)
-	    /*@-unqualifiedtrans@*/
 	    fl.currentLangs[i] = _free(fl.currentLangs[i]);
-	    /*@=unqualifiedtrans@*/
 	fl.currentLangs = _free(fl.currentLangs);
     }
 
@@ -2178,7 +2008,6 @@ exit:
 	fl.docDirs[fl.docDirCount] = _free(fl.docDirs[fl.docDirCount]);
     return fl.processingFailed;
 }
-/*@=boundswrite@*/
 
 void initSourceHeader(Spec spec)
 {
@@ -2188,7 +2017,6 @@ void initSourceHeader(Spec spec)
 
     spec->sourceHeader = headerNew();
     /* Only specific tags are added to the source package header */
-    /*@-branchstate@*/
     for (hi = headerInitIterator(spec->packages->header);
 	headerNextIterator(hi, &tag, &type, &ptr, &count);
 	ptr = headerFreeData(ptr, type))
@@ -2215,17 +2043,15 @@ void initSourceHeader(Spec spec)
 	case HEADER_I18NTABLE:
 	    if (ptr)
 		(void)headerAddEntry(spec->sourceHeader, tag, type, ptr, count);
-	    /*@switchbreak@*/ break;
+	    break;
 	default:
 	    /* do not copy */
-	    /*@switchbreak@*/ break;
+	    break;
 	}
     }
     hi = headerFreeIterator(hi);
-    /*@=branchstate@*/
 
     /* Add the build restrictions */
-    /*@-branchstate@*/
     for (hi = headerInitIterator(spec->buildRestrictions);
 	headerNextIterator(hi, &tag, &type, &ptr, &count);
 	ptr = headerFreeData(ptr, type))
@@ -2234,7 +2060,6 @@ void initSourceHeader(Spec spec)
 	    (void) headerAddEntry(spec->sourceHeader, tag, type, ptr, count);
     }
     hi = headerFreeIterator(hi);
-    /*@=branchstate@*/
 
     if (spec->BANames && spec->BACount > 0) {
 	(void) headerAddEntry(spec->sourceHeader, RPMTAG_BUILDARCHS,
@@ -2414,12 +2239,8 @@ int processSourceFiles(Spec spec)
  * @return		-1 if skipped, 0 on OK, 1 on error
  */
 static int checkFiles(StringBuf fileList)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
-/*@-readonlytrans@*/
     static const char * av_ckfile[] = { "%{?__check_files}", NULL };
-/*@=readonlytrans@*/
     StringBuf sb_stdout = NULL;
     const char * s;
     int rc;
@@ -2433,9 +2254,7 @@ static int checkFiles(StringBuf fileList)
 
     rpmMessage(RPMMESS_NORMAL, _("Checking for unpackaged file(s): %s\n"), s);
 
-/*@-boundswrite@*/
     rc = rpmfcExec(av_ckfile, fileList, &sb_stdout, 0);
-/*@=boundswrite@*/
     if (rc < 0)
 	goto exit;
     
@@ -2458,10 +2277,7 @@ exit:
     return rc;
 }
 
-/*@-incondefs@*/
 int processBinaryFiles(Spec spec, int installSpecialDoc, int test)
-	/*@globals check_fileList @*/
-	/*@modifies check_fileList @*/
 {
     Package pkg;
     int res = 0;
@@ -2500,4 +2316,3 @@ int processBinaryFiles(Spec spec, int installSpecialDoc, int test)
     
     return res;
 }
-/*@=incondefs@*/
diff --git a/build/misc.c b/build/misc.c
index e14f75d8d..05e08067e 100644
--- a/build/misc.c
+++ b/build/misc.c
@@ -6,7 +6,6 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-/*@-boundswrite@*/
 int parseNum(const char * line, int * res)
 {
     char * s1 = NULL;
@@ -17,4 +16,3 @@ int parseNum(const char * line, int * res)
     if (res) *res = rc;
     return (((*s1) || (s1 == line) || (rc == ULONG_MAX)) ? 1 : 0);
 }
-/*@=boundswrite@*/
diff --git a/build/names.c b/build/names.c
index 5ddcad97f..87c9465bc 100644
--- a/build/names.c
+++ b/build/names.c
@@ -1,4 +1,3 @@
-/*@-mods@*/
 /** \ingroup rpmbuild
  * \file build/names.c
  * Simple user/group name/id cache (plus hostname and buildtime)
@@ -10,23 +9,16 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-typedef /*@owned@*/ /*@null@*/ const char * ugstr_t;
+typedef const char * ugstr_t;
 
-/*@unchecked@*/
 static uid_t uids[1024];
-/*@unchecked@*/
 static ugstr_t unames[1024];
-/*@unchecked@*/
 static int uid_used = 0;
 
-/*@unchecked@*/
 static gid_t gids[1024];
-/*@unchecked@*/
 static ugstr_t gnames[1024];
-/*@unchecked@*/
 static int gid_used = 0;
     
-/*@-boundswrite@*/
 void freeNames(void)
 {
     int x;
@@ -35,12 +27,8 @@ void freeNames(void)
     for (x = 0; x < gid_used; x++)
 	gnames[x] = _free(gnames[x]);
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 const char *getUname(uid_t uid)
-	/*@globals uid_used, uids, unames @*/
-	/*@modifies uid_used, uids, unames @*/
 {
     struct passwd *pw;
     int x;
@@ -61,12 +49,8 @@ const char *getUname(uid_t uid)
     unames[uid_used] = xstrdup(pw->pw_name);
     return unames[uid_used++];
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 const char *getUnameS(const char *uname)
-	/*@globals uid_used, uids, unames @*/
-	/*@modifies uid_used, uids, unames @*/
 {
     struct passwd *pw;
     int x;
@@ -90,12 +74,8 @@ const char *getUnameS(const char *uname)
     }
     return unames[uid_used++];
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 uid_t getUidS(const char *uname)
-	/*@globals uid_used, uids, unames @*/
-	/*@modifies uid_used, uids, unames @*/
 {
     struct passwd *pw;
     int x;
@@ -119,12 +99,8 @@ uid_t getUidS(const char *uname)
     }
     return uids[uid_used++];
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 const char *getGname(gid_t gid)
-	/*@globals gid_used, gids, gnames @*/
-	/*@modifies gid_used, gids, gnames @*/
 {
     struct group *gr;
     int x;
@@ -145,12 +121,8 @@ const char *getGname(gid_t gid)
     gnames[gid_used] = xstrdup(gr->gr_name);
     return gnames[gid_used++];
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 const char *getGnameS(const char *gname)
-	/*@globals gid_used, gids, gnames @*/
-	/*@modifies gid_used, gids, gnames @*/
 {
     struct group *gr;
     int x;
@@ -174,12 +146,8 @@ const char *getGnameS(const char *gname)
     }
     return gnames[gid_used++];
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 gid_t getGidS(const char *gname)
-	/*@globals gid_used, gids, gnames @*/
-	/*@modifies gid_used, gids, gnames @*/
 {
     struct group *gr;
     int x;
@@ -203,20 +171,16 @@ gid_t getGidS(const char *gname)
     }
     return gids[gid_used++];
 }
-/*@=boundswrite@*/
 
 int_32 * getBuildTime(void)
 {
     static int_32 buildTime[1];
 
-/*@-boundsread@*/
     if (buildTime[0] == 0)
 	buildTime[0] = (int_32) time(NULL);
-/*@=boundsread@*/
     return buildTime;
 }
 
-/*@-boundswrite@*/
 const char * buildHost(void)
 {
     static char hostname[1024];
@@ -225,11 +189,7 @@ const char * buildHost(void)
 
     if (! oneshot) {
         (void) gethostname(hostname, sizeof(hostname));
-	/*@-unrecog -multithreaded @*/
-	/*@-globs@*/	/* FIX: h_errno access */
 	hbn = gethostbyname(hostname);
-	/*@=globs@*/
-	/*@=unrecog =multithreaded @*/
 	if (hbn)
 	    strcpy(hostname, hbn->h_name);
 	else
@@ -239,5 +199,3 @@ const char * buildHost(void)
     }
     return(hostname);
 }
-/*@=boundswrite@*/
-/*@=mods@*/
diff --git a/build/pack.c b/build/pack.c
index fa32c1b09..981b35004 100644
--- a/build/pack.c
+++ b/build/pack.c
@@ -25,17 +25,9 @@
 #include "rpmlead.h"
 #include "debug.h"
 
-/*@access rpmts @*/
-/*@access rpmfi @*/	/* compared with NULL */
-/*@access Header @*/	/* compared with NULL */
-/*@access FD_t @*/	/* compared with NULL */
-/*@access StringBuf @*/	/* compared with NULL */
-/*@access CSA_t @*/
-
 /**
  */
 static inline int genSourceRpmName(Spec spec)
-	/*@modifies spec->sourceRpmName @*/
 {
     if (spec->sourceRpmName == NULL) {
 	const char *name, *version, *release;
@@ -53,11 +45,8 @@ static inline int genSourceRpmName(Spec spec)
 /**
  * @todo Create transaction set *much* earlier.
  */
-static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
+static int cpio_doio(FD_t fdo, Header h, CSA_t csa,
 		const char * fmodeMacro)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies fdo, csa, rpmGlobalMacroContext,
-		fileSystem, internalState @*/
 {
     rpmts ts = rpmtsCreate();
     rpmfi fi = csa->cpioList;
@@ -65,17 +54,13 @@ static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
     FD_t cfd;
     int rc, ec;
 
-/*@-boundsread@*/
     {	const char *fmode = rpmExpand(fmodeMacro, NULL);
 	if (!(fmode && fmode[0] == 'w'))
 	    fmode = xstrdup("w9.gzdio");
-	/*@-nullpass@*/
 	(void) Fflush(fdo);
 	cfd = Fdopen(fdDup(Fileno(fdo)), fmode);
-	/*@=nullpass@*/
 	fmode = _free(fmode);
     }
-/*@=boundsread@*/
     if (cfd == NULL)
 	return 1;
 
@@ -104,8 +89,6 @@ 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, internalState @*/
-	/*@modifies fdo, csa, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     size_t nb;
@@ -128,10 +111,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, h_errno, fileSystem, internalState @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
+static StringBuf addFileToTagAux(Spec spec,
+		const char * file, StringBuf sb)
 {
     char buf[BUFSIZ];
     const char * fn = buf;
@@ -146,9 +127,8 @@ static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
 	sb = freeStringBuf(sb);
 	return NULL;
     }
-    /*@-type@*/ /* FIX: cast? */
+    /* FIX: cast? */
     if ((f = fdGetFp(fd)) != NULL)
-    /*@=type@*/
     while (fgets(buf, sizeof(buf), f)) {
 	/* XXX display fn in error msg */
 	if (expandMacros(spec, spec->macros, buf, sizeof(buf))) {
@@ -166,8 +146,6 @@ static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
 /**
  */
 static int addFileToTag(Spec spec, const char * file, Header h, int tag)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     StringBuf sb = newStringBuf();
@@ -190,8 +168,6 @@ 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, h_errno, fileSystem, internalState @*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     StringBuf sb = newStringBuf();
     char *s;
@@ -209,9 +185,6 @@ static int addFileToArrayTag(Spec spec, const char *file, Header h, int tag)
 /**
  */
 static int processScriptFiles(Spec spec, Package pkg)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies pkg->header, rpmGlobalMacroContext,
-		fileSystem, internalState @*/
 {
     struct TriggerFileEntry *p;
     
@@ -292,7 +265,6 @@ static int processScriptFiles(Spec spec, Package pkg)
     return 0;
 }
 
-/*@-boundswrite@*/
 int readRPM(const char *fileName, Spec *specp, struct rpmlead *lead,
 		Header *sigs, CSA_t csa)
 {
@@ -313,14 +285,12 @@ int readRPM(const char *fileName, Spec *specp, struct rpmlead *lead,
     }
 
     /* Get copy of lead */
-    /*@-sizeoftype@*/
     if ((rc = Fread(lead, sizeof(char), sizeof(*lead), fdi)) != sizeof(*lead)) {
 	rpmError(RPMERR_BADMAGIC, _("readRPM: read %s: %s\n"),
 		(fileName ? fileName : "<stdin>"),
 		Fstrerror(fdi));
 	return RPMERR_BADMAGIC;
     }
-    /*@=sizeoftype@*/
 
     /* XXX FIXME: EPIPE on <stdin> */
     if (Fseek(fdi, 0, SEEK_SET) == -1) {
@@ -340,10 +310,9 @@ int readRPM(const char *fileName, Spec *specp, struct rpmlead *lead,
     {	rpmts ts = rpmtsCreate();
 
 	/* XXX W2DO? pass fileName? */
-	/*@-mustmod@*/      /* LCL: segfault */
+	     /* LCL: segfault */
 	rc = rpmReadPackageFile(ts, fdi, "readRPM",
 			 &spec->packages->header);
-	/*@=mustmod@*/
 
 	ts = rpmtsFree(ts);
 
@@ -364,15 +333,13 @@ int readRPM(const char *fileName, Spec *specp, struct rpmlead *lead,
 	rpmError(RPMERR_BADMAGIC, _("readRPM: reading header from %s\n"),
 		(fileName ? fileName : "<stdin>"));
 	return RPMERR_BADMAGIC;
-	/*@notreached@*/ break;
+	break;
     }
 
-    /*@-branchstate@*/
     if (specp)
 	*specp = spec;
     else
 	spec = freeSpec(spec);
-    /*@=branchstate@*/
 
     if (csa != NULL)
 	csa->cpioFdIn = fdi;
@@ -381,10 +348,8 @@ int readRPM(const char *fileName, Spec *specp, struct rpmlead *lead,
 
     return 0;
 }
-/*@=boundswrite@*/
 
 #ifdef	DYING
-/*@unchecked@*/
 static unsigned char header_magic[8] = {
         0x8e, 0xad, 0xe8, 0x01, 0x00, 0x00, 0x00, 0x00
 };
@@ -392,12 +357,9 @@ static unsigned char header_magic[8] = {
 
 #define	RPMPKGVERSION_MIN	30004
 #define	RPMPKGVERSION_MAX	40003
-/*@unchecked@*/
 static int rpmpkg_version = -1;
 
 static int rpmLeadVersion(void)
-	/*@globals rpmpkg_version, rpmGlobalMacroContext, h_errno @*/
-	/*@modifies rpmpkg_version, rpmGlobalMacroContext @*/
 {
     int rpmlead_version;
 
@@ -416,7 +378,6 @@ static int rpmLeadVersion(void)
     return rpmlead_version;
 }
 
-/*@-boundswrite@*/
 int writeRPM(Header *hdrp, unsigned char ** pkgidp, const char *fileName,
 		int type, CSA_t csa, char *passPhrase, const char **cookie)
 {
@@ -453,7 +414,6 @@ int writeRPM(Header *hdrp, unsigned char ** pkgidp, const char *fileName,
 	providePackageNVR(h);
 
     /* Save payload information */
-    /*@-branchstate@*/
     switch(type) {
     case RPMLEAD_SOURCE:
 	rpmio_flags = rpmExpand("%{?_source_payload}", NULL);
@@ -462,7 +422,6 @@ int writeRPM(Header *hdrp, unsigned char ** pkgidp, const char *fileName,
 	rpmio_flags = rpmExpand("%{?_binary_payload}", NULL);
 	break;
     }
-    /*@=branchstate@*/
     if (!(rpmio_flags && *rpmio_flags)) {
 	rpmio_flags = _free(rpmio_flags);
 	rpmio_flags = xstrdup("w9.gzdio");
@@ -741,9 +700,7 @@ exit:
 
     return rc;
 }
-/*@=boundswrite@*/
 
-/*@unchecked@*/
 static int_32 copyTags[] = {
     RPMTAG_CHANGELOGTIME,
     RPMTAG_CHANGELOGNAME,
@@ -751,7 +708,6 @@ static int_32 copyTags[] = {
     0
 };
 
-/*@-boundswrite@*/
 int packageBinaries(Spec spec)
 {
     struct cpioSourceArchive_s csabuf;
@@ -822,12 +778,11 @@ int packageBinaries(Spec spec)
 		    switch(errno) {
 		    case  ENOENT:
 			if (Mkdir(dn, 0755) == 0)
-			    /*@switchbreak@*/ break;
-			/*@fallthrough@*/
+			    break;
 		    default:
 			rpmError(RPMERR_BADFILENAME,_("cannot create %s: %s\n"),
 			    dn, strerror(errno));
-			/*@switchbreak@*/ break;
+			break;
 		    }
 		}
 		dn = _free(dn);
@@ -837,18 +792,15 @@ int packageBinaries(Spec spec)
 
 	memset(csa, 0, sizeof(*csa));
 	csa->cpioArchiveSize = 0;
-	/*@-type@*/ /* LCL: function typedefs */
+	/* LCL: function typedefs */
 	csa->cpioFdIn = fdNew("init (packageBinaries)");
-	/*@-assignexpose -newreftrans@*/
 	csa->cpioList = rpmfiLink(pkg->cpioList, "packageBinaries");
-	/*@=assignexpose =newreftrans@*/
 
 	rc = writeRPM(&pkg->header, NULL, fn, RPMLEAD_BINARY,
 		    csa, spec->passPhrase, NULL);
 
 	csa->cpioList = rpmfiFree(csa->cpioList);
 	csa->cpioFdIn = fdFree(csa->cpioFdIn, "init (packageBinaries)");
-	/*@=type@*/
 	fn = _free(fn);
 	if (rc)
 	    return rc;
@@ -856,9 +808,7 @@ int packageBinaries(Spec spec)
     
     return 0;
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 int packageSources(Spec spec)
 {
     struct cpioSourceArchive_s csabuf;
@@ -882,11 +832,9 @@ int packageSources(Spec spec)
 
 	memset(csa, 0, sizeof(*csa));
 	csa->cpioArchiveSize = 0;
-	/*@-type@*/ /* LCL: function typedefs */
+	/* LCL: function typedefs */
 	csa->cpioFdIn = fdNew("init (packageSources)");
-	/*@-assignexpose -newreftrans@*/
 	csa->cpioList = rpmfiLink(spec->sourceCpioList, "packageSources");
-	/*@=assignexpose =newreftrans@*/
 
 	spec->sourcePkgId = NULL;
 	rc = writeRPM(&spec->sourceHeader, &spec->sourcePkgId, fn, RPMLEAD_SOURCE,
@@ -894,9 +842,7 @@ int packageSources(Spec spec)
 
 	csa->cpioList = rpmfiFree(csa->cpioList);
 	csa->cpioFdIn = fdFree(csa->cpioFdIn, "init (packageSources)");
-	/*@=type@*/
 	fn = _free(fn);
     }
     return rc;
 }
-/*@=boundswrite@*/
diff --git a/build/parseBuildInstallClean.c b/build/parseBuildInstallClean.c
index f086f7c17..148be463e 100644
--- a/build/parseBuildInstallClean.c
+++ b/build/parseBuildInstallClean.c
@@ -7,16 +7,13 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-/*@access StringBuf @*/
 
-/*@-boundswrite@*/
 int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
 {
     int nextPart, rc;
     StringBuf *sbp = NULL;
     const char *name = NULL;
 
-    /*@-branchstate@*/
     if (parsePart == PART_BUILD) {
 	sbp = &(spec->build);
 	name = "%build";
@@ -30,7 +27,6 @@ int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
 	sbp = &(spec->clean);
 	name = "%clean";
     }
-    /*@=branchstate@*/
     
     if (*sbp != NULL) {
 	rpmError(RPMERR_BADSPEC, _("line %d: second %s\n"),
@@ -56,4 +52,3 @@ int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
 
     return nextPart;
 }
-/*@=boundswrite@*/
diff --git a/build/parseChangelog.c b/build/parseChangelog.c
index 6ba8a2814..1f0df48ce 100644
--- a/build/parseChangelog.c
+++ b/build/parseChangelog.c
@@ -34,19 +34,17 @@ void addChangelogEntry(Header h, time_t time, const char *name, const char *text
  * @retval secs		secs since the unix epoch
  * @return 		0 on success, -1 on error
  */
-/*@-boundswrite@*/
-static int dateToTimet(const char * datestr, /*@out@*/ time_t * secs)
-	/*@modifies *secs @*/
+static int dateToTimet(const char * datestr, time_t * secs)
 {
     struct tm time;
     char * p, * pe, * q, ** idx;
     char * date = strcpy(alloca(strlen(datestr) + 1), datestr);
-/*@observer@*/ static char * days[] =
+static char * days[] =
 	{ "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat", NULL };
-/*@observer@*/ static char * months[] =
+static char * months[] =
 	{ "Jan", "Feb", "Mar", "Apr", "May", "Jun",
  	  "Jul", "Aug", "Sep", "Oct", "Nov", "Dec", NULL };
-/*@observer@*/ static char lengths[] =
+static char lengths[] =
 	{ 31, 29, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31 };
     
     memset(&time, 0, sizeof(time));
@@ -99,7 +97,6 @@ static int dateToTimet(const char * datestr, /*@out@*/ time_t * secs)
 
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  * Add %changelog section to header.
@@ -107,9 +104,7 @@ static int dateToTimet(const char * datestr, /*@out@*/ time_t * secs)
  * @param sb		changelog strings
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int addChangelog(Header h, StringBuf sb)
-	/*@modifies h @*/
 {
     char *s;
     int i;
@@ -136,9 +131,7 @@ static int addChangelog(Header h, StringBuf sb)
 	    rpmError(RPMERR_BADSPEC, _("incomplete %%changelog entry\n"));
 	    return RPMERR_BADSPEC;
 	}
-	/*@-modobserver@*/
 	*s = '\0';
-	/*@=modobserver@*/
 	text = s + 1;
 	
 	/* 4 fields of date */
@@ -204,7 +197,6 @@ static int addChangelog(Header h, StringBuf sb)
 
     return 0;
 }
-/*@=boundswrite@*/
 
 int parseChangelog(Spec spec)
 {
diff --git a/build/parseDescription.c b/build/parseDescription.c
index e76666b36..19198f5df 100644
--- a/build/parseDescription.c
+++ b/build/parseDescription.c
@@ -8,18 +8,12 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-/*@-exportheadervar@*/
-/*@unchecked@*/
 extern int noLang;
-/*@=exportheadervar@*/
 
 /* These have to be global scope to make up for *stupid* compilers */
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *name = NULL;
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *lang = NULL;
+    static const char *name = NULL;
+    static const char *lang = NULL;
 
-/*@unchecked@*/
     static struct poptOption optionsTable[] = {
 	{ NULL, 'n', POPT_ARG_STRING, &name, 'n',	NULL, NULL},
 	{ NULL, 'l', POPT_ARG_STRING, &lang, 'l',	NULL, NULL},
@@ -27,8 +21,6 @@ extern int noLang;
     };
 
 int parseDescription(Spec spec)
-	/*@globals name, lang @*/
-	/*@modifies name, lang @*/
 {
     int nextPart = RPMERR_BADSPEC;	/* assume error */
     StringBuf sb;
diff --git a/build/parseFiles.c b/build/parseFiles.c
index 759fc0ca6..f4271a18a 100644
--- a/build/parseFiles.c
+++ b/build/parseFiles.c
@@ -8,15 +8,9 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-/*@access StringBuf @*/		/* compared with NULL */
-/*@access poptContext @*/	/* compared with NULL */
-
 /* These have to be global scope to make up for *stupid* compilers */
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *name = NULL;
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *file = NULL;
-/*@unchecked@*/
+    static const char *name = NULL;
+    static const char *file = NULL;
     static struct poptOption optionsTable[] = {
 	{ NULL, 'n', POPT_ARG_STRING, &name, 'n',	NULL, NULL},
 	{ NULL, 'f', POPT_ARG_STRING, &file, 'f',	NULL, NULL},
@@ -33,10 +27,8 @@ int parseFiles(Spec spec)
     int flag = PART_SUBNAME;
     poptContext optCon = NULL;
 
-    /*@-mods@*/
     name = NULL;
     file = NULL;
-    /*@=mods@*/
 
     if ((rc = poptParseArgvString(spec->line, &argc, &argv))) {
 	rpmError(RPMERR_BADSPEC, _("line %d: Error parsing %%files: %s\n"),
@@ -62,10 +54,8 @@ int parseFiles(Spec spec)
     }
 
     if (poptPeekArg(optCon)) {
-	/*@-mods@*/
 	if (name == NULL)
 	    name = poptGetArg(optCon);
-	/*@=mods@*/
 	if (poptPeekArg(optCon)) {
 	    rpmError(RPMERR_BADSPEC, _("line %d: Too many names: %s\n"),
 		     spec->lineNum,
diff --git a/build/parsePreamble.c b/build/parsePreamble.c
index cc8aaeeb3..34098ef90 100644
--- a/build/parsePreamble.c
+++ b/build/parsePreamble.c
@@ -9,11 +9,8 @@
 #include <rpmbuild.h>
 #include "debug.h"
 
-/*@access FD_t @*/	/* compared with NULL */
-
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static rpmTag copyTagsDuringParse[] = {
     RPMTAG_EPOCH,
     RPMTAG_VERSION,
@@ -37,7 +34,6 @@ static rpmTag copyTagsDuringParse[] = {
 
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static rpmTag requiredTags[] = {
     RPMTAG_NAME,
     RPMTAG_VERSION,
@@ -51,7 +47,6 @@ static rpmTag requiredTags[] = {
 /**
  */
 static void addOrAppendListEntry(Header h, int_32 tag, char * line)
-	/*@modifies h @*/
 {
     int xx;
     int argc;
@@ -68,10 +63,7 @@ static void addOrAppendListEntry(Header h, int_32 tag, char * line)
 
 /**
  */
-/*@-boundswrite@*/
-static int parseSimplePart(char *line, /*@out@*/char **name, /*@out@*/int *flag)
-	/*@globals internalState@*/
-	/*@modifies *name, *flag, internalState @*/
+static int parseSimplePart(char *line,char **name,int *flag)
 {
     char *tok;
     char linebuf[BUFSIZ];
@@ -99,12 +91,10 @@ static int parseSimplePart(char *line, /*@out@*/char **name, /*@out@*/int *flag)
 
     return (strtok(NULL, " \t\n")) ? 1 : 0;
 }
-/*@=boundswrite@*/
 
 /**
  */
 static inline int parseYesNo(const char * s)
-	/*@*/
 {
     return ((!s || (s[0] == 'n' || s[0] == 'N' || s[0] == '0') ||
 	!xstrcasecmp(s, "false") || !xstrcasecmp(s, "off"))
@@ -112,14 +102,12 @@ static inline int parseYesNo(const char * s)
 }
 
 typedef struct tokenBits_s {
-/*@observer@*/ /*@null@*/
     const char * name;
     rpmsenseFlags bits;
 } * tokenBits;
 
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static struct tokenBits_s installScriptBits[] = {
     { "interp",		RPMSENSE_INTERP },
     { "prereq",		RPMSENSE_PREREQ },
@@ -134,7 +122,6 @@ static struct tokenBits_s installScriptBits[] = {
 
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static struct tokenBits_s buildScriptBits[] = {
     { "prep",		RPMSENSE_SCRIPT_PREP },
     { "build",		RPMSENSE_SCRIPT_BUILD },
@@ -145,10 +132,8 @@ static struct tokenBits_s buildScriptBits[] = {
 
 /**
  */
-/*@-boundswrite@*/
 static int parseBits(const char * s, const tokenBits tokbits,
-		/*@out@*/ rpmsenseFlags * bp)
-	/*@modifies *bp @*/
+		rpmsenseFlags * bp)
 {
     tokenBits tb;
     const char * se;
@@ -165,7 +150,7 @@ static int parseBits(const char * s, const tokenBits tokbits,
 	    for (tb = tokbits; tb->name; tb++) {
 		if (tb->name != NULL &&
 		    strlen(tb->name) == (se-s) && !strncmp(tb->name, s, (se-s)))
-		    /*@innerbreak@*/ break;
+		    break;
 	    }
 	    if (tb->name == NULL)
 		break;
@@ -179,32 +164,25 @@ static int parseBits(const char * s, const tokenBits tokbits,
     if (c == 0 && bp) *bp = bits;
     return (c ? RPMERR_BADSPEC : 0);
 }
-/*@=boundswrite@*/
 
 /**
  */
 static inline char * findLastChar(char * s)
-	/*@*/
 {
     char *res = s;
 
-/*@-boundsread@*/
     while (*s != '\0') {
 	if (! xisspace(*s))
 	    res = s;
 	s++;
     }
-/*@=boundsread@*/
 
-    /*@-temptrans -retalias@*/
     return res;
-    /*@=temptrans =retalias@*/
 }
 
 /**
  */
 static int isMemberInEntry(Header h, const char *name, rpmTag tag)
-	/*@*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -214,20 +192,17 @@ static int isMemberInEntry(Header h, const char *name, rpmTag tag)
 
     if (!hge(h, tag, &type, (void **)&names, &count))
 	return -1;
-/*@-boundsread@*/
     while (count--) {
 	if (!xstrcasecmp(names[count], name))
 	    break;
     }
     names = hfd(names, type);
-/*@=boundsread@*/
     return (count >= 0 ? 1 : 0);
 }
 
 /**
  */
 static int checkForValidArchitectures(Spec spec)
-	/*@*/
 {
 #ifndef	DYING
     const char *arch = NULL;
@@ -271,12 +246,11 @@ static int checkForValidArchitectures(Spec spec)
  * @return		0 if OK
  */
 static int checkForRequired(Header h, const char * NVR)
-	/*@modifies h @*/ /* LCL: parse error here with modifies */
+	/* LCL: parse error here with modifies */
 {
     int res = 0;
     rpmTag * p;
 
-/*@-boundsread@*/
     for (p = requiredTags; *p != 0; p++) {
 	if (!headerIsEntry(h, *p)) {
 	    rpmError(RPMERR_BADSPEC,
@@ -285,7 +259,6 @@ static int checkForRequired(Header h, const char * NVR)
 	    res = 1;
 	}
     }
-/*@=boundsread@*/
 
     return res;
 }
@@ -297,7 +270,6 @@ static int checkForRequired(Header h, const char * NVR)
  * @return		0 if OK
  */
 static int checkForDuplicates(Header h, const char * NVR)
-	/*@modifies h @*/
 {
     int res = 0;
     int lastTag, tag;
@@ -320,10 +292,8 @@ static int checkForDuplicates(Header h, const char * NVR)
 
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static struct optionalTag {
     rpmTag	ot_tag;
-/*@observer@*/ /*@null@*/
     const char * ot_mac;
 } optionalTags[] = {
     { RPMTAG_VENDOR,		"%{vendor}" },
@@ -336,29 +306,22 @@ static struct optionalTag {
 /**
  */
 static void fillOutMainPackage(Header h)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies h, rpmGlobalMacroContext @*/
 {
     struct optionalTag *ot;
 
     for (ot = optionalTags; ot->ot_mac != NULL; ot++) {
 	if (!headerIsEntry(h, ot->ot_tag)) {
-/*@-boundsread@*/
 	    const char *val = rpmExpand(ot->ot_mac, NULL);
 	    if (val && *val != '%')
 		(void) headerAddEntry(h, ot->ot_tag, RPM_STRING_TYPE, (void *)val, 1);
 	    val = _free(val);
-/*@=boundsread@*/
 	}
     }
 }
 
 /**
  */
-/*@-boundswrite@*/
 static int readIcon(Header h, const char * file)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     const char *fn = NULL;
     char *icon;
@@ -413,7 +376,6 @@ exit:
     fn = _free(fn);
     return rc;
 }
-/*@=boundswrite@*/
 
 spectag stashSt(Spec spec, Header h, int tag, const char * lang)
 {
@@ -441,9 +403,7 @@ spectag stashSt(Spec spec, Header h, int tag, const char * lang)
 	    }
 	}
     }
-    /*@-usereleased -compdef@*/
     return t;
-    /*@=usereleased =compdef@*/
 }
 
 #define SINGLE_TOKEN_ONLY \
@@ -453,22 +413,12 @@ if (multiToken) { \
     return RPMERR_BADSPEC; \
 }
 
-/*@-redecl@*/
 extern int noLang;
-/*@=redecl@*/
 
 /**
  */
-/*@-boundswrite@*/
 static int handlePreambleTag(Spec spec, Package pkg, rpmTag tag,
 		const char *macro, const char *lang)
-	/*@globals rpmGlobalMacroContext, h_errno, 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, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -539,7 +489,6 @@ static int handlePreambleTag(Spec spec, Package pkg, rpmTag tag,
     case RPMTAG_GROUP:
     case RPMTAG_SUMMARY:
 	(void) stashSt(spec, pkg->header, tag, lang);
-	/*@fallthrough@*/
     case RPMTAG_DISTRIBUTION:
     case RPMTAG_VENDOR:
     case RPMTAG_LICENSE:
@@ -571,9 +520,7 @@ static int handlePreambleTag(Spec spec, Package pkg, rpmTag tag,
 
 		buildRootURL = _free(buildRootURL);
 		(void) urlPath(specURL, (const char **)&field);
-		/*@-branchstate@*/
 		if (*field == '\0') field = "/";
-		/*@=branchstate@*/
 		buildRootURL = rpmGenPath(spec->rootURL, field, NULL);
 		spec->buildRootURL = buildRootURL;
 		field = (char *) buildRootURL;
@@ -584,9 +531,7 @@ static int handlePreambleTag(Spec spec, Package pkg, rpmTag tag,
 	}
 	buildRootURL = rpmGenPath(NULL, spec->buildRootURL, NULL);
 	(void) urlPath(buildRootURL, &buildRoot);
-	/*@-branchstate@*/
 	if (*buildRoot == '\0') buildRoot = "/";
-	/*@=branchstate@*/
 	if (!strcmp(buildRoot, "/")) {
 	    rpmError(RPMERR_BADSPEC,
 		     _("BuildRoot can not be \"/\": %s\n"), spec->buildRootURL);
@@ -721,7 +666,6 @@ static int handlePreambleTag(Spec spec, Package pkg, rpmTag tag,
     
     return 0;
 }
-/*@=boundswrite@*/
 
 /* This table has to be in a peculiar order.  If one tag is the */
 /* same as another, plus a few letters, it must come first.     */
@@ -733,11 +677,9 @@ typedef struct PreambleRec_s {
     int len;
     int multiLang;
     int obsolete;
-/*@observer@*/ /*@null@*/
     const char * token;
 } * PreambleRec;
 
-/*@unchecked@*/
 static struct PreambleRec_s preambleList[] = {
     {RPMTAG_NAME,		0, 0, 0, "name"},
     {RPMTAG_VERSION,		0, 0, 0, "version"},
@@ -783,16 +725,13 @@ static struct PreambleRec_s preambleList[] = {
     {RPMTAG_DISTTAG,		0, 0, 0, "disttag"},
     {RPMTAG_CVSID,		0, 0, 0, "cvsid"},
     {RPMTAG_SVNID,		0, 0, 0, "svnid"},
-    /*@-nullassign@*/	/* LCL: can't add null annotation */
+   	/* LCL: can't add null annotation */
     {0, 0, 0, 0, 0}
-    /*@=nullassign@*/
 };
 
 /**
  */
 static inline void initPreambleList(void)
-	/*@globals preambleList @*/
-	/*@modifies preambleList @*/
 {
     PreambleRec p;
     for (p = preambleList; p->token != NULL; p++)
@@ -801,10 +740,8 @@ static inline void initPreambleList(void)
 
 /**
  */
-/*@-boundswrite@*/
-static int findPreambleTag(Spec spec, /*@out@*/rpmTag * tag,
-		/*@null@*/ /*@out@*/ const char ** macro, /*@out@*/ char * lang)
-	/*@modifies *tag, *macro, *lang @*/
+static int findPreambleTag(Spec spec,rpmTag * tag,
+		const char ** macro, char * lang)
 {
     PreambleRec p;
     char *s;
@@ -858,14 +795,10 @@ static int findPreambleTag(Spec spec, /*@out@*/rpmTag * tag,
 
     *tag = p->tag;
     if (macro)
-	/*@-onlytrans -observertrans -dependenttrans@*/	/* FIX: double indirection. */
 	*macro = p->token;
-	/*@=onlytrans =observertrans =dependenttrans@*/
     return 0;
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 int parsePreamble(Spec spec, int initialPackage)
 {
     int nextPart;
@@ -963,4 +896,3 @@ int parsePreamble(Spec spec, int initialPackage)
 
     return nextPart;
 }
-/*@=boundswrite@*/
diff --git a/build/parsePrep.c b/build/parsePrep.c
index 74a6d6dc8..d2d5d3ce4 100644
--- a/build/parsePrep.c
+++ b/build/parsePrep.c
@@ -9,17 +9,11 @@
 #include <rpmbuild.h>
 #include "debug.h"
 
-/*@access StringBuf @*/	/* compared with NULL */
-
 /* These have to be global to make up for stupid compilers */
-/*@unchecked@*/
     static int leaveDirs, skipDefaultAction;
-/*@unchecked@*/
     static int createDir, quietly;
-/*@unchecked@*/
-/*@observer@*/ /*@null@*/ static const char * dirName = NULL;
-/*@unchecked@*/
-/*@observer@*/ static struct poptOption optionsTable[] = {
+static const char * dirName = NULL;
+static struct poptOption optionsTable[] = {
 	    { NULL, 'a', POPT_ARG_STRING, NULL, 'a',	NULL, NULL},
 	    { NULL, 'b', POPT_ARG_STRING, NULL, 'b',	NULL, NULL},
 	    { NULL, 'c', 0, &createDir, 0,		NULL, NULL},
@@ -36,8 +30,6 @@
  * @return		0 on success
  */
 static int checkOwners(const char * urlfn)
-	/*@globals h_errno, fileSystem, internalState @*/
-	/*@modifies fileSystem, internalState @*/
 {
     struct stat sb;
 
@@ -65,12 +57,9 @@ static int checkOwners(const char * urlfn)
  * @param removeEmpties	include -E?
  * @return		expanded %patch macro (NULL on error)
  */
-/*@-boundswrite@*/
-/*@observer@*/ 
+
 static char *doPatch(Spec spec, int c, int strip, const char *db,
 		     int reverse, int removeEmpties, int fuzz)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -127,7 +116,7 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
     case URL_IS_DASH:
 	urlfn = _free(urlfn);
 	return NULL;
-	/*@notreached@*/ break;
+	break;
     }
 
     if (compressed) {
@@ -142,7 +131,7 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
 		"if [ $STATUS -ne 0 ]; then\n"
 		"  exit $STATUS\n"
 		"fi",
-		c, /*@-unrecog@*/ (const char *) basename(fn), /*@=unrecog@*/
+		c, (const char *) basename(fn),
 		zipper,
 		fn, strip, args);
 	zipper = _free(zipper);
@@ -156,7 +145,6 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
     urlfn = _free(urlfn);
     return buf;
 }
-/*@=boundswrite@*/
 
 /**
  * Expand %setup macro into %prep scriptlet.
@@ -165,10 +153,7 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
  * @param quietly	should -vv be omitted from tar?
  * @return		expanded %setup macro (NULL on error)
  */
-/*@-boundswrite@*/
-/*@observer@*/ static const char *doUntar(Spec spec, int c, int quietly)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
+static const char *doUntar(Spec spec, int c, int quietly)
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -190,9 +175,8 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
 
     urlfn = rpmGetPath("%{_sourcedir}/", sp->source, NULL);
 
-    /*@-internalglobs@*/ /* FIX: shrug */
+    /* FIX: shrug */
     taropts = ((rpmIsVerbose() && !quietly) ? "-xvvf" : "-xf");
-    /*@=internalglobs@*/
 
 #ifdef AUTOFETCH_NOT	/* XXX don't expect this code to be enabled */
     /* XXX
@@ -233,7 +217,7 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
     case URL_IS_DASH:
 	urlfn = _free(urlfn);
 	return NULL;
-	/*@notreached@*/ break;
+	break;
     }
 
     if (compressed != COMPRESSED_NOT) {
@@ -281,7 +265,6 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
     urlfn = _free(urlfn);
     return buf;
 }
-/*@=boundswrite@*/
 
 /**
  * Parse %setup macro.
@@ -291,9 +274,6 @@ static char *doPatch(Spec spec, int c, int strip, const char *db,
  * @return		0 on success
  */
 static int doSetupMacro(Spec spec, char *line)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->buildSubdir, spec->macros, spec->prep,
-		rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     StringBuf before;
@@ -306,11 +286,9 @@ static int doSetupMacro(Spec spec, char *line)
     int rc;
     int num;
 
-    /*@-mods@*/
     leaveDirs = skipDefaultAction = 0;
     createDir = quietly = 0;
     dirName = NULL;
-    /*@=mods@*/
 
     if ((rc = poptParseArgvString(line, &argc, &argv))) {
 	rpmError(RPMERR_BADSPEC, _("Error parsing %%setup: %s\n"),
@@ -421,18 +399,16 @@ static int doSetupMacro(Spec spec, char *line)
 
     /* XXX FIXME: owner & group fixes were conditioned on !geteuid() */
     /* Fix the owner, group, and permissions of the setup build tree */
-    {	/*@observer@*/ static const char *fixmacs[] =
+    {	static const char *fixmacs[] =
 		{ "%{_fixowner}", "%{_fixgroup}", "%{_fixperms}", NULL };
 	const char ** fm;
 
 	for (fm = fixmacs; *fm; fm++) {
 	    const char *fix;
-/*@-boundsread@*/
 	    fix = rpmExpand(*fm, " .", NULL);
 	    if (fix && *fix != '%')
 		appendLineStringBuf(spec->prep, fix);
 	    fix = _free(fix);
-/*@=boundsread@*/
 	}
     }
     
@@ -445,12 +421,7 @@ static int doSetupMacro(Spec spec, char *line)
  * @param line		current line from spec file
  * @return		0 on success
  */
-/*@-boundswrite@*/
 static int doPatchMacro(Spec spec, char *line)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies spec->prep, rpmGlobalMacroContext,
-		fileSystem, internalState  @*/
 {
     char *opt_b;
     int opt_P, opt_p, opt_R, opt_E, opt_F;
@@ -471,7 +442,7 @@ static int doPatchMacro(Spec spec, char *line)
 	strcpy(buf, line);
     }
     
-    /*@-internalglobs@*/	/* FIX: strtok has state */
+   	/* FIX: strtok has state */
     for (bp = buf; (s = strtok(bp, " \t\n")) != NULL;) {
 	if (bp) {	/* remove 1st token (%patch) */
 	    bp = NULL;
@@ -551,7 +522,6 @@ static int doPatchMacro(Spec spec, char *line)
 	    patch_index++;
 	}
     }
-    /*@=internalglobs@*/
 
     /* All args processed */
 
@@ -571,7 +541,6 @@ static int doPatchMacro(Spec spec, char *line)
     
     return 0;
 }
-/*@=boundswrite@*/
 
 int parsePrep(Spec spec)
 {
@@ -608,10 +577,8 @@ int parsePrep(Spec spec)
     }
 
     saveLines = splitString(getStringBuf(sb), strlen(getStringBuf(sb)), '\n');
-    /*@-usereleased@*/
     for (lines = saveLines; *lines; lines++) {
 	res = 0;
-/*@-boundsread@*/
 	if (! strncmp(*lines, "%setup", sizeof("%setup")-1)) {
 	    res = doSetupMacro(spec, *lines);
 	} else if (! strncmp(*lines, "%patch", sizeof("%patch")-1)) {
@@ -619,14 +586,12 @@ int parsePrep(Spec spec)
 	} else {
 	    appendLineStringBuf(spec->prep, *lines);
 	}
-/*@=boundsread@*/
 	if (res && !spec->force) {
 	    freeSplitString(saveLines);
 	    sb = freeStringBuf(sb);
 	    return res;
 	}
     }
-    /*@=usereleased@*/
 
     freeSplitString(saveLines);
     sb = freeStringBuf(sb);
diff --git a/build/parseReqs.c b/build/parseReqs.c
index 96b533de3..666fad7f3 100644
--- a/build/parseReqs.c
+++ b/build/parseReqs.c
@@ -10,9 +10,8 @@
 
 /**
  */
-/*@observer@*/ /*@unchecked@*/
 static struct ReqComp {
-/*@observer@*/ /*@null@*/ const char * token;
+const char * token;
     rpmsenseFlags sense;
 } ReqComparisons[] = {
     { "<=", RPMSENSE_LESS | RPMSENSE_EQUAL},
@@ -88,7 +87,6 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 	break;
     }
 
-/*@-boundsread@*/
     for (r = field; *r != '\0'; r = re) {
 	SKIPWHITE(r);
 	if (*r == '\0')
@@ -123,7 +121,7 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 	  struct ReqComp *rc;
 	  for (rc = ReqComparisons; rc->token != NULL; rc++) {
 	    if ((ve-v) != strlen(rc->token) || strncmp(v, rc->token, (ve-v)))
-		/*@innercontinue@*/ continue;
+		continue;
 
 	    if (r[0] == '/') {
 		rpmError(RPMERR_BADSPEC,
@@ -140,9 +138,9 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 		/* Add prereq on rpmlib that has versioned dependencies. */
 		if (!rpmExpandNumeric("%{?_noVersionedDependencies}"))
 		    (void) rpmlibNeedsFeature(h, "VersionedDependencies", "3.0.3-1");
-		/*@switchbreak@*/ break;
+		break;
 	    default:
-		/*@switchbreak@*/ break;
+		break;
 	    }
 	    Flags |= rc->sense;
 
@@ -151,11 +149,10 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 	    SKIPWHITE(v);
 	    ve = v;
 	    SKIPNONWHITE(ve);
-	    /*@innerbreak@*/ break;
+	    break;
 	  }
 	}
 
-	/*@-branchstate@*/
 	if (Flags & RPMSENSE_SENSEMASK) {
 	    if (*v == '\0' || ve == v) {
 		rpmError(RPMERR_BADSPEC, _("line %d: Version required: %s\n"),
@@ -168,7 +165,6 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 	    re = ve;	/* ==> next token after EVR string starts here */
 	} else
 	    EVR = NULL;
-	/*@=branchstate@*/
 
 	(void) addReqProv(spec, h, tagN, N, EVR, Flags, index);
 
@@ -176,7 +172,6 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, rpmTag tagN,
 	EVR = _free(EVR);
 
     }
-/*@=boundsread@*/
 
     return 0;
 }
diff --git a/build/parseScript.c b/build/parseScript.c
index e8bbb7717..028effe82 100644
--- a/build/parseScript.c
+++ b/build/parseScript.c
@@ -10,14 +10,10 @@
 
 #include <rpmlua.h>
 
-/*@access StringBuf@*/	/* XXX compared with NULL */
-/*@access poptContext @*/	/* compared with NULL */
-
 /**
  */
 static int addTriggerIndex(Package pkg, const char *file,
 	const char *script, const char *prog)
-	/*@modifies pkg->triggerFiles @*/
 {
     struct TriggerFileEntry *tfe;
     struct TriggerFileEntry *list = pkg->triggerFiles;
@@ -49,13 +45,9 @@ static int addTriggerIndex(Package pkg, const char *file,
 }
 
 /* these have to be global because of stupid compilers */
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *name = NULL;
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *prog = NULL;
-/*@unchecked@*/
-    /*@observer@*/ /*@null@*/ static const char *file = NULL;
-/*@unchecked@*/
+    static const char *name = NULL;
+    static const char *prog = NULL;
+    static const char *file = NULL;
     static struct poptOption optionsTable[] = {
 	{ NULL, 'p', POPT_ARG_STRING, &prog, 'p',	NULL, NULL},
 	{ NULL, 'n', POPT_ARG_STRING, &name, 'n',	NULL, NULL},
@@ -68,7 +60,6 @@ static int addTriggerIndex(Package pkg, const char *file,
 /* We then pass the remaining arguments to parseRCPOT, along with   */
 /* an index we just determined.                                     */
 
-/*@-boundswrite@*/
 int parseScript(Spec spec, int parsePart)
 {
     /* There are a few options to scripts: */
@@ -99,13 +90,10 @@ int parseScript(Spec spec, int parsePart)
     poptContext optCon = NULL;
     
     reqargs[0] = '\0';
-    /*@-mods@*/
     name = NULL;
     prog = "/bin/sh";
     file = NULL;
-    /*@=mods@*/
     
-    /*@-branchstate@*/
     switch (parsePart) {
       case PART_PRE:
 	tag = RPMTAG_PREIN;
@@ -171,7 +159,6 @@ int parseScript(Spec spec, int parsePart)
 	partname = "%triggerpostun";
 	break;
     }
-    /*@=branchstate@*/
 
     if (tag == RPMTAG_TRIGGERSCRIPTS) {
 	/* break line into two */
@@ -211,10 +198,10 @@ int parseScript(Spec spec, int parsePart)
 		rc = RPMERR_BADSPEC;
 		goto exit;
 	    }
-	    /*@switchbreak@*/ break;
+	    break;
 	case 'n':
 	    flag = PART_NAME;
-	    /*@switchbreak@*/ break;
+	    break;
 	}
     }
     
@@ -228,10 +215,8 @@ int parseScript(Spec spec, int parsePart)
     }
 
     if (poptPeekArg(optCon)) {
-	/*@-mods@*/
 	if (name == NULL)
 	    name = poptGetArg(optCon);
-	/*@=mods@*/
 	if (poptPeekArg(optCon)) {
 	    rpmError(RPMERR_BADSPEC, _("line %d: Too many names: %s\n"),
 		     spec->lineNum,
@@ -364,4 +349,3 @@ exit:
     
     return rc;
 }
-/*@=boundswrite@*/
diff --git a/build/parseSpec.c b/build/parseSpec.c
index 912b9778a..4e267be0d 100644
--- a/build/parseSpec.c
+++ b/build/parseSpec.c
@@ -11,15 +11,11 @@
 #include "rpmts.h"
 #include "debug.h"
 
-/*@access FD_t @*/	/* compared with NULL */
-
 /**
  */
-/*@unchecked@*/
 static struct PartRec {
     int part;
     int len;
-/*@observer@*/ /*@null@*/
     const char * token;
 } partList[] = {
     { PART_PREAMBLE,      0, "%package"},
@@ -48,7 +44,6 @@ static struct PartRec {
 /**
  */
 static inline void initParts(struct PartRec *p)
-	/*@modifies p->len @*/
 {
     for (; p->token != NULL; p++)
 	p->len = strlen(p->token);
@@ -58,18 +53,14 @@ rpmParseState isPart(const char *line)
 {
     struct PartRec *p;
 
-/*@-boundsread@*/
     if (partList[0].len == 0)
 	initParts(partList);
-/*@=boundsread@*/
     
     for (p = partList; p->token != NULL; p++) {
 	char c;
 	if (xstrncasecmp(line, p->token, p->len))
 	    continue;
-/*@-boundsread@*/
 	c = *(line + p->len);
-/*@=boundsread@*/
 	if (c == '\0' || xisspace(c))
 	    break;
     }
@@ -80,13 +71,11 @@ rpmParseState isPart(const char *line)
 /**
  */
 static int matchTok(const char *token, const char *line)
-	/*@*/
 {
     const char *b, *be = line;
     size_t toklen = strlen(token);
     int rc = 0;
 
-/*@-boundsread@*/
     while ( *(b = be) != '\0' ) {
 	SKIPSPACE(b);
 	be = b;
@@ -98,24 +87,20 @@ static int matchTok(const char *token, const char *line)
 	rc = 1;
 	break;
     }
-/*@=boundsread@*/
 
     return rc;
 }
 
-/*@-boundswrite@*/
 void handleComments(char *s)
 {
     SKIPSPACE(s);
     if (*s == '#')
 	*s = '\0';
 }
-/*@=boundswrite@*/
 
 /**
  */
 static void forceIncludeFile(Spec spec, const char * fileName)
-	/*@modifies spec->fileStack @*/
 {
     OFI_t * ofi;
 
@@ -127,13 +112,7 @@ static void forceIncludeFile(Spec spec, const char * fileName)
 
 /**
  */
-/*@-boundswrite@*/
 static int copyNextLine(Spec spec, OFI_t *ofi, int strip)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem @*/
-	/*@modifies spec->nextline, spec->nextpeekc, spec->lbuf, spec->line,
-		ofi->readPtr,
-		rpmGlobalMacroContext, fileSystem @*/
 {
     char *last;
     char ch;
@@ -152,9 +131,7 @@ static int copyNextLine(Spec spec, OFI_t *ofi, int strip)
 	ch = ' ';
 	while (*from && ch != '\n')
 	    ch = *to++ = *from++;
-/*@-mods@*/
 	spec->lbufPtr = to;
-/*@=mods@*/
 	*to++ = '\0';
 	ofi->readPtr = from;
 
@@ -163,37 +140,33 @@ static int copyNextLine(Spec spec, OFI_t *ofi, int strip)
 	    switch (*p) {
 		case '\\':
 		    switch (*(p+1)) {
-			case '\n': p++, nc = 1; /*@innerbreak@*/ break;
-			case '\0': /*@innerbreak@*/ break;
-			default: p++; /*@innerbreak@*/ break;
+			case '\n': p++, nc = 1; break;
+			case '\0': break;
+			default: p++; break;
 		    }
-		    /*@switchbreak@*/ break;
-		case '\n': nc = 0; /*@switchbreak@*/ break;
+		    break;
+		case '\n': nc = 0; break;
 		case '%':
 		    switch (*(p+1)) {
-			case '{': p++, bc++; /*@innerbreak@*/ break;
-			case '(': p++, pc++; /*@innerbreak@*/ break;
-			case '%': p++; /*@innerbreak@*/ break;
+			case '{': p++, bc++; break;
+			case '(': p++, pc++; break;
+			case '%': p++; break;
 		    }
-		    /*@switchbreak@*/ break;
-		case '{': if (bc > 0) bc++; /*@switchbreak@*/ break;
-		case '}': if (bc > 0) bc--; /*@switchbreak@*/ break;
-		case '(': if (pc > 0) pc++; /*@switchbreak@*/ break;
-		case ')': if (pc > 0) pc--; /*@switchbreak@*/ break;
+		    break;
+		case '{': if (bc > 0) bc++; break;
+		case '}': if (bc > 0) bc--; break;
+		case '(': if (pc > 0) pc++; break;
+		case ')': if (pc > 0) pc--; break;
 	    }
 	}
 	
 	/* If it doesn't, ask for one more line. We need a better
 	 * error code for this. */
 	if (pc || bc || nc ) {
-/*@-observertrans -readonlytrans@*/
 	    spec->nextline = "";
-/*@=observertrans =readonlytrans@*/
 	    return RPMERR_UNMATCHEDIF;
 	}
-/*@-mods@*/
 	spec->lbufPtr = spec->lbuf;
-/*@=mods@*/
 
 	/* Don't expand macros (eg. %define) in false branch of %if clause */
 	if (spec->readStack->reading &&
@@ -228,9 +201,7 @@ static int copyNextLine(Spec spec, OFI_t *ofi, int strip)
 
     return 0;
 }
-/*@=boundswrite@*/
 
-/*@-boundswrite@*/
 int readLine(Spec spec, int strip)
 {
 #ifdef	DYING
@@ -245,7 +216,6 @@ int readLine(Spec spec, int strip)
 
 retry:
     /* Make sure the current file is open */
-    /*@-branchstate@*/
     if (ofi->fd == NULL) {
 	ofi->fd = Fopen(ofi->fileName, "r.fpio");
 	if (ofi->fd == NULL || Ferror(ofi->fd)) {
@@ -256,13 +226,11 @@ retry:
 	}
 	spec->lineNum = ofi->lineNum = 0;
     }
-    /*@=branchstate@*/
 
     /* Make sure we have something in the read buffer */
     if (!(ofi->readPtr && *(ofi->readPtr))) {
-	/*@-type@*/ /* FIX: cast? */
+	/* FIX: cast? */
 	FILE * f = fdGetFp(ofi->fd);
-	/*@=type@*/
 	if (f == NULL || !fgets(ofi->readBuf, BUFSIZ, f)) {
 	    /* EOF */
 	    if (spec->readStack->next) {
@@ -410,11 +378,9 @@ retry:
 	spec->line[0] = '\0';
     }
 
-    /*@-compmempass@*/ /* FIX: spec->readStack->next should be dependent */
+    /* FIX: spec->readStack->next should be dependent */
     return 0;
-    /*@=compmempass@*/
 }
-/*@=boundswrite@*/
 
 void closeSpec(Spec spec)
 {
@@ -429,13 +395,8 @@ void closeSpec(Spec spec)
     }
 }
 
-/*@-redecl@*/
-/*@unchecked@*/
 extern int noLang;		/* XXX FIXME: pass as arg */
-/*@=redecl@*/
 
-/*@todo Skip parse recursion if os is not compatible. @*/
-/*@-boundswrite@*/
 int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 		const char *buildRootURL, int recursing, const char *passPhrase,
 		const char *cookie, int anyarch, int force)
@@ -464,9 +425,7 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
     if (buildRootURL) {
 	const char * buildRoot;
 	(void) urlPath(buildRootURL, &buildRoot);
-	/*@-branchstate@*/
 	if (*buildRoot == '\0') buildRoot = "/";
-	/*@=branchstate@*/
 	if (!strcmp(buildRoot, "/")) {
             rpmError(RPMERR_BADSPEC,
                      _("BuildRoot can not be \"/\": %s\n"), buildRootURL);
@@ -494,28 +453,28 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
     /* in the spec's line buffer.  Except for parsePreamble(),   */
     /* which handles the initial entry into a spec file.         */
     
-    /*@-infloops@*/	/* LCL: parsePart is modified @*/
+   	/* LCL: parsePart is modified @*/
     while (parsePart < PART_LAST && parsePart != PART_NONE) {
 	switch (parsePart) {
 	case PART_PREAMBLE:
 	    parsePart = parsePreamble(spec, initialPackage);
 	    initialPackage = 0;
-	    /*@switchbreak@*/ break;
+	    break;
 	case PART_PREP:
 	    parsePart = parsePrep(spec);
-	    /*@switchbreak@*/ break;
+	    break;
 	case PART_BUILD:
 	case PART_INSTALL:
 	case PART_CHECK:
 	case PART_CLEAN:
 	    parsePart = parseBuildInstallClean(spec, parsePart);
-	    /*@switchbreak@*/ break;
+	    break;
 	case PART_CHANGELOG:
 	    parsePart = parseChangelog(spec);
-	    /*@switchbreak@*/ break;
+	    break;
 	case PART_DESCRIPTION:
 	    parsePart = parseDescription(spec);
-	    /*@switchbreak@*/ break;
+	    break;
 
 	case PART_PRE:
 	case PART_POST:
@@ -528,16 +487,16 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 	case PART_TRIGGERUN:
 	case PART_TRIGGERPOSTUN:
 	    parsePart = parseScript(spec, parsePart);
-	    /*@switchbreak@*/ break;
+	    break;
 
 	case PART_FILES:
 	    parsePart = parseFiles(spec);
-	    /*@switchbreak@*/ break;
+	    break;
 
 	case PART_NONE:		/* XXX avoid gcc whining */
 	case PART_LAST:
 	case PART_BUILDARCHITECTURES:
-	    /*@switchbreak@*/ break;
+	    break;
 	}
 
 	if (parsePart >= PART_LAST) {
@@ -559,7 +518,7 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 
 		/* Skip if not arch is not compatible. */
 		if (!rpmMachineScore(RPM_MACHTABLE_BUILDARCH, spec->BANames[x]))
-		    /*@innercontinue@*/ continue;
+		    continue;
 #ifdef	DYING
 		rpmGetMachine(&saveArch, NULL);
 		saveArch = xstrdup(saveArch);
@@ -573,10 +532,8 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 		 || (spec->BASpecs[index] = rpmtsSetSpec(ts, NULL)) == NULL)
 		{
 			spec->BACount = index;
-/*@-nullstate@*/
 			spec = freeSpec(spec);
 			return RPMERR_BADSPEC;
-/*@=nullstate@*/
 		}
 #ifdef	DYING
 		rpmSetMachine(saveArch, NULL);
@@ -591,10 +548,8 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 	    if (! index) {
 		rpmError(RPMERR_BADSPEC,
 			_("No compatible architectures found for build\n"));
-/*@-nullstate@*/
 		spec = freeSpec(spec);
 		return RPMERR_BADSPEC;
-/*@=nullstate@*/
 	    }
 
 	    /*
@@ -606,20 +561,18 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 	     * further problem that the macro context, particularly
 	     * %{_target_cpu}, disagrees with the info in the header.
 	     */
-	    /*@-branchstate@*/
 	    if (spec->BACount >= 1) {
 		Spec nspec = spec->BASpecs[0];
 		spec->BASpecs = _free(spec->BASpecs);
 		spec = freeSpec(spec);
 		spec = nspec;
 	    }
-	    /*@=branchstate@*/
 
 	    (void) rpmtsSetSpec(ts, spec);
 	    return 0;
 	}
     }
-    /*@=infloops@*/	/* LCL: parsePart is modified @*/
+   	/* LCL: parsePart is modified @*/
 
     /* Check for description in each package and add arch and os */
   {
@@ -681,4 +634,3 @@ int parseSpec(rpmts ts, const char *specFile, const char *rootURL,
 
     return 0;
 }
-/*@=boundswrite@*/
diff --git a/build/poptBT.c b/build/poptBT.c
index 07ac2cf6e..df266e88e 100644
--- a/build/poptBT.c
+++ b/build/poptBT.c
@@ -12,7 +12,6 @@
 #include "legacy.h"	/* XXX _noDirTokens */
 #include "debug.h"
 
-/*@unchecked@*/
 struct rpmBuildArguments_s         rpmBTArgs;
 
 #define	POPT_USECATALOG		-1011
@@ -43,32 +42,22 @@ struct rpmBuildArguments_s         rpmBTArgs;
 #define	POPT_TP			0x7470
 #define	POPT_TS			0x7473
 
-/*@-redecl@*/
-/*@unchecked@*/
 extern int _fsm_debug;
-/*@=redecl@*/
 
-/*@-exportlocal@*/
-/*@unchecked@*/
 int noLang = 0;
-/*@=exportlocal@*/
 
-/*@unchecked@*/
 static int noBuild = 0;
 
-/*@unchecked@*/
 static int signIt = 0;
 
-/*@unchecked@*/
 static int useCatalog = 0;
 
 /**
  */
-/*@-boundswrite@*/
-static void buildArgCallback( /*@unused@*/ poptContext con,
-	/*@unused@*/ enum poptCallbackReason reason,
+static void buildArgCallback( poptContext con,
+	enum poptCallbackReason reason,
 	const struct poptOption * opt, const char * arg,
-	/*@unused@*/ const void * data)
+	const void * data)
 {
     BTA_t rba = &rpmBTArgs;
 
@@ -144,17 +133,13 @@ static void buildArgCallback( /*@unused@*/ poptContext con,
 
     }
 }
-/*@=boundswrite@*/
 
 /**
  */
-/*@-bitwisesigned -compmempass @*/
-/*@unchecked@*/
 struct poptOption rpmBuildPoptTable[] = {
-/*@-type@*/ /* FIX: cast? */
+/* FIX: cast? */
  { NULL, '\0', POPT_ARG_CALLBACK | POPT_CBFLAG_INC_DATA | POPT_CBFLAG_CONTINUE,
 	buildArgCallback, 0, NULL, NULL },
-/*@=type@*/
 
  { "bp", 0, POPT_ARGFLAG_ONEDASH, 0, POPT_BP,
 	N_("build through %prep (unpack sources and apply patches) from <specfile>"),
@@ -249,4 +234,3 @@ struct poptOption rpmBuildPoptTable[] = {
 
    POPT_TABLEEND
 };
-/*@=bitwisesigned =compmempass @*/
diff --git a/build/reqprov.c b/build/reqprov.c
index 0178b1573..3d68ac797 100644
--- a/build/reqprov.c
+++ b/build/reqprov.c
@@ -8,7 +8,7 @@
 #include "rpmbuild.h"
 #include "debug.h"
 
-int addReqProv(/*@unused@*/ Spec spec, Header h, /*@unused@*/ rpmTag tagN,
+int addReqProv(Spec spec, Header h, rpmTag tagN,
 		const char * N, const char * EVR, rpmsenseFlags Flags,
 		int index)
 {
@@ -57,10 +57,8 @@ int addReqProv(/*@unused@*/ Spec spec, Header h, /*@unused@*/ rpmTag tagN,
 
     Flags = (Flags & RPMSENSE_SENSEMASK) | extra;
 
-    /*@-branchstate@*/
     if (EVR == NULL)
 	EVR = "";
-    /*@=branchstate@*/
     
     /* Check for duplicate dependencies. */
     if (hge(h, nametag, &dnt, (void **) &names, &len)) {
@@ -77,7 +75,6 @@ int addReqProv(/*@unused@*/ Spec spec, Header h, /*@unused@*/ rpmTag tagN,
 	if (indextag)
 	    xx = hge(h, indextag, NULL, (void **) &indexes, NULL);
 
-/*@-boundsread@*/
 	while (len > 0) {
 	    len--;
 	    if (strcmp(names[len], N))
@@ -93,7 +90,6 @@ int addReqProv(/*@unused@*/ Spec spec, Header h, /*@unused@*/ rpmTag tagN,
 
 	    break;
 	}
-/*@=boundsread@*/
 	names = hfd(names, dnt);
 	versions = hfd(versions, dvt);
 	if (duplicate)
@@ -114,7 +110,6 @@ int addReqProv(/*@unused@*/ Spec spec, Header h, /*@unused@*/ rpmTag tagN,
     return 0;
 }
 
-/*@-boundswrite@*/
 int rpmlibNeedsFeature(Header h, const char * feature, const char * featureEVR)
 {
     char * reqname = alloca(sizeof("rpmlib()") + strlen(feature));
@@ -125,4 +120,3 @@ int rpmlibNeedsFeature(Header h, const char * feature, const char * featureEVR)
    return addReqProv(NULL, h, RPMTAG_REQUIRENAME, reqname, featureEVR,
 	RPMSENSE_RPMLIB|(RPMSENSE_LESS|RPMSENSE_EQUAL), 0);
 }
-/*@=boundswrite@*/
diff --git a/build/rpmbuild.h b/build/rpmbuild.h
index c94ddf1ca..12cf6ab82 100644
--- a/build/rpmbuild.h
+++ b/build/rpmbuild.h
@@ -18,11 +18,8 @@
 /** \ingroup rpmbuild
  * Bit(s) to control buildSpec() operation.
  */
-/*@-typeuse@*/
 typedef enum rpmBuildFlags_e {
-/*@-enummemuse@*/
     RPMBUILD_NONE	= 0,
-/*@=enummemuse@*/
     RPMBUILD_PREP	= (1 <<  0),	/*!< Execute %%prep. */
     RPMBUILD_BUILD	= (1 <<  1),	/*!< Execute %%build. */
     RPMBUILD_INSTALL	= (1 <<  2),	/*!< Execute %%install. */
@@ -36,7 +33,6 @@ typedef enum rpmBuildFlags_e {
     RPMBUILD_STRINGBUF	= (1 << 10),	/*!< only for doScript() */
     RPMBUILD_RMSPEC	= (1 << 11)	/*!< Remove spec file. */
 } rpmBuildFlags;
-/*@=typeuse@*/
 
 #include <ctype.h>
 
@@ -81,14 +77,11 @@ typedef enum rpmParseState_e {
 #ifdef __cplusplus
 extern "C" {
 #endif
-/*@-redecl@*/
 
 /** \ingroup rpmbuild
  * Destroy uid/gid caches.
  */
-void freeNames(void)
-	/*@globals internalState@*/
-	/*@modifies internalState */;
+void freeNames(void);
 
 /** \ingroup rpmbuild
  * Return cached user name from user id.
@@ -96,9 +89,7 @@ void freeNames(void)
  * @param uid		user id
  * @return		cached user name
  */
-extern /*@observer@*/ const char * getUname(uid_t uid)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+extern const char * getUname(uid_t uid);
 
 /** \ingroup rpmbuild
  * Return cached user name.
@@ -106,9 +97,7 @@ extern /*@observer@*/ const char * getUname(uid_t uid)
  * @param uname		user name
  * @return		cached user name
  */
-extern /*@observer@*/ const char * getUnameS(const char * uname)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+extern const char * getUnameS(const char * uname);
 
 /** \ingroup rpmbuild
  * Return cached user id.
@@ -116,9 +105,7 @@ extern /*@observer@*/ const char * getUnameS(const char * uname)
  * @param uname		user name
  * @return		cached uid
  */
-uid_t getUidS(const char * uname)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+uid_t getUidS(const char * uname);
 
 /** \ingroup rpmbuild
  * Return cached group name from group id.
@@ -126,9 +113,7 @@ uid_t getUidS(const char * uname)
  * @param gid		group id
  * @return		cached group name
  */
-extern /*@observer@*/ const char * getGname(gid_t gid)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+extern const char * getGname(gid_t gid);
 
 /** \ingroup rpmbuild
  * Return cached group name.
@@ -136,9 +121,7 @@ extern /*@observer@*/ const char * getGname(gid_t gid)
  * @param gname		group name
  * @return		cached group name
  */
-extern /*@observer@*/ const char * getGnameS(const char * gname)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+extern const char * getGnameS(const char * gname);
 
 /** \ingroup rpmbuild
  * Return cached group id.
@@ -146,21 +129,19 @@ extern /*@observer@*/ const char * getGnameS(const char * gname)
  * @param gname		group name
  * @return		cached gid
  */
-gid_t getGidS(const char * gname)
-	/*@globals internalState @*/
-	/*@modifies internalState @*/;
+gid_t getGidS(const char * gname);
 
 /** \ingroup rpmbuild
  * Return build hostname.
  * @return		build hostname
  */
-extern /*@observer@*/ const char * buildHost(void)	/*@*/;
+extern const char * buildHost(void)	;
 
 /** \ingroup rpmbuild
  * Return build time stamp.
  * @return		build time stamp
  */
-extern /*@observer@*/ int_32 * getBuildTime(void)	/*@*/;
+extern int_32 * getBuildTime(void)	;
 
 /** \ingroup rpmbuild
  * Read next line from spec file.
@@ -168,33 +149,26 @@ extern /*@observer@*/ int_32 * getBuildTime(void)	/*@*/;
  * @param strip		truncate comments?
  * @return		0 on success, 1 on EOF, <0 on error
  */
-int readLine(Spec spec, int strip)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem, internalState  @*/;
+int readLine(Spec spec, int strip);
 
 /** \ingroup rpmbuild
  * Stop reading from spec file, freeing resources.
  * @param spec		spec file control structure
  */
-void closeSpec(/*@partial@*/ Spec spec)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies spec->fileStack, fileSystem, internalState @*/;
+void closeSpec(Spec spec);
 
 /** \ingroup rpmbuild
  * Truncate comment lines.
  * @param s		skip white space, truncate line at '#'
  */
-void handleComments(char * s)
-	/*@modifies s @*/;
+void handleComments(char * s);
 
 /** \ingroup rpmbuild
  * Check line for section separator, return next parser state.
  * @param		line from spec file
  * @return		next parser state
  */
-rpmParseState isPart(const char * line)	/*@*/;
+rpmParseState isPart(const char * line)	;
 
 /** \ingroup rpmbuild
  * Parse a number.
@@ -202,8 +176,7 @@ rpmParseState isPart(const char * line)	/*@*/;
  * @retval res		pointer to int
  * @return		0 on success, 1 on failure
  */
-int parseNum(/*@null@*/ const char * line, /*@null@*/ /*@out@*/int * res)
-	/*@modifies *res @*/;
+int parseNum(const char * line,int * res);
 
 /** \ingroup rpmbuild
  * Add changelog entry to header.
@@ -213,8 +186,7 @@ int parseNum(/*@null@*/ const char * line, /*@null@*/ /*@out@*/int * res)
  * @param text		description of change
  */
 void addChangelogEntry(Header h, time_t time, const char * name,
-		const char * text)
-	/*@modifies h @*/;
+		const char * text);
 
 /** \ingroup rpmbuild
  * Parse %%build/%%install/%%clean section(s) of a spec file.
@@ -222,50 +194,28 @@ void addChangelogEntry(Header h, time_t time, const char * name,
  * @param parsePart	current rpmParseState
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->build, spec->install, spec->check, spec->clean,
-		spec->macros,
-		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int parseBuildInstallClean(Spec spec, rpmParseState parsePart);
 
 /** \ingroup rpmbuild
  * Parse %%changelog section of a spec file.
  * @param spec		spec file control structure
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parseChangelog(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		spec->packages->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int parseChangelog(Spec spec);
 
 /** \ingroup rpmbuild
  * Parse %%description section of a spec file.
  * @param spec		spec file control structure
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parseDescription(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, 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, internalState  @*/;
+int parseDescription(Spec spec);
 
 /** \ingroup rpmbuild
  * Parse %%files section of a spec file.
  * @param spec		spec file control structure
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parseFiles(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->packages,
-		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int parseFiles(Spec spec);
 
 /** \ingroup rpmbuild
  * Parse tags from preamble of a spec file.
@@ -273,30 +223,14 @@ int parseFiles(Spec spec)
  * @param initialPackage
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parsePreamble(Spec spec, int initialPackage)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies spec->packages,
-		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->buildSubdir,
-		spec->macros, spec->st, spec->buildRootURL,
-		spec->sources, spec->numSources, spec->noSource,
-		spec->buildRestrictions, spec->BANames, spec->BACount,
-		spec->gotBuildRootURL,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int parsePreamble(Spec spec, int initialPackage);
 
 /** \ingroup rpmbuild
  * Parse %%prep section of a spec file.
  * @param spec		spec file control structure
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parsePrep(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, 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, internalState @*/;
+int parsePrep(Spec spec);
 
 /** \ingroup rpmbuild
  * Parse dependency relations from spec file and/or autogenerated output buffer.
@@ -309,9 +243,7 @@ int parsePrep(Spec spec)
  * @return		0 on success, RPMERR_BADSPEC on failure
  */
 int parseRCPOT(Spec spec, Package pkg, const char * field, rpmTag tagN,
-		int index, rpmsenseFlags tagflags)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies rpmGlobalMacroContext @*/;
+		int index, rpmsenseFlags tagflags);
 
 /** \ingroup rpmbuild
  * Parse %%pre et al scriptlets from a spec file.
@@ -319,12 +251,7 @@ int parseRCPOT(Spec spec, Package pkg, const char * field, rpmTag tagN,
  * @param parsePart	current rpmParseState
  * @return		>= 0 next rpmParseState, < 0 on error
  */
-int parseScript(Spec spec, int parsePart)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->packages,
-		spec->fileStack, spec->readStack, spec->line, spec->lineNum,
-		spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-		rpmGlobalMacroContext, fileSystem, internalState  @*/;
+int parseScript(Spec spec, int parsePart);
 
 /** \ingroup rpmbuild
  * Evaluate boolean expression.
@@ -332,9 +259,7 @@ int parseScript(Spec spec, int parsePart)
  * @param expr		expression to parse
  * @return
  */
-int parseExpressionBoolean(Spec spec, const char * expr)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies rpmGlobalMacroContext @*/;
+int parseExpressionBoolean(Spec spec, const char * expr);
 
 /** \ingroup rpmbuild
  * Evaluate string expression.
@@ -342,10 +267,7 @@ int parseExpressionBoolean(Spec spec, const char * expr)
  * @param expr		expression to parse
  * @return
  */
-/*@unused@*/ /*@null@*/
-char * parseExpressionString(Spec spec, const char * expr)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies rpmGlobalMacroContext @*/;
+char * parseExpressionString(Spec spec, const char * expr);
 
 /** \ingroup rpmbuild
  * Run a build script, assembled from spec file scriptlet section.
@@ -357,12 +279,8 @@ char * parseExpressionString(Spec spec, const char * expr)
  * @param test		don't execute scripts or package if testing
  * @return		0 on success, RPMERR_SCRIPT on failure
  */
-int doScript(Spec spec, int what, /*@null@*/ const char * name,
-		/*@null@*/ StringBuf sb, int test)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies spec->macros,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int doScript(Spec spec, int what, const char * name,
+		StringBuf sb, int test);
 
 /** \ingroup rpmbuild
  * Find sub-package control structure by name.
@@ -372,38 +290,29 @@ int doScript(Spec spec, int what, /*@null@*/ const char * name,
  * @retval pkg		package control structure
  * @return		0 on success, 1 on failure
  */
-int lookupPackage(Spec spec, /*@null@*/ const char * name, int flag,
-		/*@out@*/ Package * pkg)
-	/*@modifies spec->packages, *pkg @*/;
+int lookupPackage(Spec spec, const char * name, int flag,
+		Package * pkg);
 
 /** \ingroup rpmbuild
  * Create and initialize package control structure.
  * @param spec		spec file control structure
  * @return		package control structure
  */
-/*@only@*/
-Package newPackage(Spec spec)
-	/*@modifies spec->packages, spec->packages->next @*/;
+Package newPackage(Spec spec);
 
 /** \ingroup rpmbuild
  * Destroy all packages associated with spec file.
  * @param packages	package control structure chain
  * @return		NULL
  */
-/*@null@*/
-Package freePackages(/*@only@*/ /*@null@*/ Package packages)
-	/*@globals fileSystem @*/
-	/*@modifies packages, fileSystem @*/;
+Package freePackages(Package packages);
 
 /** \ingroup rpmbuild
  * Destroy package control structure.
  * @param pkg		package control structure
  * @return		NULL
  */
-/*@null@*/
-Package  freePackage(/*@only@*/ /*@null@*/ Package pkg)
-	/*@globals fileSystem @*/
-	/*@modifies pkg, fileSystem @*/;
+Package  freePackage(Package pkg);
 
 /** \ingroup rpmbuild
  * Add dependency to header, filtering duplicates.
@@ -416,10 +325,9 @@ Package  freePackage(/*@only@*/ /*@null@*/ Package pkg)
  * @param index		(0 always)
  * @return		0 always
  */
-int addReqProv(/*@unused@*/Spec spec, Header h, rpmTag tagN,
+int addReqProv(Spec spec, Header h, rpmTag tagN,
 		const char * N, const char * EVR, rpmsenseFlags Flags,
-		int index)
-	/*@modifies h @*/;
+		int index);
 
 /** \ingroup rpmbuild
  * Add rpmlib feature dependency.
@@ -428,8 +336,7 @@ int addReqProv(/*@unused@*/Spec spec, Header h, rpmTag tagN,
  * @param featureEVR	rpm feature epoch/version/release
  * @return		0 always
  */
-int rpmlibNeedsFeature(Header h, const char * feature, const char * featureEVR)
-	/*@modifies h @*/;
+int rpmlibNeedsFeature(Header h, const char * feature, const char * featureEVR);
 
 /** \ingroup rpmbuild
  * Post-build processing for binary package(s).
@@ -438,33 +345,20 @@ int rpmlibNeedsFeature(Header h, const char * feature, const char * featureEVR)
  * @param test		don't execute scripts or package if testing
  * @return		0 on success
  */
-int processBinaryFiles(Spec spec, int installSpecialDoc, int test)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->macros,
-		spec->packages->cpioList, spec->packages->fileList,
-		spec->packages->specialDoc, spec->packages->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int processBinaryFiles(Spec spec, int installSpecialDoc, int test);
 
 /** \ingroup rpmbuild
  * Create and initialize header for source package.
  * @param spec		spec file control structure
  */
-void initSourceHeader(Spec spec)
-	/*@modifies spec->sourceHeader,
-		spec->buildRestrictions, spec->BANames,
-		spec->packages->header @*/;
+void initSourceHeader(Spec spec);
 
 /** \ingroup rpmbuild
  * Post-build processing for source package.
  * @param spec		spec file control structure
  * @return		0 on success
  */
-int processSourceFiles(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->sourceHeader, spec->sourceCpioList,
-		spec->buildRestrictions, spec->BANames,
-		spec->packages->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int processSourceFiles(Spec spec);
 
 /** \ingroup rpmbuild
  * Parse spec file into spec control structure.
@@ -480,14 +374,12 @@ int processSourceFiles(Spec spec)
  * @return
  */
 int parseSpec(rpmts ts, const char * specFile,
-		/*@null@*/ const char * rootURL,
-		/*@null@*/ const char * buildRootURL,
+		const char * rootURL,
+		const char * buildRootURL,
 		int recursing,
-		/*@null@*/ const char * passPhrase,
-		/*@null@*/ const char * cookie,
-		int anyarch, int force)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies ts, rpmGlobalMacroContext, fileSystem, internalState @*/;
+		const char * passPhrase,
+		const char * cookie,
+		int anyarch, int force);
 
 /** \ingroup rpmbuild
  * Build stages state machine driver.
@@ -497,39 +389,22 @@ int parseSpec(rpmts ts, const char * specFile,
  * @param test		don't execute scripts or package if testing
  * @return		0 on success
  */
-int buildSpec(rpmts ts, Spec spec, int what, int test)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->sourceHeader, spec->sourceCpioList, spec->cookie,
-		spec->sourceRpmName, spec->sourcePkgId,
-		spec->macros, spec->BASpecs,
-		spec->buildRestrictions, spec->BANames,
-		spec->packages->cpioList, spec->packages->fileList,
-		spec->packages->specialDoc, spec->packages->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int buildSpec(rpmts ts, Spec spec, int what, int test);
 
 /** \ingroup rpmbuild
  * Generate binary package(s).
  * @param spec		spec file control structure
  * @return		0 on success
  */
-int packageBinaries(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->packages->header, spec->packages->cpioList,
-		spec->sourceRpmName,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int packageBinaries(Spec spec);
 
 /** \ingroup rpmbuild
  * Generate source package.
  * @param spec		spec file control structure
  * @return		0 on success
  */
-int packageSources(Spec spec)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies spec->sourceHeader, spec->cookie, spec->sourceCpioList,
-		spec->sourceRpmName, spec->sourcePkgId,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int packageSources(Spec spec);
 
-/*@=redecl@*/
 #ifdef __cplusplus
 }
 #endif
diff --git a/build/rpmfc.c b/build/rpmfc.c
index 9dfafdc36..5b33b9169 100644
--- a/build/rpmfc.c
+++ b/build/rpmfc.c
@@ -21,23 +21,17 @@
 
 #include "debug.h"
 
-/*@access rpmds @*/
 
 /**
  */
-static int rpmfcExpandAppend(/*@out@*/ ARGV_t * argvp, const ARGV_t av)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies *argvp, rpmGlobalMacroContext @*/
-	/*@requires maxRead(argvp) >= 0 @*/
+static int rpmfcExpandAppend(ARGV_t * argvp, const ARGV_t av)
 {
     ARGV_t argv = *argvp;
     int argc = argvCount(argv);
     int ac = argvCount(av);
     int i;
 
-/*@-bounds@*/	/* LCL: internal error */
     argv = xrealloc(argv, (argc + ac + 1) * sizeof(*argv));
-/*@=bounds@*/
     for (i = 0; i < ac; i++)
 	argv[argc + i] = rpmExpand(av[i], NULL);
     argv[argc + ac] = NULL;
@@ -55,12 +49,9 @@ static int rpmfcExpandAppend(/*@out@*/ ARGV_t * argvp, const ARGV_t av)
  * @param failNonZero	is script failure an error?
  * @return		buffered stdout from script, NULL on error
  */     
-/*@null@*/
-static StringBuf getOutputFrom(/*@null@*/ const char * dir, ARGV_t argv,
+static StringBuf getOutputFrom(const char * dir, ARGV_t argv,
                         const char * writePtr, int writeBytesLeft,
                         int failNonZero)
-        /*@globals fileSystem, internalState@*/
-        /*@modifies fileSystem, internalState@*/
 {
     pid_t child, reaped;
     int toProg[2];
@@ -70,9 +61,8 @@ static StringBuf getOutputFrom(/*@null@*/ const char * dir, ARGV_t argv,
     StringBuf readBuff;
     int done;
 
-    /*@-type@*/ /* FIX: cast? */
+    /* FIX: cast? */
     oldhandler = signal(SIGPIPE, SIG_IGN);
-    /*@=type@*/
 
     toProg[0] = toProg[1] = 0;
     (void) pipe(toProg);
@@ -164,14 +154,12 @@ top:
 	}
 	
 	/* Read any data from prog */
-/*@-boundswrite@*/
 	{   char buf[BUFSIZ+1];
 	    while ((nbr = read(fromProg[0], buf, sizeof(buf)-1)) > 0) {
 		buf[nbr] = '\0';
 		appendStringBuf(readBuff, buf);
 	    }
 	}
-/*@=boundswrite@*/
 
 	/* terminate on (non-blocking) EOF or error */
 	done = (nbr == 0 || (nbr < 0 && errno != EAGAIN));
@@ -183,9 +171,8 @@ top:
     	(void) close(toProg[1]);
     if (fromProg[0] >= 0)
 	(void) close(fromProg[0]);
-    /*@-type@*/ /* FIX: cast? */
+    /* FIX: cast? */
     (void) signal(SIGPIPE, oldhandler);
-    /*@=type@*/
 
     /* Collect status from prog */
     reaped = waitpid(child, &status, 0);
@@ -234,11 +221,9 @@ int rpmfcExec(ARGV_t av, StringBuf sb_stdin, StringBuf * sb_stdoutp,
 
     /* Build argv, appending args to the executable args. */
     xav = NULL;
-/*@-boundswrite@*/
     xx = argvAppend(&xav, pav);
     if (av[1])
 	xx = rpmfcExpandAppend(&xav, av + 1);
-/*@=boundswrite@*/
 
     if (sb_stdin != NULL) {
 	buf_stdin = getStringBuf(sb_stdin);
@@ -248,12 +233,10 @@ int rpmfcExec(ARGV_t av, StringBuf sb_stdin, StringBuf * sb_stdoutp,
     /* Read output from exec'd helper. */
     sb = getOutputFrom(NULL, xav, buf_stdin, buf_stdin_len, failnonzero);
 
-/*@-branchstate@*/
     if (sb_stdoutp != NULL) {
 	*sb_stdoutp = sb;
 	sb = NULL;	/* XXX don't free */
     }
-/*@=branchstate@*/
 
     ec = 0;
 
@@ -267,9 +250,7 @@ exit:
 
 /**
  */
-static int rpmfcSaveArg(/*@out@*/ ARGV_t * argvp, const char * key)
-	/*@modifies *argvp @*/
-	/*@requires maxSet(argvp) >= 0 @*/
+static int rpmfcSaveArg(ARGV_t * argvp, const char * key)
 {
     int rc = 0;
 
@@ -280,11 +261,8 @@ static int rpmfcSaveArg(/*@out@*/ ARGV_t * argvp, const char * key)
     return rc;
 }
 
-static char * rpmfcFileDep(/*@returned@*/ char * buf, int ix,
-		/*@null@*/ rpmds ds)
-	/*@modifies buf @*/
-	/*@requires maxSet(buf) >= 0 @*/
-	/*@ensures maxRead(buf) == 0 @*/
+static char * rpmfcFileDep(char * buf, int ix,
+		rpmds ds)
 {
     int_32 tagN = rpmdsTagN(ds);
     char deptype = 'X';
@@ -298,11 +276,9 @@ static char * rpmfcFileDep(/*@returned@*/ char * buf, int ix,
 	deptype = 'R';
 	break;
     }
-/*@-nullpass@*/
     if (ds != NULL)
 	sprintf(buf, "%08d%c %s %s 0x%08x", ix, deptype,
 		rpmdsN(ds), rpmdsEVR(ds), rpmdsFlags(ds));
-/*@=nullpass@*/
     return buf;
 };
 
@@ -314,8 +290,6 @@ static char * rpmfcFileDep(/*@returned@*/ char * buf, int ix,
  * @return		0 on success
  */
 static int rpmfcHelper(rpmfc fc, unsigned char deptype, const char * nsdep)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies fc, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char * fn = fc->fn[fc->ix];
     char buf[BUFSIZ];
@@ -335,7 +309,7 @@ static int rpmfcHelper(rpmfc fc, unsigned char deptype, const char * nsdep)
     switch (deptype) {
     default:
 	return -1;
-	/*@notreached@*/ break;
+	break;
     case 'P':
 	if (fc->skipProv)
 	    return 0;
@@ -360,9 +334,7 @@ static int rpmfcHelper(rpmfc fc, unsigned char deptype, const char * nsdep)
     sb_stdin = newStringBuf();
     appendLineStringBuf(sb_stdin, fn);
     sb_stdout = NULL;
-/*@-boundswrite@*/
     xx = rpmfcExec(av, sb_stdin, &sb_stdout, 0);
-/*@=boundswrite@*/
     sb_stdin = freeStringBuf(sb_stdin);
 
     if (xx == 0 && sb_stdout != NULL) {
@@ -374,30 +346,28 @@ static int rpmfcHelper(rpmfc fc, unsigned char deptype, const char * nsdep)
 	    N = pav[i];
 	    EVR = "";
 	    Flags = dsContext;
-/*@-branchstate@*/
 	    if (pav[i+1] && strchr("=<>", *pav[i+1])) {
 		i++;
 		for (s = pav[i]; *s; s++) {
 		    switch(*s) {
 		    default:
 assert(*s != '\0');
-			/*@switchbreak@*/ break;
+			break;
 		    case '=':
 			Flags |= RPMSENSE_EQUAL;
-			/*@switchbreak@*/ break;
+			break;
 		    case '<':
 			Flags |= RPMSENSE_LESS;
-			/*@switchbreak@*/ break;
+			break;
 		    case '>':
 			Flags |= RPMSENSE_GREATER;
-			/*@switchbreak@*/ break;
+			break;
 		    }
 		}
 		i++;
 		EVR = pav[i];
 assert(EVR != NULL);
 	    }
-/*@=branchstate@*/
 
 
 	    /* Add tracking dependency for versioned Provides: */
@@ -416,9 +386,7 @@ assert(EVR != NULL);
 	    xx = rpmdsMerge(depsp, ds);
 
 	    /* Add to file dependencies. */
-/*@-boundswrite@*/
 	    xx = rpmfcSaveArg(&fc->ddict, rpmfcFileDep(buf, fc->ix, ds));
-/*@=boundswrite@*/
 
 	    ds = rpmdsFree(ds);
 	}
@@ -432,7 +400,6 @@ assert(EVR != NULL);
 
 /**
  */
-/*@unchecked@*/ /*@observer@*/
 static struct rpmfcTokens_s rpmfcTokens[] = {
   { "directory",		RPMFC_DIRECTORY|RPMFC_INCLUDE },
 
@@ -595,7 +562,7 @@ assert(fx < fc->fddictn->nvals);
 	    switch (deptype) {
 	    default:
 assert(depval != NULL);
-		/*@switchbreak@*/ break;
+		break;
 	    case 'P':
 		if (nprovides > 0) {
 assert(ix < nprovides);
@@ -603,7 +570,7 @@ assert(ix < nprovides);
 		    if (rpmdsNext(fc->provides) >= 0)
 			depval = rpmdsDNEVR(fc->provides);
 		}
-		/*@switchbreak@*/ break;
+		break;
 	    case 'R':
 		if (nrequires > 0) {
 assert(ix < nrequires);
@@ -611,7 +578,7 @@ assert(ix < nrequires);
 		    if (rpmdsNext(fc->requires) >= 0)
 			depval = rpmdsDNEVR(fc->requires);
 		}
-		/*@switchbreak@*/ break;
+		break;
 	    }
 	    if (depval)
 		fprintf(fp, "\t%s\n", depval);
@@ -655,8 +622,6 @@ rpmfc rpmfcNew(void)
  * @return		0 on success
  */
 static int rpmfcSCRIPT(rpmfc fc)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies fc, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char * fn = fc->fn[fc->ix];
     const char * bn;
@@ -681,7 +646,6 @@ static int rpmfcSCRIPT(rpmfc fc)
     }
 
     /* Look for #! interpreter in first 10 lines. */
-/*@-boundswrite@*/
     for (i = 0; i < 10; i++) {
 
 	s = fgets(buf, sizeof(buf) - 1, fp);
@@ -701,7 +665,7 @@ static int rpmfcSCRIPT(rpmfc fc)
 
 	for (se = s+1; *se; se++) {
 	    if (strchr(" \t\n\r", *se) != NULL)
-		/*@innerbreak@*/ break;
+		break;
 	}
 	*se = '\0';
 	se++;
@@ -726,7 +690,6 @@ static int rpmfcSCRIPT(rpmfc fc)
 
 	break;
     }
-/*@=boundswrite@*/
 
     (void) fclose(fp);
 
@@ -772,8 +735,6 @@ static int rpmfcSCRIPT(rpmfc fc)
  * @return		0 on success
  */
 static int rpmfcELF(rpmfc fc)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies fc, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
 #if HAVE_GELF_H && HAVE_LIBELF
     const char * fn = fc->fn[fc->ix];
@@ -822,19 +783,16 @@ static int rpmfcELF(rpmfc fc)
 
     (void) elf_version(EV_CURRENT);
 
-/*@-evalorder@*/
     elf = NULL;
     if ((elf = elf_begin (fdno, ELF_C_READ, NULL)) == NULL
      || elf_kind(elf) != ELF_K_ELF
      || (ehdr = gelf_getehdr(elf, &ehdr_mem)) == NULL
      || !(ehdr->e_type == ET_DYN || ehdr->e_type == ET_EXEC))
 	goto exit;
-/*@=evalorder@*/
 
     isElf64 = ehdr->e_ident[EI_CLASS] == ELFCLASS64;
     isDSO = ehdr->e_type == ET_DYN;
 
-    /*@-branchstate -uniondef @*/
     scn = NULL;
     while ((scn = elf_nextscn(elf, scn)) != NULL) {
 	shdr = gelf_getshdr(scn, &shdr_mem);
@@ -845,7 +803,7 @@ static int rpmfcELF(rpmfc fc)
 	switch (shdr->sh_type) {
 	default:
 	    continue;
-	    /*@notreached@*/ /*@switchbreak@*/ break;
+	    break;
 	case SHT_GNU_verdef:
 	    data = NULL;
 	    if (!fc->skipProv)
@@ -855,23 +813,23 @@ static int rpmfcELF(rpmfc fc)
 		
 		    def = gelf_getverdef (data, offset, &def_mem);
 		    if (def == NULL)
-			/*@innerbreak@*/ break;
+			break;
 		    auxoffset = offset + def->vd_aux;
 		    for (cnt2 = def->vd_cnt; --cnt2 >= 0; ) {
 			GElf_Verdaux aux_mem, * aux;
 
 			aux = gelf_getverdaux (data, auxoffset, &aux_mem);
 			if (aux == NULL)
-			    /*@innerbreak@*/ break;
+			    break;
 
 			s = elf_strptr(elf, shdr->sh_link, aux->vda_name);
 			if (s == NULL)
-			    /*@innerbreak@*/ break;
+			    break;
 			if (def->vd_flags & VER_FLG_BASE) {
 			    soname = _free(soname);
 			    soname = xstrdup(s);
 			    auxoffset += aux->vda_next;
-			    /*@innercontinue@*/ continue;
+			    continue;
 			} else
 			if (soname != NULL
 			 && !(filter_GLIBC_PRIVATE != 0
@@ -903,7 +861,7 @@ static int rpmfcELF(rpmfc fc)
 		    offset += def->vd_next;
 		}
 	    }
-	    /*@switchbreak@*/ break;
+	    break;
 	case SHT_GNU_verneed:
 	    data = NULL;
 	    /* Files with executable bit set only. */
@@ -913,11 +871,11 @@ static int rpmfcELF(rpmfc fc)
 		for (cnt = shdr->sh_info; --cnt >= 0; ) {
 		    need = gelf_getverneed (data, offset, &need_mem);
 		    if (need == NULL)
-			/*@innerbreak@*/ break;
+			break;
 
 		    s = elf_strptr(elf, shdr->sh_link, need->vn_file);
 		    if (s == NULL)
-			/*@innerbreak@*/ break;
+			break;
 		    soname = _free(soname);
 		    soname = xstrdup(s);
 		    auxoffset = offset + need->vn_aux;
@@ -926,11 +884,11 @@ static int rpmfcELF(rpmfc fc)
 
 			aux = gelf_getvernaux (data, auxoffset, &aux_mem);
 			if (aux == NULL)
-			    /*@innerbreak@*/ break;
+			    break;
 
 			s = elf_strptr(elf, shdr->sh_link, aux->vna_name);
 			if (s == NULL)
-			    /*@innerbreak@*/ break;
+			    break;
 
 			/* Filter dependencies that contain GLIBC_PRIVATE */
 			if (soname != NULL
@@ -962,54 +920,53 @@ static int rpmfcELF(rpmfc fc)
 		    offset += need->vn_next;
 		}
 	    }
-	    /*@switchbreak@*/ break;
+	    break;
 	case SHT_DYNAMIC:
 	    data = NULL;
 	    while ((data = elf_getdata (scn, data)) != NULL) {
-/*@-boundswrite@*/
 		for (cnt = 0; cnt < (shdr->sh_size / shdr->sh_entsize); ++cnt) {
 		    dyn = gelf_getdyn (data, cnt, &dyn_mem);
 		    if (dyn == NULL)
-			/*@innerbreak@*/ break;
+			break;
 		    s = NULL;
 		    switch (dyn->d_tag) {
 		    default:
-			/*@innercontinue@*/ continue;
-			/*@notreached@*/ /*@switchbreak@*/ break;
+			continue;
+			break;
                     case DT_HASH:    
 			gotHASH= 1;
-			/*@innercontinue@*/ continue;
+			continue;
                     case DT_GNU_HASH:
 			gotGNUHASH= 1;
-			/*@innercontinue@*/ continue;
+			continue;
                     case DT_DEBUG:    
 			gotDEBUG = 1;
-			/*@innercontinue@*/ continue;
+			continue;
 		    case DT_NEEDED:
 			/* Files with executable bit set only. */
 			if (fc->skipReq || !(st->st_mode & (S_IXUSR|S_IXGRP|S_IXOTH)))
-			    /*@innercontinue@*/ continue;
+			    continue;
 			/* Add to package requires. */
 			depsp = &fc->requires;
 			tagN = RPMTAG_REQUIRENAME;
 			dsContext = RPMSENSE_FIND_REQUIRES;
 			s = elf_strptr(elf, shdr->sh_link, dyn->d_un.d_val);
 assert(s != NULL);
-			/*@switchbreak@*/ break;
+			break;
 		    case DT_SONAME:
 			gotSONAME = 1;
 			/* Add to package provides. */
 			if (fc->skipProv)
-			    /*@innercontinue@*/ continue;
+			    continue;
 			depsp = &fc->provides;
 			tagN = RPMTAG_PROVIDENAME;
 			dsContext = RPMSENSE_FIND_PROVIDES;
 			s = elf_strptr(elf, shdr->sh_link, dyn->d_un.d_val);
 assert(s != NULL);
-			/*@switchbreak@*/ break;
+			break;
 		    }
 		    if (s == NULL)
-			/*@innercontinue@*/ continue;
+			continue;
 
 		    buf[0] = '\0';
 		    t = buf;
@@ -1031,12 +988,10 @@ assert(s != NULL);
 
 		    ds = rpmdsFree(ds);
 		}
-/*@=boundswrite@*/
 	    }
-	    /*@switchbreak@*/ break;
+	    break;
 	}
     }
-    /*@=branchstate =uniondef @*/
 
     /* For DSOs which use the .gnu_hash section and don't have a .hash
      * section, we need to ensure that we have a new enough glibc. */ 
@@ -1062,18 +1017,15 @@ assert(s != NULL);
 	else
 	    s = fn;
 
-/*@-boundswrite@*/
 	buf[0] = '\0';
 	t = buf;
-/*@-nullpass@*/ /* LCL: s is not null. */
+/* LCL: s is not null. */
 	t = stpcpy(t, s);
-/*@=nullpass@*/
 
 #if !defined(__alpha__)
 	if (isElf64)
 	    t = stpcpy(t, "()(64bit)");
 #endif
-/*@=boundswrite@*/
 	t++;
 
 	/* Add to package dependencies. */
@@ -1081,9 +1033,7 @@ assert(s != NULL);
 	xx = rpmdsMerge(depsp, ds);
 
 	/* Add to file dependencies. */
-/*@-boundswrite@*/
 	xx = rpmfcSaveArg(&fc->ddict, rpmfcFileDep(t, fc->ix, ds));
-/*@=boundswrite@*/
 
 	ds = rpmdsFree(ds);
     }
@@ -1105,7 +1055,6 @@ typedef struct rpmfcApplyTbl_s {
 
 /**
  */
-/*@unchecked@*/
 static struct rpmfcApplyTbl_s rpmfcApplyTable[] = {
     { rpmfcELF,		RPMFC_ELF },
     { rpmfcSCRIPT,	(RPMFC_SCRIPT|RPMFC_PERL) },
@@ -1152,12 +1101,11 @@ int rpmfcApply(rpmfc fc)
 	if (fc->fcolor->vals[fc->ix])
 	for (fcat = rpmfcApplyTable; fcat->func != NULL; fcat++) {
 	    if (!(fc->fcolor->vals[fc->ix] & fcat->colormask))
-		/*@innercontinue@*/ continue;
+		continue;
 	    xx = (*fcat->func) (fc);
 	}
     }
 
-/*@-boundswrite@*/
     /* Generate per-file indices into package dependencies. */
     nddict = argvCount(fc->ddict);
     previx = -1;
@@ -1182,17 +1130,17 @@ assert(se != NULL);
 	dix = -1;
 	switch (deptype) {
 	default:
-	    /*@switchbreak@*/ break;
+	    break;
 	case 'P':	
 	    ds = rpmdsSingle(RPMTAG_PROVIDENAME, N, EVR, Flags);
 	    dix = rpmdsFind(fc->provides, ds);
 	    ds = rpmdsFree(ds);
-	    /*@switchbreak@*/ break;
+	    break;
 	case 'R':
 	    ds = rpmdsSingle(RPMTAG_REQUIRENAME, N, EVR, Flags);
 	    dix = rpmdsFind(fc->requires, ds);
 	    ds = rpmdsFree(ds);
-	    /*@switchbreak@*/ break;
+	    break;
 	}
 
 /* XXX assertion incorrect while generating -debuginfo deps. */
@@ -1213,7 +1161,6 @@ assert(dix >= 0);
 	if (fc->fddictn && fc->fddictn->vals)
 	    fc->fddictn->vals[ix]++;
     }
-/*@=boundswrite@*/
 
     return 0;
 }
@@ -1226,7 +1173,6 @@ int rpmfcClassify(rpmfc fc, ARGV_t argv, int_16 * fmode)
     size_t slen;
     int fcolor;
     int xx;
-/*@observer@*/
     int msflags = MAGIC_CHECK;	/* XXX MAGIC_COMPRESS flag? */
     magic_t ms = NULL;
 
@@ -1303,7 +1249,6 @@ assert(s != NULL);
 assert(ftype != NULL);	/* XXX figger a proper return path. */
 	    }
 	}
-/*@=branchstate@*/
 
 	se = ftype;
         rpmMessage(RPMMESS_DEBUG, "%s: %s\n", s, se);
@@ -1318,10 +1263,8 @@ assert(ftype != NULL);	/* XXX figger a proper return path. */
 	fcolor = rpmfcColoring(se);
 	xx = argiAdd(&fc->fcolor, fc->ix, fcolor);
 
-/*@-boundswrite@*/
 	if (fcolor != RPMFC_WHITE && (fcolor & RPMFC_INCLUDE))
 	    xx = rpmfcSaveArg(&fc->cdict, se);
-/*@=boundswrite@*/
     }
 
     /* Build per-file class index array. */
@@ -1355,9 +1298,7 @@ typedef struct DepMsg_s * DepMsg_t;
 /**
  */
 struct DepMsg_s {
-/*@observer@*/ /*@null@*/
     const char * msg;
-/*@observer@*/
     const char * argv[4];
     rpmTag ntag;
     rpmTag vtag;
@@ -1368,7 +1309,6 @@ struct DepMsg_s {
 
 /**
  */
-/*@unchecked@*/
 static struct DepMsg_s depMsgs[] = {
   { "Provides",		{ "%{?__find_provides}", NULL, NULL, NULL },
 	RPMTAG_PROVIDENAME, RPMTAG_PROVIDEVERSION, RPMTAG_PROVIDEFLAGS,
@@ -1415,14 +1355,11 @@ static struct DepMsg_s depMsgs[] = {
   { NULL,		{ NULL, NULL, NULL, NULL },	0, 0, 0, 0, 0 }
 };
 
-/*@unchecked@*/
 static DepMsg_t DepMsgs = depMsgs;
 
 /**
  */
 static void printDeps(Header h)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies h, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     DepMsg_t dm;
     rpmds ds = NULL;
@@ -1449,13 +1386,13 @@ static void printDeps(Header h)
 	    Flags = rpmdsFlags(ds);
 	
 	    if (!((Flags & dm->mask) ^ dm->xor))
-		/*@innercontinue@*/ continue;
+		continue;
 	    if (bingo == 0) {
 		rpmMessage(RPMMESS_NORMAL, "%s:", (dm->msg ? dm->msg : ""));
 		bingo = 1;
 	    }
 	    if ((DNEVR = rpmdsDNEVR(ds)) == NULL)
-		/*@innercontinue@*/ continue;	/* XXX can't happen */
+		continue;	/* XXX can't happen */
 	    rpmMessage(RPMMESS_NORMAL, " %s", DNEVR+2);
 	}
 	if (bingo)
@@ -1467,8 +1404,6 @@ static void printDeps(Header h)
 /**
  */
 static int rpmfcGenerateDependsHelper(const Spec spec, Package pkg, rpmfi fi)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-        /*@modifies fi, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     StringBuf sb_stdin;
     StringBuf sb_stdout;
@@ -1500,21 +1435,19 @@ static int rpmfcGenerateDependsHelper(const Spec spec, Package pkg, rpmfi fi)
 		continue;
 	    failnonzero = 1;
 	    tagflags = RPMSENSE_FIND_PROVIDES;
-	    /*@switchbreak@*/ break;
+	    break;
 	case RPMTAG_REQUIREFLAGS:
 	    if (!pkg->autoReq)
 		continue;
 	    failnonzero = 0;
 	    tagflags = RPMSENSE_FIND_REQUIRES;
-	    /*@switchbreak@*/ break;
+	    break;
 	default:
 	    continue;
-	    /*@notreached@*/ /*@switchbreak@*/ break;
+	    break;
 	}
 
-/*@-boundswrite@*/
 	xx = rpmfcExec(dm->argv, sb_stdin, &sb_stdout, failnonzero);
-/*@=boundswrite@*/
 	if (xx == -1)
 	    continue;
 
@@ -1582,7 +1515,6 @@ int rpmfcGenerateDepends(const Spec spec, Package pkg)
     av = xcalloc(ac+1, sizeof(*av));
     fmode = xcalloc(ac+1, sizeof(*fmode));
 
-/*@-boundswrite@*/
     genConfigDeps = 0;
     fi = rpmfiInit(fi, 0);
     if (fi != NULL)
@@ -1597,7 +1529,6 @@ int rpmfcGenerateDepends(const Spec spec, Package pkg)
 	fmode[c] = rpmfiFMode(fi);
     }
     av[ac] = NULL;
-/*@=boundswrite@*/
 
     fc = rpmfcNew();
     fc->skipProv = !pkg->autoProv;
@@ -1687,13 +1618,11 @@ assert(ac == c);
 			p, c);
 
     /* Add Provides: */
-/*@-branchstate@*/
     if (fc->provides != NULL && (c = rpmdsCount(fc->provides)) > 0 && !fc->skipProv) {
 	p = (const void **) fc->provides->N;
 	xx = headerAddEntry(pkg->header, RPMTAG_PROVIDENAME, RPM_STRING_ARRAY_TYPE,
 			p, c);
 	/* XXX rpm prior to 3.0.2 did not always supply EVR and Flags. */
-/*@-nullpass@*/
 	p = (const void **) fc->provides->EVR;
 assert(p != NULL);
 	xx = headerAddEntry(pkg->header, RPMTAG_PROVIDEVERSION, RPM_STRING_ARRAY_TYPE,
@@ -1702,18 +1631,14 @@ assert(p != NULL);
 assert(p != NULL);
 	xx = headerAddEntry(pkg->header, RPMTAG_PROVIDEFLAGS, RPM_INT32_TYPE,
 			p, c);
-/*@=nullpass@*/
     }
-/*@=branchstate@*/
 
     /* Add Requires: */
-/*@-branchstate@*/
     if (fc->requires != NULL && (c = rpmdsCount(fc->requires)) > 0 && !fc->skipReq) {
 	p = (const void **) fc->requires->N;
 	xx = headerAddEntry(pkg->header, RPMTAG_REQUIRENAME, RPM_STRING_ARRAY_TYPE,
 			p, c);
 	/* XXX rpm prior to 3.0.2 did not always supply EVR and Flags. */
-/*@-nullpass@*/
 	p = (const void **) fc->requires->EVR;
 assert(p != NULL);
 	xx = headerAddEntry(pkg->header, RPMTAG_REQUIREVERSION, RPM_STRING_ARRAY_TYPE,
@@ -1722,9 +1647,7 @@ assert(p != NULL);
 assert(p != NULL);
 	xx = headerAddEntry(pkg->header, RPMTAG_REQUIREFLAGS, RPM_INT32_TYPE,
 			p, c);
-/*@=nullpass@*/
     }
-/*@=branchstate@*/
 
     /* Add dependency dictionary(#dependencies) */
     p = (const void **) argiData(fc->ddictx);
diff --git a/build/rpmfc.h b/build/rpmfc.h
index f7405c9b6..30171d725 100644
--- a/build/rpmfc.h
+++ b/build/rpmfc.h
@@ -3,14 +3,11 @@
 
 #include "magic.h"
 
-/*@-exportlocal@*/
-/*@unchecked@*/
 extern int _rpmfc_debug;
-/*@=exportlocal@*/
 
 /**
  */
-typedef /*@abstract@*/ struct rpmfc_s * rpmfc;
+typedef struct rpmfc_s * rpmfc;
 
 /**
  */
@@ -33,9 +30,7 @@ struct rpmfc_s {
     ARGV_t ddict;	/*!< (#dependencies) file depends dictionary */
     ARGI_t ddictx;	/*!< (#dependencies) file->dependency mapping */
 
-/*@relnull@*/
     rpmds provides;	/*!< (#provides) package provides */
-/*@relnull@*/
     rpmds requires;	/*!< (#requires) package requires */
 
     StringBuf sb_java;	/*!< concatenated list of java colored files. */
@@ -89,7 +84,6 @@ typedef	enum FCOLOR_e FCOLOR_t;
 /**
  */
 struct rpmfcTokens_s {
-/*@observer@*/
     const char * token;
     int colors;
 };
@@ -109,22 +103,15 @@ extern "C" {
  * @retval *sb_stdoutp	helper output
  * @param failnonzero	IS non-zero helper exit status a failure?
  */
-int rpmfcExec(ARGV_t av, StringBuf sb_stdin, /*@out@*/ StringBuf * sb_stdoutp,
-		int failnonzero)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies *sb_stdoutp, rpmGlobalMacroContext,
-		fileSystem, internalState @*/
-        /*@requires maxSet(sb_stdoutp) >= 0 @*/;
+int rpmfcExec(ARGV_t av, StringBuf sb_stdin, StringBuf * sb_stdoutp,
+		int failnonzero);
 
 /**
  * Return file color given file(1) string.
  * @param fmstr		file(1) string
  * @return		file color
  */
-/*@-exportlocal@*/
-int rpmfcColoring(const char * fmstr)
-	/*@*/;
-/*@=exportlocal@*/
+int rpmfcColoring(const char * fmstr);
 
 /**
  * Print results of file classification.
@@ -133,31 +120,20 @@ int rpmfcColoring(const char * fmstr)
  * @param fc		file classifier
  * @param fp		output file handle (NULL for stderr)
  */
-/*@-exportlocal@*/
-void rpmfcPrint(/*@null@*/ const char * msg, rpmfc fc, /*@null@*/ FILE * fp)
-	/*@globals fileSystem @*/
-	/*@modifies *fp, fc, fileSystem @*/;
-/*@=exportlocal@*/
+void rpmfcPrint(const char * msg, rpmfc fc, FILE * fp);
 
 /**
  * Destroy a file classifier.
  * @param fc		file classifier
  * @return		NULL always
  */
-/*@-exportlocal@*/
-/*@null@*/
-rpmfc rpmfcFree(/*@only@*/ /*@null@*/ rpmfc fc)
-	/*@modifies fc @*/;
-/*@=exportlocal@*/
+rpmfc rpmfcFree(rpmfc fc);
 
 /**
  * Create a file classifier.
  * @return		new file classifier
  */
-/*@-exportlocal@*/
-rpmfc rpmfcNew(void)
-	/*@*/;
-/*@=exportlocal@*/
+rpmfc rpmfcNew(void);
 
 /**
  * Build file class dictionary and mappings.
@@ -166,21 +142,14 @@ rpmfc rpmfcNew(void)
  * @param fmode		files mode_t array (or NULL)
  * @return		0 on success
  */
-/*@-exportlocal@*/
-int rpmfcClassify(rpmfc fc, ARGV_t argv, /*@null@*/ int16_t * fmode)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies fc, fileSystem, internalState @*/;
-/*@=exportlocal@*/
+int rpmfcClassify(rpmfc fc, ARGV_t argv, int16_t * fmode);
 
 /**
  * Build file/package dependency dictionary and mappings.
  * @param fc		file classifier
  * @return		0 on success
  */
-/*@-exportlocal@*/
-int rpmfcApply(rpmfc fc)
-	/*@modifies fc @*/;
-/*@=exportlocal@*/
+int rpmfcApply(rpmfc fc);
 
 /**
  * Generate package dependencies.
@@ -188,10 +157,7 @@ int rpmfcApply(rpmfc fc)
  * @param pkg		package control
  * @return		0 on success
  */
-int rpmfcGenerateDepends(const Spec spec, Package pkg)
-	/*@globals rpmGlobalMacroContext, h_errno, fileSystem, internalState @*/
-	/*@modifies pkg->cpioList, pkg->header,
-		rpmGlobalMacroContext, fileSystem, internalState @*/;
+int rpmfcGenerateDepends(const Spec spec, Package pkg);
 
 #ifdef __cplusplus
 }
diff --git a/build/rpmspec.h b/build/rpmspec.h
index 763bd2cbf..161d3947f 100644
--- a/build/rpmspec.h
+++ b/build/rpmspec.h
@@ -14,10 +14,10 @@ typedef struct Package_s * Package;
  */
 struct TriggerFileEntry {
     int index;
-/*@only@*/ char * fileName;
-/*@only@*/ char * script;
-/*@only@*/ char * prog;
-/*@owned@*/ struct TriggerFileEntry * next;
+char * fileName;
+char * script;
+char * prog;
+struct TriggerFileEntry * next;
 };
 
 #define RPMBUILD_ISSOURCE	(1 << 0)
@@ -30,33 +30,28 @@ struct TriggerFileEntry {
 /** \ingroup rpmbuild
  */
 struct Source {
-/*@owned@*/ char * fullSource;
-/*@dependent@*/ char * source;     /* Pointer into fullSource */
+char * fullSource;
+char * source;     /* Pointer into fullSource */
     int flags;
     int num;
-/*@owned@*/ struct Source * next;
+struct Source * next;
 };
 
 /** \ingroup rpmbuild
  */
-/*@-typeuse@*/
 typedef struct ReadLevelEntry {
     int reading;
-/*@dependent@*/
     struct ReadLevelEntry * next;
 } RLE_t;
-/*@=typeuse@*/
 
 /** \ingroup rpmbuild
  */
 typedef struct OpenFileInfo {
-/*@only@*/ const char * fileName;
+const char * fileName;
     FD_t fd;
     int lineNum;
     char readBuf[BUFSIZ];
-/*@dependent@*/
     char * readPtr;
-/*@owned@*/
     struct OpenFileInfo * next;
 } OFI_t;
 
@@ -66,14 +61,14 @@ typedef struct spectag_s {
     int t_tag;
     int t_startx;
     int t_nlines;
-/*@only@*/ const char * t_lang;
-/*@only@*/ const char * t_msgid;
+const char * t_lang;
+const char * t_msgid;
 } * spectag;
 
 /** \ingroup rpmbuild
  */
 typedef struct spectags_s {
-/*@owned@*/ spectag st_t;
+spectag st_t;
     int st_nalloc;
     int st_ntags;
 } * spectags;
@@ -81,7 +76,7 @@ typedef struct spectags_s {
 /** \ingroup rpmbuild
  */
 typedef struct speclines_s {
-/*@only@*/ char **sl_lines;
+char **sl_lines;
     int sl_nalloc;
     int sl_nlines;
 } * speclines;
@@ -90,40 +85,26 @@ typedef struct speclines_s {
  * The structure used to store values parsed from a spec file.
  */
 struct Spec_s {
-/*@only@*/
     const char * specFile;	/*!< Name of the spec file. */
-/*@only@*/
     const char * buildRootURL;
-/*@only@*/
     const char * buildSubdir;
-/*@only@*/
     const char * rootURL;
 
-/*@owned@*/ /*@null@*/
     speclines sl;
-/*@owned@*/ /*@null@*/
     spectags st;
 
-/*@owned@*/
     struct OpenFileInfo * fileStack;
     char lbuf[10*BUFSIZ];
-/*@dependent@*/
     char *lbufPtr;
     char nextpeekc;
-/*@dependent@*/
     char * nextline;
-/*@dependent@*/
     char * line;
     int lineNum;
 
-/*@owned@*/
     struct ReadLevelEntry * readStack;
 
-/*@refcounted@*/
     Header buildRestrictions;
-/*@owned@*/ /*@null@*/
     Spec * BASpecs;
-/*@only@*/ /*@null@*/
     const char ** BANames;
     int BACount;
     int recursing;		/*!< parse is recursive? */
@@ -133,41 +114,27 @@ struct Spec_s {
 
     int gotBuildRootURL;
 
-/*@null@*/
     char * passPhrase;
     int timeCheck;
-/*@null@*/
     const char * cookie;
 
-/*@owned@*/
     struct Source * sources;
     int numSources;
     int noSource;
 
-/*@only@*/
     const char * sourceRpmName;
-/*@only@*/
     unsigned char * sourcePkgId;
-/*@refcounted@*/
     Header sourceHeader;
-/*@refcounted@*/
     rpmfi sourceCpioList;
 
-/*@dependent@*/ /*@null@*/
     MacroContext macros;
 
-/*@only@*/
     StringBuf prep;		/*!< %prep scriptlet. */
-/*@only@*/
     StringBuf build;		/*!< %build scriptlet. */
-/*@only@*/
     StringBuf install;		/*!< %install scriptlet. */
-/*@only@*/
     StringBuf check;		/*!< %check scriptlet. */
-/*@only@*/
     StringBuf clean;		/*!< %clean scriptlet. */
 
-/*@owned@*/
     Package packages;		/*!< Package list. */
 };
 
@@ -175,46 +142,30 @@ struct Spec_s {
  * The structure used to store values for a package.
  */
 struct Package_s {
-/*@refcounted@*/
     Header header;
-/*@refcounted@*/
     rpmds ds;			/*!< Requires: N = EVR */
-/*@refcounted@*/
     rpmfi cpioList;
 
-/*@owned@*/
     struct Source * icon;
 
     int autoReq;
     int autoProv;
 
-/*@only@*/
     const char * preInFile;	/*!< %pre scriptlet. */
-/*@only@*/
     const char * postInFile;	/*!< %post scriptlet. */
-/*@only@*/
     const char * preUnFile;	/*!< %preun scriptlet. */
-/*@only@*/
     const char * postUnFile;	/*!< %postun scriptlet. */
-/*@only@*/
     const char * preTransFile;	/*!< %pretrans scriptlet. */
-/*@only@*/
     const char * postTransFile;	/*!< %posttrans scriptlet. */
-/*@only@*/
     const char * verifyFile;	/*!< %verifyscript scriptlet. */
 
-/*@only@*/
     StringBuf specialDoc;
 
-/*@only@*/
     struct TriggerFileEntry * triggerFiles;
 
-/*@only@*/
     const char * fileFile;
-/*@only@*/
     StringBuf fileList;		/* If NULL, package will not be written */
 
-/*@dependent@*/
     Package next;
 };
 
@@ -226,18 +177,14 @@ extern "C" {
  * Create and initialize Spec structure.
  * @return spec		spec file control structure
  */
-/*@only@*/ Spec newSpec(void)
-	/*@globals rpmGlobalMacroContext @*/
-	/*@modifies rpmGlobalMacroContext @*/;
+Spec newSpec(void);
 
 /** \ingroup rpmbuild
  * Destroy Spec structure.
  * @param spec		spec file control structure
  * @return		NULL always
  */
-/*@null@*/ Spec freeSpec(/*@only@*/ /*@null@*/ Spec spec)
-	/*@globals fileSystem, internalState @*/
-	/*@modifies spec, fileSystem, internalState @*/;
+Spec freeSpec(Spec spec);
 
 /** \ingroup rpmbuild
  * Function to query spec file(s).
@@ -246,16 +193,11 @@ extern "C" {
  * @param arg		query argument
  * @return		0 on success, else no. of failures
  */
-int rpmspecQuery(rpmts ts, QVA_t qva, const char * arg)
-	/*@globals rpmGlobalMacroContext, h_errno,
-		fileSystem, internalState @*/
-	/*@modifies ts, qva, rpmGlobalMacroContext,
-		fileSystem, internalState @*/;
+int rpmspecQuery(rpmts ts, QVA_t qva, const char * arg);
 
 /** \ingroup rpmbuild
  */
-struct OpenFileInfo * newOpenFileInfo(void)
-	/*@*/;
+struct OpenFileInfo * newOpenFileInfo(void);
 
 /** \ingroup rpmbuild
  * @param spec		spec file control structure
@@ -263,8 +205,7 @@ struct OpenFileInfo * newOpenFileInfo(void)
  * @param tag
  * @param lang
  */
-spectag stashSt(Spec spec, Header h, int tag, const char * lang)
-	/*@modifies spec->st @*/;
+spectag stashSt(Spec spec, Header h, int tag, const char * lang);
 
 /** \ingroup rpmbuild
  * @param spec		spec file control structure
@@ -272,20 +213,14 @@ spectag stashSt(Spec spec, Header h, int tag, const char * lang)
  * @param field
  * @param tag
  */
-int addSource(Spec spec, Package pkg, const char * field, int tag)
-	/*@globals rpmGlobalMacroContext, h_errno @*/
-	/*@modifies spec->sources, spec->numSources,
-		spec->st, spec->macros,
-		pkg->icon,
-		rpmGlobalMacroContext @*/;
+int addSource(Spec spec, Package pkg, const char * field, int tag);
 
 /** \ingroup rpmbuild
  * @param spec		spec file control structure
  * @param field
  * @param tag
  */
-int parseNoSource(Spec spec, const char * field, int tag)
-	/*@modifies nothing @*/;
+int parseNoSource(Spec spec, const char * field, int tag);
 
 #ifdef __cplusplus
 }
diff --git a/build/spec.c b/build/spec.c
index 13dba2620..c3272b334 100644
--- a/build/spec.c
+++ b/build/spec.c
@@ -12,23 +12,17 @@
 
 #include "debug.h"
 
-/*@-redecl@*/
 extern int specedit;
-/*@=redecl@*/
 
 #define SKIPWHITE(_x)	{while(*(_x) && (xisspace(*_x) || *(_x) == ',')) (_x)++;}
 #define SKIPNONWHITE(_x){while(*(_x) &&!(xisspace(*_x) || *(_x) == ',')) (_x)++;}
 
-/*@access Header @*/	/* compared with NULL */
-/*@access rpmfi @*/	/* compared with NULL */
-
 /**
  * @param p		trigger entry chain
  * @return		NULL always
  */
 static inline
-/*@null@*/ struct TriggerFileEntry * freeTriggerFiles(/*@only@*/ /*@null@*/ struct TriggerFileEntry * p)
-	/*@modifies p @*/
+struct TriggerFileEntry * freeTriggerFiles(struct TriggerFileEntry * p)
 {
     struct TriggerFileEntry *o, *q = p;
     
@@ -49,8 +43,7 @@ static inline
  * @return		NULL always
  */
 static inline
-/*@null@*/ struct Source * freeSources(/*@only@*/ /*@null@*/ struct Source * s)
-	/*@modifies s @*/
+struct Source * freeSources(struct Source * s)
 {
     struct Source *r, *t = s;
 
@@ -63,8 +56,7 @@ static inline
     return NULL;
 }
 
-/*@-boundswrite@*/
-int lookupPackage(Spec spec, const char *name, int flag, /*@out@*/Package *pkg)
+int lookupPackage(Spec spec, const char *name, int flag,Package *pkg)
 {
     const char *pname;
     const char *fullName;
@@ -87,9 +79,7 @@ int lookupPackage(Spec spec, const char *name, int flag, /*@out@*/Package *pkg)
     } else {
 	fullName = n = alloca(strlen(name)+1);
     }
-    /*@-mayaliasunique@*/
     strcpy(n, name);
-    /*@=mayaliasunique@*/
   }
 
     /* Locate package with fullName */
@@ -101,10 +91,9 @@ int lookupPackage(Spec spec, const char *name, int flag, /*@out@*/Package *pkg)
     }
 
     if (pkg)
-	/*@-dependenttrans@*/ *pkg = p; /*@=dependenttrans@*/
+	*pkg = p;
     return ((p == NULL) ? 1 : 0);
 }
-/*@=boundswrite@*/
 
 Package newPackage(Spec spec)
 {
@@ -196,8 +185,7 @@ Package freePackages(Package packages)
 
 /**
  */
-static inline /*@owned@*/ struct Source *findSource(Spec spec, int num, int flag)
-	/*@*/
+static inline struct Source *findSource(Spec spec, int num, int flag)
 {
     struct Source *p;
 
@@ -207,7 +195,6 @@ static inline /*@owned@*/ struct Source *findSource(Spec spec, int num, int flag
     return NULL;
 }
 
-/*@-boundsread@*/
 int parseNoSource(Spec spec, const char * field, int tag)
 {
     const char *f, *fe;
@@ -251,9 +238,7 @@ int parseNoSource(Spec spec, const char * field, int tag)
 
     return 0;
 }
-/*@=boundsread@*/
 
-/*@-boundswrite@*/
 int addSource(Spec spec, Package pkg, const char *field, int tag)
 {
     struct Source *p;
@@ -265,7 +250,6 @@ int addSource(Spec spec, Package pkg, const char *field, int tag)
     int num = 0;
 
     buf[0] = '\0';
-    /*@-branchstate@*/
     switch (tag) {
       case RPMTAG_SOURCE:
 	flag = RPMBUILD_ISSOURCE;
@@ -282,7 +266,6 @@ int addSource(Spec spec, Package pkg, const char *field, int tag)
 	fieldp = NULL;
 	break;
     }
-    /*@=branchstate@*/
 
     /* Get the number */
     if (tag != RPMTAG_ICON) {
@@ -333,9 +316,7 @@ int addSource(Spec spec, Package pkg, const char *field, int tag)
     spec->numSources++;
 
     if (tag != RPMTAG_ICON) {
-	/*@-nullpass@*/		/* LCL: varargs needs null annotate. */
 	const char *body = rpmGetPath("%{_sourcedir}/", p->source, NULL);
-	/*@=nullpass@*/
 
 	sprintf(buf, "%s%d",
 		(flag & RPMBUILD_ISPATCH) ? "PATCH" : "SOURCE", num);
@@ -348,63 +329,50 @@ int addSource(Spec spec, Package pkg, const char *field, int tag)
     
     return 0;
 }
-/*@=boundswrite@*/
 
 /**
  */
-static inline /*@only@*/ /*@null@*/ speclines newSl(void)
-	/*@*/
+static inline speclines newSl(void)
 {
     speclines sl = NULL;
-    /*@-branchstate@*/
     if (specedit) {
 	sl = xmalloc(sizeof(*sl));
 	sl->sl_lines = NULL;
 	sl->sl_nalloc = 0;
 	sl->sl_nlines = 0;
     }
-    /*@=branchstate@*/
     return sl;
 }
 
 /**
  */
-/*@-boundswrite@*/
-static inline /*@null@*/ speclines freeSl(/*@only@*/ /*@null@*/ speclines sl)
-	/*@modifies sl @*/
+static inline speclines freeSl(speclines sl)
 {
     int i;
     if (sl == NULL) return NULL;
     for (i = 0; i < sl->sl_nlines; i++)
-	/*@-unqualifiedtrans@*/
 	sl->sl_lines[i] = _free(sl->sl_lines[i]);
-	/*@=unqualifiedtrans@*/
     sl->sl_lines = _free(sl->sl_lines);
     return _free(sl);
 }
-/*@=boundswrite@*/
 
 /**
  */
-static inline /*@only@*/ /*@null@*/ spectags newSt(void)
-	/*@*/
+static inline spectags newSt(void)
 {
     spectags st = NULL;
-    /*@-branchstate@*/
     if (specedit) {
 	st = xmalloc(sizeof(*st));
 	st->st_t = NULL;
 	st->st_nalloc = 0;
 	st->st_ntags = 0;
     }
-    /*@=branchstate@*/
     return st;
 }
 
 /**
  */
-static inline /*@null@*/ spectags freeSt(/*@only@*/ /*@null@*/ spectags st)
-	/*@modifies st @*/
+static inline spectags freeSt(spectags st)
 {
     int i;
     if (st == NULL) return NULL;
@@ -427,9 +395,7 @@ Spec newSpec(void)
     spec->st = newSt();
 
     spec->fileStack = NULL;
-/*@-boundswrite@*/
     spec->lbuf[0] = '\0';
-/*@=boundswrite@*/
     spec->line = spec->lbuf;
     spec->nextline = NULL;
     spec->nextpeekc = '\0';
@@ -472,7 +438,7 @@ Spec newSpec(void)
     spec->force = 0;
     spec->anyarch = 0;
 
-/*@i@*/	spec->macros = rpmGlobalMacroContext;
+    spec->macros = rpmGlobalMacroContext;
     
     return spec;
 }
@@ -513,9 +479,7 @@ Spec freeSpec(Spec spec)
 
     while (spec->readStack) {
 	rl = spec->readStack;
-	/*@-dependenttrans@*/
 	spec->readStack = rl->next;
-	/*@=dependenttrans@*/
 	rl->next = NULL;
 	rl = _free(rl);
     }
@@ -533,18 +497,12 @@ Spec freeSpec(Spec spec)
     spec->buildRestrictions = headerFree(spec->buildRestrictions);
 
     if (!spec->recursing) {
-/*@-boundswrite@*/
 	if (spec->BASpecs != NULL)
 	while (spec->BACount--) {
-	    /*@-unqualifiedtrans@*/
 	    spec->BASpecs[spec->BACount] =
 			freeSpec(spec->BASpecs[spec->BACount]);
-	    /*@=unqualifiedtrans@*/
 	}
-/*@=boundswrite@*/
-	/*@-compdef@*/
 	spec->BASpecs = _free(spec->BASpecs);
-	/*@=compdef@*/
     }
     spec->BANames = _free(spec->BANames);
 
@@ -559,7 +517,6 @@ Spec freeSpec(Spec spec)
     return spec;
 }
 
-/*@only@*/
 struct OpenFileInfo * newOpenFileInfo(void)
 {
     struct OpenFileInfo *ofi;
@@ -568,9 +525,7 @@ struct OpenFileInfo * newOpenFileInfo(void)
     ofi->fd = NULL;
     ofi->fileName = NULL;
     ofi->lineNum = 0;
-/*@-boundswrite@*/
     ofi->readBuf[0] = '\0';
-/*@=boundswrite@*/
     ofi->readPtr = NULL;
     ofi->next = NULL;
 
@@ -583,8 +538,6 @@ struct OpenFileInfo * newOpenFileInfo(void)
  */
 static void
 printNewSpecfile(Spec spec)
-	/*@globals fileSystem @*/
-	/*@modifies spec->sl->sl_lines[], fileSystem @*/
 {
     Header h;
     speclines sl = spec->sl;
@@ -595,7 +548,6 @@ 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);
@@ -609,19 +561,17 @@ printNewSpecfile(Spec spec)
 	    Package pkg;
 	    char *fe;
 
-/*@-bounds@*/
 	    strcpy(fmt, t->t_msgid);
 	    for (fe = fmt; *fe && *fe != '('; fe++)
 		{} ;
 	    if (*fe == '(') *fe = '\0';
-/*@=bounds@*/
 	    h = NULL;
 	    for (pkg = spec->packages; pkg != NULL; pkg = pkg->next) {
 		const char *pkgname;
 		h = pkg->header;
 		(void) headerNVR(h, &pkgname, NULL, NULL);
 		if (!strcmp(pkgname, fmt))
-		    /*@innerbreak@*/ break;
+		    break;
 	    }
 	    if (pkg == NULL || h == NULL)
 		h = spec->packages->header;
@@ -631,9 +581,7 @@ printNewSpecfile(Spec spec)
 	    continue;
 
 	fmt[0] = '\0';
-/*@-boundswrite@*/
 	(void) stpcpy( stpcpy( stpcpy( fmt, "%{"), tn), "}");
-/*@=boundswrite@*/
 	msgstr = _free(msgstr);
 
 	/* XXX this should use queryHeader(), but prints out tn as well. */
@@ -643,28 +591,23 @@ printNewSpecfile(Spec spec)
 	    return;
 	}
 
-/*@-boundswrite@*/
 	switch(t->t_tag) {
 	case RPMTAG_SUMMARY:
 	case RPMTAG_GROUP:
-	    /*@-unqualifiedtrans@*/
 	    sl->sl_lines[t->t_startx] = _free(sl->sl_lines[t->t_startx]);
-	    /*@=unqualifiedtrans@*/
 	    if (t->t_lang && strcmp(t->t_lang, RPMBUILD_DEFAULT_LANG))
 		continue;
 	    {   char *buf = xmalloc(strlen(tn) + sizeof(": ") + strlen(msgstr));
 		(void) stpcpy( stpcpy( stpcpy(buf, tn), ": "), msgstr);
 		sl->sl_lines[t->t_startx] = buf;
 	    }
-	    /*@switchbreak@*/ break;
+	    break;
 	case RPMTAG_DESCRIPTION:
 	    for (j = 1; j < t->t_nlines; j++) {
 		if (*sl->sl_lines[t->t_startx + j] == '%')
-		    /*@innercontinue@*/ continue;
-		/*@-unqualifiedtrans@*/
+		    continue;
 		sl->sl_lines[t->t_startx + j] =
 			_free(sl->sl_lines[t->t_startx + j]);
-		/*@=unqualifiedtrans@*/
 	    }
 	    if (t->t_lang && strcmp(t->t_lang, RPMBUILD_DEFAULT_LANG)) {
 		sl->sl_lines[t->t_startx] = _free(sl->sl_lines[t->t_startx]);
@@ -673,14 +616,11 @@ printNewSpecfile(Spec spec)
 	    sl->sl_lines[t->t_startx + 1] = xstrdup(msgstr);
 	    if (t->t_nlines > 2)
 		sl->sl_lines[t->t_startx + 2] = xstrdup("\n\n");
-	    /*@switchbreak@*/ break;
+	    break;
 	}
-/*@=boundswrite@*/
     }
-    /*@=branchstate@*/
     msgstr = _free(msgstr);
 
-/*@-boundsread@*/
     for (i = 0; i < sl->sl_nlines; i++) {
 	const char * s = sl->sl_lines[i];
 	if (s == NULL)
@@ -689,7 +629,6 @@ printNewSpecfile(Spec spec)
 	if (strchr(s, '\n') == NULL && s[strlen(s)-1] != '\n')
 	    printf("\n");
     }
-/*@=boundsread@*/
 }
 
 int rpmspecQuery(rpmts ts, QVA_t qva, const char * arg)
@@ -708,8 +647,7 @@ int rpmspecQuery(rpmts ts, QVA_t qva, const char * arg)
     if (qva->qva_showPackage == NULL)
 	goto exit;
 
-/*@-branchstate@*/
-    /*@-mods@*/ /* FIX: make spec abstract */
+    /* FIX: make spec abstract */
     if (parseSpec(ts, arg, "/", buildRoot, recursing, passPhrase,
 		cookie, anyarch, force)
       || (spec = rpmtsSetSpec(ts, NULL)) == NULL)
@@ -718,8 +656,6 @@ int rpmspecQuery(rpmts ts, QVA_t qva, const char * arg)
 	    		_("query of specfile %s failed, can't parse\n"), arg);
 	goto exit;
     }
-    /*@=mods@*/
-/*@=branchstate@*/
 
     res = 0;
     if (specedit) {