spliddles.

CVS patchset: 6801
CVS date: 2003/05/01 19:55:27

30 files changed, 312 insertions, 267 deletions

diff --git a/beecrypt/.splintrc b/beecrypt/.splintrc
index 64c80d55c..a35876258 100644
--- a/beecrypt/.splintrc
+++ b/beecrypt/.splintrc
@@ -13,23 +13,18 @@
 +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
@@ -39,12 +34,8 @@
 
 -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
diff --git a/beecrypt/aes.c b/beecrypt/aes.c
index 837c6db64..97b5e0a2e 100644
--- a/beecrypt/aes.c
+++ b/beecrypt/aes.c
@@ -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
diff --git a/beecrypt/base64.c b/beecrypt/base64.c
index 306ed3d02..0843754fa 100644
--- a/beecrypt/base64.c
+++ b/beecrypt/base64.c
@@ -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);
diff --git a/beecrypt/beecrypt.c b/beecrypt/beecrypt.c
index 6ce1f905f..aaabf9660 100644
--- a/beecrypt/beecrypt.c
+++ b/beecrypt/beecrypt.c
@@ -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;
 
diff --git a/beecrypt/beecrypt.h b/beecrypt/beecrypt.h
index b709581a2..86f881337 100644
--- a/beecrypt/beecrypt.h
+++ b/beecrypt/beecrypt.h
@@ -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
diff --git a/beecrypt/blockmode.c b/beecrypt/blockmode.c
index 07c3ce57a..66c19716a 100644
--- a/beecrypt/blockmode.c
+++ b/beecrypt/blockmode.c
@@ -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;
 			}
 
diff --git a/beecrypt/blockpad.c b/beecrypt/blockpad.c
index 2f98a3433..eb8e1b813 100644
--- a/beecrypt/blockpad.c
+++ b/beecrypt/blockpad.c
@@ -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;
 
diff --git a/beecrypt/blockpad.h b/beecrypt/blockpad.h
index f8ec5873b..e5a09047c 100644
--- a/beecrypt/blockpad.h
+++ b/beecrypt/blockpad.h
@@ -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.
diff --git a/beecrypt/dhaes.c b/beecrypt/dhaes.c
index ecc4a0b9d..ed1ec5e02 100644
--- a/beecrypt/dhaes.c
+++ b/beecrypt/dhaes.c
@@ -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;
diff --git a/beecrypt/dhaes.h b/beecrypt/dhaes.h
index 4cdc1d32d..e2f96c4f2 100644
--- a/beecrypt/dhaes.h
+++ b/beecrypt/dhaes.h
@@ -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
 }
diff --git a/beecrypt/dldp.h b/beecrypt/dldp.h
index 6d1d60831..71635a1fb 100644
--- a/beecrypt/dldp.h
+++ b/beecrypt/dldp.h
@@ -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 @*/;
 
 /**
diff --git a/beecrypt/dlkp.h b/beecrypt/dlkp.h
index 7755afbc3..9e7557efc 100644
--- a/beecrypt/dlkp.h
+++ b/beecrypt/dlkp.h
@@ -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
 }
diff --git a/beecrypt/dlpk.h b/beecrypt/dlpk.h
index 97039b0b6..8726222d2 100644
--- a/beecrypt/dlpk.h
+++ b/beecrypt/dlpk.h
@@ -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 @*/;
 
 /**
  */
diff --git a/beecrypt/dlsvdp-dh.h b/beecrypt/dlsvdp-dh.h
index 3e7594eff..7b486a7cf 100644
--- a/beecrypt/dlsvdp-dh.h
+++ b/beecrypt/dlsvdp-dh.h
@@ -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
 }
