Add boundsread annotations throughout, enable +bounds checking.
authorjbj <devnull@localhost>
Tue, 2 Jul 2002 23:54:35 +0000 (23:54 +0000)
committerjbj <devnull@localhost>
Tue, 2 Jul 2002 23:54:35 +0000 (23:54 +0000)
Start narrowing the scope of bounds annotations by adding more annotations.

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

68 files changed:
.lclintrc
beecrypt/.lclintrc
beecrypt/aes.c
beecrypt/base64.c
beecrypt/beecrypt.c
beecrypt/blockpad.c
beecrypt/blowfish.c
beecrypt/endianness.c
beecrypt/md5.c
beecrypt/mp32.c
beecrypt/mp32barrett.c
beecrypt/mp32prime.c
beecrypt/mtprng.c
beecrypt/sha1.c
beecrypt/sha256.c
build.c
build/.lclintrc
build/build.c
build/expression.c
build/files.c
build/names.c
build/pack.c
build/parsePreamble.c
build/parsePrep.c
build/parseReqs.c
build/parseSpec.c
build/reqprov.c
build/spec.c
lib/.lclintrc
lib/cpio.c
lib/depends.c
lib/formats.c
lib/fs.c
lib/fsm.c
lib/misc.c
lib/package.c
lib/poptALL.c
lib/poptI.c
lib/poptQV.c
lib/psm.c
lib/rpmlib.h
lib/transaction.c
popt/.lclintrc
popt/popt.c
popt/popthelp.c
popt/test1.c
rpmdb/.lclintrc
rpmdb/dbconfig.c
rpmdb/fprint.c
rpmdb/header.c
rpmdb/header.h
rpmdb/header_internal.c
rpmdb/header_internal.h
rpmdb/legacy.c
rpmdb/rpmdb.c
rpmdb/rpmhash.c
rpmio/.lclintrc
rpmio/digest.c
rpmio/fts.c
rpmio/macro.c
rpmio/rpmio.c
rpmio/rpmlog.c
rpmio/rpmpgp.c
rpmio/rpmrpc.c
rpmio/rpmurl.h
rpmio/strcasecmp.c
rpmio/url.c
rpmqv.c

index 9f56f67..85f7f3f 100644 (file)
--- a/.lclintrc
+++ b/.lclintrc
@@ -13,8 +13,8 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds
-+boundswrite
++bounds
+#+boundswrite
 +slovak-fcns
 -redecl
 
index 674899a..652a599 100644 (file)
@@ -13,8 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds               # 416
-+boundswrite           # 169
++bounds
 
 # --- not-yet at strict level
 -exportconst           # 4
index e30e7ec..01f7f6a 100644 (file)
@@ -889,6 +889,7 @@ int aesSetup(aesParam* ap, const uint32* key, int keybits, cipherOperation op)
 /*@=boundswrite@*/
 
 #ifndef ASM_AESSETIV
+/*@-boundsread@*/
 int aesSetIV(aesParam* ap, const uint32* iv)
 {
        if (iv)
@@ -908,6 +909,7 @@ int aesSetIV(aesParam* ap, const uint32* iv)
 
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #define etfs(i) \
@@ -1266,6 +1268,7 @@ int aesCBCEncrypt(aesParam* ap, int count, uint32* dst, const uint32* src)
 #endif
 
 #ifndef ASM_AESCBCDECRYPT
+/*@-boundsread@*/
 int aesCBCDecrypt(aesParam* ap, int count, uint32* dst, const uint32* src)
 {
        if (count > 0)
@@ -1356,4 +1359,5 @@ int aesCBCDecrypt(aesParam* ap, int count, uint32* dst, const uint32* src)
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
index 4df5ba0..7f042f6 100644 (file)
@@ -334,6 +334,7 @@ fprintf(stderr, "%7u %02x %02x %02x -> %02x %02x %02x %02x\n",
 #define CRC24_INIT 0xb704ceL
 #define CRC24_POLY 0x1864cfbL
 
+/*@-boundsread@*/
 char * b64crc (const unsigned char * data, int ns)
 {
     const unsigned char *s = data;
@@ -359,6 +360,7 @@ char * b64crc (const unsigned char * data, int ns)
     ns = 3;
     return b64encode(data, ns);
 }
+/*@=boundsread@*/
 /*@=internalglobs =modfilesys @*/
 
 const char * b64decode_whitespace = B64DECODE_WHITESPACE;
index 6f304b7..cdcce31 100644 (file)
@@ -99,6 +99,7 @@ const entropySource* entropySourceGet(int index)
        return entropySourceList+index;
 }
 
+/*@-boundsread@*/
 const entropySource* entropySourceFind(const char* name)
 {
        register int index;
@@ -110,6 +111,7 @@ const entropySource* entropySourceFind(const char* name)
        }
        return (const entropySource*) 0;
 }
+/*@=boundsread@*/
 
 const entropySource* entropySourceDefault()
 {
@@ -123,6 +125,7 @@ const entropySource* entropySourceDefault()
                return (const entropySource*) 0;
 }
 
+/*@-boundsread@*/
 int entropyGatherNext(uint32* data, int size)
 {
        const char* selection = getenv("BEECRYPT_ENTROPY");
@@ -146,6 +149,7 @@ int entropyGatherNext(uint32* data, int size)
        }
        return -1;
 }
+/*@=boundsread@*/
 
 /*@-type@*/ /* FIX: cast? */
 /*@observer@*/ /*@unchecked@*/
@@ -173,6 +177,7 @@ const randomGenerator* randomGeneratorGet(int index)
        /*@=compmempass@*/
 }
 
+/*@-boundsread@*/
 const randomGenerator* randomGeneratorFind(const char* name)
 {
        register int index;
@@ -186,6 +191,7 @@ const randomGenerator* randomGeneratorFind(const char* name)
        }
        return (const randomGenerator*) 0;
 }
+/*@=boundsread@*/
 
 const randomGenerator* randomGeneratorDefault()
 {
@@ -290,6 +296,7 @@ const hashFunction* hashFunctionGet(int index)
        /*@=compmempass@*/
 }
 
+/*@-boundsread@*/
 const hashFunction* hashFunctionFind(const char* name)
 {
        register int index;
@@ -303,6 +310,7 @@ const hashFunction* hashFunctionFind(const char* name)
        }
        return (const hashFunction*) 0;
 }
+/*@=boundsread@*/
 
 int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
 {
@@ -508,6 +516,7 @@ const keyedHashFunction* keyedHashFunctionGet(int index)
        /*@=compmempass@*/
 }
 
+/*@-boundsread@*/
 const keyedHashFunction* keyedHashFunctionFind(const char* name)
 {
        register int index;
@@ -521,6 +530,7 @@ const keyedHashFunction* keyedHashFunctionFind(const char* name)
        }
        return (const keyedHashFunction*) 0;
 }
+/*@=boundsread@*/
 
 int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHashFunction* mac)
 {
@@ -747,6 +757,7 @@ const blockCipher* blockCipherGet(int index)
        /*@=compmempass@*/
 }
 
+/*@-boundsread@*/
 const blockCipher* blockCipherFind(const char* name)
 {
        register int index;
@@ -761,6 +772,7 @@ const blockCipher* blockCipherFind(const char* name)
 
        return (const blockCipher*) 0;
 }
+/*@=boundsread@*/
 
 int blockCipherContextInit(blockCipherContext* ctxt, const blockCipher* ciph)
 {
index 22a6a10..a6637ec 100644 (file)
@@ -46,6 +46,7 @@ memchunk* pkcs5Pad(int blockbytes, memchunk* tmp)
 }
 /*@=boundswrite@*/
 
+/*@-boundsread@*/
 memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
 {
        if (tmp)
@@ -73,6 +74,7 @@ memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
        return tmp;
        /*@=temptrans@*/
 }
+/*@=boundsread@*/
 
 /*@-boundswrite@*/
 memchunk* pkcs5PadCopy(int blockbytes, const memchunk* src)
index 00029b1..9842fc9 100644 (file)
@@ -328,6 +328,7 @@ static const blockMode blowfishModes[2] =
 const blockCipher blowfish = { "Blowfish", sizeof(blowfishParam), 8, 64, 448, 32, (blockCipherSetup) blowfishSetup, (blockCipherSetIV) blowfishSetIV, (blockCipherEncrypt) blowfishEncrypt, (blockCipherDecrypt) blowfishDecrypt, blowfishModes };
 /*@=sizeoftype@*/
 
