spliddles.
authorjbj <devnull@localhost>
Thu, 1 May 2003 19:55:27 +0000 (19:55 +0000)
committerjbj <devnull@localhost>
Thu, 1 May 2003 19:55:27 +0000 (19:55 +0000)
CVS patchset: 6801
CVS date: 2003/05/01 19:55:27

30 files changed:
beecrypt/.splintrc
beecrypt/aes.c
beecrypt/base64.c
beecrypt/beecrypt.c
beecrypt/beecrypt.h
beecrypt/blockmode.c
beecrypt/blockpad.c
beecrypt/blockpad.h
beecrypt/dhaes.c
beecrypt/dhaes.h
beecrypt/dldp.h
beecrypt/dlkp.h
beecrypt/dlpk.h
beecrypt/dlsvdp-dh.h
beecrypt/endianness.c
beecrypt/endianness.h
beecrypt/entropy.c
beecrypt/fips186.h
beecrypt/hmac.h
beecrypt/md5.c
beecrypt/mp.c
beecrypt/mp.h
beecrypt/mpnumber.c
beecrypt/mtprng.c
beecrypt/mtprng.h
beecrypt/rsa.h
beecrypt/rsakp.c
beecrypt/sha1.h
beecrypt/tests/beetest.c
beecrypt/types.h.in

index 64c80d5..a358762 100644 (file)
 +strict                        # lclint level
 
 # --- in progress
-#+bounds
++likelybounds
 -bufferoverflowhigh
 -aliasunique
 -mayaliasunique
+-compdef               # 83
+-noeffectuncon         # 11
+
 -elseifcomplete
--exportheader
--exportheadervar
--exportlocal
--fcnuse
--typeuse
--varuse
--compdef
--noeffectuncon
 -whileempty
 
 # --- not-yet at strict level
--exportconst           # 4
+-exportconst           # 3
 -exportfcn             # 308
 -exporttype            # 53
 -exportvar             # 14
 
 -ptrarith              # 212
 
--compdestroy           # 6
--mustdefine            # 49
-
--bitwisesigned         # 77
--strictops             # 48
--sizeoftype            # 22
+-mustdefine            # 54
+-strictops             # 23
 
 -impcheckedstrictglobs
 -impcheckedstrictstatics
@@ -60,6 +51,7 @@
 -ansi-reserved         # goofy
 
 # --- not-yet at standard level
--boolops               # 49
+-boolops               # 53
 -predboolint           # 238
--type                  # 965
++matchanyintegral
+-type                  # 150
index 837c6db..97b5e0a 100644 (file)
@@ -784,10 +784,10 @@ int aesSetup(aesParam* ap, const byte* key, size_t keybits, cipherOperation op)
                        {
                                t = rk[3];
                                rk[4] = rk[0] ^
-                                       (_ae4[(t >> 16) & 0xff] & 0xff000000) ^
-                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000) ^
-                                       (_ae4[(t      ) & 0xff] & 0x0000ff00) ^
-                                       (_ae4[(t >> 24)       ] & 0x000000ff) ^
+                                       (_ae4[(t >> 16) & 0xff] & 0xff000000U) ^
+                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000U) ^
+                                       (_ae4[(t      ) & 0xff] & 0x0000ff00U) ^
+                                       (_ae4[(t >> 24)       ] & 0x000000ffU) ^
                                         _arc[i];
                                rk[5] = rk[1] ^ rk[4];
                                rk[6] = rk[2] ^ rk[5];
@@ -803,10 +803,10 @@ int aesSetup(aesParam* ap, const byte* key, size_t keybits, cipherOperation op)
                        {
                                t = rk[5];
                                rk[ 6] = rk[0] ^
-                                       (_ae4[(t >> 16) & 0xff] & 0xff000000) ^
-                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000) ^
-                                       (_ae4[(t      ) & 0xff] & 0x0000ff00) ^
-                                       (_ae4[(t >> 24)       ] & 0x000000ff) ^
+                                       (_ae4[(t >> 16) & 0xff] & 0xff000000U) ^
+                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000U) ^
+                                       (_ae4[(t      ) & 0xff] & 0x0000ff00U) ^
+                                       (_ae4[(t >> 24)       ] & 0x000000ffU) ^
                                         _arc[i];
                                rk[ 7] = rk[1] ^ rk[ 6];
                                rk[ 8] = rk[2] ^ rk[ 7];
@@ -824,10 +824,10 @@ int aesSetup(aesParam* ap, const byte* key, size_t keybits, cipherOperation op)
                        {
                                t = rk[7];
                                rk[8] = rk[0] ^
-                                       (_ae4[(t >> 16) & 0xff] & 0xff000000) ^
-                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000) ^
-                                       (_ae4[(t      ) & 0xff] & 0x0000ff00) ^
-                                       (_ae4[(t >> 24)       ] & 0x000000ff) ^
+                                       (_ae4[(t >> 16) & 0xff] & 0xff000000U) ^
+                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000U) ^
+                                       (_ae4[(t      ) & 0xff] & 0x0000ff00U) ^
+                                       (_ae4[(t >> 24)       ] & 0x000000ffU) ^
                                         _arc[i];
                                rk[ 9] = rk[1] ^ rk[ 8];
                                rk[10] = rk[2] ^ rk[ 9];
@@ -836,10 +836,10 @@ int aesSetup(aesParam* ap, const byte* key, size_t keybits, cipherOperation op)
                                        break;
                                t = rk[7];
                                rk[12] = rk[4] ^
-                                       (_ae4[(t >> 16) & 0xff] & 0xff000000) ^
-                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000) ^
-                                       (_ae4[(t      ) & 0xff] & 0x0000ff00) ^
-                                       (_ae4[(t >> 24)       ] & 0x000000ff);
+                                       (_ae4[(t >> 16) & 0xff] & 0xff000000U) ^
+                                       (_ae4[(t >>  8) & 0xff] & 0x00ff0000U) ^
+                                       (_ae4[(t      ) & 0xff] & 0x0000ff00U) ^
+                                       (_ae4[(t >> 24)       ] & 0x000000ffU);
                                rk[13] = rk[5] ^ rk[12];
                                rk[14] = rk[6] ^ rk[13];
                                rk[15] = rk[7] ^ rk[14];
@@ -954,28 +954,28 @@ int aesSetIV(aesParam* ap, const byte* iv)
 
 #define elr() \
        s0 = \