diff --git a/beecrypt/endianness.c b/beecrypt/endianness.c
index 8ff018734..c280fc64b 100644
--- a/beecrypt/endianness.c
+++ b/beecrypt/endianness.c
@@ -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)
 {
diff --git a/beecrypt/endianness.h b/beecrypt/endianness.h
index eda0496bd..13ab1d12c 100644
--- a/beecrypt/endianness.h
+++ b/beecrypt/endianness.h
@@ -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
 }
diff --git a/beecrypt/entropy.c b/beecrypt/entropy.c
index f7bfee047..9c9ee74a3 100644
--- a/beecrypt/entropy.c
+++ b/beecrypt/entropy.c
@@ -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);
 	}
diff --git a/beecrypt/fips186.h b/beecrypt/fips186.h
index ea2454071..e78774f51 100644
--- a/beecrypt/fips186.h
+++ b/beecrypt/fips186.h
@@ -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
diff --git a/beecrypt/hmac.h b/beecrypt/hmac.h
index 7e888e845..6d182818c 100644
--- a/beecrypt/hmac.h
+++ b/beecrypt/hmac.h
@@ -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
 }
diff --git a/beecrypt/md5.c b/beecrypt/md5.c
index 743a0227c..d180adb38 100644
--- a/beecrypt/md5.c
+++ b/beecrypt/md5.c
@@ -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)
diff --git a/beecrypt/mp.c b/beecrypt/mp.c
index 3e20b6f09..d19cc812d 100644
--- a/beecrypt/mp.c
+++ b/beecrypt/mp.c
@@ -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--)
 	{
diff --git a/beecrypt/mp.h b/beecrypt/mp.h
index e053dbaab..c54c70e02 100644
--- a/beecrypt/mp.h
+++ b/beecrypt/mp.h
@@ -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 @*/;
 
diff --git a/beecrypt/mpnumber.c b/beecrypt/mpnumber.c
index 53962eee4..855bfab07 100644
--- a/beecrypt/mpnumber.c
+++ b/beecrypt/mpnumber.c
@@ -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;
diff --git a/beecrypt/mtprng.c b/beecrypt/mtprng.c
index b01d4ace0..f612e8785 100644
--- a/beecrypt/mtprng.c
+++ b/beecrypt/mtprng.c
@@ -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;
diff --git a/beecrypt/mtprng.h b/beecrypt/mtprng.h
index 3c746d05b..673cf5dc9 100644
--- a/beecrypt/mtprng.h
+++ b/beecrypt/mtprng.h
@@ -43,7 +43,7 @@
 
 #define N	624
 #define M	397
-#define K	0x9908B0DF
+#define K	0x9908B0DFU
 
 /**
  */
diff --git a/beecrypt/rsa.h b/beecrypt/rsa.h
index b227388fb..f3a4022bc 100644
--- a/beecrypt/rsa.h
+++ b/beecrypt/rsa.h
@@ -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)
 	/*@*/;
 
diff --git a/beecrypt/rsakp.c b/beecrypt/rsakp.c
index db82fc767..e846b1e68 100644
--- a/beecrypt/rsakp.c
+++ b/beecrypt/rsakp.c
@@ -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;
 
diff --git a/beecrypt/sha1.h b/beecrypt/sha1.h
index 547d941c3..e9bf331b6 100644
--- a/beecrypt/sha1.h
+++ b/beecrypt/sha1.h
@@ -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
 }
diff --git a/beecrypt/tests/beetest.c b/beecrypt/tests/beetest.c
index f50a1e73e..6a43b3804 100644
--- a/beecrypt/tests/beetest.c
+++ b/beecrypt/tests/beetest.c
@@ -24,7 +24,6 @@
  */
 
 #include "system.h"
-
 #include "beecrypt.h"
 #include "blockmode.h"
 #include "aes.h"
@@ -40,34 +39,37 @@
 #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;
 
diff --git a/beecrypt/types.h.in b/beecrypt/types.h.in
index 663b3fd0f..5ca7bd922 100644
--- a/beecrypt/types.h.in
+++ b/beecrypt/types.h.in
@@ -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