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

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

diff --git a/beecrypt/beecrypt.c b/beecrypt/beecrypt.c
index cdcce31..d5a6f24 100644 (file)
--- a/beecrypt/beecrypt.c
+++ b/beecrypt/beecrypt.c
@@ -172,9 +172,11 @@ const randomGenerator* randomGeneratorGet(int index)
        if ((index < 0) || (index >= RANDOMGENERATORS))
                return (const randomGenerator*) 0;
 
+/*@-boundsread@*/
        /*@-compmempass@*/
        return randomGeneratorList[index];
        /*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -291,9 +293,11 @@ const hashFunction* hashFunctionGet(int index)
        if ((index < 0) || (index >= HASHFUNCTIONS))
                return (const hashFunction*) 0;
 
+/*@-boundsread@*/
        /*@-compmempass@*/
        return hashFunctionList[index];
        /*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -511,9 +515,11 @@ const keyedHashFunction* keyedHashFunctionGet(int index)
        if ((index < 0) || (index >= KEYEDHASHFUNCTIONS))
                return (const keyedHashFunction*) 0;
 
+/*@-boundsread@*/
        /*@-compmempass@*/
        return keyedHashFunctionList[index];
        /*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/
@@ -752,9 +758,11 @@ const blockCipher* blockCipherGet(int index)
        if ((index < 0) || (index >= BLOCKCIPHERS))
                return (const blockCipher*) 0;
 
+/*@-boundsread@*/
        /*@-compmempass@*/
        return blockCipherList[index];
        /*@=compmempass@*/
+/*@=boundsread@*/
 }
 
 /*@-boundsread@*/

diff --git a/beecrypt/blockpad.c b/beecrypt/blockpad.c
index a6637ec..466e44d 100644 (file)
--- a/beecrypt/blockpad.c
+++ b/beecrypt/blockpad.c
@@ -70,9 +70,9 @@ memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
 /*             tmp->data = (byte*) realloc(tmp->data, tmp->size; */
        }
 
-       /*@-temptrans@*/
+       /*@-temptrans -compdef @*/
        return tmp;
-       /*@=temptrans@*/
+       /*@=temptrans =compdef @*/
 }
 /*@=boundsread@*/
 

diff --git a/beecrypt/blockpad.h b/beecrypt/blockpad.h
index 265cc15..e0f152d 100644 (file)
--- a/beecrypt/blockpad.h
+++ b/beecrypt/blockpad.h
@@ -51,7 +51,8 @@ memchunk* pkcs5Pad  (int blockbytes, /*@only@*/ /*@null@*/ memchunk* tmp)
  * @return             buffer with pad removed
  */
 BEECRYPTAPI /*@only@*/ /*@null@*/