-               (_ae4[(t0 >> 24)       ] & 0xff000000) ^ \
-               (_ae4[(t1 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ae4[(t2 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ae4[(t3      ) & 0xff] & 0x000000ff) ^ \
+               (_ae4[(t0 >> 24)       ] & 0xff000000U) ^ \
+               (_ae4[(t1 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ae4[(t2 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ae4[(t3      ) & 0xff] & 0x000000ffU) ^ \
                rk[0]; \
        s1 = \
-               (_ae4[(t1 >> 24)       ] & 0xff000000) ^ \
-               (_ae4[(t2 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ae4[(t3 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ae4[(t0      ) & 0xff] & 0x000000ff) ^ \
+               (_ae4[(t1 >> 24)       ] & 0xff000000U) ^ \
+               (_ae4[(t2 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ae4[(t3 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ae4[(t0      ) & 0xff] & 0x000000ffU) ^ \
                rk[1]; \
        s2 = \
-               (_ae4[(t2 >> 24)       ] & 0xff000000) ^ \
-               (_ae4[(t3 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ae4[(t0 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ae4[(t1      ) & 0xff] & 0x000000ff) ^ \
+               (_ae4[(t2 >> 24)       ] & 0xff000000U) ^ \
+               (_ae4[(t3 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ae4[(t0 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ae4[(t1      ) & 0xff] & 0x000000ffU) ^ \
                rk[2]; \
        s3 = \
-               (_ae4[(t3 >> 24)       ] & 0xff000000) ^ \
-               (_ae4[(t0 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ae4[(t1 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ae4[(t2      ) & 0xff] & 0x000000ff) ^ \
+               (_ae4[(t3 >> 24)       ] & 0xff000000U) ^ \
+               (_ae4[(t0 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ae4[(t1 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ae4[(t2      ) & 0xff] & 0x000000ffU) ^ \
                rk[3];
 
 #ifndef ASM_AESENCRYPT
@@ -1092,28 +1092,28 @@ int aesEncrypt(aesParam* ap, uint32_t* dst, const uint32_t* src)
 
 #define dlr() \
        s0 = \
-               (_ad4[(t0 >> 24)       ] & 0xff000000) ^ \
-               (_ad4[(t3 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ad4[(t2 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ad4[(t1      ) & 0xff] & 0x000000ff) ^ \
+               (_ad4[(t0 >> 24)       ] & 0xff000000U) ^ \
+               (_ad4[(t3 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ad4[(t2 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ad4[(t1      ) & 0xff] & 0x000000ffU) ^ \
                rk[0]; \
        s1 = \
-               (_ad4[(t1 >> 24)       ] & 0xff000000) ^ \
-               (_ad4[(t0 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ad4[(t3 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ad4[(t2      ) & 0xff] & 0x000000ff) ^ \
+               (_ad4[(t1 >> 24)       ] & 0xff000000U) ^ \
+               (_ad4[(t0 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ad4[(t3 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ad4[(t2      ) & 0xff] & 0x000000ffU) ^ \
                rk[1]; \
        s2 = \
-               (_ad4[(t2 >> 24)       ] & 0xff000000) ^ \
-               (_ad4[(t1 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ad4[(t0 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ad4[(t3      ) & 0xff] & 0x000000ff) ^ \
+               (_ad4[(t2 >> 24)       ] & 0xff000000U) ^ \
+               (_ad4[(t1 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ad4[(t0 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ad4[(t3      ) & 0xff] & 0x000000ffU) ^ \
                rk[2]; \
        s3 = \
-               (_ad4[(t3 >> 24)       ] & 0xff000000) ^ \
-               (_ad4[(t2 >> 16) & 0xff] & 0x00ff0000) ^ \
-               (_ad4[(t1 >>  8) & 0xff] & 0x0000ff00) ^ \
-               (_ad4[(t0      ) & 0xff] & 0x000000ff) ^ \
+               (_ad4[(t3 >> 24)       ] & 0xff000000U) ^ \
+               (_ad4[(t2 >> 16) & 0xff] & 0x00ff0000U) ^ \
+               (_ad4[(t1 >>  8) & 0xff] & 0x0000ff00U) ^ \
+               (_ad4[(t0      ) & 0xff] & 0x000000ffU) ^ \
                rk[3];
 
 #ifndef ASM_AESDECRYPT
index 306ed3d..0843754 100644 (file)
@@ -402,7 +402,7 @@ fprintf(stderr, "--- b64decode %c(%02x) %02x\n", *t, (unsigned)(*t & 0xff), (uns
        }
     }
     
-    if (ns & 0x3)      return 2;
+    if (((unsigned)ns) & 0x3)  return 2;
 
     nt = (ns / 4) * 3;
     t = te = malloc(nt + 1);
index 6ce1f90..aaabf96 100644 (file)
@@ -322,8 +322,6 @@ int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
                return -1;
 
        ctxt->algo = hash;
-       if (ctxt->param)        /* XXX error? */
-               free(ctxt->param);
        ctxt->param = (hashFunctionParam*) calloc(hash->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -577,8 +575,6 @@ int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHash
                return -1;
 
        ctxt->algo = mac;
-       if (ctxt->param)        /* XXX error? */
-               free(ctxt->param);
        ctxt->param = (keyedHashFunctionParam*) calloc(mac->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -849,8 +845,6 @@ int blockCipherContextInit(blockCipherContext* ctxt, const blockCipher* ciph)
                return -1;
 
        ctxt->algo = ciph;
-       if (ctxt->param)        /* XXX error? */
-               free(ctxt->param);
        ctxt->param = (blockCipherParam*) calloc(ciph->paramsize, 1);
        ctxt->op = NOCRYPT;
 
index b709581..86f8813 100644 (file)
@@ -253,7 +253,8 @@ extern "C" {
  * Initialize a randomGenerator instance.
  */
 BEECRYPTAPI /*@unused@*/
-int randomGeneratorContextInit(randomGeneratorContext* ctxt, /*@observer@*/ /*@dependent@*/ const randomGenerator* rng)
+int randomGeneratorContextInit(/*@special@*/ /*@null@*/ randomGeneratorContext* ctxt, /*@observer@*/ /*@dependent@*/ /*@null@*/ const randomGenerator* rng)
+       /*@defines ctxt->rng, ctxt->param @*/
        /*@modifies ctxt->rng, ctxt->param @*/;
 
 /** \ingroup PRNG_m
@@ -400,8 +401,9 @@ extern "C" {
  * Initialize a hashFunction instance.
  */
 BEECRYPTAPI
-int hashFunctionContextInit(hashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const hashFunction* hash)
-       /*@modifies ctxt->algo, ctxt->param */;
+int hashFunctionContextInit(/*@special@*/ hashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const hashFunction* hash)
+       /*@defines ctxt->algo, ctxt->param @*/
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup HASH_m
  * Destroy a hashFunction instance.
@@ -409,49 +411,51 @@ int hashFunctionContextInit(hashFunctionContext* ctxt, /*@observer@*/ /*@depende
 BEECRYPTAPI
 int hashFunctionContextFree(/*@special@*/ hashFunctionContext* ctxt)
        /*@releases ctxt->param @*/
-       /*@modifies ctxt->algo, ctxt->param */;
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI
 int hashFunctionContextReset(hashFunctionContext* ctxt)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI /*@unused@*/
 int hashFunctionContextUpdate(hashFunctionContext* ctxt, const byte* data, size_t size)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI /*@unused@*/
 int hashFunctionContextUpdateMC(hashFunctionContext* ctxt, const memchunk* m)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI
 int hashFunctionContextUpdateMP(hashFunctionContext* ctxt, const mpnumber* n)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI
 int hashFunctionContextDigest(hashFunctionContext* ctxt, byte* digest)
-       /*@modifies ctxt, *digest */;
+       /*@modifies ctxt, *digest @*/;
 
 /** \ingroup HASH_m
  */
+/*@-exportlocal@*/
 BEECRYPTAPI
 int hashFunctionContextDigestMP(hashFunctionContext* ctxt, mpnumber* d)
-       /*@modifies ctxt, *d */;
+       /*@modifies ctxt, *d @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_m
  */
 BEECRYPTAPI /*@unused@*/
 int hashFunctionContextDigestMatch(hashFunctionContext* ctxt, const mpnumber* d)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 #ifdef __cplusplus
 }
@@ -602,7 +606,8 @@ extern "C" {
  * Initialize a keyedHashFunction instance.
  */
 BEECRYPTAPI
-int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const keyedHashFunction* mac)
+int keyedHashFunctionContextInit(/*@special@*/ keyedHashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const keyedHashFunction* mac)
+       /*@defines ctxt->algo, ctxt->param @*/
        /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup HMAC_m
@@ -646,7 +651,7 @@ int keyedHashFunctionContextUpdateMP(keyedHashFunctionContext* ctxt, const mpnum
 
 /** \ingroup HMAC_m
  */
-BEECRYPTAPI
+BEECRYPTAPI /*@unused@*/
 int keyedHashFunctionContextDigest(keyedHashFunctionContext* ctxt, byte* digest)
        /*@modifies ctxt, *digest @*/;
 
@@ -681,34 +686,6 @@ typedef enum
 } cipherOperation;
 
 /** \ingroup BC_m
- * @param param                blockcipher parameters
- * @param size         no. of ints
- * @retval dst         ciphertext block
- * @param src          plaintext block
- * @return             0 on success, -1 on failure
- */
-typedef int (*blockModeEncrypt) (blockCipherParam* param, int count, byte* dst, const byte* src)
-       /*@modifies *param, *dst @*/;
-
-/** \ingroup BC_m
- * @param param                blockcipher parameters
- * @param size         no. of ints
- * @retval dst         plainttext block
- * @param src          ciphertext block
- * @return             0 on success, -1 on failure
- */
-typedef int (*blockModeDecrypt) (blockCipherParam* param, int count, byte* dst, const byte* src)
-       /*@modifies *param, *dst @*/;
-
-/** \ingroup BC_m
- */
-typedef struct
-{
-       const blockModeEncrypt  encrypt;
-       const blockModeDecrypt  decrypt;
-} blockMode;
-
-/** \ingroup BC_m
  * Setup the blockcipher parameters with the given secret key for either
  * encryption or decryption.
  *
@@ -845,7 +822,8 @@ extern "C" {
  * Initialize a blockCipher instance.
  */
 BEECRYPTAPI
-int blockCipherContextInit(blockCipherContext* ctxt, /*@observer@*/ /*@dependent@*/ const blockCipher* ciph)
+int blockCipherContextInit(/*@special@*/ blockCipherContext* ctxt, /*@observer@*/ /*@dependent@*/ const blockCipher* ciph)
+       /*@defines ctxt->algo, ctxt->param, ctxt->op @*/
        /*@modifies ctxt->algo, ctxt->param, ctxt->op @*/;
 
 /** \ingroup BC_m
index 07c3ce5..66c1971 100644 (file)
@@ -84,6 +84,7 @@ int blockEncryptCBC(const blockCipher* bc, blockCipherParam* bp, uint32_t* dst,
 
                nblocks--;
 
+/*@-usedef@*/ /* LCL: dst is initialized. */
                while (nblocks > 0)
                {
                        for (i = 0; i < blockwords; i++)
@@ -99,6 +100,7 @@ int blockEncryptCBC(const blockCipher* bc, blockCipherParam* bp, uint32_t* dst,
 
                for (i = 0; i < blockwords; i++)
                        fdback[i] = dst[i-blockwords];
+/*@=usedef@*/
        }
        return 0;
 }
@@ -108,7 +110,7 @@ int blockDecryptCBC(const blockCipher* bc, blockCipherParam* bp, uint32_t* dst,
        /* assumes that every blockcipher's blocksize is a multiple of 32 bits */
        register int blockwords = bc->blocksize >> 2;
        register uint32_t* fdback = bc->getfb(bp);
-       register uint32_t* buf = (uint32_t*) malloc(blockwords * sizeof(uint32_t));
+       register uint32_t* buf = (uint32_t*) malloc(blockwords * sizeof(*buf));
 
        if (buf)
        {
@@ -122,7 +124,9 @@ int blockDecryptCBC(const blockCipher* bc, blockCipherParam* bp, uint32_t* dst,
                        for (i = 0; i < blockwords; i++)
                        {
                                tmp = src[i];
+/*@-usedef@*/ /* LCL: buf is initialized. */
                                dst[i] = buf[i] ^ fdback[i];
+/*@-usedef@*/
                                fdback[i] = tmp;
                        }
 
index 2f98a34..eb8e1b8 100644 (file)
@@ -53,9 +53,11 @@ memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
                byte padvalue;
                int i;
 
+/*@-usedef@*/ /* LCL: tmp->{data,size} not initialized? */
                if (tmp->data == (byte*) 0)
                        return (memchunk*) 0;
                padvalue = tmp->data[tmp->size - 1];
+/*@=usedef@*/
                if (padvalue > blockbytes)
                        return (memchunk*) 0;
 
index f8ec587..e5a0904 100644 (file)
@@ -51,7 +51,7 @@ memchunk* pkcs5Pad  (int blockbytes, /*@only@*/ /*@null@*/ memchunk* tmp)
 BEECRYPTAPI /*@only@*/ /*@null@*/
 memchunk* pkcs5Unpad(int blockbytes,
                /*@returned@*/ /*@null@*/ /*@out@*/ memchunk* tmp)
-       /*@modifies tmp */;
+       /*@modifies tmp @*/;
 
 /**
  * Copy/enlarge buffer to boundary.
index ecc4a0b..ed1ec5e 100644 (file)
@@ -227,7 +227,7 @@ static int dhaes_pContextSetup(dhaes_pContext* ctxt, const mpnumber* privkey, co
        if (ctxt->hash.algo->digestsize > 0)
        {
                byte* mackey = digest;
-               byte* cipherkey = digest + ((ctxt->mackeybits + 7) >> 3);
+               byte* cipherkey = digest + ((ctxt->mackeybits + 7U) >> 3);
 
                if ((rc = keyedHashFunctionContextSetup(&ctxt->mac, mackey, ctxt->mackeybits)))
                        goto setup_end;
index 4cdc1d3..e2f96c4 100644 (file)
@@ -71,39 +71,40 @@ int dhaes_pUsable(const dhaes_pParameters* params)
  */
 /*@-exportlocal@*/
 BEECRYPTAPI
-int dhaes_pContextInit       (dhaes_pContext* ctxt, const dhaes_pParameters* params)
-       /*@modifies ctxt */;
+int dhaes_pContextInit       (/*@special@*/ dhaes_pContext* ctxt, const dhaes_pParameters* params)
+       /*@defines ctxt->hash, ctxt->cipher, ctxt->mac @*/
+       /*@modifies ctxt @*/;
 /*@=exportlocal@*/
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dhaes_pContextInitDecrypt(dhaes_pContext* ctxt, const dhaes_pParameters* params, const mpnumber* pri)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dhaes_pContextInitEncrypt(dhaes_pContext* ctxt, const dhaes_pParameters* params, const mpnumber* pub)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dhaes_pContextFree       (/*@only@*/ dhaes_pContext* ctxt)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 /**
  */
 BEECRYPTAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* dhaes_pContextEncrypt(dhaes_pContext* ctxt,       mpnumber* ephemeralPublicKey,       mpnumber* mac, const memchunk* cleartext, randomGeneratorContext* rng)
-       /*@modifies ctxt, ephemeralPublicKey, mac, rng */;
+       /*@modifies ctxt, ephemeralPublicKey, mac, rng @*/;
 
 /**
  */
 BEECRYPTAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* dhaes_pContextDecrypt(dhaes_pContext* ctxt, const mpnumber* ephemeralPublicKey, const mpnumber* mac, const memchunk* ciphertext)
-       /*@modifies ctxt */;
+       /*@modifies ctxt @*/;
 
 #ifdef __cplusplus
 }
index 6d1d608..71635a1 100644 (file)
@@ -117,7 +117,8 @@ int  dldp_pEqual(const dldp_p* a, const dldp_p* b)
 /**
  */
 BEECRYPTAPI /*@unused@*/
-int dldp_pgoqMake(dldp_p* dp, randomGeneratorContext* rgc, size_t pbits, size_t qbits, int cofactor)
+int dldp_pgoqMake(/*@special@*/ dldp_p* dp, randomGeneratorContext* rgc, size_t pbits, size_t qbits, int cofactor)
+       /*@defines dp->p, dp->q, dp->n @*/
        /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
index 7755afb..9e7557e 100644 (file)
@@ -45,25 +45,25 @@ extern "C" {
  */
 BEECRYPTAPI /*@unused@*/
 int dlkp_pPair(dlkp_p* kp, randomGeneratorContext* rgc, const dldp_p* param)
-       /*@modifies kp, rgc */;
+       /*@modifies kp, rgc @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dlkp_pInit(dlkp_p* kp)
-       /*@modifies kp */;
+       /*@modifies kp @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dlkp_pFree(dlkp_p* kp)
-       /*@modifies kp */;
+       /*@modifies kp @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dlkp_pCopy(dlkp_p* dst, const dlkp_p* src)
-       /*@modifies dst */;
+       /*@modifies dst @*/;
 
 #ifdef __cplusplus
 }
index 97039b0..8726222 100644 (file)
@@ -44,19 +44,19 @@ extern "C" {
  */
 BEECRYPTAPI /*@unused@*/
 int dlpk_pInit(dlpk_p* pk)
-       /*@modifies pk */;
+       /*@modifies pk @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dlpk_pFree(dlpk_p* pk)
-       /*@modifies pk */;
+       /*@modifies pk @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int dlpk_pCopy(dlpk_p* dst, const dlpk_p* src)
-       /*@modifies dst */;
+       /*@modifies dst @*/;
 
 /**
  */
index 3e7594e..7b486a7 100644 (file)
@@ -47,7 +47,7 @@ extern "C" {
  */
 BEECRYPTAPI
 int dlsvdp_pDHSecret(const dldp_p* dp, const mpnumber* x, const mpnumber* y, mpnumber* s)
-       /*@modifies s */;
+       /*@modifies s @*/;
 
 #ifdef __cplusplus
 }
index 8ff0187..c280fc6 100644 (file)
@@ -26,7 +26,7 @@
 #include "endianness.h"
 #include "debug.h"
 
-/*@-shiftimplementation@*/
+/*@-bitwisesigned -shiftimplementation@*/
 int16_t swap16(int16_t n)
 {
        return (    ((n & 0xff) << 8) |
@@ -77,7 +77,7 @@ int64_t swap64(int64_t n)
                                ((n & 0xff00000000000000L) >> 56) );
        #endif
 }
-/*@=shiftimplementation@*/
+/*@=bitwisesigned =shiftimplementation@*/
 
 int encodeByte(javabyte b, byte *data)
 {
index eda0496..13ab1d1 100644 (file)
@@ -132,117 +132,117 @@ extern "C" {
  */
 BEECRYPTAPI /*@unused@*/
 int encodeByte(javabyte b, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeShort(javashort s, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeInt(javaint i, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeLong(javalong l, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeChar(javachar c, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI
 int encodeInts(const javaint* i, /*@out@*/ byte* data, int count)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeIntsPartial(const javaint* i, /*@out@*/ byte* data, int bytecount)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeIntsPartialPad(const javaint* i, byte* data, int bytecount, byte padvalue)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int encodeChars(const javachar* c, /*@out@*/ byte* data, int count)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeByte(/*@out@*/ javabyte* b, const byte* data)
-       /*@modifies b */;
+       /*@modifies b @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeShort(/*@out@*/ javashort* s, const byte* data)
-       /*@modifies s */;
+       /*@modifies s @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeInt(/*@out@*/ javaint* i, const byte* data)
-       /*@modifies i */;
+       /*@modifies i @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeLong(/*@out@*/ javalong* l, const byte* data)
-       /*@modifies l */;
+       /*@modifies l @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeChar(/*@out@*/ javachar* c, const byte* data)
-       /*@modifies c */;
+       /*@modifies c @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeInts(/*@out@*/ javaint* i, const byte* data, int count)
-       /*@modifies i */;
+       /*@modifies i @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeIntsPartial(/*@out@*/ javaint* i, const byte* data, int bytecount)
-       /*@modifies i */;
+       /*@modifies i @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int decodeChars(/*@out@*/ javachar* c, const byte* data, int count)
-       /*@modifies c */;
+       /*@modifies c @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int writeByte(javabyte b, FILE* ofp)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int writeShort(javashort s, FILE* ofp)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 
 /**
  */
@@ -250,7 +250,7 @@ int writeShort(javashort s, FILE* ofp)
 BEECRYPTAPI
 int writeInt(javaint i, FILE* ofp)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 /*@=exportlocal@*/
 
 /**
@@ -258,7 +258,7 @@ int writeInt(javaint i, FILE* ofp)
 BEECRYPTAPI /*@unused@*/
 int writeLong(javalong l, FILE* ofp)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 
 /**
  */
@@ -266,7 +266,7 @@ int writeLong(javalong l, FILE* ofp)
 BEECRYPTAPI
 int writeChar(javachar c, FILE* ofp)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 /*@=exportlocal@*/
 
 /**
@@ -274,63 +274,63 @@ int writeChar(javachar c, FILE* ofp)
 BEECRYPTAPI /*@unused@*/
 int writeInts(const javaint* i, FILE* ofp, int count)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int writeChars(const javachar* c, FILE* ofp, int count)
        /*@globals fileSystem @*/
-       /*@modifies ofp, fileSystem */;
+       /*@modifies ofp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readByte(/*@out@*/ javabyte* b, FILE* ifp)
        /*@globals fileSystem @*/
-       /*@modifies b, ifp, fileSystem */;
+       /*@modifies b, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readShort(/*@out@*/ javashort* s, FILE* ifp)
        /*@globals fileSystem @*/
-       /*@modifies s, ifp, fileSystem */;
+       /*@modifies s, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readInt(/*@out@*/ javaint* i, FILE* ifp)
        /*@globals fileSystem @*/
-       /*@modifies i, ifp, fileSystem */;
+       /*@modifies i, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readLong(/*@out@*/ javalong* l, FILE* ifp)
        /*@globals fileSystem @*/
-       /*@modifies l, ifp, fileSystem */;
+       /*@modifies l, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readChar(/*@out@*/ javachar* c, FILE* ifp)
        /*@globals fileSystem @*/
-       /*@modifies c, ifp, fileSystem */;
+       /*@modifies c, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readInts(/*@out@*/ javaint* i, FILE* ifp, int count)
        /*@globals fileSystem @*/
-       /*@modifies i, ifp, fileSystem */;
+       /*@modifies i, ifp, fileSystem @*/;
 
 /**
  */
 BEECRYPTAPI /*@unused@*/
 int readChars(/*@out@*/ javachar* c, FILE* ifp, int count)
        /*@globals fileSystem @*/
-       /*@modifies c, ifp, fileSystem */;
+       /*@modifies c, ifp, fileSystem @*/;
 
 #ifdef __cplusplus
 }
index f7bfee0..9c9ee74 100644 (file)
@@ -57,7 +57,7 @@
 #  include <aio.h>
 #  if defined(__LCLINT__)
 /*@-declundef -exportheader -incondefs -constuse -warnmissingglobs @*/
-       extern int
+       extern int /*@unused@*/
 nanosleep (const struct timespec *__requested_time,
                       /*@out@*/ /*@null@*/ struct timespec *__remaining)
        /*@modifies *__remaining, errno @*/;
@@ -156,7 +156,8 @@ static int entropy_noise_filter(void* sampledata, int samplecount, int samplesiz
        /*@globals errno @*/
        /*@modifies sampledata, errno @*/
 {
-       register int rc = 0, i;
+       register int rc = 0;
+       register unsigned i;
 
        switch (samplesize)
        {
@@ -198,7 +199,7 @@ static int entropy_noise_filter(void* sampledata, int samplecount, int samplesiz
 
                                        for (i = 0; i < samplecount; i++)
                                        {
-                                               if (i & 1)
+                                               if (i & 1U)
                                                {
                                                        if ((samples[i] & 0x1) != 0)
                                                                ones_count_left++;
@@ -339,9 +340,9 @@ static int entropy_noise_filter(void* sampledata, int samplecount, int samplesiz
 static int entropy_noise_gather(HWAVEIN wavein, int samplesize, int channels, int swap, int timeout, byte* data, size_t size)
 #else
 /*@-mustmod@*/ /* data is modified, annotations incorrect */
-static int entropy_noise_gather(int fd, int samplesize, int channels, int swap, int timeout, /*@out@*/ byte* data, size_t size)
+static int entropy_noise_gather(int fd, int samplesize, int channels, int swap, /*@unused@*/ int timeout, /*@out@*/ byte* data, size_t size)
        /*@globals errno, fileSystem @*/
-       /*@modifies data, errno, fileSystem @*/
+       /*@modifies *data, errno, fileSystem @*/
 #endif
 {
        size_t randombits = size << 3;
@@ -963,8 +964,8 @@ static int opendevice(const char *device)
  * @param size
  * @return
  */
-static int entropy_randombits(int fd, int timeout, byte* data, size_t size)
-       /*@*/
+static int entropy_randombits(int fd, /*@unused@*/ int timeout, byte* data, size_t size)
+       /*@modifies *data @*/
 {
        register int rc;
 
@@ -1109,8 +1110,10 @@ static int entropy_ttybits(int fd, byte* data, size_t size)
        tio_set.c_cc[VMIN] = 1;                         /* read 1 tty character at a time */
        tio_set.c_cc[VTIME] = 0;                        /* don't timeout the read */
        /*@=noeffect@*/
+/*@-bitwisesigned@*/
        tio_set.c_iflag |= IGNBRK;                      /* ignore <ctrl>-c */
        tio_set.c_lflag &= ~(ECHO|ICANON);      /* don't echo characters */
+/*@=bitwisesigned@*/
 
        /* change the tty settings, and flush input characters */
        if (tcsetattr(fd, TCSAFLUSH, &tio_set) < 0)
@@ -1329,9 +1332,9 @@ int entropy_dev_dsp(byte *data, size_t size)
                int mask, format, samplesize, stereo, speed, swap;
 
                mask = 0;
-               /*@-shiftimplementation@*/
+               /*@-bitwisesigned -shiftimplementation@*/
                if ((rc = ioctl(dev_dsp_fd, SNDCTL_DSP_GETFMTS, &mask)) < 0)
-               /*@=shiftimplementation@*/
+               /*@=bitwisesigned =shiftimplementation@*/
                {
                        #if HAVE_ERRNO_H
                        perror("ioctl SNDCTL_DSP_GETFMTS failed");
@@ -1341,6 +1344,7 @@ int entropy_dev_dsp(byte *data, size_t size)
                        goto dev_dsp_end;
                }
 
+/*@-bitwisesigned@*/
                #if WORDS_BIGENDIAN
                if (mask & AFMT_S16_BE)
                {
@@ -1383,10 +1387,11 @@ int entropy_dev_dsp(byte *data, size_t size)
 
                        goto dev_dsp_end;
                }
+/*@=bitwisesigned@*/
 
-               /*@-shiftimplementation@*/
+               /*@-bitwisesigned -shiftimplementation@*/
                if ((rc = ioctl(dev_dsp_fd, SNDCTL_DSP_SETFMT, &format)) < 0)
-               /*@=shiftimplementation@*/
+               /*@=bitwisesigned =shiftimplementation@*/
                {
                        #if HAVE_ERRNO_H
                        perror("ioctl SNDCTL_DSP_SETFMT failed");
@@ -1398,14 +1403,14 @@ int entropy_dev_dsp(byte *data, size_t size)
 
                /* the next two commands are not critical */
                stereo = 1;
-               /*@-shiftimplementation@*/
+               /*@-bitwisesigned -shiftimplementation@*/
                (void) ioctl(dev_dsp_fd, SNDCTL_DSP_STEREO, &stereo);
-               /*@=shiftimplementation@*/
+               /*@=bitwisesigned =shiftimplementation@*/
 
                speed = 44100;
-               /*@-shiftimplementation@*/
+               /*@-bitwisesigned -shiftimplementation@*/
                (void) ioctl(dev_dsp_fd, SNDCTL_DSP_SPEED, &speed);
-               /*@=shiftimplementation@*/
+               /*@=bitwisesigned =shiftimplementation@*/
 
                rc = entropy_noise_gather(dev_dsp_fd, samplesize, 2, swap, timeout_env ? atoi(timeout_env) : 1000, data, size);
        }
index ea24540..e78774f 100644 (file)
@@ -90,7 +90,7 @@ extern BEECRYPTAPI const randomGenerator fips186prng;
 /*@-exportlocal@*/
 BEECRYPTAPI
 int fips186Setup  (fips186Param* fp)
-       /*@modifies fp */;
+       /*@modifies fp @*/;
 /*@=exportlocal@*/
 
 /**
@@ -98,7 +98,7 @@ int fips186Setup  (fips186Param* fp)
 /*@-exportlocal@*/
 BEECRYPTAPI
 int fips186Seed   (fips186Param* fp, const byte* data, size_t size)
-       /*@modifies fp */;
+       /*@modifies fp @*/;
 /*@=exportlocal@*/
 
 /**
@@ -106,7 +106,7 @@ int fips186Seed   (fips186Param* fp, const byte* data, size_t size)
 /*@-exportlocal@*/
 BEECRYPTAPI
 int fips186Next   (fips186Param* fp, byte* data, size_t size)
-       /*@modifies fp, data */;
+       /*@modifies fp, data @*/;
 /*@=exportlocal@*/
 
 /**
@@ -114,7 +114,7 @@ int fips186Next   (fips186Param* fp, byte* data, size_t size)
 /*@-exportlocal@*/
 BEECRYPTAPI
 int fips186Cleanup(fips186Param* fp)
-       /*@modifies fp */;
+       /*@modifies fp @*/;
 /*@=exportlocal@*/
 
 #ifdef __cplusplus
index 7e888e8..6d18281 100644 (file)
@@ -39,25 +39,25 @@ extern "C" {
  */
 BEECRYPTAPI
 int hmacSetup (byte* kxi, byte* kxo, const hashFunction* hash, hashFunctionParam* param, const byte* key, size_t keybits)
-       /*@modifies kxi, kxo, param */;
+       /*@modifies kxi, kxo, param @*/;
 
 /**
  */
 BEECRYPTAPI
 int hmacReset (const byte* kxi, const hashFunction* hash, hashFunctionParam* param)
-       /*@modifies param */;
+       /*@modifies param @*/;
 
 /**
  */
 BEECRYPTAPI
 int hmacUpdate(const hashFunction* hash, hashFunctionParam* param, const byte* data, size_t size)
-       /*@modifies param */;
+       /*@modifies param @*/;
 
 /**
  */
 BEECRYPTAPI
 int hmacDigest(const byte* kxo, const hashFunction* hash, hashFunctionParam* param, /*@out@*/ byte* data)
-       /*@modifies data */;
+       /*@modifies data @*/;
 
 #ifdef __cplusplus
 }
index 743a022..d180adb 100644 (file)
@@ -42,8 +42,8 @@ const hashFunction md5 = { "MD5", sizeof(md5Param), 64, 16, (hashFunctionReset)
 
 int md5Reset(register md5Param* p)
 {
-       memcpy(p->h, md5hinit, 4 * sizeof(uint32_t));
-       memset(p->data, 0, 16 * sizeof(uint32_t));
+       memcpy(p->h, md5hinit, sizeof(p->h));
+       memset(p->data, 0, sizeof(p->data));
        #if (MP_WBITS == 64)
        mpzero(1, p->length);
        #elif (MP_WBITS == 32)
index 3e20b6f..d19cc81 100644 (file)
@@ -1169,7 +1169,7 @@ mpw mppndiv(mpw xhi, mpw xlo, mpw y)
 
        while (count--)
        {
-               if (carry | (xhi >= y))
+               if (((unsigned)carry) | (unsigned)(xhi >= y))
                {
                        xhi -= y;
                        result |= 1;
@@ -1180,7 +1180,7 @@ mpw mppndiv(mpw xhi, mpw xlo, mpw y)
                xlo <<= 1;
                result <<= 1;
        }
-       if (carry | (xhi >= y))
+       if (((unsigned)carry) | (unsigned)(xhi >= y))
        {
                xhi -= y;
                result |= 1;
@@ -1272,10 +1272,11 @@ void mpndivmod(mpw* result, size_t xsize, const mpw* xdata, size_t ysize, const
        if (mpge(ysize, result+1, ydata))
        {
                (void) mpsub(ysize, result+1, ydata);
-               *(result++) = 1;
+               *result = 1;
        }
        else
-               *(result++) = 0;
+               *result = 0;
+       result++;
 
        while (qsize--)
        {
index e053dba..c54c70e 100644 (file)
@@ -71,7 +71,7 @@ BEECRYPTAPI /*@unused@*/
 void mpcopy(size_t size, /*@out@*/ mpw* dst, const mpw* src)
        /*@modifies dst @*/;
 #ifndef ASM_MPCOPY
-# define mpcopy(size, dst, src) memcpy(dst, src, MP_WORDS_TO_BYTES(size))
+# define mpcopy(size, dst, src) memcpy(dst, src, MP_WORDS_TO_BYTES((unsigned)size))
 #endif
 
 /**
@@ -80,7 +80,7 @@ BEECRYPTAPI /*@unused@*/
 void mpmove(size_t size, /*@out@*/ mpw* dst, const mpw* src)
        /*@modifies dst @*/;
 #ifndef ASM_MPMOVE
-# define mpmove(size, dst, src) memmove(dst, src, MP_WORDS_TO_BYTES(size))
+# define mpmove(size, dst, src) memmove(dst, src, MP_WORDS_TO_BYTES((unsigned)size))
 #endif
 
 /**
@@ -353,7 +353,7 @@ size_t mpsize(size_t size, const mpw* data)
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 size_t mpbits(size_t size, const mpw* data)
        /*@*/;
 
@@ -365,7 +365,7 @@ size_t mpmszcnt(size_t size, const mpw* data)
 
 /**
  */
-BEECRYPTAPI
+BEECRYPTAPI /*@unused@*/
 size_t mpbitcnt(size_t size, const mpw* data)
        /*@*/;
 
@@ -379,11 +379,9 @@ size_t mplszcnt(size_t size, const mpw* data)
 
 /**
  */
-/*@-exportlocal@*/
 BEECRYPTAPI
 void mplshift(size_t size, mpw* data, size_t count)
        /*@modifies data @*/;
-/*@=exportlocal@*/
 
 /**
  */
@@ -455,9 +453,11 @@ void mpgcd_w(size_t size, const mpw* xdata, const mpw* ydata, /*@out@*/ mpw* res
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+/*@-exportlocal@*/
+BEECRYPTAPI
 mpw mppndiv(mpw xhi, mpw xlo, mpw y)
        /*@*/;
+/*@=exportlocal@*/
 
 /**
  */
@@ -467,7 +467,7 @@ mpw mpnmodw(/*@out@*/ mpw* result, size_t xsize, const mpw* xdata, mpw y, /*@out
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 void mpnmod(/*@out@*/ mpw* result, size_t xsize, const mpw* xdata, size_t ysize, const mpw* ydata, /*@out@*/ mpw* workspace)
        /*@modifies result, workspace @*/;
 
@@ -486,26 +486,26 @@ void mpprint(/*@null@*/ FILE * fp, size_t size, /*@null@*/ const mpw* data)
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 void mpprintln(/*@null@*/ FILE * fp, size_t size, /*@null@*/ const mpw* data)
        /*@globals fileSystem @*/
        /*@modifies *fp, fileSystem @*/;
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 int i2osp(/*@out@*/ byte *osdata, size_t ossize, const mpw* idata, size_t isize)
        /*@modifies osdata @*/;
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 int os2ip(/*@out@*/ mpw *idata, size_t isize, const byte* osdata, size_t ossize)
        /*@modifies idata @*/;
 
 /**
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 int hs2ip(/*@out@*/ mpw* idata, size_t isize, const char* hsdata, size_t hssize)
        /*@modifies idata @*/;
 
index 53962ee..855bfab 100644 (file)
@@ -113,9 +113,12 @@ void mpnset(mpnumber* n, size_t size, const mpw* data)
                        n->data = (mpw*) malloc(size * sizeof(*n->data));
 
                if (n->data && data)
+               {
+                       n->size = size;
                        /*@-nullpass@*/ /* data is notnull */
-                       mpcopy(n->size = size, n->data, data);
+                       mpcopy(n->size, n->data, data);
                        /*@=nullpass@*/
+               }
                else
                {
                        n->size = 0;
index b01d4ac..f612e87 100644 (file)
@@ -41,9 +41,9 @@
 #include "mp.h"
 #include "debug.h"
 
-#define hiBit(a)               ((a) & 0x80000000)
-#define loBit(a)               ((a) & 0x1)
-#define loBits(a)              ((a) & 0x7FFFFFFF)
+#define hiBit(a)               ((a) & 0x80000000U)
+#define loBit(a)               ((a) & 0x1U)
+#define loBits(a)              ((a) & 0x7FFFFFFFU)
 #define mixBits(a, b)  (hiBit(a) | loBits(b))
 
 /*@-sizeoftype@*/
@@ -182,8 +182,8 @@ int mtprngNext(mtprngParam* mp, uint32_t* data, size_t size)
 
                        tmp = *(mp->nextw++);
                        tmp ^= (tmp >> 11);
-                       tmp ^= (tmp << 7) & 0x9D2C5680;
-                       tmp ^= (tmp << 15) & 0xEFC60000;
+                       tmp ^= (tmp << 7) & 0x9D2C5680U;
+                       tmp ^= (tmp << 15) & 0xEFC60000U;
                        tmp ^= (tmp >> 18);
                        mp->left--;
                        *(data++) = tmp;
index 3c746d0..673cf5d 100644 (file)
@@ -43,7 +43,7 @@
 
 #define N      624
 #define M      397
-#define K      0x9908B0DF
+#define K      0x9908B0DFU
 
 /**
  */
index b227388..f3a4022 100644 (file)
@@ -45,8 +45,9 @@ extern "C" {
  * @param c            ciphertext
  * @retval             0 on success, -1 on failure
  */ 
+BEECRYPTAPI /*@unused@*/
  int rsapub(const rsapk* pk, const mpnumber* m, mpnumber* c)
-       /*@modifies c */;
+       /*@modifies c @*/;
 
 /**
  * The raw RSA private key operation.
@@ -63,7 +64,7 @@ extern "C" {
  */
 BEECRYPTAPI /*@unused@*/
 int rsapri   (const rsakp* kp, const mpnumber* c, mpnumber* m)
-       /*@modifies m */;
+       /*@modifies m @*/;
 
 /**
  * The raw RSA private key operation, with Chinese Remainder Theorem.
@@ -79,9 +80,9 @@ int rsapri   (const rsakp* kp, const mpnumber* c, mpnumber* m)
  * @param m            message
  * @retval             0 on success, -1 on failure.
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 int rsapricrt(const rsakp* kp, const mpnumber* c, mpnumber* m)
-       /*@modifies m */;
+       /*@modifies m @*/;
 
 /**
  * Verify if ciphertext \e c was encrypted from cleartext \e m
@@ -95,7 +96,7 @@ int rsapricrt(const rsakp* kp, const mpnumber* c, mpnumber* m)
  * @param c            ciphertext message
  * @retval             1 on success, 0 on failure
  */
-BEECRYPTAPI /*@unused@*/
+BEECRYPTAPI
 int rsavrfy  (const rsapk* pk, const mpnumber* m, const mpnumber* c)
        /*@*/;
 
index db82fc7..e846b1e 100644 (file)
@@ -39,7 +39,7 @@ int rsakpMake(rsakp* kp, randomGeneratorContext* rgc, size_t nsize)
         * Generates an RSA Keypair for use with the Chinese Remainder Theorem
         */
 
-       register size_t pqsize = (nsize+1) >> 1;
+       register size_t pqsize = (nsize + 1U) >> 1;
        register mpw* temp = (mpw*) malloc((16*pqsize+6) * sizeof(*temp));
        register int newn = 1;
 
index 547d941..e9bf331 100644 (file)
@@ -57,25 +57,25 @@ extern BEECRYPTAPI const hashFunction sha1;
  */
 BEECRYPTAPI
 void sha1Process(sha1Param* p)
-       /*@modifies p */;
+       /*@modifies p @*/;
 
 /** \ingroup HASH_sha1_m
  */
 BEECRYPTAPI /*@unused@*/
 int  sha1Reset  (sha1Param* p)
-       /*@modifies p */;
+       /*@modifies p @*/;
 
 /** \ingroup HASH_sha1_m
  */
 BEECRYPTAPI /*@unused@*/
 int  sha1Update (sha1Param* p, const byte* data, size_t size)
-       /*@modifies p */;
+       /*@modifies p @*/;
 
 /** \ingroup HASH_sha1_m
  */
 BEECRYPTAPI /*@unused@*/
 int  sha1Digest (sha1Param* p, /*@out@*/ byte* data)
-       /*@modifies p, data */;
+       /*@modifies p, data @*/;
 
 #ifdef __cplusplus
 }
index f50a1e7..6a43b38 100644 (file)
@@ -24,7 +24,6 @@
  */
 
 #include "system.h"
-
 #include "beecrypt.h"
 #include "blockmode.h"
 #include "aes.h"
 #include "sha1.h"
 #include "sha256.h"
 #include "mp.h"
-
 #include "debug.h"
 
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* dsa_p = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8324f0d7882e5d0762fc5b7210eafc2e9adac32ab7aac49693dfbf83724c2ec0736ee31c80291";
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* dsa_q = "c773218c737ec8ee993b4f2ded30f48edace915f";
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* dsa_g = "626d027839ea0a13413163a55b4cb500299d5522956cefcb3bff10f399ce2c2e71cb9de5fa24babf58e5b79521925c9cc42e9f6f464b088cc572af53e6d78802";
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* dsa_x = "2070b3223dba372fde1c0ffc7b2e3b498b260614";
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* dsa_y = "19131871d75b1612a819f29d78d1b0d7346f7aa77bb62a859bfd6c5675da9d212d3a36ef1672ef660b8c7c255cc0ec74858fba33f44c06699630a76b030ee333";
-/*@unchecked@*/ /*@observer@*/
+/*@unchecked@*/ /*@observer@*/ /*@unused@*/
 static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8324f0d7882e5d0762fc5b7210eafc2e9adac32ab7aac49693dfbf83724c2ec0736ee31c80290";
 
+/*@unused@*/
 static int testVectorInvMod(const dlkp_p* keypair)
        /*@*/
 {
        randomGeneratorContext rngc;
+       int rc = -1;
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
-               register int rc;
-
                register size_t  size = keypair->param.p.size;
                register mpw* temp = (mpw*) malloc((8*size+6) * sizeof(*temp));
 
+               assert(temp != NULL);
                mpbrndinv_w(&keypair->param.n, &rngc, temp, temp+size, temp+2*size);
 
                mpbmulmod_w(&keypair->param.n, size, temp, size, temp+size, temp, temp+2*size);
@@ -76,13 +78,15 @@ static int testVectorInvMod(const dlkp_p* keypair)
 
                free(temp);
 
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
-
-               return rc;
+               /*@=modobserver =usedef @*/
        }
-       return -1;
+/*@=branchstate@*/
+       return rc;
 }
 
+/*@unused@*/
 static int testVectorExpMod(const dlkp_p* keypair)
        /*@*/
 {
@@ -100,6 +104,7 @@ static int testVectorExpMod(const dlkp_p* keypair)
        return rc;
 }
 
+/*@unused@*/
 static int testVectorElGamalV1(const dlkp_p* keypair)
        /*@*/
 {
@@ -107,7 +112,10 @@ static int testVectorElGamalV1(const dlkp_p* keypair)
 
        randomGeneratorContext rngc;
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
                mpnumber digest, r, s;
 
@@ -116,6 +124,7 @@ static int testVectorElGamalV1(const dlkp_p* keypair)
                mpnzero(&s);
 
                mpnsize(&digest, 5);
+               memset(digest.data, 0, digest.size * sizeof(*digest.data));
 
                (void) rngc.rng->next(rngc.param, digest.data, digest.size);
 
@@ -127,11 +136,15 @@ static int testVectorElGamalV1(const dlkp_p* keypair)
                mpnfree(&r);
                mpnfree(&s);
 
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver =usedef @*/
        }
+/*@=branchstate@*/
        return rc;
 }
 
+/*@unused@*/
 static int testVectorElGamalV3(const dlkp_p* keypair)
        /*@*/
 {
@@ -139,7 +152,10 @@ static int testVectorElGamalV3(const dlkp_p* keypair)
 
        randomGeneratorContext rngc;
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
                mpnumber digest, r, s;
 
@@ -148,6 +164,7 @@ static int testVectorElGamalV3(const dlkp_p* keypair)
                mpnzero(&s);
 
                mpnsize(&digest, 5);
+               memset(digest.data, 0, digest.size * sizeof(*digest.data));
 
                (void) rngc.rng->next(rngc.param, digest.data, digest.size);
 
@@ -159,8 +176,11 @@ static int testVectorElGamalV3(const dlkp_p* keypair)
                mpnfree(&r);
                mpnfree(&s);
 
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver =usedef @*/
        }
+/*@=branchstate@*/
        return rc;
 }
 
@@ -186,16 +206,18 @@ static uint32_t keyValue[] =
 };
        
 static void testBlockInit(uint8_t* block, int length)
-       /*@modifies block @*/
+       /*@modifies *block @*/
 {
        register int i;
-       for (i = 1; i <= length; i++)
-               *(block++) = (uint8_t) i;
+       for (i = 1; i <= length; i++) {
+               *block = (uint8_t) i;
+               block++;
+       }
 }
 
 static void testBlockCiphers(void)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        int i, k;
 
@@ -217,6 +239,13 @@ static void testBlockCiphers(void)
                        void* encrypt_param = (void*) malloc(tmp->paramsize);
                        void* decrypt_param = (void*) malloc(tmp->paramsize);
 
+                       assert(src_block != NULL);
+                       assert(enc_block != NULL);
+                       assert(dec_block != NULL);
+                       assert(spd_block != NULL);
+                       assert(encrypt_param != NULL);
+                       assert(decrypt_param != NULL);
+
                        printf("  %s:\n", tmp->name);
 
                        for (k = tmp->keybitsmin; k <= tmp->keybitsmax; k += tmp->keybitsinc)
@@ -261,7 +290,7 @@ static void testBlockCiphers(void)
                                        #if HAVE_TIME_H
                                        tstop = clock();
                                        ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
-                                       printf("      ECB encrypts 1M blocks of %d bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
+                                       printf("      ECB encrypts 1M blocks of %u bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
                                        #endif
                                        #if HAVE_TIME_H
                                        tstart = clock();
@@ -270,7 +299,7 @@ static void testBlockCiphers(void)
                                        #if HAVE_TIME_H
                                        tstop = clock();
                                        ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
-                                       printf("      ECB decrypts 1M blocks of %d bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
+                                       printf("      ECB decrypts 1M blocks of %u bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
                                        #endif
                                        #if HAVE_TIME_H
                                        tstart = clock();
@@ -279,16 +308,16 @@ static void testBlockCiphers(void)
                                        #if HAVE_TIME_H
                                        tstop = clock();
                                        ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
-                                       printf("      CBC encrypts 1M blocks of %d bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
+                                       printf("      CBC encrypts 1M blocks of %u bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
                                        #endif
                                        #if HAVE_TIME_H
                                        tstart = clock();
                                        #endif
-                                       (void) blockDecrypt(tmp, decrypt_param, CBC, 1024 * 1024, spd_block, spd_block);
+                                       (void) blockDecryptCBC(tmp, decrypt_param, 1024 * 1024, spd_block, spd_block);
                                        #if HAVE_TIME_H
                                        tstop = clock();
                                        ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
-                                       printf("      CBC decrypts 1M blocks of %d bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
+                                       printf("      CBC decrypts 1M blocks of %u bits in %.3f seconds (%.3f MB/s)\n", tmp->blocksize << 3, ttime, (tmp->blocksize) / ttime);
                                        #endif
                                }
                        }
@@ -303,8 +332,8 @@ static void testBlockCiphers(void)
 }
 
 static void testHashFunctions(void)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        int i, j;
 
@@ -320,6 +349,7 @@ static void testHashFunctions(void)
                {
                        const hashFunction* tmp = hashFunctionGet(i);
 
+/*@-branchstate@*/
                        if (tmp)
                        {
                                #if HAVE_TIME_H
@@ -332,7 +362,9 @@ static void testHashFunctions(void)
 
                                printf("  %s:\n", tmp->name);
 
+                               /*@-modobserver -usedef @*/
                                if (hashFunctionContextInit(&hfc, tmp) == 0)
+                               /*@=modobserver =usedef @*/
                                {
                                        for (j = 0; j < 4; j++)
                                        {
@@ -350,18 +382,22 @@ static void testHashFunctions(void)
                                                #endif
                                        }
 
+                                       /*@-modobserver -usedef @*/
                                        (void) hashFunctionContextFree(&hfc);
+                                       /*@=modobserver =usedef @*/
                                }
 
                                mpnfree(&digest);
                        }
+/*@=branchstate@*/
                }
+               free(data);
        }
 }
 
 static void testExpMods(void)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        /*@unchecked@*/ /*@observer@*/
        static const char* p_512 = "ffcf0a0767f18f9b659d92b9550351430737c3633dc6ae7d52445d937d8336e07a7ccdb119e9ab3e011a8f938151230e91187f84ac05c3220f335193fc5e351b";
@@ -386,7 +422,10 @@ static void testExpMods(void)
        mpnzero(&y);
        mpnzero(&tmp);
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
                int i;
                #if HAVE_TIME_H
@@ -466,19 +505,23 @@ static void testExpMods(void)
                mpnfree(&y);
                mpnfree(&tmp);
 
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver =usedef @*/
        }
        else
                printf("random generator setup problem\n");
+/*@=branchstate@*/
 }
 
 static void testRSA(void)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        randomGeneratorContext rngc;
        mpnumber hm, s;
        rsakp kp;
+       int xx;
 
        mpnzero(&hm);
        mpnzero(&s);
@@ -487,7 +530,10 @@ static void testRSA(void)
 
        (void) rsakpInit(&kp);
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
                int i;
 
@@ -517,7 +563,7 @@ static void testRSA(void)
                #endif
                for (i = 0; i < 100; i++)
                {
-                       (void) rsapricrt(&kp, &hm, &s);
+                       xx = rsapricrt(&kp, &hm, &s);
                }
                #if HAVE_TIME_H
                tstop = clock();
@@ -531,7 +577,7 @@ static void testRSA(void)
                #endif
                for (i = 0; i < 1000; i++)
                {
-                       (void) rsavrfy((rsapk*) &kp, &hm, &s);
+                       xx = rsavrfy((rsapk*) &kp, &hm, &s);
                }
                #if HAVE_TIME_H
                tstop = clock();
@@ -540,18 +586,23 @@ static void testRSA(void)
                #endif
 
                (void) rsakpFree(&kp);
+
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver =usedef @*/
        }
+/*@=branchstate@*/
 }
 
 static void testDLAlgorithms(void)
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        randomGeneratorContext rngc;
        mpnumber hm, r, s;
        dldp_p dp;
        dlkp_p kp;
+       int xx;
 
        mpnzero(&hm);
        mpnzero(&r);
@@ -562,7 +613,10 @@ static void testDLAlgorithms(void)
 
        printf("Timing Discrete Logarithm algorithms:\n");
 
+/*@-branchstate@*/
+       /*@-modobserver -usedef @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+       /*@=modobserver =usedef @*/
        {
                int i;
 
@@ -602,13 +656,13 @@ static void testDLAlgorithms(void)
                #endif
                for (i = 0; i < 100; i++)
                {
-                       (void) dsasign(&kp.param.p, &kp.param.q, &kp.param.g, &rngc, &hm, &kp.x, &r, &s);
+                       xx = dsasign(&kp.param.p, &kp.param.q, &kp.param.g, &rngc, &hm, &kp.x, &r, &s);
                }
-        #if HAVE_TIME_H
-        tstop = clock();
-        ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
-        printf("   100x in %.3f seconds\n", ttime);
-        #endif
+               #if HAVE_TIME_H
+               tstop = clock();
+               ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
+               printf("   100x in %.3f seconds\n", ttime);
+               #endif
 
                printf("  DSA verify:");
                #if HAVE_TIME_H
@@ -616,7 +670,7 @@ static void testDLAlgorithms(void)
                #endif
                for (i = 0; i < 100; i++)
                {
-                       (void) dsavrfy(&kp.param.p, &kp.param.q, &kp.param.g, &hm, &kp.y, &r, &s);
+                       xx = dsavrfy(&kp.param.p, &kp.param.q, &kp.param.g, &hm, &kp.y, &r, &s);
                }
                #if HAVE_TIME_H
                tstop = clock();
@@ -630,21 +684,28 @@ static void testDLAlgorithms(void)
                #if HAVE_TIME_H
                tstart = clock();
                #endif
+/*@-usereleased@*/
                (void) dldp_pgonMake(&dp, &rngc, 1024 >> 5, 768 >> 5);
+/*@=usereleased@*/
                #if HAVE_TIME_H
                tstop = clock();
                ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
                printf("    done in %.3f seconds\n", ttime);
                #endif
+/*@-usedef@*/
                (void) dldp_pFree(&dp);
+/*@=usedef@*/
 
+               /*@-modobserver -usedef @*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver =usedef @*/
        }
+/*@=branchstate@*/
 }
 
 int main(/*@unused@*/ int argc, /*@unused@*/ char *argv[])
-       /*@globals fileSystem @*/
-       /*@modifies fileSystem @*/
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        int i, j;
 
index 663b3fd..5ca7bd9 100644 (file)
@@ -113,7 +113,9 @@ typedef uint32_t mphw;
 typedef uint64_t mpdw;
 # endif
 typedef uint32_t mpw;
+/*@-typeuse@*/
 typedef uint16_t mphw;
+/*@=typeuse@*/
 #else
 # error
 #endif