+/*@-boundsread@*/
 int blowfishSetup(blowfishParam* bp, const uint32* key, int keybits, /*@unused@*/ cipherOperation op)
 {
        if (((keybits & 7) == 0) && (keybits >= 64) && (keybits <= 448))
@@ -388,8 +389,10 @@ int blowfishSetup(blowfishParam* bp, const uint32* key, int keybits, /*@unused@*
        }
        return -1;
 }
+/*@=boundsread@*/
 
 #ifndef ASM_BLOWFISHSETIV
+/*@-boundsread@*/
 int blowfishSetIV(blowfishParam* bp, const uint32* iv)
 {
        if (iv)
@@ -405,6 +408,7 @@ int blowfishSetIV(blowfishParam* bp, const uint32* iv)
 
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_BLOWFISHENCRYPT
@@ -545,6 +549,7 @@ int blowfishCBCEncrypt(blowfishParam* bp, int count, uint32* dst, const uint32*
 #endif
 
 #ifndef ASM_BLOWFISHCBCDECRYPT
+/*@-boundsread@*/
 int blowfishCBCDecrypt(blowfishParam* bp, int count, uint32* dst, const uint32* src)
 {
        if (count > 0)
@@ -617,4 +622,5 @@ int blowfishCBCDecrypt(blowfishParam* bp, int count, uint32* dst, const uint32*
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
index 98969a4..fe8a383 100644 (file)
@@ -555,7 +555,9 @@ int writeInts(const javaint* i, FILE* ofp, int count)
        register int total = 0;
        while (count-- > 0)
        {
+/*@-boundsread@*/
                register int rc = writeInt(*(i++), ofp);
+/*@=boundsread@*/
                if (rc < 0)
                        break;
                total += rc;
@@ -572,7 +574,9 @@ int writeChars(const javachar* c, FILE* ofp, int count)
        register int total = 0;
        while (count-- > 0)
        {
+/*@-boundsread@*/
                register int rc = writeChar(*(c++), ofp);
+/*@=boundsread@*/
                if (rc < 0)
                        break;
                total += rc;
index 833e12c..9f751de 100644 (file)
@@ -72,6 +72,7 @@ int md5Reset(register md5Param* p)
        a += b;
 
 #ifndef ASM_MD5PROCESS
+/*@-boundsread@*/
 void md5Process(md5Param* p)
 {
        register uint32 a,b,c,d;
@@ -166,6 +167,7 @@ void md5Process(md5Param* p)
        p->h[2] += c;
        p->h[3] += d;
 }
+/*@=boundsread@*/
 #endif
 
 /*@-boundswrite@*/
index 1649cb4..d404ec7 100644 (file)
@@ -52,20 +52,25 @@ void mp32fill(register uint32 xsize, register uint32* xdata, register uint32 val
 #endif
 
 #ifndef ASM_MP32ODD
+/*@-boundsread@*/
 int mp32odd(register uint32 xsize, register const uint32* xdata)
 {
        return (xdata[xsize-1] & 0x1);
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32EVEN
+/*@-boundsread@*/
 int mp32even(register uint32 xsize, register const uint32* xdata)
 {
        return !(xdata[xsize-1] & 0x1);
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32Z
+/*@-boundsread@*/
 int mp32z(register uint32 xsize, register const uint32* xdata)
 {
        while (xsize--)
@@ -73,9 +78,11 @@ int mp32z(register uint32 xsize, register const uint32* xdata)
                        return 0;
        return 1;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32NZ
+/*@-boundsread@*/
 int mp32nz(register uint32 xsize, register const uint32* xdata)
 {
        while (xsize--)
@@ -83,9 +90,11 @@ int mp32nz(register uint32 xsize, register const uint32* xdata)
                        return 1;
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32EQ
+/*@-boundsread@*/
 int mp32eq(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -101,6 +110,7 @@ int mp32eq(register uint32 size, register const uint32* xdata, register const ui
 
        return 1;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32EQX
@@ -122,6 +132,7 @@ int mp32eqx(register uint32 xsize, register const uint32* xdata, register uint32
 #endif
 
 #ifndef ASM_MP32NE
+/*@-boundsread@*/
 int mp32ne(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -137,6 +148,7 @@ int mp32ne(register uint32 size, register const uint32* xdata, register const ui
 
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32NEX
@@ -158,6 +170,7 @@ int mp32nex(register uint32 xsize, register const uint32* xdata, register uint32
 #endif
 
 #ifndef ASM_MP32GT
+/*@-boundsread@*/
 int mp32gt(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -170,6 +183,7 @@ int mp32gt(register uint32 size, register const uint32* xdata, register const ui
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32GTX
@@ -191,6 +205,7 @@ int mp32gtx(register uint32 xsize, register const uint32* xdata, register uint32
 #endif
 
 #ifndef ASM_MP32LT
+/*@-boundsread@*/
 int mp32lt(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -203,6 +218,7 @@ int mp32lt(register uint32 size, register const uint32* xdata, register const ui
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32LTX
@@ -224,6 +240,7 @@ int mp32ltx(register uint32 xsize, register const uint32* xdata, register uint32
 #endif
 
 #ifndef ASM_MP32GE
+/*@-boundsread@*/
 int mp32ge(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -236,9 +253,11 @@ int mp32ge(register uint32 size, register const uint32* xdata, register const ui
        }
        return 1;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32GEX
+/*@-boundsread@*/
 int mp32gex(register uint32 xsize, register const uint32* xdata, register uint32 ysize, register const uint32* ydata)
 {
        if (xsize > ysize)
@@ -254,9 +273,11 @@ int mp32gex(register uint32 xsize, register const uint32* xdata, register uint32
        else
                return mp32ge(xsize, xdata, ydata);
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32LE
+/*@-boundsread@*/
 int mp32le(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
        while (size--)
@@ -269,9 +290,11 @@ int mp32le(register uint32 size, register const uint32* xdata, register const ui
        }
        return 1;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32LEX
+/*@-boundsread@*/
 int mp32lex(register uint32 xsize, register const uint32* xdata, register uint32 ysize, register const uint32* ydata)
 {
        if (xsize > ysize)
@@ -287,10 +310,12 @@ int mp32lex(register uint32 xsize, register const uint32* xdata, register uint32
        else
                return mp32le(xsize, xdata, ydata);
 }
+/*@=boundsread@*/
 #endif
 
 
 #ifndef ASM_MP32ISONE
+/*@-boundsread@*/
 int mp32isone(register uint32 xsize, register const uint32* xdata)
 {
        xdata += xsize;
@@ -303,9 +328,11 @@ int mp32isone(register uint32 xsize, register const uint32* xdata)
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32ISTWO
+/*@-boundsread@*/
 int mp32istwo(register uint32 xsize, register const uint32* xdata)
 {
        xdata += xsize;
@@ -318,9 +345,11 @@ int mp32istwo(register uint32 xsize, register const uint32* xdata)
        }
        return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32EQMONE
+/*@-boundsread@*/
 int mp32eqmone(register uint32 size, register const uint32* xdata, register const uint32* ydata)
 {
     xdata += size;
@@ -335,9 +364,11 @@ int mp32eqmone(register uint32 size, register const uint32* xdata, register cons
     }
     return 0;
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32LEONE
+/*@-boundsread@*/
 int mp32leone(register uint32 xsize, register const uint32* xdata)
 {
        xdata += xsize;
@@ -351,47 +382,60 @@ int mp32leone(register uint32 xsize, register const uint32* xdata)
                return 1;
        }
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32MSBSET
 int mp32msbset(/*@unused@*/ register uint32 xsize, register const uint32* xdata)
 {
+/*@-boundsread@*/
        return ((*xdata) & 0x80000000);
+/*@=boundsread@*/
 }
 #endif
 
 #ifndef ASM_MP32LSBSET
 int mp32lsbset(register uint32 xsize, register const uint32* xdata)
 {
+/*@-boundsread@*/
     return xdata[xsize-1] & 0x1;
+/*@=boundsread@*/
 }
 #endif
 
 #ifndef ASM_MP32SETMSB
 void mp32setmsb(/*@unused@*/ register uint32 xsize, register uint32* xdata)
 {
+/*@-boundsread@*/
        *xdata |= 0x80000000;
+/*@=boundsread@*/
 }
 #endif
 
 #ifndef ASM_MP32SETLSB
 void mp32setlsb(register uint32 xsize, register uint32* xdata)
 {
+/*@-boundsread@*/
        xdata[xsize-1] |= 0x00000001;
+/*@=boundsread@*/
 }
 #endif
 
 #ifndef ASM_MP32CLRMSB
 void mp32clrmsb(/*@unused@*/ register uint32 xsize, register uint32* xdata)
 {
+/*@-boundsread@*/
        *xdata &= 0x7fffffff;
+/*@=boundsread@*/
 }
 #endif
 
 #ifndef ASM_MP32CLRLSB
 void mp32clrlsb(register uint32 xsize, register uint32* xdata)
 {
+/*@-boundsread@*/
     xdata[xsize-1] &= 0xfffffffe;
+/*@=boundsread@*/
 }
 #endif
 
@@ -401,7 +445,9 @@ void mp32xor(register uint32 size, register uint32* xdata, register const uint32
        do
        {
                --size;
+/*@-boundsread@*/
                xdata[size] ^= ydata[size];
+/*@=boundsread@*/
        } while (size);
 }
 #endif
@@ -737,8 +783,10 @@ uint32 mp32size(register uint32 xsize, register const uint32* xdata)
 {
        while (xsize)
        {
+/*@-boundsread@*/
                if (*xdata)
                        return xsize;
+/*@=boundsread@*/
                xdata++;
                xsize--;
        }
@@ -784,8 +832,10 @@ void mp32divtwo(register uint32 xsize, register uint32* xdata)
 void mp32sdivtwo(register uint32 xsize, register uint32* xdata)
 {
        mp32divtwo(xsize, xdata);
+/*@-boundsread@*/
        if (*xdata & 0x40000000)
                *xdata |= 0x80000000;
+/*@=boundsread@*/
 }
 #endif
 
@@ -816,7 +866,9 @@ uint32 mp32mszcnt(register uint32 xsize, register const uint32* xdata)
 
        while (i < xsize)
        {
+/*@-boundsread@*/
                register uint32 temp = xdata[i++];
+/*@=boundsread@*/
                if (temp)
                {
                        while (!(temp & 0x80000000))
@@ -840,7 +892,9 @@ uint32 mp32lszcnt(register uint32 xsize, register const uint32* xdata)
 
        while (xsize--)
        {
+/*@-boundsread@*/
                register uint32 temp = xdata[xsize];
+/*@=boundsread@*/
                if (temp)
                {
                        while (!(temp & 0x1))
@@ -1238,6 +1292,7 @@ void mp32unpack(uint32 size, uint8* bytes, const uint32* bits)
 */
 
 #ifndef ASM_MP32PRINT
+/*@-boundsread@*/
 void mp32print(register FILE * fp, register uint32 xsize, register const uint32* xdata)
 {
        if (xdata == NULL)
@@ -1248,9 +1303,11 @@ void mp32print(register FILE * fp, register uint32 xsize, register const uint32*
                fprintf(fp, "%08x", *(xdata++));
        (void) fflush(fp);
 }
+/*@=boundsread@*/
 #endif
 
 #ifndef ASM_MP32PRINTLN
+/*@-boundsread@*/
 void mp32println(register FILE * fp, register uint32 xsize, register const uint32* xdata)
 {
        if (xdata == NULL)
@@ -1262,4 +1319,5 @@ void mp32println(register FILE * fp, register uint32 xsize, register const uint3
        fprintf(fp, "\n");
        (void) fflush(fp);
 }
+/*@=boundsread@*/
 #endif
index c9c6e6f..02807fa 100644 (file)
@@ -562,6 +562,7 @@ static byte mp32bslide_postsq[16] =
  * mp32bpowmod_w
  * needs workspace of 4*size+2 words
  */
+/*@-boundsread@*/
 void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 psize, const uint32* pdata, uint32* result, uint32* wksp)
 {
        /*
@@ -599,7 +600,9 @@ void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
                /*@=nullpass@*/
        }
 }
+/*@=boundsread@*/
 
+/*@-boundsread@*/
 void mp32bpowmodsld_w(const mp32barrett* b, const uint32* slide, uint32 psize, const uint32* pdata, uint32* result, uint32* wksp)
 {
        /*
@@ -698,11 +701,13 @@ void mp32bpowmodsld_w(const mp32barrett* b, const uint32* slide, uint32 psize, c
        }       
        /*@=charindex@*/
 }
+/*@=boundsread@*/
 
 /**
  * mp32btwopowmod_w
  *  needs workspace of (4*size+2) words
  */
+/*@-boundsread@*/
 void mp32btwopowmod_w(const mp32barrett* b, uint32 psize, const uint32* pdata, uint32* result, uint32* wksp)
 {
        /*
@@ -765,6 +770,7 @@ void mp32btwopowmod_w(const mp32barrett* b, uint32 psize, const uint32* pdata, u
                }
        }
 }
+/*@=boundsread@*/
 
 #ifdef DYING
 /**
@@ -930,6 +936,7 @@ static int _debug = 0;
 /**
  *  Computes the inverse (modulo b) of x, and returns 1 if x was invertible.
  */
+/*@-boundsread@*/
 int mp32binv_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32* result, uint32* wksp)
 {
        uint32  ysize = b->size+1;
@@ -1133,12 +1140,14 @@ fprintf(stderr, "      t3: "), mp32println(stderr, ysize, t3);
 
        return 1;
 }
+/*@=boundsread@*/
 
 #endif
 
 /**
  * needs workspace of (7*size+2) words
  */
+/*@-boundsread@*/
 int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* rc, int t, uint32* wksp)
 {
        /*
@@ -1188,6 +1197,7 @@ int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* rc, int t, uint3
 
        return 0;
 }
+/*@=boundsread@*/
 
 void mp32bnrnd(const mp32barrett* b, randomGeneratorContext* rc, mp32number* result)
 {
index 7148920..96322a8 100644 (file)
@@ -1052,6 +1052,7 @@ int mp32ptrials(uint32 bits)
 
 /**
  */
+/*@-boundsread@*/
 static void mp32prndbits(mp32barrett* p, uint8 msbclr, uint8 lsbset, randomGeneratorContext* rc)
        /*@modifies p @*/
 {
@@ -1075,11 +1076,13 @@ static void mp32prndbits(mp32barrett* p, uint8 msbclr, uint8 lsbset, randomGener
                p->modl[size] |= (((uint32)0xffffffff) >> (32 - lsbset));
        /*@=shiftnegative@*/
 }
+/*@=boundsread@*/
 
 /**
  * mp32psppdiv_w
  *  needs workspace of (3*size) words
  */
+/*@-boundsread@*/
 static int mp32psppdiv_w(const mp32barrett* p, /*@out@*/ uint32* wksp)
        /*@globals mp32spprod @*/
        /*@modifies wksp @*/
@@ -1101,6 +1104,7 @@ static int mp32psppdiv_w(const mp32barrett* p, /*@out@*/ uint32* wksp)
 
        return mp32isone(size, wksp);
 }
+/*@=boundsread@*/
 
 /**
  * mp32pmilrabtwo_w
index 774d56b..c5ef6a3 100644 (file)
@@ -53,6 +53,7 @@ const randomGenerator mtprng = { "Mersenne Twister", sizeof(mtprngParam), (rando
 
 /**
  */
+/*@-boundsread@*/
 static void mtprngReload(mtprngParam* mp)
        /*@modifies mp @*/
 {
@@ -71,6 +72,7 @@ static void mtprngReload(mtprngParam* mp)
     mp->left = N;
     mp->nextw = mp->state;
 }
+/*@=boundsread@*/
 
 int mtprngSetup(mtprngParam* mp)
 {
index fad42a8..7c2cc55 100644 (file)
@@ -75,6 +75,7 @@ int sha1Reset(register sha1Param *p)
        b = ROTR32(b, 2)
 
 #ifndef ASM_SHA1PROCESS
+/*@-boundsread@*/
 void sha1Process(register sha1Param *p)
 {
        register uint32 a, b, c, d, e;
@@ -194,6 +195,7 @@ void sha1Process(register sha1Param *p)
        p->h[3] += d;
        p->h[4] += e;
 }
+/*@=boundsread@*/
 #endif
 
 /*@-boundswrite@*/
index 330a4f3..14c0a11 100644 (file)
@@ -83,6 +83,7 @@ int sha256Reset(register sha256Param *p)
        d += temp
 
 #ifndef ASM_SHA256PROCESS
+/*@-boundsread@*/
 void sha256Process(register sha256Param *p)
 {
        register uint32 a, b, c, d, e, f, g, h, temp;
@@ -187,6 +188,7 @@ void sha256Process(register sha256Param *p)
        p->h[6] += g;
        p->h[7] += h;
 }
+/*@=boundsread@*/
 #endif
 
 /*@-boundswrite@*/
diff --git a/build.c b/build.c
index 04208d5..4a00cb5 100644 (file)
--- a/build.c
+++ b/build.c
@@ -85,9 +85,11 @@ static int isSpecFile(const char * specfile)
        case ':':
            checking = 0;
            /*@switchbreak@*/ break;
+/*@-boundsread@*/
        default:
            if (checking && !(isprint(*s) || isspace(*s))) return 0;
            /*@switchbreak@*/ break;
+/*@=boundsread@*/
        }
     }
     return 1;
index a9eced2..8b1d44a 100644 (file)
@@ -13,8 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds               # 281
-+boundswrite           # 132
++bounds
 
 # --- +partial artifacts
 -declundef
index 18d13b7..b98fd19 100644 (file)
@@ -184,11 +184,13 @@ 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_FTP:
@@ -214,7 +216,9 @@ fprintf(stderr, "*** addMacros\n");
        /*@-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));
@@ -271,12 +275,14 @@ int buildSpec(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(spec->BASpecs[x],
                                (what & ~RPMBUILD_RMSOURCE) |
                                (x ? 0 : (what & RPMBUILD_PACKAGESOURCE)),
                                test))) {
                goto exit;
            }
+/*@=boundsread@*/
        }
     } else {
        if ((what & RPMBUILD_PREP) &&
index e1d8009..5ba3669 100644 (file)
@@ -711,7 +711,9 @@ 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;
index bcbf2e8..7876ccb 100644 (file)
@@ -276,11 +276,13 @@ 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@*/
 }
 
 /**
index aecb943..3743cfc 100644 (file)
@@ -185,8 +185,10 @@ int_32 *const getBuildTime(void)
 {
     static int_32 buildTime[1];
 
+/*@-boundsread@*/
     if (buildTime[0] == 0)
        buildTime[0] = (int_32) time(NULL);
+/*@=boundsread@*/
     return buildTime;
 }
 
index 21cd0a9..314edc7 100644 (file)
@@ -65,6 +65,7 @@ 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");
@@ -74,6 +75,7 @@ static int cpio_doio(FD_t fdo, /*@unused@*/ Header h, CSA_t csa,
        /*@=nullpass@*/
        fmode = _free(fmode);
     }
+/*@=boundsread@*/
     if (cfd == NULL)
        return 1;
 
index 23dccfd..259cb95 100644 (file)
@@ -185,11 +185,13 @@ static inline char * findLastChar(char * s)
 {
     char *res = s;
 
+/*@-boundsread@*/
     while (*s != '\0') {
        if (! xisspace(*s))
            res = s;
        s++;
     }
+/*@=boundsread@*/
 
     /*@-temptrans -retalias@*/
     return res;
@@ -209,11 +211,13 @@ 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);
 }
 
@@ -269,6 +273,7 @@ static int checkForRequired(Header h, const char * NVR)
     int res = 0;
     rpmTag * p;
 
+/*@-boundsread@*/
     for (p = requiredTags; *p != 0; p++) {
        if (!headerIsEntry(h, *p)) {
            rpmError(RPMERR_BADSPEC,
@@ -277,6 +282,7 @@ static int checkForRequired(Header h, const char * NVR)
            res = 1;
        }
     }
+/*@=boundsread@*/
 
     return res;
 }
@@ -333,10 +339,12 @@ static void fillOutMainPackage(Header h)
 
     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@*/
        }
     }
 }
index 489093d..a6d9f41 100644 (file)
@@ -418,12 +418,14 @@ static int doSetupMacro(Spec spec, char *line)
 
        for (fm = fixmacs; *fm; fm++) {
            const char *fix;
+/*@-boundsread@*/
            /*@-nullpass@*/
            fix = rpmExpand(*fm, " .", NULL);
            /*@=nullpass@*/
            if (fix && *fix != '%')
                appendLineStringBuf(spec->prep, fix);
            fix = _free(fix);
+/*@=boundsread@*/
        }
     }
     
@@ -584,6 +586,7 @@ int parsePrep(Spec spec)
     /*@-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)) {
@@ -591,6 +594,7 @@ int parsePrep(Spec spec)
        } else {
            appendLineStringBuf(spec->prep, *lines);
        }
+/*@=boundsread@*/
        if (res && !spec->force) {
            freeSplitString(saveLines);
            sb = freeStringBuf(sb);
index ab7c42d..0290feb 100644 (file)
@@ -88,6 +88,7 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, int tag,
        break;
     }
 
+/*@-boundsread@*/
     for (r = field; *r != '\0'; r = re) {
        SKIPWHITE(r);
        if (*r == '\0')
@@ -190,6 +191,7 @@ int parseRCPOT(Spec spec, Package pkg, const char *field, int tag,
        version = _free(version);
 
     }
+/*@=boundsread@*/
 
     return 0;
 }
index 9dc84d0..c3537fd 100644 (file)
@@ -55,14 +55,18 @@ 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;
     }
@@ -79,6 +83,7 @@ static int matchTok(const char *token, const char *line)
     size_t toklen = strlen(token);
     int rc = 0;
 
+/*@-boundsread@*/
     while ( *(b = be) != '\0' ) {
        SKIPSPACE(b);
        be = b;
@@ -90,6 +95,7 @@ static int matchTok(const char *token, const char *line)
        rc = 1;
        break;
     }
+/*@=boundsread@*/
 
     return rc;
 }
index cebdadc..9171462 100644 (file)
@@ -77,6 +77,7 @@ int addReqProv(/*@unused@*/ Spec spec, Header h,
        if (indextag)
            xx = hge(h, indextag, NULL, (void **) &indexes, NULL);
 
+/*@-boundsread@*/
        while (len > 0) {
            len--;
            if (strcmp(names[len], depName))
@@ -97,6 +98,7 @@ int addReqProv(/*@unused@*/ Spec spec, Header h,
 
            break;
        }
+/*@=boundsread@*/
        names = hfd(names, dnt);
        versions = hfd(versions, dvt);
        if (duplicate)
index d0366af..f207c38 100644 (file)
@@ -208,6 +208,7 @@ 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,6 +252,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)
index 5f94e31..b591159 100644 (file)
@@ -13,6 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
++bounds
 +slovak-fcns
 -redecl
 
index f5e2733..8585b94 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup payload
  * \file lib/cpio.c
  *  Handle cpio payloads within rpm packages.
@@ -55,7 +54,9 @@ static int strntoul(const char *str, /*@out@*/char **endptr, int base, int num)
        if ( (end - phys) != sizeof(phys) ) return CPIOERR_BAD_HEADER;
 #define SET_NUM_FIELD(phys, val, space) \
        sprintf(space, "%8.8lx", (unsigned long) (val)); \
-       memcpy(phys, space, 8);
+       /*@-boundsread@*/ \
+       memcpy(phys, space, 8) \
+       /*@=boundsread@*/
 
 int cpioTrailerWrite(FSM_t fsm)
 {
@@ -249,4 +250,3 @@ const char *const cpioStrerror(int rc)
     /*@=branchstate@*/
     return msg;
 }
-/*@=boundsread@*/
index 51fdc41..fc5ac40 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts
  * \file lib/depends.c
  */
@@ -65,7 +64,8 @@ int rpmFLAGS = RPMSENSE_EQUAL;
  * @param b            2nd instance address
  * @return             result of comparison
  */
-static int intcmp(const void * a, const void * b)      /*@*/
+static int intcmp(const void * a, const void * b)
+       /*@requires maxRead(a) == 0 /\ maxRead(b) == 0 @*/
 {
     const int * aptr = a;
     const int * bptr = b;
@@ -253,6 +253,7 @@ int rpmtsAddInstallElement(rpmts ts, Header h,
            goto exit;
     }
 
+/*@-boundsread@*/
     {  rpmdbMatchIterator mi;
        Header h2;
 
@@ -276,6 +277,7 @@ int rpmtsAddInstallElement(rpmts ts, Header h,
        }
        mi = rpmdbFreeIterator(mi);
     }
+/*@=boundsread@*/
 
     obsoletes = rpmdsLink(rpmteDS(p, RPMTAG_OBSOLETENAME), "Obsoletes");
     obsoletes = rpmdsInit(obsoletes);
@@ -319,21 +321,6 @@ exit:
     return ec;
 }
 
-#ifdef DYING
-void rpmtsAvailablePackage(rpmts ts, Header h, fnpyKey key)
-{
-    int scareMem = 0;
-    rpmds provides = rpmdsNew(h, RPMTAG_PROVIDENAME, scareMem);
-    rpmfi fi = rpmfiNew(ts, NULL, h, RPMTAG_BASENAMES, scareMem);
-
-    /* XXX FIXME: return code RPMAL_NOMATCH is error */
-    (void) rpmalAdd(&ts->availablePackages, RPMAL_NOMATCH, key,
-               provides, fi);
-    fi = rpmfiFree(fi, 1);
-    provides = rpmdsFree(provides);
-}
-#endif
-
 int rpmtsAddEraseElement(rpmts ts, Header h, int dboffset)
 {
     return removePackage(ts, h, dboffset, RPMAL_NOMATCH);
@@ -427,10 +414,12 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
        /*@-observertrans -mayaliasunique@*/
        while ((start = strstr(rcProvidesString, Name))) {
        /*@=observertrans =mayaliasunique@*/
+/*@-boundsread@*/
            if (xisspace(start[i]) || start[i] == '\0' || start[i] == ',') {
                rpmdsNotify(dep, _("(rpmrc provides)"), rc);
                goto exit;
            }
+/*@=boundsread@*/
            rcProvidesString = start + 1;
        }
     }
@@ -456,6 +445,7 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
 
     /* XXX only the installer does not have the database open here. */
     if (rpmtsGetRdb(ts) != NULL) {
+/*@-boundsread@*/
        if (Name[0] == '/') {
            /* depFlags better be 0! */
 
@@ -471,6 +461,7 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
            }
            mi = rpmdbFreeIterator(mi);
        }
+/*@=boundsread@*/
 
        mi = rpmtsInitIterator(ts, RPMTAG_PROVIDENAME, Name, 0);
        (void) rpmdbPruneIterator(mi,
@@ -503,8 +494,10 @@ static int unsatisfiedDepend(rpmts ts, rpmds dep)
     /*
      * Search for an unsatisfied dependency.
      */
+/*@-boundsread@*/
     if (!(rpmtsFlags(ts) & RPMTRANS_FLAG_NOSUGGEST) && ts->solve != NULL)
        xx = (*ts->solve) (ts, dep);
+/*@=boundsread@*/
 
 unsatisfied:
     rc = 1;    /* dependency is unsatisfied */
@@ -800,6 +793,7 @@ static void freeBadDeps(void)
  * @param q    predecessor element (i.e. with Provides: )
  * @return     1 if dependency is to be ignored.
  */
+/*@-boundsread@*/
 static int ignoreDep(const rpmte p, const rpmte q)
        /*@globals badDeps, badDepsInitialized @*/
        /*@modifies badDeps, badDepsInitialized @*/
@@ -852,6 +846,7 @@ static int ignoreDep(const rpmte p, const rpmte q)
     return 0;
     /*@=compdef@*/
 }
+/*@=boundsread@*/
 
 /**
  * Recursively mark all nodes with their predecessors.
@@ -1051,8 +1046,10 @@ fprintf(stderr, "addRelation: q %p(%s) from %p[%d:%d]\n", q, rpmteN(q), ts->orde
 
     /* Avoid redundant relations. */
     /* XXX TODO: add control bit. */
+/*@-boundsread@*/
     if (selected[i] != 0)
        return 0;
+/*@=boundsread@*/
 /*@-boundswrite@*/
     selected[i] = 1;
 /*@=boundswrite@*/
@@ -1816,4 +1813,3 @@ exit:
     /*@=branchstate@*/
     return rc;
 }
-/*@=boundsread@*/
index 4259f71..f4be621 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup header
  * \file lib/formats.c
  */
@@ -21,8 +20,9 @@
  * @return             formatted string
  */
 static /*@only@*/ char * triggertypeFormat(int_32 type, const void * data, 
-       /*@unused@*/ char * formatPrefix, /*@unused@*/ int padding,
-       /*@unused@*/ int element)       /*@*/
+               /*@unused@*/ char * formatPrefix, /*@unused@*/ int padding,
+               /*@unused@*/ int element)
+       /*@requires maxRead(data) >= 0 @*/
 {
     const int_32 * item = data;
     char * val;
@@ -45,26 +45,27 @@ static /*@only@*/ char * triggertypeFormat(int_32 type, const void * data,
  * @param element      (unused)
  * @return             formatted string
  */
-static /*@only@*/ char * permsFormat(int_32 type, const void * data, char * formatPrefix,
-       int padding, /*@unused@*/ int element)
-               /*@modifies formatPrefix @*/
+static /*@only@*/ char * permsFormat(int_32 type, const void * data,
+               char * formatPrefix, int padding, /*@unused@*/ int element)
+       /*@modifies formatPrefix @*/
+       /*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char * buf;
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
        val = xstrdup(_("(not a number)"));
     } else {
        val = xmalloc(15 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "s");
+/*@=boundswrite@*/
        buf = rpmPermsString(*((int_32 *) data));
        /*@-formatconst@*/
        sprintf(val, formatPrefix, buf);
        /*@=formatconst@*/
        buf = _free(buf);
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -79,18 +80,19 @@ static /*@only@*/ char * permsFormat(int_32 type, const void * data, char * form
  * @return             formatted string
  */
 static /*@only@*/ char * fflagsFormat(int_32 type, const void * data, 
-       char * formatPrefix, int padding, /*@unused@*/ int element)
-               /*@modifies formatPrefix @*/
+               char * formatPrefix, int padding, /*@unused@*/ int element)
+       /*@modifies formatPrefix @*/
+       /*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char buf[15];
     int anint = *((int_32 *) data);
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
        val = xstrdup(_("(not a number)"));
     } else {
        buf[0] = '\0';
+/*@-boundswrite@*/
        if (anint & RPMFILE_DOC)
            strcat(buf, "d");
        if (anint & RPMFILE_CONFIG)
@@ -107,14 +109,16 @@ static /*@only@*/ char * fflagsFormat(int_32 type, const void * data,
            strcat(buf, "l");
        if (anint & RPMFILE_README)
            strcat(buf, "r");
+/*@=boundswrite@*/
 
        val = xmalloc(5 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "s");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(val, formatPrefix, buf);
        /*@=formatconst@*/
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -223,7 +227,6 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
 {
     char * val;
 
-/*@-boundswrite@*/
     if (type != RPM_BIN_TYPE) {
        val = xstrdup(_("(not a blob)"));
     } else {
@@ -232,6 +235,7 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
        int lc;
        int nt = ((element + 2) / 3) * 4;
 
+/*@-boundswrite@*/
        /*@-globs@*/
        /* Add additional bytes necessary for eol string(s). */
        if (b64encode_chars_per_line > 0 && b64encode_eolstr != NULL) {
@@ -249,8 +253,8 @@ static /*@only@*/ char * base64Format(int_32 type, const void * data,
            t = stpcpy(t, enc);
            enc = _free(enc);
        }
-    }
 /*@=boundswrite@*/
+    }
 
     return val;
 }
@@ -289,33 +293,36 @@ static /*@only@*/ char * pgppktFormat(int_32 type, const void * data,
  * @return             formatted string
  */
 static /*@only@*/ char * depflagsFormat(int_32 type, const void * data, 
-       char * formatPrefix, int padding, /*@unused@*/ int element)
-               /*@modifies formatPrefix @*/
+               char * formatPrefix, int padding, /*@unused@*/ int element)
+       /*@modifies formatPrefix @*/
+       /*@requires maxRead(data) >= 0 @*/
 {
     char * val;
     char buf[10];
     int anint = *((int_32 *) data);
 
-/*@-boundswrite@*/
     if (type != RPM_INT32_TYPE) {
        val = xstrdup(_("(not a number)"));
     } else {
        buf[0] = '\0';
 
+/*@-boundswrite@*/
        if (anint & RPMSENSE_LESS) 
            strcat(buf, "<");
        if (anint & RPMSENSE_GREATER)
            strcat(buf, ">");
        if (anint & RPMSENSE_EQUAL)
            strcat(buf, "=");
+/*@=boundswrite@*/
 
        val = xmalloc(5 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "s");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(val, formatPrefix, buf);
        /*@=formatconst@*/
     }
-/*@=boundswrite@*/
 
     return val;
 }
@@ -335,19 +342,21 @@ static int fsnamesTag( /*@unused@*/ Header h, /*@out@*/ int_32 * type,
        /*@globals fileSystem, internalState @*/
        /*@modifies *type, *data, *count, *freeData,
                fileSystem, internalState @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     const char ** list;
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemList(&list, count)) {
        return 1;
     }
+/*@=boundswrite@*/
 
-/*@-boundswrite@*/
     *type = RPM_STRING_ARRAY_TYPE;
     *((const char ***) data) = list;
 
     *freeData = 0;
-/*@=boundswrite@*/
 
     return 0; 
 }
@@ -362,28 +371,30 @@ static int fsnamesTag( /*@unused@*/ Header h, /*@out@*/ int_32 * type,
  * @return             0 on success
  */
 static int instprefixTag(Header h, /*@null@*/ /*@out@*/ rpmTagType * type,
-       /*@null@*/ /*@out@*/ const void ** data,
-       /*@null@*/ /*@out@*/ int_32 * count,
-       /*@null@*/ /*@out@*/ int * freeData)
-               /*@modifies *type, *data, *freeData @*/
+               /*@null@*/ /*@out@*/ const void ** data,
+               /*@null@*/ /*@out@*/ int_32 * count,
+               /*@null@*/ /*@out@*/ int * freeData)
+       /*@modifies *type, *data, *freeData @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
     rpmTagType ipt;
     char ** array;
 
-/*@-boundswrite@*/
     if (hge(h, RPMTAG_INSTALLPREFIX, type, (void **)data, count)) {
        if (freeData) *freeData = 0;
        return 0;
     } else if (hge(h, RPMTAG_INSTPREFIXES, &ipt, (void **) &array, count)) {
+/*@-boundsread@*/
        if (data) *data = xstrdup(array[0]);
+/*@=boundsread@*/
        if (freeData) *freeData = 1;
        if (type) *type = RPM_STRING_TYPE;
        array = hfd(array, ipt);
        return 0;
     }
-/*@=boundswrite@*/
 
     return 1;
 }
@@ -404,6 +415,8 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
                fileSystem, internalState @*/
        /*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext,
                fileSystem, internalState @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     const char ** filenames;
@@ -419,11 +432,12 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
        rpmBuildFileList(h, &filenames, &numFiles);
     }
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemList(NULL, count)) {
        return 1;
     }
+/*@=boundswrite@*/
 
-/*@-boundswrite@*/
     *type = RPM_INT32_TYPE;
     *freeData = 1;
 
@@ -434,11 +448,12 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
        return 0;
     }
 
+/*@-boundswrite@*/
     if (rpmGetFilesystemUsage(filenames, filesizes, numFiles, &usages, 0))     
        return 1;
+/*@=boundswrite@*/
 
     *data = usages;
-/*@=boundswrite@*/
 
     filenames = _free(filenames);
 
@@ -454,11 +469,13 @@ static int fssizesTag(Header h, /*@out@*/ rpmTagType * type,
  * @retval freeData    address of data-was-malloc'ed indicator
  * @return             0 on success
  */
-/*@-bounds@*/
+/*@-bounds@*/  /* LCL: segfault */
 static int triggercondsTag(Header h, /*@out@*/ rpmTagType * type,
-       /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-       /*@out@*/ int * freeData)
-               /*@modifies *type, *data, *count, *freeData @*/
+               /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+               /*@out@*/ int * freeData)
+       /*@modifies *type, *data, *count, *freeData @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -529,11 +546,12 @@ static int triggercondsTag(Header h, /*@out@*/ rpmTagType * type,
  * @retval freeData    address of data-was-malloc'ed indicator
  * @return             0 on success
  */
-/*@-bounds@*/
 static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
-       /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-       /*@out@*/ int * freeData)
-               /*@modifies *type, *data, *count, *freeData @*/
+               /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+               /*@out@*/ int * freeData)
+       /*@modifies *type, *data, *count, *freeData @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     HFD_t hfd = headerFreeData;
@@ -574,7 +592,6 @@ static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
 
     return 0;
 }
-/*@=bounds@*/
 
 /**
  * Retrieve file paths.
@@ -586,18 +603,18 @@ static int triggertypeTag(Header h, /*@out@*/ rpmTagType * type,
  * @return             0 on success
  */
 static int filenamesTag(Header h, /*@out@*/ rpmTagType * type,
-       /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
-       /*@out@*/ int * freeData)
-               /*@modifies *type, *data, *count, *freeData @*/
+               /*@out@*/ const void ** data, /*@out@*/ int_32 * count,
+               /*@out@*/ int * freeData)
+       /*@modifies *type, *data, *count, *freeData @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     *type = RPM_STRING_ARRAY_TYPE;
 
     rpmBuildFileList(h, (const char ***) data, count);
-/*@-boundswrite@*/
     *freeData = 1;
 
     *freeData = 0;     /* XXX WTFO? */
-/*@=boundswrite@*/
 
     return 0; 
 }
@@ -630,17 +647,17 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
                /*@out@*/ int * freeData)
        /*@globals rpmGlobalMacroContext @*/
        /*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     HGE_t hge = (HGE_t)headerGetEntryMinMemory;
     char * dstring = rpmExpand(_macro_i18ndomains, NULL);
     int rc;
 
-/*@-boundswrite@*/
     *type = RPM_STRING_TYPE;
     *data = NULL;
     *count = 0;
     *freeData = 0;
-/*@=boundswrite@*/
 
     if (dstring && *dstring) {
        char *domain, *de;
@@ -679,14 +696,12 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
            unsetenv(language);
 /*@i@*/        ++_nl_msg_cat_cntr;
 
-/*@-boundswrite@*/
        if (domain && msgid) {
            *data = /*@-unrecog@*/ dgettext(domain, msgid) /*@=unrecog@*/;
            *data = xstrdup(*data);     /* XXX xstrdup has side effects. */
            *count = 1;
            *freeData = 1;
        }
-/*@=boundswrite@*/
        dstring = _free(dstring);
        if (*data)
            return 0;
@@ -696,7 +711,6 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
 
     rc = hge(h, tag, type, (void **)data, count);
 
-/*@-boundswrite@*/
     if (rc && (*data) != NULL) {
        *data = xstrdup(*data);
        *freeData = 1;
@@ -706,7 +720,6 @@ static int i18nTag(Header h, int_32 tag, /*@out@*/ rpmTagType * type,
     *freeData = 0;
     *data = NULL;
     *count = 0;
-/*@=boundswrite@*/
     return 1;
 }
 
@@ -724,6 +737,8 @@ static int summaryTag(Header h, /*@out@*/ rpmTagType * type,
                /*@out@*/ int * freeData)
        /*@globals rpmGlobalMacroContext @*/
        /*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_SUMMARY, type, data, count, freeData);
 }
@@ -742,6 +757,8 @@ static int descriptionTag(Header h, /*@out@*/ rpmTagType * type,
                /*@out@*/ int * freeData)
        /*@globals rpmGlobalMacroContext @*/
        /*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_DESCRIPTION, type, data, count, freeData);
 }
@@ -760,6 +777,8 @@ static int groupTag(Header h, /*@out@*/ rpmTagType * type,
                /*@out@*/ int * freeData)
        /*@globals rpmGlobalMacroContext @*/
        /*@modifies *type, *data, *count, *freeData, rpmGlobalMacroContext @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/
 {
     return i18nTag(h, RPMTAG_GROUP, type, data, count, freeData);
 }
@@ -788,4 +807,3 @@ const struct headerSprintfExtension_s rpmHeaderFormats[] = {
     { HEADER_EXT_MORE, NULL, { (void *) headerDefaultFormats } }
 } ;
 /*@=type@*/
-/*@=boundsread@*/
index 0a5fcbb..9976f14 100644 (file)
--- a/lib/fs.c
+++ b/lib/fs.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /*@-mods@*/
 /**
  * \file lib/fs.c
@@ -174,7 +173,9 @@ static int getFilesystemList(void)
            /*@-modunconnomods -moduncon @*/
            our_mntent * itemptr = getmntent(mtab);
            if (!itemptr) break;
+/*@-boundsread@*/
            item = *itemptr;    /* structure assignment */
+/*@=boundsread@*/
            mntdir = item.our_mntdir;
 #if defined(MNTOPT_RO)
            /*@-compdef@*/
@@ -270,10 +271,12 @@ int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes, int numFiles
     sourceDir = rpmGetPath("%{_sourcedir}", NULL);
 
     maxLen = strlen(sourceDir);
+/*@-boundsread@*/
     for (i = 0; i < numFiles; i++) {
        len = strlen(fileList[i]);
        if (maxLen < len) maxLen = len;
     }
+/*@=boundsread@*/
     
 /*@-boundswrite@*/
     buf = alloca(maxLen + 1);
@@ -355,4 +358,3 @@ int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes, int numFiles
 }
 /*@=usereleased =onlytrans@*/
 /*@=mods@*/
-/*@=boundsread@*/
index 9b41922..f4fe24b 100644 (file)
--- a/lib/fsm.c
+++ b/lib/fsm.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup payload
  * \file lib/fsm.c
  * File state machine to handle a payload from a package.
@@ -161,6 +160,7 @@ static int mapNextIterator(/*@null@*/ void * a)
 
 /** \ingroup payload
  */
+/*@-boundsread@*/
 static int cpioStrCmp(const void * a, const void * b)
        /*@*/
 {
@@ -177,6 +177,7 @@ static int cpioStrCmp(const void * a, const void * b)
 
     return strcmp(afn, bfn);
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Locate archive path in file info.
@@ -184,6 +185,7 @@ static int cpioStrCmp(const void * a, const void * b)
  * @param fsmPath      archive path
  * @return             index into file info, -1 if archive path was not found
  */
+/*@-boundsread@*/
 static int mapFind(/*@null@*/ FSMI_t iter, const char * fsmPath)
        /*@modifies iter @*/
 {
@@ -207,6 +209,7 @@ static int mapFind(/*@null@*/ FSMI_t iter, const char * fsmPath)
     }
     return ix;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Directory name iterator.
@@ -256,6 +259,7 @@ static inline int dnlIndex(const DNLI_t dnli)
  * @param reverse      traverse directory names in reverse order?
  * @return             directory name iterator
  */
+/*@-boundsread@*/
 /*@-usereleased@*/
 static /*@only@*/ void * dnlInitIterator(/*@special@*/ const FSM_t fsm,
                int reverse)
@@ -338,12 +342,14 @@ static /*@only@*/ void * dnlInitIterator(/*@special@*/ const FSM_t fsm,
     return dnli;
 }
 /*@=usereleased@*/
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Return next directory name (from file info).
  * @param dnli         directory name iterator
  * @return             next directory name
  */
+/*@-boundsread@*/
 static /*@observer@*/ const char * dnlNextIterator(/*@null@*/ DNLI_t dnli)
        /*@modifies dnli @*/
 {
@@ -366,12 +372,14 @@ static /*@observer@*/ const char * dnlNextIterator(/*@null@*/ DNLI_t dnli)
     }
     return dn;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Save hard link in chain.
  * @param fsm          file state machine data
  * @return             Is chain only partially filled?
  */
+/*@-boundsread@*/
 static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
        /*@uses fsm->links, fsm->ix, fsm->sb, fsm->goal, fsm->nsuffix @*/
        /*@defines fsm->li @*/
@@ -460,6 +468,7 @@ static int saveHardLink(/*@special@*/ /*@partial@*/ FSM_t fsm)
     rc = fsmStage(fsm, FSM_MAP);
     return rc;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Destroy set of hard links.
@@ -588,6 +597,7 @@ int fsmMapPath(FSM_t fsm)
     i = fsm->ix;
     if (fi && i >= 0 && i < fi->fc) {
 
+/*@-boundsread@*/
        fsm->astriplen = fi->astriplen;
        fsm->action = (fi->actions ? fi->actions[i] : fi->action);
        fsm->fflags = (fi->fflags ? fi->fflags[i] : fi->flags);
@@ -596,6 +606,7 @@ int fsmMapPath(FSM_t fsm)
        /* src rpms have simple base name in payload. */
        fsm->dirName = fi->dnl[fi->dil[i]];
        fsm->baseName = fi->bnl[i];
+/*@=boundsread@*/
 
 /*@-boundswrite@*/
        switch (fsm->action) {
@@ -985,6 +996,7 @@ static int writeLinkedFile(/*@special@*/ FSM_t fsm)
  * @param fsm          file state machine data
  * @return             0 on success
  */
+/*@-boundsread@*/
 static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
        /*@uses fsm->path, fsm->opath, fsm->nsuffix, fsm->ix, fsm->li @*/
        /*@globals fileSystem@*/
@@ -1042,6 +1054,7 @@ static int fsmMakeLinks(/*@special@*/ FSM_t fsm)
     fsm->opath = opath;
     return ec;
 }
+/*@=boundsread@*/
 
 /** \ingroup payload
  * Commit hard linked file set atomically.
@@ -1296,6 +1309,7 @@ static int fsmStat(FSM_t fsm)
        ((_x)[sizeof("/dev/log")-1] == '\0' || \
         (_x)[sizeof("/dev/log")-1] == ';'))
 
+/*@-boundsread@*/
 /*@-compmempass@*/
 int fsmStage(FSM_t fsm, fileStage stage)
 {
@@ -2253,6 +2267,7 @@ if (!(fsm->mapFlags & CPIO_ALL_HARDLINKS)) break;
     return rc;
 }
 /*@=compmempass@*/
+/*@=boundsread@*/
 
 /*@obserever@*/ const char *const fileActionString(fileAction a)
 {
@@ -2338,4 +2353,3 @@ if (!(fsm->mapFlags & CPIO_ALL_HARDLINKS)) break;
     }
     /*@noteached@*/
 }
-/*@=boundsread@*/
index b9231c6..21f196d 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /**
  * \file lib/misc.c
  */
@@ -462,4 +461,3 @@ int rpmHeaderGetEntry(Header h, int_32 tag, int_32 *type,
     }
     /*@notreached@*/
 }
-/*@=boundsread@*/
index 96bee89..a2d3e11 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup header
  * \file lib/package.c
  */
@@ -169,8 +168,10 @@ static int rpmtsStashKeyid(rpmts ts)
 
     if (keyids != NULL)
     for (i = 0; i < nkeyids; i++) {
+/*@-boundsread@*/
        if (keyid == keyids[i])
            return 1;
+/*@=boundsread@*/
     }
 
     keyids = xrealloc(keyids, (nkeyids + 1) * sizeof(*keyids));
@@ -216,11 +217,13 @@ int rpmReadPackageFile(rpmts ts, FD_t fd,
        goto exit;
     }
 
+/*@-boundsread@*/
     if (l->magic[0] != RPMLEAD_MAGIC0 || l->magic[1] != RPMLEAD_MAGIC1
      || l->magic[2] != RPMLEAD_MAGIC2 || l->magic[3] != RPMLEAD_MAGIC3) {
        rc = RPMRC_NOTFOUND;
        goto exit;
     }
+/*@=boundsread@*/
 
     switch (l->major) {
     case 1:
@@ -469,4 +472,3 @@ exit:
     sig = rpmFreeSignature(sig);
     return rc;
 }
-/*@=boundsread@*/
index 5e2f739..221409d 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmcli
  * \file lib/poptALL.c
  *  Popt tables for all rpm modes.
@@ -224,10 +223,10 @@ rpmcliInit(int argc, char *const argv[], struct poptOption * optionsTable)
 /*@=globs =mods@*/
 
 #if !defined(__LCLINT__)
-    (void)setlocale(LC_ALL, "" );
+    (void) setlocale(LC_ALL, "" );
 
-    (void)bindtextdomain(PACKAGE, LOCALEDIR);
-    (void)textdomain(PACKAGE);
+    (void) bindtextdomain(PACKAGE, LOCALEDIR);
+    (void) textdomain(PACKAGE);
 #endif
 
     rpmSetVerbosity(RPMMESS_NORMAL);
@@ -280,5 +279,3 @@ rpmcliInit(int argc, char *const argv[], struct poptOption * optionsTable)
     return optCon;
 }
 /*@=globstate@*/
-
-/*@=boundsread@*/
index 13736de..ecf82ad 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmcli
  * \file lib/poptI.c
  *  Popt tables for install modes.
@@ -244,4 +243,3 @@ struct poptOption rpmInstallPoptTable[] = {
    POPT_TABLEEND
 };
 /*@=bitwisesigned =compmempass @*/
-/*@=boundsread@*/
index e0cb20d..3b5e25f 100644 (file)
@@ -1,4 +1,3 @@
-/*@-bounds@*/
 /** \ingroup rpmcli
  * \file lib/poptQV.c
  *  Popt tables for query/verify modes.
@@ -161,7 +160,9 @@ static void queryArgCallback(/*@unused@*/poptContext con,
            if (qf) {
                int len = strlen(qf) + strlen(arg) + 1;
                qf = xrealloc(qf, len);
+/*@-boundswrite@*/
                strcat(qf, arg);
+/*@=boundswrite@*/
            } else {
                qf = xmalloc(strlen(arg) + 1);
                strcpy(qf, arg);
@@ -313,4 +314,3 @@ struct poptOption rpmSignPoptTable[] = {
 
    POPT_TABLEEND
 };
-/*@=bounds@*/
index cfc46d7..e90beac 100644 (file)
--- a/lib/psm.c
+++ b/lib/psm.c
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts payload
  * \file lib/psm.c
  * Package state machine to handle a package from a transaction set.
@@ -68,10 +67,12 @@ int rpmVersionCompare(Header first, Header second)
     else if (!epochOne && epochTwo)
        return -1;
     else if (epochOne && epochTwo) {
+/*@-boundsread@*/
        if (*epochOne < *epochTwo)
            return -1;
        else if (*epochOne > *epochTwo)
            return 1;
+/*@=boundsread@*/
     }
 
     rc = headerGetEntry(first, RPMTAG_VERSION, NULL, (void **) &one, NULL);
@@ -139,7 +140,9 @@ static int rpmInstallLoadMacros(rpmfi fi, Header h)
            continue;
        switch (type) {
        case RPM_INT32_TYPE:
+/*@-boundsread@*/
            sprintf(numbuf, "%d", *body.i32p);
+/*@=boundsread@*/
            addMacro(NULL, tagm->macroname, NULL, numbuf, -1);
            /*@switchbreak@*/ break;
        case RPM_STRING_TYPE:
@@ -1932,4 +1935,3 @@ fprintf(stderr, "*** PSM_RDB_LOAD: header #%u not found\n", fi->record);
     /*@=nullstate@*/
 }
 /*@=nullpass@*/
-/*@=boundsread@*/
index 5b13468..c3b685f 100644 (file)
@@ -1011,10 +1011,14 @@ void freeFilesystems(void)
  * @retval num                 address of number of file systems (or NULL)
  * @return                     0 on success, 1 on error
  */
+/*@-incondefs@*/
 int rpmGetFilesystemList( /*@null@*/ /*@out@*/ const char *** listptr,
                /*@null@*/ /*@out@*/ int * num)
        /*@globals fileSystem, internalState @*/
-       /*@modifies *listptr, *num, fileSystem, internalState @*/;
+       /*@modifies *listptr, *num, fileSystem, internalState @*/
+       /*@requires maxSet(listptr) >= 0 /\ maxSet(num) >= 0 @*/
+       /*@ensures maxRead(num) == 0 @*/;
+/*@=incondefs@*/
 
 /**
  * Determine per-file system usage for a list of files.
@@ -1025,13 +1029,18 @@ int rpmGetFilesystemList( /*@null@*/ /*@out@*/ const char *** listptr,
  * @param flags                        (unused)
  * @return                     0 on success, 1 on error
  */
+/*@-incondefs@*/
 int rpmGetFilesystemUsage(const char ** fileList, int_32 * fssizes,
                int numFiles, /*@null@*/ /*@out@*/ uint_32 ** usagesPtr,
                int flags)
        /*@globals rpmGlobalMacroContext,
                fileSystem, internalState @*/
        /*@modifies *usagesPtr, rpmGlobalMacroContext,
-               fileSystem, internalState @*/;
+               fileSystem, internalState @*/
+       /*@requires maxSet(fileList) >= 0 /\ maxSet(fssizes) == 0
+               /\ maxSet(usagesPtr) >= 0 @*/
+       /*@ensures maxRead(usagesPtr) == 0 @*/;
+/*@=incondefs@*/
 
 /* ==================================================================== */
 /** \name RPMEIU */
index 3e17e0b..6ae79de 100644 (file)
@@ -1,4 +1,3 @@
-/*@-boundsread@*/
 /** \ingroup rpmts
  * \file lib/transaction.c
  */
@@ -83,6 +82,7 @@ static int sharedCmp(const void * one, const void * two)
 
 /**
  */
+/*@-boundsread@*/
 static fileAction decideFileFate(const rpmts ts,
                const rpmfi ofi, rpmfi nfi)
        /*@globals fileSystem @*/
@@ -177,9 +177,11 @@ static fileAction decideFileFate(const rpmts ts,
      */
     return save;
 }
+/*@=boundsread@*/
 
 /**
  */
+/*@-boundsread@*/
 static int filecmp(rpmfi afi, rpmfi bfi)
        /*@*/
 {
@@ -210,6 +212,7 @@ static int filecmp(rpmfi afi, rpmfi bfi)
 
     return 0;
 }
+/*@=boundsread@*/
 
 /**
  */
@@ -1483,4 +1486,3 @@ fi->actions = actions;
        return 0;
     /*@=nullstate@*/
 }
-/*@=boundsread@*/
index a3d22bc..49aac97 100644 (file)
@@ -13,8 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds               # 56
-+boundswrite           # 40
++bounds
 
 # --- +partial artifacts
 -exportlocal           # 14
index e4d6d31..d2dffa7 100644 (file)
@@ -335,8 +335,10 @@ static int handleAlias(/*@special@*/ poptContext con,
     if ((con->os - con->optionStack + 1) == POPT_OPTION_DEPTH)
        return POPT_ERROR_OPTSTOODEEP;
 
+/*@-boundsread@*/
     if (nextCharArg && *nextCharArg)
        con->os->nextCharArg = nextCharArg;
+/*@=boundsread@*/
 
     con->os++;
     con->os->next = 0;
index 5f9d54f..801dca5 100644 (file)
@@ -325,6 +325,7 @@ static void singleOptionHelp(FILE * fp, int maxLeftCol,
     }
 
     helpLength = strlen(help);
+/*@-boundsread@*/
     while (helpLength > lineLength) {
        const char * ch;
        char format[10];
@@ -343,6 +344,7 @@ static void singleOptionHelp(FILE * fp, int maxLeftCol,
        while (isspace(*help) && *help) help++;
        helpLength = strlen(help);
     }
+/*@=boundsread@*/
 
     if (helpLength) fprintf(fp, "%s\n", help);
 
@@ -479,9 +481,11 @@ static int showHelpIntro(poptContext con, FILE * fp)
 
     fprintf(fp, POPT_("Usage:"));
     if (!(con->flags & POPT_CONTEXT_KEEP_FIRST)) {
+/*@-boundsread@*/
        /*@-nullderef@*/        /* LCL: wazzup? */
        fn = con->optionStack->argv[0];
        /*@=nullderef@*/
+/*@=boundsread@*/
        if (fn == NULL) return len;
        if (strchr(fn, '/')) fn = strrchr(fn, '/') + 1;
        fprintf(fp, " %s", fn);
index d1bbc47..8d84144 100644 (file)
@@ -254,6 +254,7 @@ int main(int argc, const char ** argv)
     if (singleDash)
        fprintf(stdout, " -");
 
+/*@-boundsread@*/
     rest = poptGetArgs(optCon);
     if (rest) {
        fprintf(stdout, " rest:");
@@ -262,6 +263,7 @@ int main(int argc, const char ** argv)
            rest++;
        }
     }
+/*@=boundsread@*/
 
     fprintf(stdout, "\n");
 
index 4f1804b..36f536c 100644 (file)
@@ -13,8 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds               # 0
-+boundswrite           # 0
++bounds
 +slovak-fcns
 
 # --- +partial artifacts
index 3e65138..8b5df99 100644 (file)
@@ -248,10 +248,11 @@ struct dbOption rdbOptions[] = {
  { "q_extentsize", 0,POPT_ARG_INT,     &db3dbi.dbi_q_extentsize, 0,
        NULL, NULL },
 
- { NULL, 0,0, NULL, 0, NULL, NULL }
+    POPT_TABLEEND
 };
 /*@=compmempass =immediatetrans =exportlocal =exportheadervar@*/
 
+/*@-boundswrite@*/
 static int dbSaveLong(const struct dbOption * opt, int argInfo, long aLong)
        /*@modifies opt->arg @*/
 {
@@ -277,7 +278,9 @@ static int dbSaveLong(const struct dbOption * opt, int argInfo, long aLong)
     }
     return 0;
 }
+/*@=boundswrite@*/
 
+/*@-boundswrite@*/
 static int dbSaveInt(const struct dbOption * opt, int argInfo, long aLong)
        /*@modifies opt->arg @*/
 {
@@ -303,6 +306,7 @@ static int dbSaveInt(const struct dbOption * opt, int argInfo, long aLong)
     }
     return 0;
 }
+/*@=boundswrite@*/
 
 dbiIndex db3Free(dbiIndex dbi)
 {
@@ -326,6 +330,7 @@ dbiIndex db3Free(dbiIndex dbi)
 static const char *db3_config_default =
     "db3:hash:mpool:cdb:usecursors:verbose:mp_mmapsize=8Mb:mp_size=512Kb:pagesize=512:perms=0644";
 
+/*@-bounds@*/
 dbiIndex db3New(rpmdb rpmdb, rpmTag rpmtag)
 {
     dbiIndex dbi = xcalloc(1, sizeof(*dbi));
@@ -510,7 +515,9 @@ dbiIndex db3New(rpmdb rpmdb, rpmTag rpmtag)
     return dbi;
     /*@=globstate@*/
 }
+/*@=bounds@*/
 
+/*@-boundswrite@*/
 const char *const prDbiOpenFlags(int dbflags, int print_dbenv_flags)
 {
     static char buf[256];
@@ -545,5 +552,6 @@ const char *const prDbiOpenFlags(int dbflags, int print_dbenv_flags)
     }
     return buf;
 }
+/*@=boundswrite@*/
 
 #endif
index b0a51e3..250898d 100644 (file)
@@ -53,6 +53,7 @@ static /*@null@*/ const struct fprintCacheEntry_s * cacheContainsDirectory(
  * @param scareMemory
  * @return pointer to the finger print associated with a file path.
  */
+/*@-bounds@*/ /* LCL: segfault */
 static fingerPrint doLookup(fingerPrintCache cache,
                const char * dirName, const char * baseName, int scareMemory)
        /*@modifies cache @*/
@@ -181,6 +182,7 @@ static fingerPrint doLookup(fingerPrintCache cache,
     /*@-nullret@*/ return fp; /*@=nullret@*/   /* LCL: can't happen. */
     /*@=compdef@*/
 }
+/*@=bounds@*/
 
 fingerPrint fpLookup(fingerPrintCache cache, const char * dirName, 
                        const char * baseName, int scareMemory)
@@ -197,7 +199,9 @@ unsigned int fpHashFunction(const void * key)
 
     ch = 0;
     chptr = fp->baseName;
+/*@-boundsread@*/
     while (*chptr != '\0') ch ^= *chptr++;
+/*@=boundsread@*/
 
     hash |= ((unsigned)ch) << 24;
     hash |= (((((unsigned)fp->entry->dev) >> 8) ^ fp->entry->dev) & 0xFF) << 16;
@@ -206,6 +210,7 @@ unsigned int fpHashFunction(const void * key)
     return hash;
 }
 
+/*@-boundsread@*/
 int fpEqual(const void * key1, const void * key2)
 {
     const fingerPrint *k1 = key1;
@@ -223,7 +228,9 @@ int fpEqual(const void * key1, const void * key2)
     return 1;
 
 }
+/*@=boundsread@*/
 
+/*@-bounds@*/
 void fpLookupList(fingerPrintCache cache, const char ** dirNames, 
                  const char ** baseNames, const int * dirIndexes, 
                  int fileCount, fingerPrint * fpList)
@@ -243,6 +250,7 @@ void fpLookupList(fingerPrintCache cache, const char ** dirNames,
        }
     }
 }
+/*@=bounds@*/
 
 #ifdef UNUSED
 /**
index b9fb12e..6efe6aa 100644 (file)
@@ -184,9 +184,11 @@ Header headerNew(void)
 {
     Header h = xcalloc(1, sizeof(*h));
 
+/*@-boundsread@*/
     /*@-assignexpose@*/
     h->hv = *hdrVec;           /* structure assignment */
     /*@=assignexpose@*/
+/*@=boundsread@*/
     h->blob = NULL;
     h->indexAlloced = INDEX_MALLOC_SIZE;
     h->indexUsed = 0;
@@ -196,15 +198,16 @@ Header headerNew(void)
        ? xcalloc(h->indexAlloced, sizeof(*h->index))
        : NULL);
 
-    /*@-globstate -observertrans @*/
     h->nrefs = 0;
+    /*@-globstate -observertrans @*/
     return headerLink(h, "headerNew");
     /*@=globstate =observertrans @*/
 }
 
 /**
  */
-static int indexCmp(const void * avp, const void * bvp)        /*@*/
+static int indexCmp(const void * avp, const void * bvp)
+       /*@*/
 {
     /*@-castexpose@*/
     indexEntry ap = (indexEntry) avp, bp = (indexEntry) bvp;
@@ -221,7 +224,9 @@ void headerSort(Header h)
        /*@modifies h @*/
 {
     if (!(h->flags & HEADERFLAG_SORTED)) {
+/*@-boundsread@*/
        qsort(h->index, h->indexUsed, sizeof(*h->index), indexCmp);
+/*@=boundsread@*/
        h->flags |= HEADERFLAG_SORTED;
     }
 }
@@ -253,7 +258,9 @@ static
 void headerUnsort(Header h)
        /*@modifies h @*/
 {
+/*@-boundsread@*/
     qsort(h->index, h->indexUsed, sizeof(*h->index), offsetCmp);
+/*@=boundsread@*/
 }
 
 /** \ingroup header
@@ -309,6 +316,7 @@ unsigned int headerSizeof(/*@null@*/ Header h, enum hMagic magicp)
 
        /* Alignment */
        type = entry->info.type;
+/*@-boundsread@*/
        if (typeSizes[type] > 1) {
            diff = typeSizes[type] - (size % typeSizes[type]);
            if (diff != typeSizes[type]) {
@@ -316,6 +324,7 @@ unsigned int headerSizeof(/*@null@*/ Header h, enum hMagic magicp)
                pad += diff;
            }
        }
+/*@=boundsread@*/
 
        /*@-sizeoftype@*/
        size += sizeof(struct entryInfo_s) + entry->length;
@@ -372,18 +381,22 @@ static int dataLength(int_32 type, hPTR_t p, int_32 count, int onDisk)
            }
        } else {
            const char ** src = (const char **)p;
+/*@-boundsread@*/
            while (i--) {
                /* add one for null termination */
                length += strlen(*src++) + 1;
            }
+/*@=boundsread@*/
        }
     }  break;
 
     default:
+/*@-boundsread@*/
        if (typeSizes[type] != -1) {
            length = typeSizes[type] * count;
            break;
        }
+/*@=boundsread@*/
        /*@-modfilesys@*/
        fprintf(stderr, _("Data type %d not supported\n"), (int) type);
        /*@=modfilesys@*/
@@ -419,7 +432,6 @@ static int dataLength(int_32 type, hPTR_t p, int_32 count, int onDisk)
  * @param regionid     region offset
  * @return             no. bytes of data in region, -1 on error
  */
-/*@-boundswrite@*/
 static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
                entryInfo pe, char * dataStart, int regionid)
        /*@modifies *entry, *dataStart @*/
@@ -429,7 +441,9 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
     int tdel, tl = dl;
     struct indexEntry_s ieprev;
 
+/*@-boundswrite@*/
     memset(&ieprev, 0, sizeof(ieprev));
+/*@=boundswrite@*/
     for (; il > 0; il--, pe++) {
        struct indexEntry_s ie;
        int_32 type;
@@ -446,12 +460,15 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
 
        if (entry) {
            ie.info.offset = regionid;
+/*@-boundswrite@*/
            *entry = ie;        /* structure assignment */
+/*@=boundswrite@*/
            entry++;
        }
 
        /* Alignment */
        type = ie.info.type;
+/*@-boundsread@*/
        if (typeSizes[type] > 1) {
            unsigned diff;
            diff = typeSizes[type] - (dl % typeSizes[type]);
@@ -461,6 +478,7 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
                    ieprev.length += diff;
            }
        }
+/*@=boundsread@*/
        tdel = (tprev ? (t - tprev) : 0);
        if (ieprev.info.type == RPM_I18NSTRING_TYPE)
            tdel = ieprev.length;
@@ -478,6 +496,7 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
 
        /* Perform endian conversions */
        switch (ntohl(pe->type)) {
+/*@-bounds@*/
        case RPM_INT32_TYPE:
        {   int_32 * it = (int_32 *)t;
            for (; ie.info.count > 0; ie.info.count--, it += 1)
@@ -490,6 +509,7 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
                *it = htons(*it);
            t = (char *) it;
        }   /*@switchbreak@*/ break;
+/*@=bounds@*/
        default:
            t += ie.length;
            /*@switchbreak@*/ break;
@@ -515,14 +535,13 @@ static int regionSwab(/*@null@*/ indexEntry entry, int il, int dl,
 
     return dl;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  */
-/*@-boundswrite@*/
 static /*@only@*/ /*@null@*/ void * doHeaderUnload(Header h,
                /*@out@*/ int * lengthPtr)
        /*@modifies h, *lengthPtr @*/
+       /*@requires maxSet(lengthPtr) >= 0 @*/
 {
     int_32 * ei = NULL;
     entryInfo pe;
@@ -613,9 +632,11 @@ static /*@only@*/ /*@null@*/ void * doHeaderUnload(Header h,
 
     len = sizeof(il) + sizeof(dl) + (il * sizeof(*pe)) + dl;
 
+/*@-boundswrite@*/
     ei = xmalloc(len);
     ei[0] = htonl(il);
     ei[1] = htonl(dl);
+/*@=boundswrite@*/
 
     pe = (entryInfo) &ei[2];
     dataStart = te = (char *) (pe + il);
@@ -648,8 +669,10 @@ t = te;
                int_32 stei[4];
 
                legacy = 1;
+/*@-boundswrite@*/
                memcpy(pe+1, src, rdl);
                memcpy(te, src + rdl, rdlen);
+/*@=boundswrite@*/
                te += rdlen;
 
                pe->offset = htonl(te - dataStart);
@@ -657,7 +680,9 @@ t = te;
                stei[1] = pe->type;
                stei[2] = htonl(-rdl-entry->info.count);
                stei[3] = pe->count;
+/*@-boundswrite@*/
                memcpy(te, stei, entry->info.count);
+/*@=boundswrite@*/
                te += entry->info.count;
                ril++;
                rdlen += entry->info.count;
@@ -668,8 +693,10 @@ t = te;
 
            } else {
 
+/*@-boundswrite@*/
                memcpy(pe+1, src + sizeof(*pe), ((ril-1) * sizeof(*pe)));
                memcpy(te, src + (ril * sizeof(*pe)), rdlen+entry->info.count+drlen);
+/*@=boundswrite@*/
                te += rdlen;
                {   /*@-castexpose@*/
                    entryInfo se = (entryInfo)src;
@@ -705,7 +732,9 @@ t = te;
            unsigned diff;
            diff = typeSizes[type] - ((te - dataStart) % typeSizes[type]);
            if (diff != typeSizes[type]) {
+/*@-boundswrite@*/
                memset(te, 0, diff);
+/*@=boundswrite@*/
                te += diff;
                pad += diff;
            }
@@ -714,6 +743,7 @@ t = te;
        pe->offset = htonl(te - dataStart);
 
        /* copy data w/ endian conversions */
+/*@-boundswrite@*/
        switch (entry->info.type) {
        case RPM_INT32_TYPE:
            count = entry->info.count;
@@ -744,6 +774,7 @@ t = te;
            te += entry->length;
            /*@switchbreak@*/ break;
        }
+/*@=boundswrite@*/
        pe++;
     }
    
@@ -767,7 +798,6 @@ errxit:
     /*@=usereleased@*/
     return (void *) ei;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Convert header to on-disk representation.
@@ -779,7 +809,9 @@ void * headerUnload(Header h)
        /*@modifies h @*/
 {
     int length;
+/*@-boundswrite@*/
     void * uh = doHeaderUnload(h, &length);
+/*@=boundswrite@*/
     return uh;
 }
 
@@ -840,7 +872,6 @@ indexEntry findEntry(/*@null@*/ Header h, int_32 tag, int_32 type)
  * @param tag          tag
  * @return             0 on success, 1 on failure (INCONSISTENT)
  */
-/*@-boundswrite@*/
 static
 int headerRemoveEntry(Header h, int_32 tag)
        /*@modifies h @*/
@@ -873,20 +904,20 @@ int headerRemoveEntry(Header h, int_32 tag)
     if (ne > 0) {
        h->indexUsed -= ne;
        ne = last - first;
+/*@-boundswrite@*/
        if (ne > 0)
            memmove(entry, first, (ne * sizeof(*entry)));
+/*@=boundswrite@*/
     }
 
     return 0;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Convert header to in-memory representation.
  * @param uh           on-disk header blob (i.e. with offsets)
  * @return             header
  */
-/*@-boundswrite@*/
 static /*@null@*/
 Header headerLoad(/*@kept@*/ void * uh)
        /*@modifies uh @*/
@@ -1034,10 +1065,12 @@ Header headerLoad(/*@kept@*/ void * uh)
            }
 
            /* If any duplicate entries were replaced, move new entries down. */
+/*@-boundswrite@*/
            if (h->indexUsed < (save - ne)) {
                memmove(h->index + h->indexUsed, firstEntry,
                        (ne * sizeof(*entry)));
            }
+/*@=boundswrite@*/
            h->indexUsed += ne;
          }
        }
@@ -1063,7 +1096,6 @@ errxit:
     return h;
     /*@=refcounttrans =globstate@*/
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Convert header to on-disk representation, and then reload.
@@ -1072,7 +1104,6 @@ errxit:
  * @param tag          region tag
  * @return             on-disk header (with offsets)
  */
-/*@-boundswrite@*/
 static /*@null@*/
 Header headerReload(/*@only@*/ Header h, int tag)
        /*@modifies h @*/
@@ -1080,7 +1111,9 @@ Header headerReload(/*@only@*/ Header h, int tag)
     Header nh;
     int length;
     /*@-onlytrans@*/
+/*@-boundswrite@*/
     void * uh = doHeaderUnload(h, &length);
+/*@=boundswrite@*/
 
     h = headerFree(h, "headerReload");
     /*@=onlytrans@*/
@@ -1095,12 +1128,13 @@ Header headerReload(/*@only@*/ Header h, int tag)
        uh = _free(uh);
     nh->flags |= HEADERFLAG_ALLOCATED;
     if (ENTRY_IS_REGION(nh->index)) {
+/*@-boundswrite@*/
        if (tag == HEADER_SIGNATURES || tag == HEADER_IMMUTABLE)
            nh->index[0].info.tag = tag;
+/*@=boundswrite@*/
     }
     return nh;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Make a copy and convert header to in-memory representation.
@@ -1112,8 +1146,10 @@ Header headerCopyLoad(const void * uh)
        /*@*/
 {
     int_32 * ei = (int_32 *) uh;
+/*@-boundsread@*/
     int_32 il = ntohl(ei[0]);          /* index length */
     int_32 dl = ntohl(ei[1]);          /* data length */
+/*@=boundsread@*/
     /*@-sizeoftype@*/
     size_t pvlen = sizeof(il) + sizeof(dl) +
                        (il * sizeof(struct entryInfo_s)) + dl;
@@ -1124,7 +1160,9 @@ Header headerCopyLoad(const void * uh)
     /* Sanity checks on header intro. */
     /*@-branchstate@*/
     if (!(hdrchkTags(il) || hdrchkData(dl)) && pvlen < headerMaxbytes) {
+/*@-boundsread@*/
        nuh = memcpy(xmalloc(pvlen), uh, pvlen);
+/*@=boundsread@*/
        if ((h = headerLoad(nuh)) != NULL)
            h->flags |= HEADERFLAG_ALLOCATED;
     }
@@ -1142,7 +1180,6 @@ Header headerCopyLoad(const void * uh)
  * @param magicp       read (and verify) 8 bytes of (magic, 0)?
  * @return             header (or NULL on error)
  */
-/*@-boundswrite@*/
 static /*@null@*/
 Header headerRead(FD_t fd, enum hMagic magicp)
        /*@modifies fd @*/
@@ -1169,6 +1206,7 @@ Header headerRead(FD_t fd, enum hMagic magicp)
 
     i = 0;
 
+/*@-boundsread@*/
     if (magicp == HEADER_MAGIC_YES) {
        magic = block[i++];
        if (memcmp(&magic, header_magic, sizeof(magic)))
@@ -1178,6 +1216,7 @@ Header headerRead(FD_t fd, enum hMagic magicp)
     
     il = ntohl(block[i]);      i++;
     dl = ntohl(block[i]);      i++;
+/*@=boundsread@*/
 
     /*@-sizeoftype@*/
     len = sizeof(il) + sizeof(dl) + (il * sizeof(struct entryInfo_s)) + dl;
@@ -1187,15 +1226,19 @@ Header headerRead(FD_t fd, enum hMagic magicp)
     if (hdrchkTags(il) || hdrchkData(dl) || len > headerMaxbytes)
        goto exit;
 
+/*@-boundswrite@*/
     ei = xmalloc(len);
     ei[0] = htonl(il);
     ei[1] = htonl(dl);
     len -= sizeof(il) + sizeof(dl);
+/*@=boundswrite@*/
 
+/*@-boundsread@*/
     /*@-type@*/ /* FIX: cast? */
     if (timedRead(fd, (char *)&ei[2], len) != len)
        goto exit;
     /*@=type@*/
+/*@=boundsread@*/
     
     h = headerLoad(ei);
 
@@ -1210,7 +1253,6 @@ exit:
     return h;
     /*@-mustmod@*/
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Write (with unload) header to file handle.
@@ -1230,7 +1272,9 @@ int headerWrite(FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
 
     if (h == NULL)
        return 1;
+/*@-boundswrite@*/
     uh = doHeaderUnload(h, &length);
+/*@=boundswrite@*/
     if (uh == NULL)
        return 1;
     switch (magicp) {
@@ -1279,13 +1323,13 @@ int headerIsEntry(/*@null@*/Header h, int_32 tag)
  * @param minMem       string pointers refer to header memory?
  * @return             1 on success, otherwise error.
  */
-/*@-boundswrite@*/
 static int copyEntry(const indexEntry entry,
                /*@null@*/ /*@out@*/ hTYP_t type,
                /*@null@*/ /*@out@*/ hPTR_t * p,
                /*@null@*/ /*@out@*/ hCNT_t c,
                int minMem)
        /*@modifies *type, *p, *c @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     int_32 count = entry->info.count;
     int rc = 1;                /* XXX 1 on success. */
@@ -1304,7 +1348,9 @@ static int copyEntry(const indexEntry entry,
            /*@-castexpose@*/
            entryInfo pe = (entryInfo) (ei + 2);
            /*@=castexpose@*/
+/*@-boundsread@*/
            char * dataStart = (char *) (pe + ntohl(ei[0]));
+/*@=boundsread@*/
            int_32 rdl = -entry->info.offset;   /* negative offset */
            int_32 ril = rdl/sizeof(*pe);
 
@@ -1319,6 +1365,7 @@ static int copyEntry(const indexEntry entry,
                rdl += REGION_TAG_COUNT;
            }
 
+/*@-bounds@*/
            *p = xmalloc(count);
            ei = (int_32 *) *p;
            ei[0] = htonl(ril);
@@ -1330,6 +1377,7 @@ static int copyEntry(const indexEntry entry,
 
            dataStart = (char *) memcpy(pe + ril, dataStart, rdl);
            /*@=sizeoftype@*/
+/*@=bounds@*/
 
            rc = regionSwab(NULL, ril, 0, pe, dataStart, 0);
            /* XXX 1 on success. */
@@ -1356,6 +1404,7 @@ static int copyEntry(const indexEntry entry,
        char * t;
        int i;
 
+/*@-bounds@*/
        /*@-mods@*/
        if (minMem) {
            *p = xmalloc(tableSize);
@@ -1369,8 +1418,11 @@ static int copyEntry(const indexEntry entry,
            memcpy(t, entry->data, entry->length);
        }
        /*@=mods@*/
+/*@=bounds@*/
        for (i = 0; i < count; i++) {
+/*@-boundswrite@*/
            *ptrEntry++ = t;
+/*@=boundswrite@*/
            t = strchr(t, 0);
            t++;
        }
@@ -1384,7 +1436,6 @@ static int copyEntry(const indexEntry entry,
     if (c) *c = count;
     return rc;
 }
-/*@=boundswrite@*/
 
 /**
  * Does locale match entry in header i18n table?
@@ -1495,6 +1546,7 @@ headerFindI18NString(Header h, indexEntry entry)
        return entry->data;
     /*@=mods@*/
 
+/*@-boundsread@*/
     for (l = lang; *l != '\0'; l = le) {
        const char *td;
        char *ed;
@@ -1517,6 +1569,7 @@ headerFindI18NString(Header h, indexEntry entry)
 
        }
     }
+/*@=boundsread@*/
 
     return entry->data;
 }
@@ -1531,13 +1584,13 @@ headerFindI18NString(Header h, indexEntry entry)
  * @param minMem       string pointers reference header memory?
  * @return             1 on success, 0 on not found
  */
-/*@-boundswrite@*/
 static int intGetEntry(Header h, int_32 tag,
                /*@null@*/ /*@out@*/ hTAG_t type,
                /*@null@*/ /*@out@*/ hPTR_t * p,
                /*@null@*/ /*@out@*/ hCNT_t c,
                int minMem)
        /*@modifies *type, *p, *c @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     indexEntry entry;
     int rc;
@@ -1570,7 +1623,6 @@ static int intGetEntry(Header h, int_32 tag,
     /* XXX 1 on success */
     return ((rc == 1) ? 1 : 0);
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Free data allocated when retrieved from header.
@@ -1640,7 +1692,6 @@ int headerGetEntryMinMemory(Header h, int_32 tag,
     return intGetEntry(h, tag, type, p, c, 1);
 }
 
-/*@-boundswrite@*/
 int headerGetRawEntry(Header h, int_32 tag, int_32 * type, hPTR_t * p,
                int_32 * c)
 {
@@ -1664,11 +1715,9 @@ int headerGetRawEntry(Header h, int_32 tag, int_32 * type, hPTR_t * p,
     /* XXX 1 on success */
     return ((rc == 1) ? 1 : 0);
 }
-/*@=boundswrite@*/
 
 /**
  */
-/*@-boundswrite@*/
 static void copyData(int_32 type, /*@out@*/ void * dstPtr, const void * srcPtr,
                int_32 c, int dataLength)
        /*@modifies *dstPtr @*/
@@ -1684,6 +1733,7 @@ static void copyData(int_32 type, /*@out@*/ void * dstPtr, const void * srcPtr,
        i = c;
        src = (const char **) srcPtr;
        dst = dstPtr;
+/*@-bounds@*/
        while (i--) {
            if (*src) {
                int len = strlen(*src) + 1;
@@ -1692,14 +1742,16 @@ static void copyData(int_32 type, /*@out@*/ void * dstPtr, const void * srcPtr,
            }
            src++;
        }
+/*@=bounds@*/
        break;
 
     default:
+/*@-boundswrite@*/
        memmove(dstPtr, srcPtr, dataLength);
+/*@=boundswrite@*/
        break;
     }
 }
-/*@=boundswrite@*/
 
 /**
  * Return (malloc'ed) copy of entry data.
@@ -1709,10 +1761,10 @@ static void copyData(int_32 type, /*@out@*/ void * dstPtr, const void * srcPtr,
  * @retval lengthPtr   no. bytes in returned data
  * @return             (malloc'ed) copy of entry data
  */
-/*@-boundswrite@*/
 static void * grabData(int_32 type, hPTR_t p, int_32 c,
                /*@out@*/ int * lengthPtr)
        /*@modifies *lengthPtr @*/
+       /*@requires maxSet(lengthPtr) >= 0 @*/
 {
     int length = dataLength(type, p, c, 0);
     void * data = xmalloc(length);
@@ -1723,7 +1775,6 @@ static void * grabData(int_32 type, hPTR_t p, int_32 c,
        *lengthPtr = length;
     return data;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Add tag to header.
@@ -1761,10 +1812,14 @@ int headerAddEntry(Header h, int_32 tag, int_32 type, const void * p, int_32 c)
     entry->info.type = type;
     entry->info.count = c;
     entry->info.offset = 0;
+/*@-boundswrite@*/
     entry->data = grabData(type, p, c, &entry->length);
+/*@=boundswrite@*/
 
+/*@-boundsread@*/
     if (h->indexUsed > 0 && tag < h->index[h->indexUsed-1].info.tag)
        h->flags &= ~HEADERFLAG_SORTED;
+/*@=boundsread@*/
     h->indexUsed++;
 
     return 1;
@@ -1784,7 +1839,6 @@ int headerAddEntry(Header h, int_32 tag, int_32 type, const void * p, int_32 c)
  * @param c            number of values
  * @return             1 on success, 0 on failure
  */
-/*@-boundswrite@*/
 static
 int headerAppendEntry(Header h, int_32 tag, int_32 type,
                const void * p, int_32 c)
@@ -1807,7 +1861,9 @@ int headerAppendEntry(Header h, int_32 tag, int_32 type,
 
     if (ENTRY_IN_REGION(entry)) {
        char * t = xmalloc(entry->length + length);
+/*@-bounds@*/
        memcpy(t, entry->data, entry->length);
+/*@=bounds@*/
        entry->data = t;
        entry->info.offset = 0;
     } else
@@ -1821,7 +1877,6 @@ int headerAppendEntry(Header h, int_32 tag, int_32 type,
 
     return 1;
 }
-/*@=boundswrite@*/
 
 /** \ingroup header
  * Add or append element to tag array in header.
@@ -1863,7 +1918,6 @@ int headerAddOrAppendEntry(Header h, int_32 tag, int_32 type,
  * @param lang         locale
  * @return             1 on success, 0 on failure
  */
-/*@-bounds@*/
 static
 int headerAddI18NString(Header h, int_32 tag, const char * string,
                const char * lang)
@@ -1998,7 +2052,6 @@ int headerAddI18NString(Header h, int_32 tag, const char * string,
 
     return 0;
 }
-/*@=bounds@*/
 
 /** \ingroup header
  * Modify tag in header.
@@ -2067,7 +2120,6 @@ static char escapedChar(const char ch)    /*@*/
  * @param num          number of elements
  * @return             NULL always
  */
-/*@-boundswrite@*/
 static /*@null@*/ sprintfToken
 freeFormat( /*@only@*/ /*@null@*/ sprintfToken format, int num)
        /*@modifies *format @*/
@@ -2078,17 +2130,21 @@ freeFormat( /*@only@*/ /*@null@*/ sprintfToken format, int num)
     for (i = 0; i < num; i++) {
        switch (format[i].type) {
        case PTOK_ARRAY:
+/*@-boundswrite@*/
            format[i].u.array.format =
                freeFormat(format[i].u.array.format,
                        format[i].u.array.numTokens);
+/*@=boundswrite@*/
            /*@switchbreak@*/ break;
        case PTOK_COND:
+/*@-boundswrite@*/
            format[i].u.cond.ifFormat =
                freeFormat(format[i].u.cond.ifFormat, 
                        format[i].u.cond.numIfTokens);
            format[i].u.cond.elseFormat =
                freeFormat(format[i].u.cond.elseFormat, 
                        format[i].u.cond.numElseTokens);
+/*@=boundswrite@*/
            /*@switchbreak@*/ break;
        case PTOK_NONE:
        case PTOK_TAG:
@@ -2100,16 +2156,15 @@ freeFormat( /*@only@*/ /*@null@*/ sprintfToken format, int num)
     format = _free(format);
     return NULL;
 }
-/*@=boundswrite@*/
 
 /**
  */
-/*@-boundswrite@*/
 static void findTag(char * name, const headerTagTableEntry tags, 
                    const headerSprintfExtension extensions,
                    /*@out@*/ headerTagTableEntry * tagMatch,
                    /*@out@*/ headerSprintfExtension * extMatch)
        /*@modifies *tagMatch, *extMatch @*/
+       /*@requires maxSet(tagMatch) >= 0 /\ maxSet(extMatch) >= 0 @*/
 {
     headerTagTableEntry entry;
     headerSprintfExtension ext;
@@ -2119,9 +2174,11 @@ static void findTag(char * name, const headerTagTableEntry tags,
     *extMatch = NULL;
 
     if (strncmp("RPMTAG_", name, sizeof("RPMTAG_")-1)) {
+/*@-boundswrite@*/
        char * t = alloca(strlen(name) + sizeof("RPMTAG_"));
        (void) stpcpy( stpcpy(t, "RPMTAG_"), name);
        tagname = t;
+/*@=boundswrite@*/
     } else {
        tagname = name;
     }
@@ -2154,14 +2211,14 @@ static void findTag(char * name, const headerTagTableEntry tags,
        return;
     }
 }
-/*@=boundswrite@*/
 
 /* forward ref */
 static int parseExpression(sprintfToken token, char * str, 
                const headerTagTableEntry tags, 
                const headerSprintfExtension extensions,
                /*@out@*/char ** endPtr, /*@null@*/ /*@out@*/ errmsg_t * errmsg)
-       /*@modifies str, *str, *token, *endPtr, *errmsg @*/;
+       /*@modifies str, *str, *token, *endPtr, *errmsg @*/
+       /*@requires maxSet(endPtr) >= 0 /\ maxSet(errmsg) >= 0 @*/;
 
 /**
  */
@@ -2172,6 +2229,8 @@ static int parseFormat(/*@null@*/ char * str, const headerTagTableEntry tags,
                /*@null@*/ /*@out@*/ char ** endPtr, int state,
                /*@null@*/ /*@out@*/ errmsg_t * errmsg)
        /*@modifies str, *str, *formatPtr, *numTokensPtr, *endPtr, *errmsg @*/
+       /*@requires maxSet(formatPtr) >= 0 /\ maxSet(numTokensPtr) >= 0
+               /\ maxSet(endPtr) >= 0 /\ maxSet(errmsg) >= 0 @*/
 {
     char * chptr, * start, * next, * dst;
     sprintfToken format;
@@ -2549,6 +2608,12 @@ static int parseExpression(sprintfToken token, char * str,
 /*@=boundswrite@*/
 
 /**
+ * @param h
+ * @param fn
+ * @retval typeptr
+ * @retval data
+ * @retval countptr
+ * @param ext
  * @return             0 on success, 1 on failure
  */
 static int getExtension(Header h, headerTagTagFunction fn,
@@ -2557,6 +2622,8 @@ static int getExtension(Header h, headerTagTagFunction fn,
                /*@out@*/ hCNT_t countptr,
                extensionCache ext)
        /*@modifies *typeptr, *data, *countptr, ext @*/
+       /*@requires maxSet(typeptr) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(countptr) >= 0 @*/
 {
     if (!ext->avail) {
        if (fn(h, &ext->type, &ext->data, &ext->count, &ext->freeit))
@@ -2564,11 +2631,9 @@ static int getExtension(Header h, headerTagTagFunction fn,
        ext->avail = 1;
     }
 
-/*@-boundswrite@*/
     if (typeptr) *typeptr = ext->type;
     if (data) *data = ext->data;
     if (countptr) *countptr = ext->count;
-/*@=boundswrite@*/
 
     return 0;
 }
@@ -2581,6 +2646,8 @@ static char * formatValue(sprintfTag tag, Header h,
                extensionCache extCache, int element,
                char ** valp, int * vallenp, int * allocedp)
        /*@modifies extCache, *valp, *vallenp, *allocedp @*/
+       /*@requires maxSet(valp) >= 0 /\ maxSet(vallenp) >= 0
+               /\ maxSet(allocedp) >= 0 @*/
 {
     char * val = NULL;
     int need = 0;
@@ -2598,6 +2665,7 @@ static char * formatValue(sprintfTag tag, Header h,
     memset(buf, 0, sizeof(buf));
     /*@-branchstate@*/
     if (tag->ext) {
+/*@-boundswrite@*/
        if (getExtension(h, tag->ext, &type, &data, &count, 
                         extCache + tag->extNum))
        {
@@ -2605,6 +2673,7 @@ static char * formatValue(sprintfTag tag, Header h,
            type = RPM_STRING_TYPE;     
            data = "(none)";
        }
+/*@=boundswrite@*/
     } else {
        if (!headerGetEntry(h, tag->tag, &type, (void **)&data, &count)) {
            count = 1;
@@ -2760,7 +2829,6 @@ static char * formatValue(sprintfTag tag, Header h,
 
     /*@-branchstate@*/
     if (val && need > 0) {
-/*@-boundswrite@*/
        if (((*vallenp) + need) >= (*allocedp)) {
            if ((*allocedp) <= need)
                (*allocedp) += need;
@@ -2772,10 +2840,11 @@ static char * formatValue(sprintfTag tag, Header h,
 /*@=unqualifiedtrans@*/
        }
        t = (*valp) + (*vallenp);
+/*@-boundswrite@*/
        te = stpcpy(t, val);
+/*@=boundswrite@*/
        (*vallenp) += (te - t);
        val = _free(val);
-/*@=boundswrite@*/
     }
     /*@=branchstate@*/
 
@@ -2790,6 +2859,8 @@ static char * singleSprintf(Header h, sprintfToken token,
                extensionCache extCache, int element,
                char ** valp, int * vallenp, int * allocedp)
        /*@modifies h, extCache, *valp, *vallenp, *allocedp @*/
+       /*@requires maxSet(valp) >= 0 /\ maxSet(vallenp) >= 0
+               /\ maxSet(allocedp) >= 0 @*/
 {
     char * t, * te;
     int i, j;
@@ -2806,7 +2877,6 @@ static char * singleSprintf(Header h, sprintfToken token,
        break;
 
     case PTOK_STRING:
-/*@-boundswrite@*/
        need = token->u.string.len;
        if (need <= 0) break;
        if (((*vallenp) + need) >= (*allocedp)) {
@@ -2820,9 +2890,10 @@ static char * singleSprintf(Header h, sprintfToken token,
 /*@=unqualifiedtrans@*/
        }
        t = (*valp) + (*vallenp);
+/*@-boundswrite@*/
        te = stpcpy(t, token->u.string.string);
-       (*vallenp) += (te - t);
 /*@=boundswrite@*/
+       (*vallenp) += (te - t);
        break;
 
     case PTOK_TAG:
@@ -2844,7 +2915,6 @@ static char * singleSprintf(Header h, sprintfToken token,
 
        need = condNumFormats * 20;
        if (condFormat == NULL || need <= 0) break;
-/*@-boundswrite@*/
        if (((*vallenp) + need) >= (*allocedp)) {
            if ((*allocedp) <= need)
                (*allocedp) += need;
@@ -2855,7 +2925,6 @@ static char * singleSprintf(Header h, sprintfToken token,
            (*valp) = xrealloc((*valp), (*allocedp)+1); 
 /*@=unqualifiedtrans@*/
        }
-/*@=boundswrite@*/
 
        t = (*valp) + (*vallenp);
        for (i = 0; i < condNumFormats; i++)
@@ -2872,11 +2941,13 @@ static char * singleSprintf(Header h, sprintfToken token,
 
            if (token->u.array.format[i].u.tag.ext) {
                const void * data;
+/*@-boundswrite@*/
                if (getExtension(h, token->u.array.format[i].u.tag.ext,
                                 &type, &data, &numElements, 
                                 extCache + 
                                   token->u.array.format[i].u.tag.extNum))
                     continue;
+/*@=boundswrite@*/
            } else {
                if (!headerGetEntry(h, token->u.array.format[i].u.tag.tag, 
                                    &type, NULL, &numElements))
@@ -2885,7 +2956,6 @@ static char * singleSprintf(Header h, sprintfToken token,
            /*@loopbreak@*/ break;
        }
 
-/*@-boundswrite@*/
        if (numElements == -1) {
            need = sizeof("(none)") - 1;
            if (((*vallenp) + need) >= (*allocedp)) {
@@ -2899,7 +2969,9 @@ static char * singleSprintf(Header h, sprintfToken token,
 /*@=unqualifiedtrans@*/
            }
            t = (*valp) + (*vallenp);
+/*@-boundswrite@*/
            te = stpcpy(t, "(none)");
+/*@=boundswrite@*/
            (*vallenp) += (te - t);
        } else {
            need = numElements * token->u.array.numTokens * 10;
@@ -2923,7 +2995,6 @@ static char * singleSprintf(Header h, sprintfToken token,
                                        valp, vallenp, allocedp);
            }
        }
-/*@=boundswrite@*/
        break;
     }
 
@@ -3014,20 +3085,24 @@ char * headerSprintf(Header h, const char * fmt,
     /*fmtString = escapeString(fmt);*/
     fmtString = xstrdup(fmt);
    
+/*@-boundswrite@*/
     if (parseFormat(fmtString, tags, exts, &format, &numTokens, 
                    NULL, PARSER_BEGIN, errmsg)) {
        fmtString = _free(fmtString);
        return NULL;
     }
+/*@=boundswrite@*/
 
     extCache = allocateExtensionCache(exts);
 
     val = xstrdup("");
     for (i = 0; i < numTokens; i++) {
+/*@-boundswrite@*/
        /*@-mods@*/
        t = singleSprintf(h, format + i, exts, extCache, 0,
                &val, &vallen, &alloced);
        /*@=mods@*/
+/*@=boundswrite@*/
     }
 
     if (val != NULL && vallen < alloced)
@@ -3051,13 +3126,13 @@ static char * octalFormat(int_32 type, hPTR_t data,
     if (type != RPM_INT32_TYPE) {
        val = xstrdup(_("(not a number)"));
     } else {
-/*@-boundswrite@*/
        val = xmalloc(20 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "o");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(val, formatPrefix, *((int_32 *) data));
        /*@=formatconst@*/
-/*@=boundswrite@*/
     }
 
     return val;
@@ -3074,13 +3149,13 @@ static char * hexFormat(int_32 type, hPTR_t data,
     if (type != RPM_INT32_TYPE) {
        val = xstrdup(_("(not a number)"));
     } else {
-/*@-boundswrite@*/
        val = xmalloc(20 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "x");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(val, formatPrefix, *((int_32 *) data));
        /*@=formatconst@*/
-/*@=boundswrite@*/
     }
 
     return val;
@@ -3101,9 +3176,10 @@ static char * realDateFormat(int_32 type, hPTR_t data,
        struct tm * tstruct;
        char buf[50];
 
-/*@-boundswrite@*/
        val = xmalloc(50 + padding);
+/*@-boundswrite@*/
        strcat(formatPrefix, "s");
+/*@=boundswrite@*/
 
        /* this is important if sizeof(int_32) ! sizeof(time_t) */
        {   time_t dateint = *((int_32 *) data);
@@ -3115,7 +3191,6 @@ static char * realDateFormat(int_32 type, hPTR_t data,
        /*@-formatconst@*/
        sprintf(val, formatPrefix, buf);
        /*@=formatconst@*/
-/*@=boundswrite@*/
     }
 
     return val;
@@ -3142,7 +3217,6 @@ static char * dayFormat(int_32 type, hPTR_t data,
 
 /**
  */
-/*@-boundswrite@*/
 static char * shescapeFormat(int_32 type, hPTR_t data, 
                char * formatPrefix, int padding, /*@unused@*/int element)
        /*@modifies formatPrefix @*/
@@ -3151,17 +3225,22 @@ static char * shescapeFormat(int_32 type, hPTR_t data,
 
     if (type == RPM_INT32_TYPE) {
        result = xmalloc(padding + 20);
+/*@-boundswrite@*/
        strcat(formatPrefix, "d");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(result, formatPrefix, *((int_32 *) data));
        /*@=formatconst@*/
     } else {
        buf = alloca(strlen(data) + padding + 2);
+/*@-boundswrite@*/
        strcat(formatPrefix, "s");
+/*@=boundswrite@*/
        /*@-formatconst@*/
        sprintf(buf, formatPrefix, data);
        /*@=formatconst@*/
 
+/*@-boundswrite@*/
        result = dst = xmalloc(strlen(buf) * 4 + 3);
        *dst++ = '\'';
        for (src = buf; *src != '\0'; src++) {
@@ -3176,12 +3255,12 @@ static char * shescapeFormat(int_32 type, hPTR_t data,
        }
        *dst++ = '\'';
        *dst = '\0';
+/*@=boundswrite@*/
 
     }
 
     return result;
 }
-/*@=boundswrite@*/
 
 /*@-type@*/ /* FIX: cast? */
 const struct headerSprintfExtension_s headerDefaultFormats[] = {
@@ -3279,6 +3358,8 @@ int headerNextIterator(HeaderIterator hi,
                /*@null@*/ /*@out@*/ hPTR_t * p,
                /*@null@*/ /*@out@*/ hCNT_t c)
        /*@modifies hi, *tag, *type, *p, *c @*/
+       /*@requires maxSet(tag) >= 0 /\ maxSet(type) >= 0
+               /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/
 {
     Header h = hi->h;
     int slot = hi->next_index;
@@ -3297,10 +3378,8 @@ int headerNextIterator(HeaderIterator hi,
     hi->next_index++;
     /*@=noeffect@*/
 
-/*@-boundswrite@*/
     if (tag)
        *tag = entry->info.tag;
-/*@=boundswrite@*/
 
     rc = copyEntry(entry, type, p, c, 0);
 
index 2aab899..086b8bc 100644 (file)
@@ -137,7 +137,7 @@ struct headerTagTableEntry_s {
 
 /** \ingroup header
  */
-enum headerSprintfExtenstionType {
+enum headerSprintfExtensionType {
     HEADER_EXT_LAST = 0,       /*!< End of extension chain. */
     HEADER_EXT_FORMAT,         /*!< headerTagFormatFunction() extension */
     HEADER_EXT_MORE,           /*!< Chain to next table. */
@@ -158,7 +158,9 @@ enum headerSprintfExtenstionType {
  */
 typedef /*only@*/ char * (*headerTagFormatFunction)(int_32 type,
                                const void * data, char * formatPrefix,
-                               int padding, int element);
+                               int padding, int element)
+       /*@requires maxSet(data) >= 0 @*/;
+
 /** \ingroup header
  * HEADER_EXT_FORMAT format function prototype.
  * This is allowed to fail, which indicates the tag doesn't exist.
@@ -174,14 +176,16 @@ typedef int (*headerTagTagFunction) (Header h,
                /*@null@*/ /*@out@*/ hTYP_t type,
                /*@null@*/ /*@out@*/ hPTR_t * data,
                /*@null@*/ /*@out@*/ hCNT_t count,
-               /*@null@*/ /*@out@*/ int * freeData);
+               /*@null@*/ /*@out@*/ int * freeData)
+       /*@requires maxSet(type) >= 0 /\ maxSet(data) >= 0
+               /\ maxSet(count) >= 0 /\ maxSet(freeData) >= 0 @*/;
 
 /** \ingroup header
  * Define header tag output formats.
  */
 typedef /*@abstract@*/ struct headerSprintfExtension_s * headerSprintfExtension;
 struct headerSprintfExtension_s {
-    enum headerSprintfExtenstionType type;     /*!< Type of extension. */
+    enum headerSprintfExtensionType type;      /*!< Type of extension. */
 /*@observer@*/ /*@null@*/
     const char * name;                         /*!< Name of extension. */
     union {
@@ -205,8 +209,8 @@ extern const struct headerSprintfExtension_s headerDefaultFormats[];
  * Include calculation for 8 bytes of (magic, 0)?
  */
 enum hMagic {
-       HEADER_MAGIC_NO         = 0,
-       HEADER_MAGIC_YES        = 1
+    HEADER_MAGIC_NO            = 0,
+    HEADER_MAGIC_YES           = 1
 };
 
 /** \ingroup header
@@ -237,11 +241,11 @@ typedef enum rpmTagType_e {
  */
 /*@-enummemuse -typeuse @*/
 typedef enum rpmSubTagType_e {
-       RPM_REGION_TYPE         = -10,
-       RPM_BIN_ARRAY_TYPE      = -11,
+    RPM_REGION_TYPE            = -10,
+    RPM_BIN_ARRAY_TYPE         = -11,
   /*!<@todo Implement, kinda like RPM_STRING_ARRAY_TYPE for known (but variable)
        length binary data. */
-       RPM_XREF_TYPE           = -12
+    RPM_XREF_TYPE              = -12
   /*!<@todo Implement, intent is to to carry a (???,tagNum,valNum) cross
        reference to retrieve data from other tags. */
 } rpmSubTagType;
@@ -408,7 +412,7 @@ typedef
  * @return             header (or NULL on error)
  */
 typedef
-/*@null@*/ Header (*HDRhdrread) (FD_t fd, enum hMagic magicp)
+/*@null@*/ Header (*HDRread) (FD_t fd, enum hMagic magicp)
        /*@modifies fd @*/;
 
 /** \ingroup header
@@ -419,7 +423,7 @@ typedef
  * @return             0 on success, 1 on error
  */
 typedef
-int (*HDRhdrwrite) (FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
+int (*HDRwrite) (FD_t fd, /*@null@*/ Header h, enum hMagic magicp)
        /*@globals fileSystem @*/
        /*@modifies fd, h, fileSystem @*/;
 
@@ -598,7 +602,7 @@ int (*HDRremove) (Header h, int_32 tag)
  * @return             formatted output string (malloc'ed)
  */
 typedef
-/*@only@*/ char * (*HDRhdrsprintf) (Header h, const char * fmt,
+/*@only@*/ char * (*HDRsprintf) (Header h, const char * fmt,
                     const struct headerTagTableEntry_s * tags,
                     const struct headerSprintfExtension_s * extensions,
                     /*@null@*/ /*@out@*/ errmsg_t * errmsg)
@@ -666,8 +670,8 @@ struct HV_s {
     HDRcopy    hdrcopy;
     HDRload    hdrload;
     HDRcopyload        hdrcopyload;
-    HDRhdrread hdrread;
-    HDRhdrwrite        hdrwrite;
+    HDRread    hdrread;
+    HDRwrite   hdrwrite;
     HDRisentry hdrisentry;
     HDRfreetag hdrfreetag;
     HDRget     hdrget;
@@ -678,7 +682,7 @@ struct HV_s {
     HDRaddi18n hdraddi18n;
     HDRmodify  hdrmodify;
     HDRremove  hdrremove;
-    HDRhdrsprintf hdrsprintf;
+    HDRsprintf hdrsprintf;
     HDRcopytags        hdrcopytags;
     HDRfreeiter        hdrfreeiter;
     HDRinititer        hdrinititer;
index 87849c2..cc29887 100644 (file)
@@ -9,6 +9,7 @@
 
 #include "debug.h"
 
+/*@-boundswrite@*/
 char ** headerGetLangs(Header h)
 {
     char **s, *e, **table;
@@ -21,15 +22,15 @@ char ** headerGetLangs(Header h)
     if ((table = (char **)xcalloc((count+1), sizeof(char *))) == NULL)
        return NULL;
 
-/*@-boundswrite@*/
     for (i = 0, e = *s; i < count > 0; i++, e += strlen(e)+1)
        table[i] = e;
     table[count] = NULL;
-/*@=boundswrite@*/
 
     /*@-nullret@*/ return table; /*@=nullret@*/        /* LCL: double indirection? */
 }
+/*@=boundswrite@*/
 
+/*@-boundsread@*/
 /*@-type@*/ /* FIX: shrug */
 void headerDump(Header h, FILE *f, int flags,
        const struct headerTagTableEntry_s * tags)
@@ -170,3 +171,4 @@ void headerDump(Header h, FILE *f, int flags,
 }
 /*@=type@*/
 /*@=sizeoftype@*/
+/*@=boundsread@*/
index b51dec7..f9e0198 100644 (file)
@@ -151,11 +151,14 @@ extern "C" {
  * @return             1 on success, 0 on failure
  */
 /*@-exportlocal@*/
+/*@-incondefs@*/
 int headerGetRawEntry(Header h, int_32 tag,
                        /*@null@*/ /*@out@*/ hTYP_t type,
                        /*@null@*/ /*@out@*/ hPTR_t * p, 
                        /*@null@*/ /*@out@*/ hCNT_t c)
-       /*@modifies *type, *p, *c @*/;
+       /*@modifies *type, *p, *c @*/
+       /*@requires maxSet(type) >= 0 /\ maxSet(p) >= 0 /\ maxSet(c) >= 0 @*/;
+/*@=incondefs@*/
 /*@=exportlocal@*/
 
 /** \ingroup header
index 213b7d4..64033c0 100644 (file)
@@ -65,8 +65,10 @@ static int open_dso(const char * path, /*@null@*/ pid_t * pidp, /*@null@*/ size_
     if (fdno < 0)
        return fdno;
 
+/*@-boundsread@*/
     if (!(cmd && *cmd))
        return fdno;
+/*@=boundsread@*/
 
 #if HAVE_LIBELF_GELF_H && HAVE_LIBELF
  {  Elf *elf = NULL;
index 2e90730..abb5662 100644 (file)
@@ -111,8 +111,10 @@ static int dbiTagToDbix(int rpmtag)
 
     if (dbiTags != NULL)
     for (dbix = 0; dbix < dbiTagsMax; dbix++) {
+/*@-boundsread@*/
        if (rpmtag == dbiTags[dbix])
            return dbix;
+/*@=boundsread@*/
     }
     return -1;
 }
@@ -120,6 +122,7 @@ static int dbiTagToDbix(int rpmtag)
 /**
  * Initialize database (index, tag) tuple from configuration.
  */
+/*@-bounds@*/
 static void dbiTagsInit(void)
        /*@globals rpmGlobalMacroContext, dbiTags, dbiTagsMax @*/
        /*@modifies rpmGlobalMacroContext, dbiTags, dbiTagsMax @*/
@@ -176,6 +179,7 @@ static void dbiTagsInit(void)
 
     dbiTagStr = _free(dbiTagStr);
 }
+/*@=bounds@*/
 
 /*@-redecl@*/
 #define        DB1vec          NULL
@@ -195,6 +199,7 @@ static struct _dbiVec *mydbvecs[] = {
 };
 /*@=nullassign@*/
 
+/*@-bounds@*/
 dbiIndex dbiOpen(rpmdb db, rpmTag rpmtag, /*@unused@*/ unsigned int flags)
 {
     int dbix;
@@ -297,6 +302,7 @@ exit:
     return dbi;
 /*@=compdef =nullstate@*/
 }
+/*@=bounds@*/
 
 /**
  * Create and initialize item for index database set.
@@ -351,6 +357,7 @@ static int dbt2set(dbiIndex dbi, DBT * data, /*@out@*/ dbiIndexSet * setp)
     set->count = data->size / dbi->dbi_jlen;
     set->recs = xmalloc(set->count * sizeof(*(set->recs)));
 
+/*@-boundswrite@*/
     switch (dbi->dbi_jlen) {
     default:
     case 2*sizeof(int_32):
@@ -361,10 +368,12 @@ static int dbt2set(dbiIndex dbi, DBT * data, /*@out@*/ dbiIndexSet * setp)
            sdbir += sizeof(hdrNum.ui);
            memcpy(&tagNum.ui, sdbir, sizeof(tagNum.ui));
            sdbir += sizeof(tagNum.ui);
+/*@-boundsread@*/
            if (_dbbyteswapped) {
                _DBSWAP(hdrNum);
                _DBSWAP(tagNum);
            }
+/*@=boundsread@*/
            set->recs[i].hdrNum = hdrNum.ui;
            set->recs[i].tagNum = tagNum.ui;
            set->recs[i].fpNum = 0;
@@ -376,9 +385,11 @@ static int dbt2set(dbiIndex dbi, DBT * data, /*@out@*/ dbiIndexSet * setp)
 
            memcpy(&hdrNum.ui, sdbir, sizeof(hdrNum.ui));
            sdbir += sizeof(hdrNum.ui);
+/*@-boundsread@*/
            if (_dbbyteswapped) {
                _DBSWAP(hdrNum);
            }
+/*@=boundsread@*/
            set->recs[i].hdrNum = hdrNum.ui;
            set->recs[i].tagNum = 0;
            set->recs[i].fpNum = 0;
@@ -386,6 +397,7 @@ static int dbt2set(dbiIndex dbi, DBT * data, /*@out@*/ dbiIndexSet * setp)
        break;
     }
     *setp = set;
+/*@=boundswrite@*/
 /*@-compdef@*/
     return 0;
 /*@=compdef@*/
@@ -398,6 +410,7 @@ static int dbt2set(dbiIndex dbi, DBT * data, /*@out@*/ dbiIndexSet * setp)
  * @param set          index set
  * @return             0 on success
  */
+/*@-bounds@*/
 static int set2dbt(dbiIndex dbi, DBT * data, dbiIndexSet set)
        /*@modifies *data @*/
 {
@@ -454,6 +467,7 @@ static int set2dbt(dbiIndex dbi, DBT * data, dbiIndexSet set)
     return 0;
 /*@=compdef@*/
 }
+/*@=bounds@*/
 
 /* XXX assumes hdrNum is first int in dbiIndexItem */
 static int hdrNumCmp(const void * one, const void * two)
@@ -472,6 +486,7 @@ static int hdrNumCmp(const void * one, const void * two)
  * @param sortset      should resulting set be sorted?
  * @return             0 success, 1 failure (bad args)
  */
+/*@-bounds@*/ /* LCL: segfault */
 static int dbiAppendSet(dbiIndexSet set, const void * recs,
        int nrecs, size_t recsize, int sortset)
        /*@modifies *set @*/
@@ -501,6 +516,7 @@ static int dbiAppendSet(dbiIndexSet set, const void * recs,
 
     return 0;
 }
+/*@=bounds@*/
 
 /**
  * Remove element(s) from set of index database items.
index ac4c270..a95718f 100644 (file)
@@ -47,7 +47,9 @@ hashBucket findEntry(hashTable ht, const void * key)
 
     /*@-modunconnomods@*/
     hash = ht->fn(key) % ht->numBuckets;
+/*@-boundsread@*/
     b = ht->buckets[hash];
+/*@=boundsread@*/
 
     while (b && b->key && ht->eq(b->key, key))
        b = b->next;
@@ -72,10 +74,12 @@ unsigned int hashFunctionString(const void * string)
     const char * chp = string;
 
     len = strlen(string);
+/*@-boundsread@*/
     for (i = 0; i < len; i++, chp++) {
        xorValue ^= *chp;
        sum += *chp;
     }
+/*@=boundsread@*/
 
     return ((((unsigned)len) << 16) + (((unsigned)sum) << 8) + xorValue);
 }
@@ -138,7 +142,9 @@ hashTable htFree(hashTable ht)
     int i;
 
     for (i = 0; i < ht->numBuckets; i++) {
+/*@-boundsread@*/
        b = ht->buckets[i];
+/*@=boundsread@*/
        if (b == NULL)
            continue;
 /*@-boundswrite@*/
index 9d47e41..47210a3 100644 (file)
@@ -13,8 +13,7 @@
 +strict                        # lclint level
 
 # --- in progress
-#+bounds               # 334
-+boundswrite           # 152
++bounds
 
 # --- +partial artifacts
 -declundef
index 29ec824..1746720 100644 (file)
@@ -35,6 +35,7 @@ struct DIGEST_CTX_s {
        /*@modifies param, digest @*/;  /*!< Digest finish. */
 };
 
+/*@-boundsread@*/
 DIGEST_CTX
 rpmDigestDup(DIGEST_CTX octx)
 {
@@ -42,6 +43,7 @@ rpmDigestDup(DIGEST_CTX octx)
     nctx->param = memcpy(xcalloc(1, nctx->paramlen), octx->param, nctx->paramlen);
     return nctx;
 }
+/*@=boundsread@*/
 
 DIGEST_CTX
 rpmDigestInit(pgpHashAlgo hashalgo, rpmDigestFlags flags)
@@ -88,7 +90,9 @@ rpmDigestInit(pgpHashAlgo hashalgo, rpmDigestFlags flags)
        /*@notreached@*/ break;
     }
 
+/*@-boundsread@*/
     xx = (*ctx->Reset) (ctx->param);
+/*@=boundsread@*/
 
 DPRINTF((stderr, "*** Init(%x) ctx %p param %p\n", flags, ctx, ctx->param));
     return ctx;
index 1039219..8052281 100644 (file)
@@ -1,3 +1,4 @@
+/*@-boundsread@*/
 /*@-sysunrecog -noeffectuncon -nullpass -sizeoftype -unrecog -usereleased @*/
 /*@-compdef -compmempass -dependenttrans -retalias @*/
 /*-
@@ -1186,3 +1187,4 @@ bail:
 }
 /*@=compdef =compmempass =dependenttrans =retalias @*/
 /*@=sysunrecog =noeffectuncon =nullpass =sizeoftype =unrecog =usereleased @*/
+/*@=boundsread@*/
index a5276b6..4610555 100644 (file)
@@ -1,3 +1,4 @@
+/*@-boundsread@*/
 /** \ingroup rpmrc rpmio
  * \file rpmio/macro.c
  */
@@ -2043,3 +2044,4 @@ main(int argc, char *argv[])
 }
 #endif /* EVAL_MACROS */
 #endif /* DEBUG_MACROS */
+/*@=boundsread@*/
index ff60004..3ae20a5 100644 (file)
@@ -743,6 +743,7 @@ static int mygethostbyname(const char * host,
 }
 #endif
 
+/*@-boundsread@*/
 /*@-compdef@*/ /* FIX: address->s_addr undefined. */
 static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
        /*@globals errno @*/
@@ -765,6 +766,7 @@ static int getHostAddress(const char * host, /*@out@*/ struct in_addr * address)
     return 0;
 }
 /*@=compdef@*/
+/*@=boundsread@*/
 
 static int tcpConnect(FD_t ctrl, const char * host, int port)
        /*@globals fileSystem @*/
@@ -1302,10 +1304,12 @@ int ufdCopy(FD_t sfd, FD_t tfd)
     int notifier = -1;
 
     if (urlNotify) {
+/*@-boundsread@*/
        /*@-noeffectuncon @*/ /* FIX: check rc */
        (void)(*urlNotify) (NULL, RPMCALLBACK_INST_OPEN_FILE,
                0, 0, NULL, urlNotifyData);
        /*@=noeffectuncon @*/
+/*@=boundsread@*/
     }
     
     while (1) {
@@ -1329,10 +1333,12 @@ int ufdCopy(FD_t sfd, FD_t tfd)
        if (urlNotify && urlNotifyCount > 0) {
            int n = itemsCopied/urlNotifyCount;
            if (n != notifier) {
+/*@-boundsread@*/
                /*@-noeffectuncon @*/ /* FIX: check rc */
                (void)(*urlNotify) (NULL, RPMCALLBACK_INST_PROGRESS,
                        itemsCopied, 0, NULL, urlNotifyData);
                /*@=noeffectuncon @*/
+/*@=boundsread@*/
                notifier = n;
            }
        }
@@ -1344,10 +1350,12 @@ int ufdCopy(FD_t sfd, FD_t tfd)
 /*@=modfilesys@*/
 
     if (urlNotify) {
+/*@-boundsread@*/
        /*@-noeffectuncon @*/ /* FIX: check rc */
        (void)(*urlNotify) (NULL, RPMCALLBACK_INST_OPEN_FILE,
                itemsCopied, itemsCopied, NULL, urlNotifyData);
        /*@=noeffectuncon @*/
+/*@=boundsread@*/
     }
     
     return rc;
@@ -2150,7 +2158,9 @@ static inline /*@dependent@*/ /*@null@*/ void * gzdFileno(FD_t fd)
 
     FDSANE(fd);
     for (i = fd->nfps; i >= 0; i--) {
+/*@-boundsread@*/
        FDSTACK_t * fps = &fd->fps[i];
+/*@=boundsread@*/
        if (fps->io != gzdio)
            continue;
        rc = fps->fp;
@@ -2407,7 +2417,9 @@ static inline /*@dependent@*/ void * bzdFileno(FD_t fd)
 
     FDSANE(fd);
     for (i = fd->nfps; i >= 0; i--) {
+/*@-boundsread@*/
        FDSTACK_t * fps = &fd->fps[i];
+/*@=boundsread@*/
        if (fps->io != bzdio)
            continue;
        rc = fps->fp;
@@ -2655,9 +2667,11 @@ DBGIO(fd, (stderr, "==> Fwrite(%p,%u,%u,%p) %s\n", buf, (unsigned)size, (unsigne
 /*@=modfilesys@*/
 
     if (fdGetIo(fd) == fpio) {
+/*@-boundsread@*/
        /*@+voidabstract -nullpass@*/
        rc = fwrite(buf, size, nmemb, fdGetFILE(fd));
        /*@=voidabstract =nullpass@*/
+/*@=boundsread@*/
        return rc;
     }
 
@@ -2715,7 +2729,9 @@ DBGIO(fd, (stderr, "==> Fclose(%p) %s\n", (fd ? fd : NULL), fdbg(fd)));
     fd = fdLink(fd, "Fclose");
     /*@-branchstate@*/
     while (fd->nfps >= 0) {
+/*@-boundsread@*/
        FDSTACK_t * fps = &fd->fps[fd->nfps];
+/*@=boundsread@*/
        
        if (fps->io == fpio) {
            FILE *fp;
@@ -2981,6 +2997,7 @@ FD_t Fopen(const char *path, const char *fmode)
     if (path == NULL || fmode == NULL)
        return NULL;
 
+    stdio[0] = '\0';
     cvtfmode(fmode, stdio, sizeof(stdio), other, sizeof(other), &end, &flags);
     if (stdio[0] == '\0')
        return NULL;
@@ -3073,7 +3090,9 @@ int Ferror(FD_t fd)
 
     if (fd == NULL) return -1;
     for (i = fd->nfps; rc == 0 && i >= 0; i--) {
+/*@-boundsread@*/
        FDSTACK_t * fps = &fd->fps[i];
+/*@=boundsread@*/
        int ec;
        
        if (fps->io == fpio) {
@@ -3107,7 +3126,9 @@ int Fileno(FD_t fd)
     int i, rc = -1;
 
     for (i = fd->nfps ; rc == -1 && i >= 0; i--) {
+/*@-boundsread@*/
        rc = fd->fps[i].fdno;
+/*@=boundsread@*/
     }
 /*@-modfilesys@*/
 DBGIO(fd, (stderr, "==> Fileno(%p) rc %d %s\n", (fd ? fd : NULL), rc, fdbg(fd)));
index 63b17cb..61d8af4 100644 (file)
@@ -1,3 +1,4 @@
+/*@-boundsread@*/
 /** \ingroup rpmio
  * \file rpmio/rpmlog.c
  */
@@ -261,3 +262,4 @@ rpmlogCallback rpmErrorSetCallback(rpmlogCallback cb)
 {
     return rpmlogSetCallback(cb);
 }
+/*@=boundsread@*/
index 6d42293..4a58574 100644 (file)
@@ -1,3 +1,4 @@
+/*@-boundsread@*/
 /** \ingroup rpmio signature
  * \file rpmio/rpmpgp.c
  * Routines to handle RFC-2440 detached signatures.
@@ -1241,3 +1242,4 @@ exit:
     return ec;
 }
 /*@=boundswrite@*/
+/*@=boundsread@*/
index 939d061..0eeca5a 100644 (file)
@@ -297,6 +297,7 @@ vfs_split_text (char *p)
 }
 /*@=boundswrite@*/
 
+/*@-boundsread@*/
 static int
 is_num (int idx)
        /*@*/
@@ -305,7 +306,9 @@ is_num (int idx)
        return 0;
     return 1;
 }
+/*@=boundsread@*/
 
+/*@-boundsread@*/
 static int
 is_dos_date(/*@null@*/ const char *str)
        /*@*/
@@ -315,6 +318,7 @@ is_dos_date(/*@null@*/ const char *str)
        return 1;
     return 0;
 }
+/*@=boundsread@*/
 
 static int
 is_week (/*@null@*/ const char * str, /*@out@*/ struct tm * tim)
@@ -1251,8 +1255,10 @@ static struct dirent * ftpReaddir(DIR * dir)
     dt = (char *) (av + (ac + 1));
     i = dir->offset + 1;
 
+/*@-boundsread@*/
     if (i < 0 || i >= ac || av[i] == NULL)
        return NULL;
+/*@=boundsread@*/
 
     dir->offset = i;
 
@@ -1260,7 +1266,9 @@ static struct dirent * ftpReaddir(DIR * dir)
     dp->d_ino = i + 1;         /* W2DO? */
     dp->d_off = 0;             /* W2DO? */
     dp->d_reclen = 0;          /* W2DO? */
+/*@-boundsread@*/
     dp->d_type = dt[i];
+/*@=boundsread@*/
 
     strncpy(dp->d_name, av[i], sizeof(dp->d_name));
 /*@+voidabstract@*/
index b555d59..0f06eb2 100644 (file)
@@ -139,8 +139,11 @@ urltype    urlIsURL(const char * url)
  * @retval pathp       pointer to path component of url
  * @return             type of url
  */
+/*@-incondefs@*/
 urltype        urlPath(const char * url, /*@out@*/ const char ** pathp)
+       /*@ensures maxSet(*pathp) == 0 /\ maxRead(*pathp) == 0 @*/
        /*@modifies *pathp @*/;
+/*@=incondefs@*/
 
 /**
  * Parse URL string into a control structure.
index 669522b..7743650 100644 (file)
@@ -17,8 +17,10 @@ int xstrcasecmp(const char * s1, const char * s2)
 
   do
     {
+/*@-boundsread@*/
       c1 = xtolower (*p1++);
       c2 = xtolower (*p2++);
+/*@=boundsread@*/
       if (c1 == '\0')
         break;
     }
@@ -38,8 +40,10 @@ int xstrncasecmp(const char *s1, const char *s2, size_t n)
 
   do
     {
+/*@-boundsread@*/
       c1 = xtolower (*p1++);
       c2 = xtolower (*p2++);
+/*@=boundsread@*/
       if (c1 == '\0' || c1 != c2)
        break;
     } while (--n > 0);
index 2a39b86..cbb3eba 100644 (file)
@@ -350,6 +350,7 @@ urltype urlIsURL(const char * url)
 {
     struct urlstring *us;
 
+/*@-boundsread@*/
     if (url && *url) {
        for (us = urlstrings; us->leadin != NULL; us++) {
            if (strncmp(url, us->leadin, strlen(us->leadin)))
@@ -357,6 +358,7 @@ urltype urlIsURL(const char * url)
            return us->ret;
        }
     }
+/*@=boundsread@*/
 
     return URL_IS_UNKNOWN;
 }
@@ -403,7 +405,7 @@ urltype urlPath(const char * url, const char ** pathp)
  * Split URL into components. The URL can look like
  *     service://user:password@host:port/path
  */
-/*@-boundswrite@*/
+/*@-bounds@*/
 /*@-modfilesys@*/
 int urlSplit(const char * url, urlinfo *uret)
 {
@@ -500,7 +502,7 @@ int urlSplit(const char * url, urlinfo *uret)
     return 0;
 }
 /*@=modfilesys@*/
-/*@=boundswrite@*/
+/*@=bounds@*/
 
 int urlGetFile(const char * url, const char * dest)
 {
diff --git a/rpmqv.c b/rpmqv.c
index 920ae0b..6b9cfb3 100755 (executable)
--- a/rpmqv.c
+++ b/rpmqv.c
@@ -279,6 +279,7 @@ static void printUsage(void)
 
 }
 
+/*@-bounds@*/ /* LCL: segfault */
 /*@-mods@*/ /* FIX: shrug */
 #if !defined(__GLIBC__) && !defined(__LCLINT__)
 int main(int argc, const char ** argv, /*@unused@*/ char ** envp)
@@ -1237,3 +1238,4 @@ exit:
     /*@=globstate@*/
 }
 /*@=mods@*/
+/*@=bounds@*/