-memchunk* pkcs5Unpad(int blockbytes, /*@returned@*/ /*@null@*/ memchunk* tmp)
+memchunk* pkcs5Unpad(int blockbytes,
+               /*@returned@*/ /*@null@*/ /*@out@*/ memchunk* tmp)
        /*@modifies tmp */;
 
 /**

diff --git a/beecrypt/endianness.c b/beecrypt/endianness.c
index fe8a383..762bc52 100644 (file)
--- a/beecrypt/endianness.c
+++ b/beecrypt/endianness.c
@@ -512,7 +512,9 @@ int readChars(javachar* c, FILE* ifp, int count)
 
 int writeByte(javabyte b, FILE* ofp)
 {
+/*@-boundsread@*/
        return fwrite(&b, 1, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeShort(javashort s, FILE* ofp)
@@ -520,7 +522,9 @@ int writeShort(javashort s, FILE* ofp)
        #if !(WORDS_BIGENDIAN)
        s = swap16(s);
        #endif
+/*@-boundsread@*/
        return fwrite(&s, 2, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeInt(javaint i, FILE* ofp)
@@ -528,7 +532,9 @@ int writeInt(javaint i, FILE* ofp)
        #if !(WORDS_BIGENDIAN)
        i = swap32(i);
        #endif
+/*@-boundsread@*/
        return fwrite(&i, 4, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeLong(javalong l, FILE* ofp)
@@ -536,7 +542,9 @@ int writeLong(javalong l, FILE* ofp)
        #if !(WORDS_BIGENDIAN)
        l = swap64(l);
        #endif
+/*@-boundsread@*/
        return fwrite(&l, 8, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeChar(javachar c, FILE* ofp)
@@ -544,7 +552,9 @@ int writeChar(javachar c, FILE* ofp)
        #if !(WORDS_BIGENDIAN)
        c = swap16(c);
        #endif
+/*@-boundsread@*/
        return fwrite(&c, 2, 1, ofp);
+/*@=boundsread@*/
 }
 
 int writeInts(const javaint* i, FILE* ofp, int count)

diff --git a/build.c b/build.c
index 4a00cb5..6ed926a 100644 (file)
--- a/build.c
+++ b/build.c
@@ -57,8 +57,8 @@ static int checkSpec(rpmts ts, Header h)
 /**
  */
 static int isSpecFile(const char * specfile)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     char buf[256];
     const char * s;

diff --git a/build/build.c b/build/build.c
index b98fd19..e5625f9 100644 (file)
--- a/build/build.c
+++ b/build/build.c
@@ -20,9 +20,8 @@ static int _build_debug = 0;
 /**
  */
 static void doRmSource(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     struct Source *p;
     Package pkg;

diff --git a/build/files.c b/build/files.c
index 7876ccb..b51152b 100644 (file)
--- a/build/files.c
+++ b/build/files.c
@@ -710,9 +710,12 @@ static int parseForConfig(char * buf, FileList fl)
 
 /**
  */
-static int langCmp(const void * ap, const void * bp)   /*@*/
+static int langCmp(const void * ap, const void * bp)
+       /*@*/
 {
+/*@-boundsread@*/
     return strcmp(*(const char **)ap, *(const char **)bp);
+/*@=boundsread@*/
 }
 
 /**
@@ -1124,10 +1127,9 @@ static int checkHardLinks(FileList fl)
 /*@-bounds@*/
 static void genCpioListAndHeader(/*@partial@*/ FileList fl,
                rpmfi * cpioList, Header h, int isSrc)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies h, *cpioList, fl->processingFailed, fl->fileList,
-               rpmGlobalMacroContext, fileSystem @*/
+               rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int _addDotSlash = !(isSrc || rpmExpandNumeric("%{_noPayloadPrefix}"));
     uint_32 multiLibMask = 0;
@@ -1503,12 +1505,11 @@ static /*@null@*/ FileListRec freeFileList(/*@only@*/ FileListRec fileList,
 /*@-boundswrite@*/
 static int addFile(FileList fl, const char * diskURL,
                /*@null@*/ struct stat * statp)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies *statp, *fl, fl->processingFailed,
                fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
                fl->totalFileSize, fl->fileCount, fl->inFtw, fl->isDir,
-               rpmGlobalMacroContext, fileSystem @*/
+               rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     const char *fileURL = diskURL;
     struct stat statbuf;
@@ -1727,12 +1728,11 @@ static int addFile(FileList fl, const char * diskURL,
 /*@-boundswrite@*/
 static int processBinaryFile(/*@unused@*/ Package pkg, FileList fl,
                const char * fileURL)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies *fl, fl->processingFailed,
                fl->fileList, fl->fileListRecsAlloced, fl->fileListRecsUsed,
                fl->totalFileSize, fl->fileCount, fl->inFtw, fl->isDir,
-               rpmGlobalMacroContext, fileSystem @*/
+               rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     int doGlob;
     const char *diskURL = NULL;

diff --git a/build/myftw.c b/build/myftw.c
index a55b067..7c3c717 100644 (file)
--- a/build/myftw.c
+++ b/build/myftw.c
@@ -58,8 +58,8 @@ myftw_dir (DIR **dirs, int level, int descriptors,
           char *dir, size_t len, 
           myftwFunc func,
           void *fl)
-       /*@globals errno, fileSystem @*/
-       /*@modifies *dirs, *dir, errno, fileSystem @*/
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies *dirs, *dir, errno, fileSystem, internalState @*/
 {
   int got;
   struct dirent *entry;

diff --git a/build/myftw.h b/build/myftw.h
index f4e7209..2330de1 100644 (file)
--- a/build/myftw.h
+++ b/build/myftw.h
@@ -22,8 +22,8 @@ typedef int (*myftwFunc) (void *fl, const char *name, struct stat *statp)
        /*@*/;
 
 int myftw (const char *dir, int descriptors, myftwFunc func, void *fl)
-       /*@globals fileSystem @*/
-       /*@modifies *fl, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *fl, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }

diff --git a/build/pack.c b/build/pack.c
index 314edc7..61a8223 100644 (file)
--- a/build/pack.c
+++ b/build/pack.c
@@ -55,9 +55,9 @@ static inline int genSourceRpmName(Spec spec)
  */
 static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
                const char * fmodeMacro)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies fdo, csa, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies fdo, csa, rpmGlobalMacroContext,
+               fileSystem, internalState @*/
 {
     rpmts ts = rpmtsCreate();
     rpmfi fi = csa->cpioList;
@@ -104,8 +104,8 @@ static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
 /**
  */
 static int cpio_copy(FD_t fdo, CSA_t csa)
-       /*@globals fileSystem@*/
-       /*@modifies fdo, csa, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fdo, csa, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     size_t nb;
@@ -130,9 +130,8 @@ static int cpio_copy(FD_t fdo, CSA_t csa)
  */
 static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
                const char * file, /*@only@*/ StringBuf sb)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     const char * fn = buf;
@@ -168,9 +167,8 @@ static /*@only@*/ /*@null@*/ StringBuf addFileToTagAux(Spec spec,
 /**
  */
 static int addFileToTag(Spec spec, const char * file, Header h, int tag)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies h, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     StringBuf sb = newStringBuf();
@@ -193,9 +191,8 @@ static int addFileToTag(Spec spec, const char * file, Header h, int tag)
 /**
  */
 static int addFileToArrayTag(Spec spec, const char *file, Header h, int tag)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     StringBuf sb = newStringBuf();
     char *s;
@@ -213,9 +210,9 @@ static int addFileToArrayTag(Spec spec, const char *file, Header h, int tag)
 /**
  */
 static int processScriptFiles(Spec spec, Package pkg)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies pkg->header, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies pkg->header, rpmGlobalMacroContext,
+               fileSystem, internalState @*/
 {
     struct TriggerFileEntry *p;
     

diff --git a/build/parsePreamble.c b/build/parsePreamble.c
index 259cb95..9186a75 100644 (file)
--- a/build/parsePreamble.c
+++ b/build/parsePreamble.c
@@ -353,9 +353,8 @@ static void fillOutMainPackage(Header h)
  */
 /*@-boundswrite@*/
 static int readIcon(Header h, const char * file)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies h, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies h, rpmGlobalMacroContext, fileSystem, internalState  @*/
 {
     const char *fn = NULL;
     char *icon;
@@ -459,14 +458,13 @@ extern int noLang;
 /*@-boundswrite@*/
 static int handlePreambleTag(Spec spec, Package pkg, int tag, const char *macro,
                             const char *lang)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->macros, spec->st, spec->buildRootURL,
                spec->sources, spec->numSources, spec->noSource,
                spec->buildRestrictions, spec->BANames, spec->BACount,
                spec->line, spec->gotBuildRootURL,
                pkg->header, pkg->autoProv, pkg->autoReq, pkg->icon,
-               rpmGlobalMacroContext, fileSystem @*/
+               rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;

diff --git a/build/parsePrep.c b/build/parsePrep.c
index a6d9f41..7b31724 100644 (file)
--- a/build/parsePrep.c
+++ b/build/parsePrep.c
@@ -36,8 +36,8 @@
  * @return             0 on success
  */
 static int checkOwners(const char * urlfn)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     struct stat sb;
 
@@ -67,9 +67,8 @@ static int checkOwners(const char * urlfn)
 /*@-boundswrite@*/
 /*@observer@*/ static char *doPatch(Spec spec, int c, int strip, const char *db,
                     int reverse, int removeEmpties)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -162,9 +161,8 @@ static int checkOwners(const char * urlfn)
  */
 /*@-boundswrite@*/
 /*@observer@*/ static const char *doUntar(Spec spec, int c, int quietly)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     const char *fn, *urlfn;
     static char buf[BUFSIZ];
@@ -281,10 +279,9 @@ static int checkOwners(const char * urlfn)
  * @return             0 on success
  */
 static int doSetupMacro(Spec spec, char *line)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->buildSubdir, spec->macros, spec->prep,
-               rpmGlobalMacroContext, fileSystem @*/
+               rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     char buf[BUFSIZ];
     StringBuf before;
@@ -441,8 +438,9 @@ static int doSetupMacro(Spec spec, char *line)
 /*@-boundswrite@*/
 static int doPatchMacro(Spec spec, char *line)
        /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
-       /*@modifies spec->prep, rpmGlobalMacroContext, fileSystem @*/
+               fileSystem, internalState @*/
+       /*@modifies spec->prep, rpmGlobalMacroContext,
+               fileSystem, internalState  @*/
 {
     char *opt_b;
     int opt_P, opt_p, opt_R, opt_E;

diff --git a/build/rpmbuild.h b/build/rpmbuild.h
index 769a9b7..2f42550 100644 (file)
--- a/build/rpmbuild.h
+++ b/build/rpmbuild.h
@@ -153,19 +153,18 @@ extern /*@observer@*/ int_32 * const getBuildTime(void)   /*@*/;
  * @return             0 on success, 1 on EOF, <0 on error
  */
 int readLine(Spec spec, int strip)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Stop reading from spec file, freeing resources.
  * @param spec         spec file control structure
  */
 void closeSpec(/*@partial@*/ Spec spec)
-       /*@globals fileSystem@*/
-       /*@modifies spec->fileStack, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies spec->fileStack, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Truncate comment lines.
@@ -208,12 +207,11 @@ void addChangelogEntry(Header h, time_t time, const char * name,
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->build, spec->install, spec->clean, spec->macros,
                spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse %%changelog section of a spec file.
@@ -221,12 +219,11 @@ int parseBuildInstallClean(Spec spec, rpmParseState parsePart)
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parseChangelog(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
                spec->packages->header,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse %%description section of a spec file.
@@ -234,13 +231,12 @@ int parseChangelog(Spec spec)
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parseDescription(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->packages,
                spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
                spec->st,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Parse %%files section of a spec file.
@@ -248,12 +244,11 @@ int parseDescription(Spec spec)
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parseFiles(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->packages,
                spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse tags from preamble of a spec file.
@@ -280,12 +275,11 @@ int parsePreamble(Spec spec, int initialPackage)
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parsePrep(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->prep, spec->buildSubdir, spec->macros,
                spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse dependency relations from spec file and/or autogenerated output buffer.
@@ -309,12 +303,11 @@ int parseRCPOT(Spec spec, Package pkg, const char * field, int tag, int index,
  * @return             >= 0 next rpmParseState, < 0 on error
  */
 int parseScript(Spec spec, int parsePart)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem@*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->packages,
                spec->fileStack, spec->readStack, spec->line, spec->lineNum,
                spec->nextline, spec->nextpeekc, spec->lbuf, spec->sl,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState  @*/;
 
 /** \ingroup rpmbuild
  * Evaluate boolean expression.
@@ -444,12 +437,11 @@ void initSourceHeader(Spec spec)
  * @return             0 on success
  */
 int processSourceFiles(Spec spec)
-       /*@globals rpmGlobalMacroContext,
-               fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies spec->sourceHeader, spec->sourceCpioList,
                spec->buildRestrictions, spec->BANames,
                spec->packages->header,
-               rpmGlobalMacroContext, fileSystem @*/;
+               rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * Parse spec file into spec control structure.

diff --git a/build/rpmspec.h b/build/rpmspec.h
index fa28775..9145a64 100644 (file)
--- a/build/rpmspec.h
+++ b/build/rpmspec.h
@@ -192,8 +192,8 @@ extern "C" {
  * @return             NULL always
  */
 /*@null@*/ Spec freeSpec(/*@only@*/ /*@null@*/ Spec spec)
-       /*@globals fileSystem @*/
-       /*@modifies spec, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies spec, fileSystem, internalState @*/;
 
 /** \ingroup rpmbuild
  * @param spec         spec file control structure
@@ -201,8 +201,8 @@ extern "C" {
  */
 /*@-declundef@*/
 extern /*@null@*/ Spec (*freeSpecVec) (Spec spec)      /* XXX FIXME */
-       /*@globals fileSystem @*/
-       /*@modifies spec, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies spec, fileSystem, internalState @*/;
 /*@=declundef@*/
 
 /** \ingroup rpmbuild

diff --git a/lib/cpio.h b/lib/cpio.h
index 9e04d09..7cbb61b 100644 (file)
--- a/lib/cpio.h
+++ b/lib/cpio.h
@@ -101,8 +101,8 @@ extern "C" {
  * @return             0 on success
  */
 int cpioTrailerWrite(FSM_t fsm)
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/;
 
 /**
  * Write cpio header.
@@ -111,8 +111,8 @@ int cpioTrailerWrite(FSM_t fsm)
  * @return             0 on success
  */
 int cpioHeaderWrite(FSM_t fsm, struct stat * st)
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/;
 
 /**
  * Read cpio header.
@@ -121,15 +121,16 @@ int cpioHeaderWrite(FSM_t fsm, struct stat * st)
  * @return             0 on success
  */
 int cpioHeaderRead(FSM_t fsm, struct stat * st)
-       /*@globals fileSystem@*/
-       /*@modifies fsm, *st, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, *st, fileSystem, internalState @*/;
 
 /** \ingroup payload
  * Return formatted error message on payload handling failure.
  * @param rc           error code
  * @return             formatted error string
  */
-/*@observer@*/ const char *const cpioStrerror(int rc)          /*@*/;
+/*@observer@*/ const char *const cpioStrerror(int rc)
+       /*@*/;
 
 #ifdef __cplusplus
 }

diff --git a/lib/depends.c b/lib/depends.c
index 4f3a9f1..b838307 100644 (file)
--- a/lib/depends.c
+++ b/lib/depends.c
@@ -334,8 +334,8 @@ int rpmtsAddEraseElement(rpmts ts, Header h, int dboffset)
  * @return             0 if satisfied, 1 if not satisfied, 2 if error
  */
 static int unsatisfiedDepend(rpmts ts, rpmds dep)
-       /*@globals _cacheDependsRC, fileSystem @*/
-       /*@modifies ts, _cacheDependsRC, fileSystem @*/
+       /*@globals _cacheDependsRC, fileSystem, internalState @*/
+       /*@modifies ts, _cacheDependsRC, fileSystem, internalState @*/
 {
     DBT * key = alloca(sizeof(*key));
     DBT * data = alloca(sizeof(*data));
@@ -556,8 +556,8 @@ exit:
 static int checkPackageDeps(rpmts ts, const char * pkgNEVR,
                /*@null@*/ rpmds requires, /*@null@*/ rpmds conflicts,
                /*@null@*/ const char * depName, uint_32 multiLib, int adding)
-       /*@globals fileSystem @*/
-       /*@modifies ts, requires, conflicts, fileSystem */
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, requires, conflicts, fileSystem, internalState */
 {
     const char * Name;
     int_32 Flags;
@@ -657,8 +657,8 @@ static int checkPackageDeps(rpmts ts, const char * pkgNEVR,
  */
 static int checkPackageSet(rpmts ts, const char * dep,
                /*@only@*/ /*@null@*/ rpmdbMatchIterator mi, int adding)
-       /*@globals fileSystem @*/
-       /*@modifies ts, mi, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, mi, fileSystem, internalState @*/
 {
     int scareMem = 1;
     Header h;
@@ -696,8 +696,8 @@ static int checkPackageSet(rpmts ts, const char * dep,
  * @return             0 no problems found
  */
 static int checkDependentPackages(rpmts ts, const char * dep)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fileSystem, internalState @*/
 {
     rpmdbMatchIterator mi;
     mi = rpmtsInitIterator(ts, RPMTAG_REQUIRENAME, dep, 0);
@@ -711,8 +711,8 @@ static int checkDependentPackages(rpmts ts, const char * dep)
  * @return             0 no problems found
  */
 static int checkDependentConflicts(rpmts ts, const char * dep)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fileSystem, internalState @*/
 {
     int rc = 0;
 

diff --git a/lib/fsm.c b/lib/fsm.c
index db694da..a1f8907 100644 (file)
--- a/lib/fsm.c
+++ b/lib/fsm.c
@@ -384,8 +384,8 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
        /*@uses fsm->links, fsm->ix, fsm->sb, fsm->goal, fsm->nsuffix @*/
        /*@defines fsm->li @*/
        /*@releases fsm->path @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     struct stat * st = &fsm->sb;
     int rc = 0;
@@ -736,8 +736,8 @@ int fsmMapAttrs(FSM_t fsm)
  */
 static int expandRegular(/*@special@*/ FSM_t fsm)
        /*@uses fsm->sb @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const struct stat * st = &fsm->sb;
     int left = st->st_size;
@@ -803,8 +803,8 @@ exit:
  */
 static int writeFile(/*@special@*/ FSM_t fsm, int writeData)
        /*@uses fsm->path, fsm->opath, fsm->sb, fsm->osb, fsm->cfd @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * opath = fsm->opath;
@@ -951,8 +951,8 @@ exit:
  */
 static int writeLinkedFile(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->nsuffix, fsm->ix, fsm->li, fsm->failedFile @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * nsuffix = fsm->nsuffix;
@@ -999,8 +999,8 @@ static int writeLinkedFile(/*@special@*/ FSM_t fsm)
 /*@-boundsread@*/
 static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->opath, fsm->nsuffix, fsm->ix, fsm->li @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * opath = fsm->opath;
@@ -1064,8 +1064,8 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
 static int fsmCommitLinks(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->nsuffix, fsm->ix, fsm->sb,
                fsm->li, fsm->links @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     const char * nsuffix = fsm->nsuffix;
@@ -1110,8 +1110,8 @@ static int fsmCommitLinks(/*@special@*/ FSM_t fsm)
  */
 static int fsmRmdirs(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->dnlx, fsm->ldn, fsm->rdbuf, fsm->iter @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     const char * path = fsm->path;
     void * dnli = dnlInitIterator(fsm, 1);
@@ -1167,8 +1167,8 @@ static int fsmMkdirs(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->sb, fsm->osb, fsm->rdbuf, fsm->iter,
                fsm->ldn, fsm->ldnlen, fsm->ldnalloc @*/
        /*@defines fsm->dnlx, fsm->ldn @*/
-       /*@globals fileSystem@*/
-       /*@modifies fsm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/
 {
     struct stat * st = &fsm->sb;
     struct stat * ost = &fsm->osb;

diff --git a/lib/fsm.h b/lib/fsm.h
index d093ca9..8cd4f0b 100644 (file)
--- a/lib/fsm.h
+++ b/lib/fsm.h
@@ -244,8 +244,9 @@ int fsmSetup(FSM_t fsm, fileStage goal,
                FD_t cfd,
                /*@out@*/ unsigned int * archiveSize,
                /*@out@*/ const char ** failedFile)
-       /*@globals fileSystem @*/
-       /*@modifies fsm, ts, fi, *archiveSize, *failedFile, fileSystem  @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, ts, fi, *archiveSize, *failedFile,
+               fileSystem, internalState @*/;
 
 /**
  * Clean file state machine.
@@ -253,8 +254,8 @@ int fsmSetup(FSM_t fsm, fileStage goal,
  * @return             0 on success
  */
 int fsmTeardown(FSM_t fsm)
-       /*@globals fileSystem @*/
-       /*@modifies fsm, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/;
 
 /*@-exportlocal@*/
 /**
@@ -295,8 +296,8 @@ int fsmMapAttrs(FSM_t fsm)
  * @return             0 on success
  */
 int fsmStage(/*@partial@*/ FSM_t fsm, fileStage stage)
-       /*@globals fileSystem @*/
-       /*@modifies fsm, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fsm, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }

diff --git a/lib/misc.c b/lib/misc.c
index 839dcb1..c879fea 100644 (file)
--- a/lib/misc.c
+++ b/lib/misc.c
@@ -122,8 +122,8 @@ int dosetenv(const char * name, const char * value, int overwrite)
 }
 
 static int rpmMkpath(const char * path, mode_t mode, uid_t uid, gid_t gid)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     char * d, * de;
     int created = 0;

diff --git a/lib/misc.h b/lib/misc.h
index ce60350..ed93b99 100644 (file)
--- a/lib/misc.h
+++ b/lib/misc.h
@@ -18,8 +18,8 @@ extern "C" {
  * @return             rpmRC return code
  */
 rpmRC rpmMkdirPath (const char * dpath, const char * dname)
-       /*@globals fileSystem@*/
-       /*@modifies fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/;
 
 /**
  * Split string into fields separated by a character.

diff --git a/lib/psm.c b/lib/psm.c
index bd73260..79bd853 100644 (file)
--- a/lib/psm.c
+++ b/lib/psm.c
@@ -355,8 +355,8 @@ static int mergeFiles(rpmfi fi, Header h, Header newH)
  */
 /*@-bounds@*/
 static int markReplacedFiles(const PSM_t psm)
-       /*@globals fileSystem@*/
-       /*@modifies psm, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies psm, fileSystem, internalState @*/
 {
     const rpmts ts = psm->ts;
     rpmfi fi = psm->fi;

diff --git a/lib/rpmchecksig.c b/lib/rpmchecksig.c
index 3efa16b..4594b0f 100644 (file)
--- a/lib/rpmchecksig.c
+++ b/lib/rpmchecksig.c
@@ -348,7 +348,7 @@ static int rpmImportPubkey(const rpmts ts,
                /*@unused@*/ QVA_t qva,
                /*@null@*/ const char ** argv)
        /*@globals RPMVERSION, fileSystem, internalState @*/
-       /*@modifies fileSystem, internalState @*/
+       /*@modifies ts, fileSystem, internalState @*/
 {
     const char * fn;
     int res = 0;

diff --git a/lib/rpmcli.h b/lib/rpmcli.h
index d6237e7..7643a76 100644 (file)
--- a/lib/rpmcli.h
+++ b/lib/rpmcli.h
@@ -372,8 +372,8 @@ int rpmcliQuery(rpmts ts, QVA_t qva, /*@null@*/ const char ** argv)
 /*@-incondefs@*/
 int rpmVerifyFile(const rpmts ts, rpmfi fi,
                /*@out@*/ rpmVerifyAttrs * res, rpmVerifyAttrs omitMask)
-       /*@globals fileSystem @*/
-       /*@modifies fi, *res, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fi, *res, fileSystem, internalState @*/
        /*@requires maxSet(res) >= 0 @*/;
 /*@=incondefs@*/
 
@@ -575,8 +575,8 @@ typedef /*@abstract@*/ struct IDTindex_s {
  * @return             id index
  */
 /*@only@*/ /*@null@*/ IDTX IDTXload(rpmts ts, rpmTag tag)
-       /*@globals fileSystem@*/
-       /*@modifies ts, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fileSystem, internalState  @*/;
 
 /**
  * Load tag (instance,value) pairs from packages, and return sorted id index.

diff --git a/lib/rpmds.c b/lib/rpmds.c
index 3dcd5c3..eb14131 100644 (file)
--- a/lib/rpmds.c
+++ b/lib/rpmds.c
@@ -271,7 +271,9 @@ rpmds rpmdsThis(Header h, rpmTag tagN, int_32 Flags)
     EVR[0] = t;
     if (ep) {
        sprintf(t, "%d:", *ep);
+/*@-compdef@*/
        t += strlen(t);
+/*@=compdef@*/
     }
     t = stpcpy( stpcpy( stpcpy( t, v), "-"), r);
 /*@=boundswrite@*/

diff --git a/lib/rpmts.c b/lib/rpmts.c
index 6c69a84..d59f16c 100644 (file)
--- a/lib/rpmts.c
+++ b/lib/rpmts.c
@@ -25,7 +25,6 @@
 /* portability fiddles */
 #if STATFS_IN_SYS_STATVFS
 /*@-incondefs@*/
-# include <sys/statvfs.h>
 #if defined(__LCLINT__)
 /*@-declundef -exportheader -protoparammatch @*/ /* LCL: missing annotation */
 extern int statvfs (const char * file, /*@out@*/ struct statvfs * buf)
@@ -33,6 +32,8 @@ extern int statvfs (const char * file, /*@out@*/ struct statvfs * buf)
        /*@modifies *buf, fileSystem @*/;
 /*@=declundef =exportheader =protoparammatch @*/
 /*@=incondefs@*/
+#else
+# include <sys/statvfs.h>
 #endif
 #else
 # if STATFS_IN_SYS_VFS

diff --git a/lib/rpmts.h b/lib/rpmts.h
index 2467dc9..b557bb1 100644 (file)
--- a/lib/rpmts.h
+++ b/lib/rpmts.h
@@ -263,8 +263,8 @@ int rpmtsOpenDB(rpmts ts, int dbmode)
 /*@only@*/ /*@null@*/
 rpmdbMatchIterator rpmtsInitIterator(const rpmts ts, int rpmtag,
                        /*@null@*/ const void * keyp, size_t keylen)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fileSystem, internalState @*/;
 
 /**
  * Attempt to solve a needed dependency.

diff --git a/lib/signature.c b/lib/signature.c
index ce20cd2..e2daeb2 100644 (file)
--- a/lib/signature.c
+++ b/lib/signature.c
@@ -272,8 +272,10 @@ Header rpmFreeSignature(Header h)
  */
 static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
                /*@out@*/ int_32 * pktlen, /*@null@*/ const char * passPhrase)
-       /*@globals errno, rpmGlobalMacroContext, fileSystem @*/
-       /*@modifies errno, *pkt, *pktlen, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals errno, rpmGlobalMacroContext,
+               fileSystem, internalState @*/
+       /*@modifies errno, *pkt, *pktlen, rpmGlobalMacroContext,
+               fileSystem, internalState @*/
 {
     char * sigfile = alloca(1024);
     int pid, status;
@@ -291,7 +293,9 @@ static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
     addMacro(NULL, "__signature_filename", NULL, sigfile, -1);
 
     inpipe[0] = inpipe[1] = 0;
+/*@-boundsread@*/
     (void) pipe(inpipe);
+/*@=boundsread@*/
 
     if (!(pid = fork())) {
        const char *pgp_path = rpmExpand("%{?_pgp_path}", NULL);
@@ -402,8 +406,10 @@ static int makePGPSignature(const char * file, /*@out@*/ byte ** pkt,
  */
 static int makeGPGSignature(const char * file, /*@out@*/ byte ** pkt,
                /*@out@*/ int_32 * pktlen, /*@null@*/ const char * passPhrase)
-       /*@globals rpmGlobalMacroContext, fileSystem @*/
-       /*@modifies *pkt, *pktlen, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext,
+               fileSystem, internalState @*/
+       /*@modifies *pkt, *pktlen, rpmGlobalMacroContext,
+               fileSystem, internalState @*/
 {
     char * sigfile = alloca(1024);
     int pid, status;
@@ -422,7 +428,9 @@ static int makeGPGSignature(const char * file, /*@out@*/ byte ** pkt,
     addMacro(NULL, "__signature_filename", NULL, sigfile, -1);
 
     inpipe[0] = inpipe[1] = 0;
+/*@-boundsread@*/
     (void) pipe(inpipe);
+/*@=boundsread@*/
 
     if (!(pid = fork())) {
        const char *gpg_path = rpmExpand("%{?_gpg_path}", NULL);
@@ -682,7 +690,9 @@ static int checkPassPhrase(const char * passPhrase, const int sigTag)
     int xx;
 
     passPhrasePipe[0] = passPhrasePipe[1] = 0;
+/*@-boundsread@*/
     xx = pipe(passPhrasePipe);
+/*@=boundsread@*/
     if (!(pid = fork())) {
        const char * cmd;
        char *const *av;
@@ -824,7 +834,9 @@ char * rpmGetPassPhrase(const char * prompt, const int sigTag)
        /*@notreached@*/ break;
     }
 
+/*@-moduncon -nullpass @*/
     pass = /*@-unrecog@*/ getpass( (prompt ? prompt : "") ) /*@=unrecog@*/ ;
+/*@=moduncon -nullpass @*/
 
     if (checkPassPhrase(pass, sigTag))
        return NULL;

diff --git a/lib/signature.h b/lib/signature.h
index 8b78cad..6a99d6c 100644 (file)
--- a/lib/signature.h
+++ b/lib/signature.h
@@ -105,7 +105,8 @@ int rpmLookupSignatureType(int action)
  * @param sigTag       signature type/tag
  * @return             pass phrase
  */
-/*@null@*/ char * rpmGetPassPhrase(/*@null@*/ const char * prompt,
+/*@dependent@*/ /*@null@*/
+char * rpmGetPassPhrase(/*@null@*/ const char * prompt,
                const int sigTag)
        /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
        /*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/;

diff --git a/lib/transaction.c b/lib/transaction.c
index 6ae79de..a5684dd 100644 (file)
--- a/lib/transaction.c
+++ b/lib/transaction.c
@@ -85,8 +85,8 @@ static int sharedCmp(const void * one, const void * two)
 /*@-boundsread@*/
 static fileAction decideFileFate(const rpmts ts,
                const rpmfi ofi, rpmfi nfi)
-       /*@globals fileSystem @*/
-       /*@modifies nfi, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies nfi, fileSystem, internalState @*/
 {
     const char * fn = rpmfiFN(nfi);
     int newFlags = rpmfiFFlags(nfi);
@@ -222,8 +222,8 @@ static int handleInstInstalledFiles(const rpmts ts,
                rpmte p, rpmfi fi,
                sharedFileInfo shared,
                int sharedCount, int reportConflicts)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fi, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fi, fileSystem, internalState @*/
 {
     const char * altNEVR = NULL;
     rpmfi otherFi = NULL;
@@ -311,8 +311,8 @@ static int handleInstInstalledFiles(const rpmts ts,
 /* XXX only ts->rpmdb modified */
 static int handleRmvdInstalledFiles(const rpmts ts, rpmfi fi,
                sharedFileInfo shared, int sharedCount)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fi, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fi, fileSystem, internalState @*/
 {
     HGE_t hge = fi->hge;
     Header h;
@@ -502,8 +502,8 @@ bingoFps->baseName);
 /* XXX only ts->{probs,di} modified */
 static void handleOverlappedFiles(const rpmts ts,
                const rpmte p, rpmfi fi)
-       /*@globals fileSystem @*/
-       /*@modifies ts, fi, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ts, fi, fileSystem, internalState @*/
 {
     uint_32 fixupSize = 0;
     rpmps ps;

diff --git a/popt/popt.c b/popt/popt.c
index d2dffa7..d4b2dc2 100644 (file)
--- a/popt/popt.c
+++ b/popt/popt.c
@@ -355,7 +355,8 @@ static int handleAlias(/*@special@*/ poptContext con,
 
 /*@-bounds -boundswrite @*/
 static int execCommand(poptContext con)
-    /*@*/
+       /*@globals internalState @*/
+       /*@modifies internalState @*/
 {
     poptItem item = con->doExec;
     const char ** argv;

diff --git a/popt/popt.h b/popt/popt.h
index c756061..fad30bc 100644 (file)
--- a/popt/popt.h
+++ b/popt/popt.h
@@ -241,8 +241,8 @@ void poptResetContext(/*@null@*/poptContext con)
  * @return             next option val, -1 on last item, POPT_ERROR_* on error
  */
 int poptGetNextOpt(/*@null@*/poptContext con)
-       /*@globals fileSystem@*/
-       /*@modifies con, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies con, fileSystem, internalState @*/;
 
 /*@-redecl@*/
 /** \ingroup popt
@@ -334,9 +334,9 @@ int poptAddItem(poptContext con, poptItem newItem, int flags)
  * @return             0 on success, POPT_ERROR_ERRNO on failure
  */
 int poptReadConfigFile(poptContext con, const char * fn)
-       /*@globals fileSystem@*/
-       /*@modifies fileSystem,
-               con->execs, con->numExecs @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies con->execs, con->numExecs,
+               fileSystem, internalState @*/;
 
 /** \ingroup popt
  * Read default configuration from /etc/popt and $HOME/.popt.
@@ -345,9 +345,9 @@ int poptReadConfigFile(poptContext con, const char * fn)
  * @return             0 on success, POPT_ERROR_ERRNO on failure
  */
 int poptReadDefaultConfig(poptContext con, /*@unused@*/ int useEnv)
-       /*@globals fileSystem@*/
-       /*@modifies fileSystem,
-               con->execs, con->numExecs @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies con->execs, con->numExecs,
+               fileSystem, internalState @*/;
 
 /** \ingroup popt
  * Duplicate an argument array.

diff --git a/popt/test1.c b/popt/test1.c
index 8d84144..a41ee09 100644 (file)
--- a/popt/test1.c
+++ b/popt/test1.c
@@ -175,8 +175,8 @@ static void resetVars(void)
 }
 
 int main(int argc, const char ** argv)
-       /*@globals pass2, fileSystem @*/
-       /*@modifies pass2, fileSystem @*/
+       /*@globals pass2, fileSystem, internalState @*/
+       /*@modifies pass2, fileSystem, internalState @*/
 {
     int rc;
     int ec = 0;

diff --git a/rpmdb/fprint.c b/rpmdb/fprint.c
index 250898d..2244a91 100644 (file)
--- a/rpmdb/fprint.c
+++ b/rpmdb/fprint.c
@@ -42,7 +42,9 @@ static /*@null@*/ const struct fprintCacheEntry_s * cacheContainsDirectory(
 
     if (htGetEntry(cache->ht, dirName, &data, NULL, NULL))
        return NULL;
+/*@-boundsread@*/
     return data[0];
+/*@=boundsread@*/
 }
 
 /**

diff --git a/rpmdb/header.c b/rpmdb/header.c
index 35a9021..bd44287 100644 (file)
--- a/rpmdb/header.c
+++ b/rpmdb/header.c
@@ -1669,6 +1669,7 @@ int headerGetEntry(Header h, int_32 tag,
                        /*@null@*/ /*@out@*/ void ** p,
                        /*@null@*/ /*@out@*/ hCNT_t c)
        /*@modifies *type, *p, *c @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     return intGetEntry(h, tag, type, (hPTR_t *)p, c, 0);
 }
@@ -1691,6 +1692,7 @@ int headerGetEntryMinMemory(Header h, int_32 tag,
                        /*@null@*/ /*@out@*/ hPTR_t * p,
                        /*@null@*/ /*@out@*/ hCNT_t c)
        /*@modifies *type, *p, *c @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     return intGetEntry(h, tag, type, p, c, 1);
 }
@@ -2678,11 +2680,13 @@ static char * formatValue(sprintfTag tag, Header h,
        }
 /*@=boundswrite@*/
     } else {
+/*@-boundswrite@*/
        if (!headerGetEntry(h, tag->tag, &type, (void **)&data, &count)) {
            count = 1;
            type = RPM_STRING_TYPE;     
            data = "(none)";
        }
+/*@=boundswrite@*/
 
        datafree = 1;
     }
@@ -2952,9 +2956,11 @@ static char * singleSprintf(Header h, sprintfToken token,
                     continue;
 /*@=boundswrite@*/
            } else {
+/*@-boundswrite@*/
                if (!headerGetEntry(h, token->u.array.format[i].u.tag.tag, 
                                    &type, NULL, &numElements))
                    continue;
+/*@=boundswrite@*/
            } 
            /*@loopbreak@*/ break;
        }
@@ -3297,9 +3303,11 @@ void headerCopyTags(Header headerFrom, Header headerTo, hTAG_t tagstocopy)
        int_32 count;
        if (headerIsEntry(headerTo, *p))
            continue;
+/*@-boundswrite@*/
        if (!headerGetEntryMinMemory(headerFrom, *p, &type,
                                (hPTR_t *) &s, &count))
            continue;
+/*@=boundswrite@*/
        (void) headerAddEntry(headerTo, *p, type, s, count);
        s = headerFreeData(s, type);
     }

diff --git a/rpmdb/legacy.c b/rpmdb/legacy.c
index 64033c0..2c1fd3f 100644 (file)
--- a/rpmdb/legacy.c
+++ b/rpmdb/legacy.c
@@ -244,6 +244,7 @@ exit:
 int _noDirTokens = 0;
 /*@=exportheadervar@*/
 
+/*@-boundsread@*/
 static int dncmp(const void * a, const void * b)
        /*@*/
 {
@@ -251,6 +252,7 @@ static int dncmp(const void * a, const void * b)
     const char *const * second = b;
     return strcmp(*first, *second);
 }
+/*@=boundsread@*/
 
 /*@-bounds@*/
 void compressFilelist(Header h)

diff --git a/rpmdb/legacy.h b/rpmdb/legacy.h
index 69ade41..d9b9331 100644 (file)
--- a/rpmdb/legacy.h
+++ b/rpmdb/legacy.h
@@ -27,8 +27,8 @@ extern "C" {
  */
 int domd5(const char * fn, /*@out@*/ unsigned char * digest, int asAscii,
                /*@null@*/ /*@out@*/ size_t *fsizep)
-       /*@globals fileSystem @*/
-       /*@modifies digest, *fsizep, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies digest, *fsizep, fileSystem, internalState @*/;
 
 /**
  * Convert absolute path tag to (dirname,basename,dirindex) tags.

diff --git a/rpmdb/rpmdb.c b/rpmdb/rpmdb.c
index e37a4da..6175d0c 100644 (file)
--- a/rpmdb/rpmdb.c
+++ b/rpmdb/rpmdb.c
@@ -3020,8 +3020,8 @@ if (key->size == 0) key->size++;  /* XXX "/" fixup. */
  * @return             1 if file exists, 0 if not
  */
 static int rpmioFileExists(const char * urlfn)
-        /*@globals fileSystem @*/
-        /*@modifies fileSystem @*/
+        /*@globals fileSystem, internalState @*/
+        /*@modifies fileSystem, internalState @*/
 {
     const char *fn;
     int urltype = urlPath(urlfn, &fn);
@@ -3054,8 +3054,8 @@ static int rpmioFileExists(const char * urlfn)
 
 static int rpmdbRemoveDatabase(const char * prefix,
                const char * dbpath, int _dbapi)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 { 
     int i;
     char * filename;
@@ -3109,8 +3109,8 @@ static int rpmdbRemoveDatabase(const char * prefix,
 static int rpmdbMoveDatabase(const char * prefix,
                const char * olddbpath, int _olddbapi,
                const char * newdbpath, int _newdbapi)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     int i;
     char * ofilename, * nfilename;

diff --git a/rpmio/digest.c b/rpmio/digest.c
index 1746720..8e7c5a2 100644 (file)
--- a/rpmio/digest.c
+++ b/rpmio/digest.c
@@ -103,7 +103,9 @@ int
 rpmDigestUpdate(DIGEST_CTX ctx, const void * data, size_t len)
 {
 DPRINTF((stderr, "*** Update(%p,%p,%d) param %p \"%s\"\n", ctx, data, len, ctx->param, ((char *)data)));
+/*@-boundsread@*/
     return (*ctx->Update) (ctx->param, data, len);
+/*@=boundsread@*/
 }
 /*@=mustmod@*/
 

diff --git a/rpmio/rpmio.c b/rpmio/rpmio.c
index 3ae20a5..e0613db 100644 (file)
--- a/rpmio/rpmio.c
+++ b/rpmio/rpmio.c
@@ -410,12 +410,16 @@ ssize_t fdWrite(void * cookie, const char * buf, size_t count)
     if (count == 0) return 0;
 
     fdstat_enter(fd, FDSTAT_WRITE);
+/*@-boundsread@*/
     rc = write(fdno, buf, (count > fd->bytesRemain ? fd->bytesRemain : count));
+/*@=boundsread@*/
     fdstat_exit(fd, FDSTAT_WRITE, rc);
 
     if (fd->wr_chunked) {
        int ec;
+/*@-boundsread@*/
        ec = write(fdno, "\r\n", sizeof("\r\n")-1);
+/*@=boundsread@*/
        if (ec == -1)   fd->syserrno = errno;
     }
 
@@ -769,8 +773,8 @@ static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
 /*@=boundsread@*/
 
 static int tcpConnect(FD_t ctrl, const char * host, int port)
-       /*@globals fileSystem @*/
-       /*@modifies ctrl, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ctrl, fileSystem, internalState @*/
 {
     struct sockaddr_in sin;
     int fdno = -1;
@@ -1054,8 +1058,8 @@ fprintf(stderr, "-> %s", t);
 }
 
 static int ftpLogin(urlinfo u)
-       /*@globals fileSystem @*/
-       /*@modifies u, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies u, fileSystem, internalState @*/
 {
     const char * host;
     const char * user;
@@ -1362,8 +1366,8 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 }
 
 static int urlConnect(const char * url, /*@out@*/ urlinfo * uret)
-       /*@globals fileSystem @*/
-       /*@modifies *uret, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *uret, fileSystem, internalState @*/
 {
     urlinfo u;
     int rc = 0;
@@ -1451,8 +1455,8 @@ int ftpCmd(const char * cmd, const char * url, const char * arg2)
 #endif
 
 static int ftpAbort(urlinfo u, FD_t data)
-       /*@globals fileSystem @*/
-       /*@modifies u, data, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies u, data, fileSystem, internalState @*/
 {
     static unsigned char ipbuf[3] = { IAC, IP, IAC };
     FD_t ctrl;
@@ -1558,8 +1562,8 @@ fprintf(stderr, "*** httpResp: rc %d ec %d\n", rc, ec);
 }
 
 static int httpReq(FD_t ctrl, const char * httpCmd, const char * httpArg)
-       /*@globals fileSystem @*/
-       /*@modifies ctrl, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies ctrl, fileSystem, internalState @*/
 {
     urlinfo u = ctrl->url;
     const char * host;
@@ -1686,6 +1690,8 @@ void * ufdGetUrlinfo(FD_t fd)
 static ssize_t ufdRead(void * cookie, /*@out@*/ char * buf, size_t count)
        /*@globals fileSystem, internalState @*/
        /*@modifies *buf, fileSystem, internalState @*/
+        /*@requires maxSet(buf) >= (count - 1) @*/
+        /*@ensures maxRead(buf) == result @*/
 {
     FD_t fd = c2f(cookie);
     int bytesRead;
@@ -2000,7 +2006,8 @@ exit:
 /*@-nullstate@*/       /* FIX: u->{ctrl,data}->url undef after XurlLink. */
 static /*@null@*/ FD_t httpOpen(const char * url, /*@unused@*/ int flags,
                /*@unused@*/ mode_t mode, /*@out@*/ urlinfo * uret)
-       /*@modifies *uret @*/
+       /*@globals internalState @*/
+       /*@modifies *uret, internalState @*/
 {
     urlinfo u = NULL;
     FD_t fd = NULL;
@@ -2045,8 +2052,8 @@ exit:
 /*@=nullstate@*/
 
 static /*@null@*/ FD_t ufdOpen(const char * url, int flags, mode_t mode)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     FD_t fd = NULL;
     const char * cmd;

diff --git a/rpmio/rpmio.h b/rpmio/rpmio.h
index a05e2a5..3046185 100644 (file)
--- a/rpmio/rpmio.h
+++ b/rpmio/rpmio.h
@@ -264,8 +264,8 @@ int Fseek(FD_t fd, _libio_off_t offset, int whence)
  * fclose(3) clone.
  */
 int Fclose( /*@killref@*/ FD_t fd)
-       /*@globals fileSystem @*/
-       /*@modifies fd, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fd, fileSystem, internalState @*/;
 
 /**
  */
@@ -278,8 +278,8 @@ int Fclose( /*@killref@*/ FD_t fd)
  */
 /*@null@*/ FD_t        Fopen(/*@null@*/ const char * path,
                        /*@null@*/ const char * fmode)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/;
 
 
 /**
@@ -321,51 +321,51 @@ int Fcntl(FD_t fd, int op, void *lip)
  * mkdir(2) clone.
  */
 int Mkdir(const char * path, mode_t mode)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * chdir(2) clone.
  */
 int Chdir(const char * path)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * rmdir(2) clone.
  */
 int Rmdir(const char * path)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * rename(2) clone.
  */
 int Rename(const char * oldpath, const char * newpath)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * link(2) clone.
  */
 int Link(const char * oldpath, const char * newpath)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * unlink(2) clone.
  */
 int Unlink(const char * path)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * readlink(2) clone.
  */
 /*@-incondefs@*/
 int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
-       /*@globals errno, fileSystem @*/
-       /*@modifies *buf, errno, fileSystem @*/
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies *buf, errno, fileSystem, internalState @*/
        /*@requires maxSet(buf) >= (bufsiz - 1) @*/
        /*@ensures maxRead(buf) <= bufsiz @*/;
 /*@=incondefs@*/
@@ -374,15 +374,15 @@ int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
  * stat(2) clone.
  */
 int Stat(const char * path, /*@out@*/ struct stat * st)
-       /*@globals errno, fileSystem @*/
-       /*@modifies *st, errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies *st, errno, fileSystem, internalState @*/;
 
 /**
  * lstat(2) clone.
  */
 int Lstat(const char * path, /*@out@*/ struct stat * st)
-       /*@globals errno, fileSystem @*/
-       /*@modifies *st, errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies *st, errno, fileSystem, internalState @*/;
 
 /**
  * access(2) clone.
@@ -414,13 +414,13 @@ void Globfree( /*@only@*/ glob_t * pglob)
  */
 /*@null@*/
 DIR * Opendir(const char * path)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 
 /**
  * readdir(3) clone.
  */
-/*@null@*/
+/*@dependent@*/ /*@null@*/
 struct dirent * Readdir(DIR * dir)
        /*@globals errno, fileSystem @*/
        /*@modifies *dir, errno, fileSystem @*/;
@@ -449,8 +449,8 @@ off_t       fdSize(FD_t fd)
 /**
  */
 /*@null@*/ FD_t fdDup(int fdno)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem@*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/;
 
 #ifdef UNUSED
 /*@null@*/ FILE *fdFdopen( /*@only@*/ void * cookie, const char * mode);
@@ -470,8 +470,8 @@ off_t       fdSize(FD_t fd)
 /**
  */
 /*@null@*/ FD_t fdOpen(const char *path, int flags, mode_t mode)
-       /*@globals errno, fileSystem @*/
-       /*@modifies errno, fileSystem @*/;
+       /*@globals errno, fileSystem, internalState @*/
+       /*@modifies errno, fileSystem, internalState @*/;
 #define        fdOpen(_path, _flags, _mode)    fdio->_open((_path), (_flags), (_mode))
 
 /**
@@ -495,8 +495,8 @@ ssize_t     fdWrite(void * cookie, const char * buf, size_t count)
 /**
  */
 int fdClose( /*@only@*/ void * cookie)
-       /*@globals errno, fileSystem, systemState @*/
-       /*@modifies *cookie, errno, fileSystem, systemState @*/;
+       /*@globals errno, fileSystem, systemState, internalState @*/
+       /*@modifies *cookie, errno, fileSystem, systemState, internalState @*/;
 #define        fdCLose(_fd)            fdio->close(_fd)
 
 /**
@@ -562,7 +562,8 @@ typedef enum ftperrCode_e {
 /**
  */
 /*@-redecl@*/
-/*@observer@*/ const char *const ftpStrerror(int errorNumber)  /*@*/;
+/*@observer@*/ const char *const ftpStrerror(int errorNumber)
+       /*@*/;
 /*@=redecl@*/
 
 /**
@@ -575,7 +576,9 @@ typedef enum ftperrCode_e {
  */
 /*@-redecl@*/
 /*@unused@*/
-/*@observer@*/ const char * urlStrerror(const char * url)      /*@*/;
+/*@observer@*/ const char * urlStrerror(const char * url)
+       /*@globals internalState @*/
+       /*@modifies internalState @*/;
 /*@=redecl@*/
 
 /**
@@ -589,8 +592,8 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 /**
  */
 int ufdGetFile( /*@killref@*/ FD_t sfd, FD_t tfd)
-       /*@globals fileSystem @*/
-       /*@modifies sfd, tfd, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies sfd, tfd, fileSystem, internalState @*/;
 
 /**
  */

diff --git a/rpmio/rpmio_internal.h b/rpmio/rpmio_internal.h
index 34accaa..a4845aa 100644 (file)
--- a/rpmio/rpmio_internal.h
+++ b/rpmio/rpmio_internal.h
@@ -180,26 +180,26 @@ int fdFgets(FD_t fd, char * buf, size_t len)
  */
 /*@null@*/ FD_t ftpOpen(const char *url, /*@unused@*/ int flags,
                 /*@unused@*/ mode_t mode, /*@out@*/ urlinfo *uret)
-       /*@globals fileSystem @*/
-       /*@modifies *uret, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *uret, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ftpReq(FD_t data, const char * ftpCmd, const char * ftpArg)
-       /*@globals fileSystem @*/
-       /*@modifies data, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ftpCmd(const char * cmd, const char * url, const char * arg2)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
 int ufdClose( /*@only@*/ void * cookie)
-       /*@globals fileSystem @*/
-       /*@modifies cookie, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies cookie, fileSystem, internalState @*/;
 
 /** \ingroup rpmio
  */
@@ -208,7 +208,9 @@ int ufdClose( /*@only@*/ void * cookie)
        /*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].io;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -234,9 +236,11 @@ void fdSetIo(FD_t fd, /*@kept@*/ /*@null@*/ FDIO_t io)
        /*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     /*@+voidabstract@*/
     return ((FILE *)fd->fps[fd->nfps].fp);
     /*@=voidabstract@*/
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -246,7 +250,9 @@ void fdSetIo(FD_t fd, /*@kept@*/ /*@null@*/ FDIO_t io)
        /*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].fp;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -272,7 +278,9 @@ int fdGetFdno(FD_t fd)
        /*@*/
 {
     FDSANE(fd);
+/*@-boundsread@*/
     return fd->fps[fd->nfps].fdno;
+/*@=boundsread@*/
 }
 
 /** \ingroup rpmio
@@ -549,16 +557,23 @@ int fdFileno(/*@null@*/ void * cookie)
     FD_t fd;
     if (cookie == NULL) return -2;
     fd = c2f(cookie);
+/*@-boundsread@*/
     return fd->fps[0].fdno;
+/*@=boundsread@*/
 }
 /*@=shadow@*/
 
 /**
+ * Read an entire file into a buffer.
+ * @param fn           file name to read
+ * @retval *bp         (malloc'd) buffer address
+ * @retval *blenp      (malloc'd) buffer length
+ * @return             0 on success
  */
 int rpmioSlurp(const char * fn,
                 /*@out@*/ const unsigned char ** bp, /*@out@*/ ssize_t * blenp)
-        /*@globals fileSystem @*/
-        /*@modifies *bp, *blenp, fileSystem @*/;
+        /*@globals fileSystem, internalState @*/
+        /*@modifies *bp, *blenp, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }

diff --git a/rpmio/rpmmacro.h b/rpmio/rpmmacro.h
index 020a954..97eae6a 100644 (file)
--- a/rpmio/rpmmacro.h
+++ b/rpmio/rpmmacro.h
@@ -137,8 +137,8 @@ void        rpmLoadMacros   (/*@null@*/ MacroContext mc, int level)
  */
 void   rpmInitMacros   (/*@null@*/ MacroContext mc, const char * macrofiles)
        /*@globals rpmGlobalMacroContext, rpmCLIMacroContext,
-               fileSystem @*/
-       /*@modifies rpmGlobalMacroContext, fileSystem @*/;
+               fileSystem, internalState @*/
+       /*@modifies rpmGlobalMacroContext, fileSystem, internalState @*/;
 
 /**
  * Destroy macro context.
@@ -163,8 +163,8 @@ typedef enum rpmCompressedMagic_e {
  */
 int    isCompressed    (const char * file,
                                /*@out@*/ rpmCompressedMagic * compressed)
-       /*@globals fileSystem@*/
-       /*@modifies *compressed, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *compressed, fileSystem, internalState @*/;
 
 /**
  * Return (malloc'ed) concatenated macro expansion(s).

diff --git a/rpmio/rpmpgp.h b/rpmio/rpmpgp.h
index 3e48869..98fa3e2 100644 (file)
--- a/rpmio/rpmpgp.h
+++ b/rpmio/rpmpgp.h
@@ -1074,6 +1074,7 @@ int pgpLen(const byte *s, /*@out@*/ unsigned int *lenp)
  */
 /*@unused@*/ static inline
 unsigned int pgpMpiBits(const byte *p)
+       /*@requires maxRead(p) >= 1 @*/
        /*@*/
 {
     return ((p[0] << 8) | p[1]);
@@ -1086,6 +1087,7 @@ unsigned int pgpMpiBits(const byte *p)
  */
 /*@unused@*/ static inline
 unsigned int pgpMpiLen(const byte *p)
+       /*@requires maxRead(p) >= 1 @*/
        /*@*/
 {
     return (2 + ((pgpMpiBits(p)+7)>>3));
@@ -1140,6 +1142,7 @@ char * pgpHexStr(const byte *p, unsigned int plen)
  */
 /*@unused@*/ static inline /*@observer@*/
 const char * pgpMpiStr(const byte *p)
+       /*@requires maxRead(p) >= 3 @*/
        /*@*/
 {
     static char prbuf[2048];
@@ -1282,8 +1285,8 @@ int pgpPrtPkts(const byte *pkts, unsigned int plen, struct pgpDig_s *dig, int pr
  */
 pgpArmor pgpReadPkts(const char * fn,
                /*@out@*/ const byte ** pkt, /*@out@*/ size_t * pktlen)
-       /*@globals fileSystem @*/
-       /*@modifies *pkt, *pktlen, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *pkt, *pktlen, fileSystem, internalState @*/;
 
 /**
  * Create a container for parsed OpenPGP packates.

diff --git a/rpmio/rpmrpc.c b/rpmio/rpmrpc.c
index 0eeca5a..8154415 100644 (file)
--- a/rpmio/rpmrpc.c
+++ b/rpmio/rpmrpc.c
@@ -18,8 +18,8 @@
 
 /* =============================================================== */
 static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     int rc;
     if ((rc = ftpCmd("MKD", path, NULL)) != 0)
@@ -34,22 +34,22 @@ static int ftpMkdir(const char * path, /*@unused@*/ mode_t mode)
 }
 
 static int ftpChdir(const char * path)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("CWD", path, NULL);
 }
 
 static int ftpRmdir(const char * path)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("RMD", path, NULL);
 }
 
 static int ftpRename(const char * oldpath, const char * newpath)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     int rc;
     if ((rc = ftpCmd("RNFR", oldpath, NULL)) != 0)
@@ -58,8 +58,8 @@ static int ftpRename(const char * oldpath, const char * newpath)
 }
 
 static int ftpUnlink(const char * path)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     return ftpCmd("DELE", path, NULL);
 }
@@ -825,8 +825,8 @@ static /*@only@*/ char * ftpBuf = NULL;
 static int ftpNLST(const char * url, ftpSysCall_t ftpSysCall,
                /*@out@*/ /*@null@*/ struct stat * st,
                /*@out@*/ /*@null@*/ char * rlbuf, size_t rlbufsiz)
-       /*@globals fileSystem @*/
-       /*@modifies *st, *rlbuf, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *st, *rlbuf, fileSystem, internalState @*/
 {
     FD_t fd;
     const char * path;
@@ -1034,8 +1034,8 @@ static const char * statstr(const struct stat * st,
 static int ftp_st_ino = 0xdead0000;
 
 static int ftpStat(const char * path, /*@out@*/ struct stat *st)
-       /*@globals fileSystem @*/
-       /*@modifies *st, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *st, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
@@ -1051,8 +1051,8 @@ fprintf(stderr, "*** ftpStat(%s) rc %d\n%s", path, rc, statstr(st, buf));
 }
 
 static int ftpLstat(const char * path, /*@out@*/ struct stat *st)
-       /*@globals fileSystem @*/
-       /*@modifies *st, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *st, fileSystem, internalState @*/
 {
     char buf[1024];
     int rc;
@@ -1068,8 +1068,8 @@ fprintf(stderr, "*** ftpLstat(%s) rc %d\n%s\n", path, rc, statstr(st, buf));
 }
 
 static int ftpReadlink(const char * path, /*@out@*/ char * buf, size_t bufsiz)
-       /*@globals fileSystem @*/
-       /*@modifies *buf, fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies *buf, fileSystem, internalState @*/
 {
     int rc;
     rc = ftpNLST(path, DO_FTP_READLINK, NULL, buf, bufsiz);
@@ -1098,8 +1098,8 @@ static int ftpmagicdir = 0x8440291;
 /*@-type@*/ /* FIX: abstract DIR */
 /*@null@*/
 static DIR * ftpOpendir(const char * path)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
     DIR * dir;
     struct dirent * dp;
@@ -1231,7 +1231,7 @@ fprintf(stderr, "*** ftpOpendir(%s)\n", path);
 }
 /*@=boundswrite@*/
 
-/*@null@*/
+/*@dependent@*/ /*@null@*/
 static struct dirent * ftpReaddir(DIR * dir)
        /*@globals fileSystem @*/
        /*@modifies fileSystem @*/
@@ -1367,7 +1367,9 @@ int Readlink(const char * path, char * buf, size_t bufsiz)
        return -2;
        /*@notreached@*/ break;
     }
+/*@-compdef@*/
     return readlink(path, buf, bufsiz);
+/*@=compdef@*/
 }
 
 int Access(const char * path, int amode)

diff --git a/rpmio/rpmurl.h b/rpmio/rpmurl.h
index 0f06eb2..770c610 100644 (file)
--- a/rpmio/rpmurl.h
+++ b/rpmio/rpmurl.h
@@ -109,21 +109,22 @@ urlinfo   XurlLink(urlinfo u, const char * msg, const char * file, unsigned line)
  * @return             dereferenced instance (NULL if freed)
  */
 /*@unused@*/ urlinfo   urlFree( /*@killref@*/ urlinfo u, const char * msg)
-       /*@modifies u @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies u, fileSystem, internalState @*/;
 
 /** @todo Remove debugging entry from the ABI. */
 urlinfo        XurlFree( /*@killref@*/ urlinfo u, const char * msg,
                const char * file, unsigned line)
-       /*@globals fileSystem@*/
-       /*@modifies u, fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies u, fileSystem, internalState @*/;
 #define        urlFree(_u, _msg) XurlFree(_u, _msg, __FILE__, __LINE__)
 
 /**
  * Free cached URL control structures.
  */
 void urlFreeCache(void)
-       /*@globals _url_cache, _url_count, fileSystem @*/
-       /*@modifies _url_cache, _url_count, fileSystem @*/;
+       /*@globals _url_cache, _url_count, fileSystem, internalState @*/
+       /*@modifies _url_cache, _url_count, fileSystem, internalState @*/;
 
 /**
  * Return type of URL.
@@ -152,7 +153,8 @@ urltype     urlPath(const char * url, /*@out@*/ const char ** pathp)
  * @return             0 on success, -1 on error
  */
 int urlSplit(const char * url, /*@out@*/ urlinfo * uret)
-       /*@modifies *uret @*/;
+       /*@globals internalState @*/
+       /*@modifies *uret, internalState @*/;
 
 /**
  * Copy data from URL to local file.
@@ -161,8 +163,8 @@ int urlSplit(const char * url, /*@out@*/ urlinfo * uret)
  * @return             0 on success, otherwise FTPERR_* code
  */
 int urlGetFile(const char * url, /*@null@*/ const char * dest)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }

diff --git a/rpmio/url.c b/rpmio/url.c
index cbb3eba..685375c 100644 (file)
--- a/rpmio/url.c
+++ b/rpmio/url.c
@@ -193,8 +193,8 @@ static int urlStrcmp(/*@null@*/ const char * str1, /*@null@*/ const char * str2)
 /*@-boundswrite@*/
 /*@-mods@*/
 static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
-       /*@globals rpmGlobalMacroContext, fileSystem@*/
-       /*@modifies *uret, rpmGlobalMacroContext, fileSystem @*/
+       /*@globals rpmGlobalMacroContext, fileSystem, internalState @*/
+       /*@modifies *uret, rpmGlobalMacroContext, fileSystem, internalState @*/
 {
     urlinfo u;
     int ucx;
@@ -266,8 +266,11 @@ static void urlFind(/*@null@*/ /*@in@*/ /*@out@*/ urlinfo * uret, int mustAsk)
            prompt = alloca(strlen(host) + strlen(user) + 256);
            sprintf(prompt, _("Password for %s@%s: "), user, host);
            u->password = _free(u->password);
+/*@-dependenttrans -moduncon @*/
            u->password = /*@-unrecog@*/ getpass(prompt) /*@=unrecog@*/;
-           u->password = xstrdup(u->password); /* XXX xstrdup has side effects. */
+/*@=dependenttrans =moduncon @*/
+           if (u->password)
+               u->password = xstrdup(u->password);
        }
 
        if (u->proxyh == NULL) {