More lclint annotations, now at the strict level with a complete program.

CVS patchset: 5069 CVS date: 2001/09/23 12:09:48
author: jbj <devnull@localhost> 2001-09-23 12:09:48 +0000
committer: jbj <devnull@localhost> 2001-09-23 12:09:48 +0000
commit: 0f7777894493527a5672d0ce09c4855e2b69495f (patch)
tree: af5511490946ca59d1abc0ae69696437bd73eac8 /beecrypt
parent: 1eef0782f60f9d8d80be273ace982ad4c2a56d98 (diff)
download: librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.tar.gz
librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.tar.bz2
librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.zip
53 files changed, 1643 insertions, 809 deletions
diff --git a/beecrypt/.lclintrc b/beecrypt/.lclintrc
index d83c74ec0..3be6606ae 100644
--- a/beecrypt/.lclintrc
+++ b/beecrypt/.lclintrc
@@ -1,6 +1,6 @@
--I. -I./build -I./lib -I./rpmdb -I./rpmio -I./popt -DHAVE_CONFIG_H -D_GNU_SOURCE
+-I. -I/usr/lib/gcc-lib/i386-redhat-linux/2.96/include -DHAVE_CONFIG_H -D_GNU_SOURCE
 
-+partial
+#+partial
 #+forcehints
 
 -warnunixlib
@@ -10,80 +10,53 @@
 
 -unrecogcomments	# XXX ignore doxygen markings
 
-#-deepbreak		# shortcut 485 occurences
-
-+standard		# lclint level
++strict			# lclint level
 
 # --- not-yet at strict level
-#+ptrarith
-#+bitwisesigned
-#+strictops
-#+sizeoftype
+-exportconst
+-exportfcn
+-exporttype
+-exportvar
+-warnmissingglobs
+-internalglobs
+-protoparamname
 
-#+mod-uncon		# shortcut alloca is painful
-#+mod-nomods
-+modglobsnomods
-+modstrictglobsnomods
+-ansi-reserved-internal	# goofy
 
-#+mod-uncon-nomods
-#+mod-internal-strict
-#+mod-file-sys
-#+globnoglobs
-#+internalglobs
-#+internalglobnoglobs
-#+modglobsunchecked
-+warnmissingglobs
-#+warnmissingglobsnomods
-#+impcheckedstrictglobs
-#+impcheckedstrictstatics
-#+strictusereleas
-#+strictbranchstate
-#+strictdestroy
-#+modobserveruncon
-+macroempty
-#+ansi-reserved-internal
-#+evalorderuncon
-#+elseifcomplete
-#+loopswitchbreak
-#+switchswitchbreak
-#+looploopcontinue
-#+whileblock
-+forempty
-#+forblock
-#+ifblock
-#+noeffectuncon
-+topuse
-#+unusedspecial
-+oldstyle
-#+sys-dir-errors
-#controlnestdepth 15
-#stringliterallen 509
-#numstructfields 127
-#numenummembers 127
+-ptrarith
+-bitwisesigned
+-strictops
+-sizeoftype
 
-# --- not-yet at checks level
-#-predboolptr	
-#+enumint
-#-allglobs
-#-ansi-reserved		# goofy
-#-infloopsuncon		# goofy
+-mod-file-sys
+
+-impcheckedstrictglobs
+-impcheckedstrictstatics
+-strictbranchstate
+-strictdestroy
 
-#-proto-param-match
+-forblock
+-ifblock
+-whileblock
+-sys-dir-errors		# 30 occurences
+
+# --- not-yet at checks level
+-predboolptr	
++enumint
+-allglobs		# painful
+-ansi-reserved		# goofy
+-infloopsuncon		# goofy
 
 # don't-bother-me-yet parameters
--branchstate		# painful
+-branchstate		# 6 occurences
 -mustfree		# alloca is painful
 
--exportlocal		# 59 occurences
--fcnuse			# 131 occurences
--compdef		# 52 occurences
-
 # --- not-yet at standard level
--boolops		# w->n
--predboolint		# w->n
--type			#
+-boolops
+-predboolint
+-type
 
-# -weak paramaters
+# --- not-yet at weak level
 #+boolint
 #-boolops
 #+ignorequals
diff --git a/beecrypt/Doxyheader b/beecrypt/Doxyheader
index 74b6a9144..efc2e1034 100644
--- a/beecrypt/Doxyheader
+++ b/beecrypt/Doxyheader
@@ -105,3 +105,5 @@ The library is currently in the process of being ported to:
  */
 /** \defgroup	MP_m	Multiple Precision Integer Arithmetic
  */
+/** \defgroup	JAVA_m	Java API
+ */
diff --git a/beecrypt/Makefile.am b/beecrypt/Makefile.am
index 89499dc8f..ad9ac6867 100644
--- a/beecrypt/Makefile.am
+++ b/beecrypt/Makefile.am
@@ -54,12 +54,9 @@ pkginclude_HEADERS = base64.h beecrypt.h blockmode.h blockpad.h blowfish.h blowf
 
 EXTRA_DIST = BENCHMARKS BUGS CONTRIBUTORS Doxyfile.in Doxyheader README.DLL README.WIN32 beecrypt.def beecrypt.mcp beecrypt.rc beecrypt.spec config.h config.gas.h config.win.h javaglue.h
 
-# beecrypt.c entropy.c javaglue.c mtprng.c
-lclintfiles = base64.c blockmode.c blockpad.c blowfish.c dhaes.c dldp.c dlkp.c dlpk.c dlsvdp-dh.c elgamal.c endianness.c fips180.c fips186.c hmac.c hmacmd5.c hmacsha1.c hmacsha256.c md5.c memchunk.c mp32.c mp32barrett.c mp32number.c mp32prime.c rsa.c rsakp.c rsapk.c sha256.c timestamp.c
-
 .PHONY: lclint
 lclint:
-	lclint $(DEFS) $(INCLUDES) ${lclintfiles}
+	lclint $(DEFS) $(INCLUDES) ${libbeecrypt_la_SOURCES} tests/beetest.c
 
 DOXYGEN = /usr/bin/doxygen
 .PHONY: doxygen
diff --git a/beecrypt/Makefile.in b/beecrypt/Makefile.in
index 3f75b0a24..295ab5f02 100644
--- a/beecrypt/Makefile.in
+++ b/beecrypt/Makefile.in
@@ -139,8 +139,7 @@ pkginclude_HEADERS = base64.h beecrypt.h blockmode.h blockpad.h blowfish.h blowf
 
 EXTRA_DIST = BENCHMARKS BUGS CONTRIBUTORS Doxyfile.in Doxyheader README.DLL README.WIN32 beecrypt.def beecrypt.mcp beecrypt.rc beecrypt.spec config.h config.gas.h config.win.h javaglue.h
 
-# beecrypt.c entropy.c javaglue.c mtprng.c
-lclintfiles = base64.c blockmode.c blockpad.c blowfish.c dhaes.c dldp.c dlkp.c dlpk.c dlsvdp-dh.c elgamal.c endianness.c fips180.c fips186.c hmac.c hmacmd5.c hmacsha1.c hmacsha256.c md5.c memchunk.c mp32.c mp32barrett.c mp32number.c mp32prime.c rsa.c rsakp.c rsapk.c sha256.c timestamp.c
+lclintfiles = base64.c beecrypt.c blockmode.c blockpad.c blowfish.c dhaes.c dldp.c dlkp.c dlpk.c dlsvdp-dh.c elgamal.c endianness.c entropy.c fips180.c fips186.c hmac.c hmacmd5.c hmacsha1.c hmacsha256.c javaglue.c md5.c memchunk.c mp32.c mp32barrett.c mp32number.c mp32prime.c mtprng.c rsa.c rsakp.c rsapk.c sha256.c timestamp.c
 
 DOXYGEN = /usr/bin/doxygen
 ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
@@ -559,7 +558,7 @@ maintainer-clean-generic clean mostlyclean distclean maintainer-clean
 
 .PHONY: lclint
 lclint:
-	lclint $(DEFS) $(INCLUDES) ${lclintfiles}
+	lclint $(DEFS) $(INCLUDES) ${libbeecrypt_la_SOURCES} tests/beetest.c
 .PHONY: doxygen
 doxygen apidocs: Doxyfile Doxyheader
 	rm -rf $@
diff --git a/beecrypt/base64.c b/beecrypt/base64.c
index d9469ca17..2c0a9f5e5 100644
--- a/beecrypt/base64.c
+++ b/beecrypt/base64.c
@@ -134,7 +134,7 @@ memchunk* b64dec(const char* string)
 					for (i = 0; i < vrfy; i++)
 					{
 						if (isspace(tmp[i]))
-							continue;
+							/*@innercontinue@*/ continue;
 
 						if (tmp[i] == '=')
 						{
@@ -146,7 +146,7 @@ memchunk* b64dec(const char* string)
 								return 0;
 
 							/* end-of-message recognized */
-							break;
+							/*@innerbreak@*/ break;
 						}
 						else
 						{
@@ -198,23 +198,25 @@ memchunk* b64dec(const char* string)
 						}
 						else if (ch == '=')
 							break;
+						else
+							{};
 
 						switch (qw++)
 						{
 						case 0:
 							data[tw+0] = (bits << 2) & 0xfc;
-							break;
+							/*@switchbreak@*/ break;
 						case 1:
 							data[tw+0] |= (bits >> 4) & 0x03;
 							data[tw+1] = (bits << 4) & 0xf0;
-							break;
+							/*@switchbreak@*/ break;
 						case 2:
 							data[tw+1] |= (bits >> 2) & 0x0f;
 							data[tw+2] = (bits << 6) & 0xc0;
-							break;
+							/*@switchbreak@*/ break;
 						case 3:
 							data[tw+2] |= bits & 0x3f;
-							break;
+							/*@switchbreak@*/ break;
 						}
 
 						if (qw == 4)
diff --git a/beecrypt/base64.h b/beecrypt/base64.h
index 3af0ec17b..ab34307c7 100644
--- a/beecrypt/base64.h
+++ b/beecrypt/base64.h
@@ -32,10 +32,15 @@
 extern "C" {
 #endif
 
-BEEDLLAPI /*@only@*/ /*@null@*/
+/**
+ */
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 char*		b64enc(const memchunk* chunk)
 	/*@*/;
-BEEDLLAPI /*@only@*/ /*@null@*/
+
+/**
+ */
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk*	b64dec(const char* string)
 	/*@*/;
 
diff --git a/beecrypt/beecrypt.c b/beecrypt/beecrypt.c
index fd6a6c968..8c8002bb5 100644
--- a/beecrypt/beecrypt.c
+++ b/beecrypt/beecrypt.c
@@ -1,8 +1,10 @@
-/*
- * beecrypt.c
- *
- * BeeCrypt library hooks & stubs, code
+/**
+ * \file beecrypt.c
  *
+ * BeeCrypt library hooks & stubs, code.
+ */
+
+/*
  * Copyright (c) 1999, 2000, 2001 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
@@ -40,6 +42,15 @@
 # include <windows.h>
 #endif
 
+#if defined(__LCLINT__)
+/* XXX from /usr/include/bits/sigest.h in glibc-2.2.4 */
+# define _SIGSET_NWORDS (1024 / (8 * sizeof (unsigned long int)))
+typedef struct
+  {
+    unsigned long int __val[_SIGSET_NWORDS];
+  } __sigset_t;
+#endif
+
 #include "endianness.h"
 #include "entropy.h"
 #include "fips180.h"
@@ -112,14 +123,11 @@ const entropySource* entropySourceDefault()
 	const char* selection = getenv("BEECRYPT_ENTROPY");
 
 	if (selection)
-	{
 		return entropySourceFind(selection);
-	}
 	else if (ENTROPYSOURCES)
-	{
 		return entropySourceList+0;
-	}
-	return (const entropySource*) 0;
+	else
+		return (const entropySource*) 0;
 }
 
 int entropyGatherNext(uint32* data, int size)
@@ -164,7 +172,9 @@ const randomGenerator* randomGeneratorGet(int index)
 	if ((index < 0) || (index >= RANDOMGENERATORS))
 		return (const randomGenerator*) 0;
 
+	/*@-compmempass@*/
 	return randomGeneratorList[index];
+	/*@=compmempass@*/
 }
 
 const randomGenerator* randomGeneratorFind(const char* name)
@@ -174,7 +184,9 @@ const randomGenerator* randomGeneratorFind(const char* name)
 	for (index = 0; index < RANDOMGENERATORS; index++)
 	{
 		if (strcmp(name, randomGeneratorList[index]->name) == 0)
+			/*@-compmempass@*/
 			return randomGeneratorList[index];
+			/*@=compmempass@*/
 	}
 	return (const randomGenerator*) 0;
 }
@@ -197,13 +209,17 @@ int randomGeneratorContextInit(randomGeneratorContext* ctxt, const randomGenerat
 	if (rng == (randomGenerator*) 0)
 		return -1;
 
+	/*@-temptrans@*/
 	ctxt->rng = rng;
+	/*@=temptrans@*/
 	ctxt->param = (randomGeneratorParam*) calloc(rng->paramsize, 1);
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	if (ctxt->param == (randomGeneratorParam*) 0)
 		return -1;
 
 	return ctxt->rng->setup(ctxt->param);
+	/*@=nullstate@*/
 }
 
 int randomGeneratorContextFree(randomGeneratorContext* ctxt)
@@ -225,7 +241,9 @@ int randomGeneratorContextFree(randomGeneratorContext* ctxt)
 
 	ctxt->param = (randomGeneratorParam*) 0;
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	return rc;
+	/*@=nullstate@*/
 }
 
 /*@observer@*/ static const hashFunction* hashFunctionList[] =
@@ -257,7 +275,9 @@ const hashFunction* hashFunctionGet(int index)
 	if ((index < 0) || (index >= HASHFUNCTIONS))
 		return (const hashFunction*) 0;
 
+	/*@-compmempass@*/
 	return hashFunctionList[index];
+	/*@=compmempass@*/
 }
 
 const hashFunction* hashFunctionFind(const char* name)
@@ -267,7 +287,9 @@ const hashFunction* hashFunctionFind(const char* name)
 	for (index = 0; index < HASHFUNCTIONS; index++)
 	{
 		if (strcmp(name, hashFunctionList[index]->name) == 0)
+			/*@-compmempass@*/
 			return hashFunctionList[index];
+			/*@=compmempass@*/
 	}
 	return (const hashFunction*) 0;
 }
@@ -280,13 +302,17 @@ int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
 	if (hash == (hashFunction*) 0)
 		return -1;
 
+	/*@-temptrans@*/
 	ctxt->algo = hash;
+	/*@=temptrans@*/
 	ctxt->param = (hashFunctionParam*) calloc(hash->paramsize, 1);
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	if (ctxt->param == (hashFunctionParam*) 0)
 		return -1;
 
 	return ctxt->algo->reset(ctxt->param);
+	/*@=nullstate@*/
 }
 
 int hashFunctionContextFree(hashFunctionContext* ctxt)
@@ -301,7 +327,9 @@ int hashFunctionContextFree(hashFunctionContext* ctxt)
 
 	ctxt->param = (hashFunctionParam*) 0;
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	return 0;
+	/*@=nullstate@*/
 }
 
 int hashFunctionContextReset(hashFunctionContext* ctxt)
@@ -368,18 +396,20 @@ int hashFunctionContextUpdateMP32(hashFunctionContext* ctxt, const mp32number* n
 		register int rc = -1;
 		register byte* temp = (byte*) malloc((n->size << 2) + 1);
 
+		/*@-nullpass -nullderef -nullptrarith @*/ /* FIX: temp may be NULL */
 		if (mp32msbset(n->size, n->data))
 		{
 			temp[0] = 0;
-			encodeInts((javaint*) n->data, temp+1, n->size);
+			(void) encodeInts((javaint*) n->data, temp+1, n->size);
 			rc = ctxt->algo->update(ctxt->param, temp, (n->size << 2) + 1);
 		}
 		else
 		{
-			encodeInts((javaint*) n->data, temp, n->size);
+			(void) encodeInts((javaint*) n->data, temp, n->size);
 			rc = ctxt->algo->update(ctxt->param, temp, n->size << 2);
 		}
 		free(temp);
+		/*@=nullpass =nullderef =nullptrarith @*/
 
 		return rc;
 	}
@@ -452,7 +482,9 @@ const keyedHashFunction* keyedHashFunctionGet(int index)
 	if ((index < 0) || (index >= KEYEDHASHFUNCTIONS))
 		return (const keyedHashFunction*) 0;
 
+	/*@-compmempass@*/
 	return keyedHashFunctionList[index];
+	/*@=compmempass@*/
 }
 
 const keyedHashFunction* keyedHashFunctionFind(const char* name)
@@ -462,7 +494,9 @@ const keyedHashFunction* keyedHashFunctionFind(const char* name)
 	for (index = 0; index < KEYEDHASHFUNCTIONS; index++)
 	{
 		if (strcmp(name, keyedHashFunctionList[index]->name) == 0)
+			/*@-compmempass@*/
 			return keyedHashFunctionList[index];
+			/*@=compmempass@*/
 	}
 	return (const keyedHashFunction*) 0;
 }
@@ -475,13 +509,17 @@ int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHash
 	if (mac == (keyedHashFunction*) 0)
 		return -1;
 
+	/*@-temptrans@*/
 	ctxt->algo = mac;
+	/*@=temptrans@*/
 	ctxt->param = (keyedHashFunctionParam*) calloc(mac->paramsize, 1);
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	if (ctxt->param == (keyedHashFunctionParam*) 0)
 		return -1;
 
 	return ctxt->algo->reset(ctxt->param);
+	/*@=nullstate@*/
 }
 
 int keyedHashFunctionContextFree(keyedHashFunctionContext* ctxt)
@@ -499,7 +537,9 @@ int keyedHashFunctionContextFree(keyedHashFunctionContext* ctxt)
 
 	ctxt->param = (keyedHashFunctionParam*) 0;
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	return 0;
+	/*@=nullstate@*/
 }
 
 int keyedHashFunctionContextSetup(keyedHashFunctionContext* ctxt, const uint32* key, int keybits)
@@ -583,18 +623,20 @@ int keyedHashFunctionContextUpdateMP32(keyedHashFunctionContext* ctxt, const mp3
 		register int rc;
 		register byte* temp = (byte*) malloc((n->size << 2) + 1);
 
+		/*@-nullpass -nullderef -nullptrarith @*/ /* FIX: temp may be NULL */
 		if (mp32msbset(n->size, n->data))
 		{
 			temp[0] = 0;
-			encodeInts((javaint*) n->data, temp+1, n->size);
+			(void) encodeInts((javaint*) n->data, temp+1, n->size);
 			rc = ctxt->algo->update(ctxt->param, temp, (n->size << 2) + 1);
 		}
 		else
 		{
-			encodeInts((javaint*) n->data, temp, n->size);
+			(void) encodeInts((javaint*) n->data, temp, n->size);
 			rc = ctxt->algo->update(ctxt->param, temp, n->size << 2);
 		}
 		free(temp);
+		/*@=nullpass =nullderef =nullptrarith @*/
 
 		return rc;
 	}
@@ -667,7 +709,9 @@ const blockCipher* blockCipherGet(int index)
 	if ((index < 0) || (index >= BLOCKCIPHERS))
 		return (const blockCipher*) 0;
 
+	/*@-compmempass@*/
 	return blockCipherList[index];
+	/*@=compmempass@*/
 }
 
 const blockCipher* blockCipherFind(const char* name)
@@ -677,7 +721,9 @@ const blockCipher* blockCipherFind(const char* name)
 	for (index = 0; index < BLOCKCIPHERS; index++)
 	{
 		if (strcmp(name, blockCipherList[index]->name) == 0)
+			/*@-compmempass@*/
 			return blockCipherList[index];
+			/*@=compmempass@*/
 	}
 
 	return (const blockCipher*) 0;
@@ -691,13 +737,17 @@ int blockCipherContextInit(blockCipherContext* ctxt, const blockCipher* ciph)
 	if (ciph == (blockCipher*) 0)
 		return -1;
 
+	/*@-temptrans@*/
 	ctxt->algo = ciph;
+	/*@=temptrans@*/
 	ctxt->param = (blockCipherParam*) calloc(ciph->paramsize, 1);
 
+	/*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
 	if (ctxt->param == (blockCipherParam*) 0)
 		return -1;
 
 	return 0;
+	/*@=nullstate@*/
 }
 
 int blockCipherContextSetup(blockCipherContext* ctxt, const uint32* key, int keybits, cipherOperation op)
@@ -745,7 +795,9 @@ int blockCipherContextFree(blockCipherContext* ctxt)
 
 	ctxt->param = (blockCipherParam*) 0;
 
+	/*@-nullstate@*/ /* FIX: ctxt->param is NULL */
 	return 0;
+	/*@=nullstate@*/
 }
 
 #if WIN32
diff --git a/beecrypt/beecrypt.h b/beecrypt/beecrypt.h
index f43d8d8c9..76f1b257d 100644
--- a/beecrypt/beecrypt.h
+++ b/beecrypt/beecrypt.h
@@ -44,7 +44,8 @@
  * @param size		no. of ints of data
  * @return		0 on success, -1 on failure
  */
-typedef int (*entropyNext) (uint32* data, int size);
+typedef int (*entropyNext) (/*@out@*/ uint32* data, int size)
+	/*@modifies data @*/;
 
 /** \ingroup ES_m
  * Methods and parameters for entropy sources.
@@ -52,7 +53,7 @@ typedef int (*entropyNext) (uint32* data, int size);
  */
 typedef struct
 {
-/*@unused@*/ const char* name;		/*!< entropy source name */
+/*@observer@*/ const char* name;	/*!< entropy source name */
 /*@unused@*/ const entropyNext next;	/*!< return entropy function */
 } entropySource;
 
@@ -73,7 +74,7 @@ int entropySourceCount(void)
  * @param index		entropy source index
  * @return		entropy source pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const entropySource* entropySourceGet(int index)
 	/*@*/;
 
@@ -82,9 +83,11 @@ const entropySource* entropySourceGet(int index)
  * @param name		entropy source name
  * @return		entropy source pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+/*@-exportlocal@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const entropySource* entropySourceFind(const char* name)
 	/*@*/;
+/*@=exportlocal@*/
 
 /** \ingroup ES_m
  * Retrieve the default entropy source.
@@ -92,7 +95,7 @@ const entropySource* entropySourceFind(const char* name)
  * entropy source. Otherwise, use the 1st entry in the internal table.
  * @return		entropy source pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/ /*@unused@*/
 const entropySource* entropySourceDefault(void)
 	/*@*/;
 
@@ -127,7 +130,7 @@ typedef void randomGeneratorParam;
  * @return		0 on success, -1 on failure
  */
 typedef int (*randomGeneratorSetup) (randomGeneratorParam* param)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup PRNG_m
  * Re-seed the random generator with user-provided entropy.
@@ -138,7 +141,7 @@ typedef int (*randomGeneratorSetup) (randomGeneratorParam* param)
  * @return		0 on success, -1 on failure
  */
 typedef int (*randomGeneratorSeed) (randomGeneratorParam* param, const uint32* data, int size)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup PRNG_m
  * Return an array of 32-bit unsigned integers of given size with
@@ -149,8 +152,8 @@ typedef int (*randomGeneratorSeed) (randomGeneratorParam* param, const uint32* d
  * @param size		no. of ints of data
  * @return		0 on success, -1 on failure
  */
-typedef int (*randomGeneratorNext) (randomGeneratorParam* param, uint32* data, int size)
-	/*@modifies param, data @*/;
+typedef int (*randomGeneratorNext) (randomGeneratorParam* param, /*@out@*/ uint32* data, int size)
+	/*@modifies *param, *data @*/;
 
 /** \ingroup PRNG_m
  * Cleanup after using a generator.
@@ -159,7 +162,7 @@ typedef int (*randomGeneratorNext) (randomGeneratorParam* param, uint32* data, i
  * @return		0 on success, -1 on failure
  */
 typedef int (*randomGeneratorCleanup) (randomGeneratorParam* param)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup PRNG_m
  * Methods and parameters for random generators.
@@ -177,7 +180,7 @@ typedef int (*randomGeneratorCleanup) (randomGeneratorParam* param)
  */
 typedef struct
 {
-    const char* name;		/*!< random generator name */
+/*@observer@*/ const char* name;	/*!< random generator name */
     const unsigned int paramsize;
     const randomGeneratorSetup setup;
     const randomGeneratorSeed seed;
@@ -202,7 +205,7 @@ int randomGeneratorCount(void)
  * @param index		generator index
  * @return		generator pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const randomGenerator* randomGeneratorGet(int index)
 	/*@*/;
 
@@ -211,9 +214,11 @@ const randomGenerator* randomGeneratorGet(int index)
  * @param name		generator name
  * @return		generator pointer (or NULL)
  */
-BEEDLLAPI
+/*@-exportlocal@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const randomGenerator* randomGeneratorFind(const char* name)
 	/*@*/;
+/*@=exportlocal@*/
 
 /** \ingroup PRNG_m
  * Retrieve the default generator.
@@ -221,7 +226,7 @@ const randomGenerator* randomGeneratorFind(const char* name)
  * generator. Otherwise, use "fips186prng".
  * @return		generator pointer
  */
-BEEDLLAPI
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const randomGenerator* randomGeneratorDefault(void)
 	/*@*/;
 
@@ -235,7 +240,7 @@ const randomGenerator* randomGeneratorDefault(void)
 typedef struct
 {
     const randomGenerator* rng;		/*!< global functions and parameters */
-    randomGeneratorParam* param;	/*!< specific parameters */
+/*@only@*/ randomGeneratorParam* param;	/*!< specific parameters */
 } randomGeneratorContext;
 
 #ifdef __cplusplus
@@ -243,18 +248,18 @@ extern "C" {
 #endif
 
 /** \ingroup PRNG_m
- * Initialize a rendomGenerator instance.
+ * Initialize a randomGenerator instance.
  */
 BEEDLLAPI
 int randomGeneratorContextInit(randomGeneratorContext* ctxt, const randomGenerator* rng)
-	/*@modifies ctxt @*/;
+	/*@modifies ctxt->rng, ctxt->param @*/;
 
 /** \ingroup PRNG_m
- * Destroy a rendomGenerator instance.
+ * Destroy a randomGenerator instance.
  */
 BEEDLLAPI
 int randomGeneratorContextFree(randomGeneratorContext* ctxt)
-	/*@modifies ctxt @*/;
+	/*@modifies ctxt->rng, ctxt->param @*/;
 
 #ifdef __cplusplus
 }
@@ -276,7 +281,7 @@ typedef void hashFunctionParam;
  * @return		0 on success, -1 on failure
  */
 typedef int (*hashFunctionReset) (hashFunctionParam* param)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup HASH_m
  * Update the hash function with an array of bytes.
@@ -287,7 +292,7 @@ typedef int (*hashFunctionReset) (hashFunctionParam* param)
  * @return		0 on success, -1 on failure
  */
 typedef int (*hashFunctionUpdate) (hashFunctionParam* param, const byte* data, int size)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup HASH_m
  * Compute the digest of all the data passed to the hash function, and return
@@ -303,8 +308,8 @@ typedef int (*hashFunctionUpdate) (hashFunctionParam* param, const byte* data, i
  * @retval data		digest
  * @return		0 on success, -1 on failure
  */
-typedef int (*hashFunctionDigest) (hashFunctionParam* param, uint32* data)
-	/*@modifies param, data @*/;
+typedef int (*hashFunctionDigest) (hashFunctionParam* param, /*@out@*/ uint32* data)
+	/*@modifies *param, *data @*/;
 
 /** \ingroup HASH_m
  * Methods and parameters for hash functions.
@@ -312,7 +317,7 @@ typedef int (*hashFunctionDigest) (hashFunctionParam* param, uint32* data)
  */
 typedef struct
 {
-    const char* name;			/*!< hash function name */
+/*@observer@*/ const char* name;	/*!< hash function name */
     const unsigned int paramsize;	/*!< in bytes */
     const unsigned int blocksize;	/*!< in bytes */
     const unsigned int digestsize;	/*!< in bytes */
@@ -338,7 +343,7 @@ int hashFunctionCount(void)
  * @param index		hash function index
  * @return		hash function pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const hashFunction* hashFunctionGet(int index)
 	/*@*/;
 
@@ -347,17 +352,19 @@ const hashFunction* hashFunctionGet(int index)
  * @param name		hash function name
  * @return		hash function pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+/*@-exportlocal@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const hashFunction* hashFunctionFind(const char* name)
 	/*@*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_m
  * Retrieve the default hash function.
  * If the BEECRYPT_HASH environment variable is set, use that
  * hash function. Otherwise, use "sha1".
- * @return		hash function pointer
+ * @return		hash function pointer (or NULL)
  */
-BEEDLLAPI
+BEEDLLAPI /*@observer@*/ /*@null@*/ /*@unused@*/
 const hashFunction* hashFunctionDefault(void)
 	/*@*/;
 
@@ -406,7 +413,7 @@ int hashFunctionContextUpdate(hashFunctionContext* ctxt, const byte* data, int s
 
 /** \ingroup HASH_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int hashFunctionContextUpdateMC(hashFunctionContext* ctxt, const memchunk* m)
 	/*@modifies ctxt */;
 
@@ -420,11 +427,11 @@ int hashFunctionContextUpdateMP32(hashFunctionContext* ctxt, const mp32number* n
  */
 BEEDLLAPI
 int hashFunctionContextDigest(hashFunctionContext* ctxt, mp32number* dig)
-	/*@modifies ctxt */;
+	/*@modifies ctxt, *dig */;
 
 /** \ingroup HASH_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int hashFunctionContextDigestMatch(hashFunctionContext* ctxt, const mp32number* match)
 	/*@modifies ctxt */;
 
@@ -453,7 +460,7 @@ typedef void keyedHashFunctionParam;
  * @return		0 on success, -1 on failure
  */
 typedef int (*keyedHashFunctionSetup) (keyedHashFunctionParam* param, const uint32* key, int keybits)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup HMAC_m
  * Re-initialize the parameters of a keyed hash function.
@@ -462,7 +469,7 @@ typedef int (*keyedHashFunctionSetup) (keyedHashFunctionParam* param, const uint
  * @return		0 on success, -1 on failure
  */
 typedef int (*keyedHashFunctionReset) (keyedHashFunctionParam* param)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup HMAC_m
  * Update the keyed hash function with an array of bytes.
@@ -473,7 +480,7 @@ typedef int (*keyedHashFunctionReset) (keyedHashFunctionParam* param)
  * @return		0 on success, -1 on failure
  */
 typedef int (*keyedHashFunctionUpdate) (keyedHashFunctionParam* param, const byte* data, int size)
-	/*@modifies param @*/;
+	/*@modifies *param @*/;
 
 /** \ingroup HMAC_m
  * Compute the digest (or authentication code) of all the data passed to
@@ -490,7 +497,7 @@ typedef int (*keyedHashFunctionUpdate) (keyedHashFunctionParam* param, const byt
  * @return		0 on success, -1 on failure
  */
 typedef int (*keyedHashFunctionDigest) (keyedHashFunctionParam* param, /*@out@*/ uint32* data)
-	/*@modifies param, data @*/;
+	/*@modifies *param, *data @*/;
 
 /** \ingroup HMAC_m
  * Methods and parameters for keyed hash functions.
@@ -498,7 +505,7 @@ typedef int (*keyedHashFunctionDigest) (keyedHashFunctionParam* param, /*@out@*/
  */
 typedef struct
 {
-    const char* name;			/*!< keyed hash function name */
+/*@observer@*/ const char* name;	/*!< keyed hash function name */
     const unsigned int paramsize;	/*!< in bytes */
     const unsigned int blocksize;	/*!< in bytes */
     const unsigned int digestsize;	/*!< in bytes */
@@ -528,7 +535,7 @@ int keyedHashFunctionCount(void)
  * @param index		keyed hash function index
  * @return		keyed hash function pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const keyedHashFunction* keyedHashFunctionGet(int index)
 	/*@*/;
 
@@ -537,9 +544,11 @@ const keyedHashFunction* keyedHashFunctionGet(int index)
  * @param name		keyed hash function name
  * @return		keyed hash function pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+/*@-exportlocal@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const keyedHashFunction* keyedHashFunctionFind(const char* name)
 	/*@*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_m
  * Retrieve the default keyed hash function.
@@ -547,7 +556,7 @@ const keyedHashFunction* keyedHashFunctionFind(const char* name)
  * hash function. Otherwise, use "hmacsha1".
  * @return		keyed hash function pointer
  */
-BEEDLLAPI
+BEEDLLAPI /*@observer@*/ /*@null@*/ /*@unused@*/
 const keyedHashFunction* keyedHashFunctionDefault(void)
 	/*@*/;
 
@@ -590,13 +599,13 @@ int keyedHashFunctionContextSetup(keyedHashFunctionContext* ctxt, const uint32*
 
 /** \ingroup HMAC_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int keyedHashFunctionContextReset(keyedHashFunctionContext* ctxt)
 	/*@modifies ctxt @*/;
 
 /** \ingroup HMAC_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int keyedHashFunctionContextUpdate(keyedHashFunctionContext* ctxt, const byte* data, int size)
 	/*@modifies ctxt @*/;
 
@@ -608,7 +617,7 @@ int keyedHashFunctionContextUpdateMC(keyedHashFunctionContext* ctxt, const memch
 
 /** \ingroup HMAC_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int keyedHashFunctionContextUpdateMP32(keyedHashFunctionContext* ctxt, const mp32number* n)
 	/*@modifies ctxt @*/;
 
@@ -616,7 +625,7 @@ int keyedHashFunctionContextUpdateMP32(keyedHashFunctionContext* ctxt, const mp3
  */
 BEEDLLAPI
 int keyedHashFunctionContextDigest(keyedHashFunctionContext* ctxt, mp32number* dig)
-	/*@modifies ctxt @*/;
+	/*@modifies ctxt, *dig @*/;
 
 /** \ingroup HMAC_m
  */
@@ -664,7 +673,7 @@ typedef enum
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockModeEncrypt) (blockCipherParam* param, int count, uint32* dst, const uint32* src)
-	/*@modifies param, dst @*/;
+	/*@modifies *param, *dst @*/;
 
 /** \ingroup BC_m
  * @param param		blockcipher parameters
@@ -674,7 +683,7 @@ typedef int (*blockModeEncrypt) (blockCipherParam* param, int count, uint32* dst
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockModeDecrypt) (blockCipherParam* param, int count, uint32* dst, const uint32* src)
-	/*@modifies param, dst @*/;
+	/*@modifies *param, *dst @*/;
 
 /** \ingroup BC_m
  */
@@ -698,7 +707,7 @@ typedef struct
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockCipherSetup) (blockCipherParam* param, const uint32* key, int keybits, cipherOperation cipherOperation)
-	/*@*/;
+	/*@modifies param @*/;
 
 /** \ingroup BC_m
  * Initialize IV for blockcipher.
@@ -707,7 +716,7 @@ typedef int (*blockCipherSetup) (blockCipherParam* param, const uint32* key, int
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockCipherSetIV) (blockCipherParam* param, const uint32* data)
-	/*@*/;
+	/*@modifies param @*/;
 
 /** \ingroup BC_m
  * Encrypt one block of data (with bit size chosen by the blockcipher).
@@ -719,7 +728,7 @@ typedef int (*blockCipherSetIV) (blockCipherParam* param, const uint32* data)
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockCipherEncrypt) (blockCipherParam* param, uint32* dst, const uint32* src)
-	/*@modifies dst @*/;
+	/*@modifies param, dst @*/;
 
 /** \ingroup BC_m
  * Decrypt one block of data (with bit size chosen by the blockcipher).
@@ -731,7 +740,7 @@ typedef int (*blockCipherEncrypt) (blockCipherParam* param, uint32* dst, const u
  * @return		0 on success, -1 on failure
  */
 typedef int (*blockCipherDecrypt) (blockCipherParam* param, uint32* dst, const uint32* src)
-	/*@modifies dst @*/;
+	/*@modifies param, dst @*/;
 
 /** \ingroup BC_m
  * Methods and parameters for block ciphers.
@@ -739,7 +748,7 @@ typedef int (*blockCipherDecrypt) (blockCipherParam* param, uint32* dst, const u
  */
 typedef struct
 {
-    const char* name;			/*!< block cipher name */
+/*@observer@*/ const char* name;	/*!< block cipher name */
     const unsigned int paramsize;	/*!< in bytes */
     const unsigned int blocksize;	/*!< in bytes */
     const unsigned int keybitsmin;	/*!< min keysize in bits */
@@ -769,7 +778,7 @@ int blockCipherCount(void)
  * @param index		blockcipher index
  * @return		blockcipher pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const blockCipher* blockCipherGet(int index)
 	/*@*/;
 
@@ -778,9 +787,11 @@ const blockCipher* blockCipherGet(int index)
  * @param name		blockcipher name
  * @return		blockcipher pointer (or NULL)
  */
-BEEDLLAPI /*@null@*/
+/*@-exportlocal@*/
+BEEDLLAPI /*@observer@*/ /*@null@*/
 const blockCipher* blockCipherFind(const char* name)
 	/*@*/;
+/*@=exportlocal@*/
 
 /** \ingroup BC_m
  * Retrieve the default blockcipher.
@@ -788,7 +799,7 @@ const blockCipher* blockCipherFind(const char* name)
  * Otherwise, use "blowfish".
  * @return		blockcipher pointer
  */
-BEEDLLAPI
+BEEDLLAPI /*@observer@*/ /*@null@*/ /*@unused@*/
 const blockCipher* blockCipherDefault(void)
 	/*@*/;
 
@@ -824,7 +835,7 @@ int blockCipherContextSetup(blockCipherContext* ctxt, const uint32* key, int key
 
 /** \ingroup BC_m
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int blockCipherContextSetIV(blockCipherContext* ctxt, const uint32* iv)
 	/*@modifies ctxt @*/;
 
diff --git a/beecrypt/blockmode.h b/beecrypt/blockmode.h
index 2dffffa0c..2d825adf9 100644
--- a/beecrypt/blockmode.h
+++ b/beecrypt/blockmode.h
@@ -44,7 +44,7 @@ extern "C" {
  * @return		0 on success, -1 on failure
  */
 BEEDLLAPI
-int blockEncrypt(const blockCipher* bc, blockCipherParam* bp, cipherMode mode, int blocks, uint32* dst, const uint32* src)
+int blockEncrypt(const blockCipher* bc, blockCipherParam* bp, cipherMode mode, int blocks, /*@out@*/ uint32* dst, const uint32* src)
 	/*@modifies bp, dst @*/;
 
 /**
@@ -57,7 +57,7 @@ int blockEncrypt(const blockCipher* bc, blockCipherParam* bp, cipherMode mode, i
  * @return		0 on success, -1 on failure
  */
 BEEDLLAPI
-int blockDecrypt(const blockCipher* bc, blockCipherParam* bp, cipherMode mode, int blocks, uint32* dst, const uint32* src)
+int blockDecrypt(const blockCipher* bc, blockCipherParam* bp, cipherMode mode, int blocks, /*@out@*/ uint32* dst, const uint32* src)
 	/*@modifies bp, dst @*/;
 
 #ifdef __cplusplus
diff --git a/beecrypt/blockpad.c b/beecrypt/blockpad.c
index d9cdc08b3..7bf7ca713 100644
--- a/beecrypt/blockpad.c
+++ b/beecrypt/blockpad.c
@@ -61,7 +61,7 @@ memchunk* pkcs5Unpad(int blockbytes, memchunk* tmp)
 		byte padvalue;
 		int i;
 
-		if (tmp->data == (memchunk*) 0)
+		if (tmp->data == (byte*) 0)
 			return (memchunk*) 0;
 		padvalue = tmp->data[tmp->size - 1];
 		if (padvalue > blockbytes)
@@ -109,7 +109,7 @@ memchunk* pkcs5UnpadCopy(/*@unused@*/ int blockbytes, const memchunk* src)
 
 	if (src == (memchunk*) 0)
 		return (memchunk*) 0;
-	if (src->data == (memchunk*) 0)
+	if (src->data == (byte*) 0)
 		return (memchunk*) 0;
 
 	padvalue = src->data[src->size - 1];
diff --git a/beecrypt/blockpad.h b/beecrypt/blockpad.h
index fac1d05a8..4c0719d06 100644
--- a/beecrypt/blockpad.h
+++ b/beecrypt/blockpad.h
@@ -40,9 +40,9 @@ extern "C" {
  * @param tmp		buffer to pad
  * @return		buffer with pad added
  */
-BEEDLLAPI /*@only@*/ /*@null@*/
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* pkcs5Pad  (int blockbytes, /*@only@*/ /*@null@*/ memchunk* tmp)
-	/*@modifies tmp */;
+	/*@*/;
 
 /**
  * Shrink buffer to boundary.
@@ -51,7 +51,7 @@ memchunk* pkcs5Pad  (int blockbytes, /*@only@*/ /*@null@*/ memchunk* tmp)
  * @return		buffer with pad removed
  */
 BEEDLLAPI /*@only@*/ /*@null@*/
-memchunk* pkcs5Unpad(int blockbytes, /*@null@*/ memchunk* tmp)
+memchunk* pkcs5Unpad(int blockbytes, /*@returned@*/ /*@null@*/ memchunk* tmp)
 	/*@modifies tmp */;
 
 /**
@@ -70,7 +70,7 @@ memchunk* pkcs5PadCopy  (int blockbytes, const memchunk* src)
  * @param tmp		buffer to unpad
  * @return		copy of buffer with pad removed
  */
-BEEDLLAPI /*@only@*/ /*@null@*/
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* pkcs5UnpadCopy(int blockbytes, const memchunk* src)
 	/*@*/;
 
diff --git a/beecrypt/blowfish.h b/beecrypt/blowfish.h
index 6d223e780..f6c4311f5 100644
--- a/beecrypt/blowfish.h
+++ b/beecrypt/blowfish.h
@@ -49,55 +49,71 @@ extern "C" {
 
 /** \ingroup BC_blowfish_m
  */
-/*@unused@*/ extern const BEEDLLAPI blockCipher blowfish;
+extern const BEEDLLAPI blockCipher blowfish;
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishSetup  (blowfishParam* bp, const uint32* key, int keybits, cipherOperation op)
 	/*@modifies bp */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishSetIV  (blowfishParam* bp, const uint32* iv)
 	/*@modifies bp */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishEncrypt(blowfishParam* bp, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishDecrypt(blowfishParam* bp, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishECBEncrypt(blowfishParam* bp, int count, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishECBDecrypt(blowfishParam* bp, int count, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishCBCEncrypt(blowfishParam* bp, int count, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 /** \ingroup BC_blowfish_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int blowfishCBCDecrypt(blowfishParam* bp, int count, uint32* dst, const uint32* src)
 	/*@modifies bp, dst */;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/blowfishopt.h b/beecrypt/blowfishopt.h
index e1b57824a..23280c43f 100644
--- a/beecrypt/blowfishopt.h
+++ b/beecrypt/blowfishopt.h
@@ -1,8 +1,10 @@
-/*
- * blowfishopt.h
- *
- * Blowfish block cipher assembler-optimized routines, header
+/** \ingroup BC_blowfish_m BC_m
+ * \file blowfishopt.h
  *
+ * Blowfish block cipher assembler-optimized routines, header.
+ */
+
+/*
  * Copyright (c) 2000 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
@@ -34,14 +36,24 @@ extern "C" {
 #endif
 
 #if WIN32
-#if __INTEL__ && __MWERKS__
-#define ASM_BLOWFISHENCRYPT
-#define ASM_BLOWFISHDECRYPT
+# if defined(_MSC_VER) && defined(_M_IX86)
+#  define ASM_BLOWFISHENCRYPT
+#  define ASM_BLOWFISHDECRYPT
+# elif __INTEL__ && __MWERKS__
+#  define ASM_BLOWFISHENCRYPT
+#  define ASM_BLOWFISHDECRYPT
+# endif
 #endif
+
+#if defined(__GNUC__)
+# if defined(OPTIMIZE_I586) || defined(OPTIMIZE_I686)
+#  define ASM_BLOWFISHENCRYPT
+#  define ASM_BLOWFISHDECRYPT
+# endif
 #endif
 
-#ifdef __GNUC__
-#if defined(i586) || defined(i686)
+#if defined(__SUNPRO_C) || defined(__SUNPRO_CC)
+#if defined(OPTIMIZE_I586) || defined(OPTIMIZE_I686)
 #define ASM_BLOWFISHENCRYPT
 #define ASM_BLOWFISHDECRYPT
 #endif
diff --git a/beecrypt/dhaes.c b/beecrypt/dhaes.c
index 0ed7b9d73..676c71597 100644
--- a/beecrypt/dhaes.c
+++ b/beecrypt/dhaes.c
@@ -8,6 +8,23 @@
  * "DHAES: An Encryption Scheme Based on the Diffie-Hellman Problem"
  * Michel Abdalla, Mihir Bellare, Phillip Rogaway
  * September 1998
+ *
+ * Good combinations will be:
+ *
+ * - For 64-bit encryption:
+ *	- DHAES(MD5, Blowfish, HMAC-MD5) <- best candidate
+ *	- DHAES(MD5, Blowfish, HMAC-SHA-1)
+ *	- DHAES(MD5, Blowfish, HMAC-SHA-256)
+ *
+ * - For 96-bit encryption with 64-bit mac:
+ *	- DHAES(SHA-1, Blowfish, HMAC-MD5, 96)
+ *	- DHAES(SHA-1, Blowfish, HMAC-SHA-1, 96) <- best candidate
+ *	- DHAES(SHA-1, Blowfish, HMAC-SHA-256, 96) <- best candidate
+ *
+ * - For 128-bit encryption:
+ *	- DHAES(SHA-256, Blowfish, HMAC-MD5)
+ *	- DHAES(SHA-256, Blowfish, HMAC-SHA-1)
+ *	- DHAES(SHA-256, Blowfish, HMAC-SHA-256)
  */
 
 /*
@@ -45,25 +62,6 @@
 # include <malloc.h>
 #endif
 
-/**
- * Good combinations will be:
- *
- * - For 64-bit encryption:
- *	- DHAES(MD5, Blowfish, HMAC-MD5) <- best candidate
- *	- DHAES(MD5, Blowfish, HMAC-SHA-1)
- *	- DHAES(MD5, Blowfish, HMAC-SHA-256)
- *
- * - For 96-bit encryption with 64-bit mac:
- *	- DHAES(SHA-1, Blowfish, HMAC-MD5, 96)
- *	- DHAES(SHA-1, Blowfish, HMAC-SHA-1, 96) <- best candidate
- *	- DHAES(SHA-1, Blowfish, HMAC-SHA-256, 96) <- best candidate
- *
- * - For 128-bit encryption:
- *	- DHAES(SHA-256, Blowfish, HMAC-MD5)
- *	- DHAES(SHA-256, Blowfish, HMAC-SHA-1)
- *	- DHAES(SHA-256, Blowfish, HMAC-SHA-256)
- */
-
 int dhaes_pUsable(const dhaes_pParameters* params)
 {
 	int keybits = (params->hash->digestsize << 3); /* digestsize in bytes times 8 bits */
@@ -190,7 +188,7 @@ int dhaes_pContextFree(dhaes_pContext* ctxt)
 
 /**
  */
-static int dhaes_pContextSetup(dhaes_pContext* ctxt, const mp32number* private, const mp32number* public, const mp32number* message, cipherOperation op)
+static int dhaes_pContextSetup(dhaes_pContext* ctxt, const mp32number* privkey, const mp32number* pubkey, const mp32number* message, cipherOperation op)
 	/*@modifies ctxt @*/
 {
 	register int rc;
@@ -200,7 +198,7 @@ static int dhaes_pContextSetup(dhaes_pContext* ctxt, const mp32number* private,
 
 	/* compute the shared secret, Diffie-Hellman style */
 	mp32nzero(&secret);
-	if (dlsvdp_pDHSecret(&ctxt->param, private, public, &secret))
+	if (dlsvdp_pDHSecret(&ctxt->param, privkey, pubkey, &secret))
 		return -1;
 
 	/* compute the hash of the message (ephemeral public) key and the shared secret */
@@ -351,5 +349,7 @@ memchunk* dhaes_pContextDecrypt(dhaes_pContext* ctxt, const mp32number* ephemera
 
 decrypt_end:
 
+	/*@-usereleased@*/ /* LCL: cleartext released??? */
 	return cleartext;
+	/*@=usereleased@*/
 }
diff --git a/beecrypt/dhaes.h b/beecrypt/dhaes.h
index af071bdbe..0676f858f 100644
--- a/beecrypt/dhaes.h
+++ b/beecrypt/dhaes.h
@@ -63,44 +63,48 @@ extern "C" {
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int dhaes_pUsable(const dhaes_pParameters* params)
 	/*@*/;
+/*@=exportlocal@*/
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int dhaes_pContextInit       (dhaes_pContext* ctxt, const dhaes_pParameters* params)
 	/*@modifies ctxt */;
+/*@=exportlocal@*/
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dhaes_pContextInitDecrypt(dhaes_pContext* ctxt, const dhaes_pParameters* params, const mp32number* pri)
 	/*@modifies ctxt */;
 
 /**
  */
-BEEDLLAPI
-int dhaes_pContextInitEncrypt(dhaes_pContext* ctxt, const dhaes_pParameters* params, const mp32number* pri)
+BEEDLLAPI /*@unused@*/
+int dhaes_pContextInitEncrypt(dhaes_pContext* ctxt, const dhaes_pParameters* params, const mp32number* pub)
 	/*@modifies ctxt */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dhaes_pContextFree       (/*@only@*/ dhaes_pContext* ctxt)
 	/*@modifies ctxt */;
 
 
 /**
  */
-BEEDLLAPI /*@only@*/ /*@null@*/
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* dhaes_pContextEncrypt(dhaes_pContext* ctxt,       mp32number* ephemeralPublicKey,       mp32number* mac, const memchunk* cleartext, randomGeneratorContext* rng)
 	/*@modifies ctxt, ephemeralPublicKey, mac, rng */;
 
 /**
  */
-BEEDLLAPI /*@only@*/ /*@null@*/
+BEEDLLAPI /*@only@*/ /*@null@*/ /*@unused@*/
 memchunk* dhaes_pContextDecrypt(dhaes_pContext* ctxt, const mp32number* ephemeralPublicKey, const mp32number* mac, const memchunk* ciphertext)
 	/*@modifies ctxt */;
 
diff --git a/beecrypt/dldp.c b/beecrypt/dldp.c
index b85a94621..cee920ac5 100644
--- a/beecrypt/dldp.c
+++ b/beecrypt/dldp.c
@@ -42,13 +42,13 @@
 
 /**
  */
-static int dldp_pgoqGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, uint32* wksp)
-	/*@modifies dp, rgc, wksp @*/;
+static int dldp_pgoqGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, /*@out@*/ uint32* wksp)
+	/*@modifies dp, wksp @*/;
 
 /**
  */
-static int dldp_pgonGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, uint32* wksp)
-	/*@modifies dp, rgc, wksp @*/;
+static int dldp_pgonGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, /*@out@*/ uint32* wksp)
+	/*@modifies dp, wksp @*/;
 
 int dldp_pPrivate(const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x)
 {
@@ -96,7 +96,8 @@ int dldp_pEqual(const dldp_p* a, const dldp_p* b)
 /**
  * needs to make workspace of 8*size+2
  */
-int dldp_pValidate(const dldp_p* dp, randomGeneratorContext* rgc)
+static int dldp_pValidate(const dldp_p* dp, randomGeneratorContext* rgc)
+	/*@*/
 {
 	register uint32  size = dp->p.size;
 	register uint32* temp = (uint32*) malloc((8*size+2) * sizeof(uint32));
diff --git a/beecrypt/dldp.h b/beecrypt/dldp.h
index 5304b03d1..03c0e3004 100644
--- a/beecrypt/dldp.h
+++ b/beecrypt/dldp.h
@@ -48,9 +48,6 @@
  * g is either a generator of a subgroup of order q, or a generator of order
  *  n = (p-1)
  */
-
-/**
- */
 typedef struct
 {
 	mp32barrett p;
@@ -88,13 +85,13 @@ int dldp_pCopy(dldp_p* dst, const dldp_p* src)
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pPrivate(const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x)
 	/*@modifies rgc, x */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pPublic (const dldp_p* dp, const mp32number* x, mp32number* y)
 	/*@modifies y */;
 
@@ -128,13 +125,13 @@ int dldp_pgoqMake     (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, ui
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pgoqMakeSafe (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
 	/*@modifies dp, rgc */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pgoqGenerator(dldp_p* dp, randomGeneratorContext* rgc)
 	/*@modifies dp, rgc */;
 
@@ -157,13 +154,13 @@ int dldp_pgonMake     (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, ui
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pgonMakeSafe (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
 	/*@modifies dp, rgc */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dldp_pgonGenerator(dldp_p* dp, randomGeneratorContext* rgc)
 	/*@modifies dp, rgc */;
 
diff --git a/beecrypt/dlkp.h b/beecrypt/dlkp.h
index fe31849aa..90d87bb7a 100644
--- a/beecrypt/dlkp.h
+++ b/beecrypt/dlkp.h
@@ -47,25 +47,25 @@ extern "C" {
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlkp_pPair(dlkp_p* kp, randomGeneratorContext* rgc, const dldp_p* param)
 	/*@modifies kp, rgc */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlkp_pInit(dlkp_p* kp)
 	/*@modifies kp */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlkp_pFree(dlkp_p* kp)
 	/*@modifies kp */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlkp_pCopy(dlkp_p* dst, const dlkp_p* src)
 	/*@modifies dst */;
 
diff --git a/beecrypt/dlpk.h b/beecrypt/dlpk.h
index 7af797c90..f663d4385 100644
--- a/beecrypt/dlpk.h
+++ b/beecrypt/dlpk.h
@@ -44,37 +44,37 @@ extern "C" {
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlpk_pInit(dlpk_p* pk)
 	/*@modifies pk */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlpk_pFree(dlpk_p* pk)
 	/*@modifies pk */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int dlpk_pCopy(dlpk_p* dst, const dlpk_p* src)
 	/*@modifies dst */;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int  dlpk_pEqual(const dlpk_p* a, const dlpk_p* b)
 	/*@*/;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int  dlpk_pgoqValidate(const dlpk_p* pk, randomGeneratorContext* rgc, int cofactor)
 	/*@modifies rgc @*/;
 
 /**
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 int  dlpk_pgonValidate(const dlpk_p* pk, randomGeneratorContext* rgc)
 	/*@modifies rgc @*/;
 
diff --git a/beecrypt/elgamal.c b/beecrypt/elgamal.c
index 655b42fb0..d0540c968 100644
--- a/beecrypt/elgamal.c
+++ b/beecrypt/elgamal.c
@@ -1,5 +1,5 @@
 /** \ingroup ELGAMAL_m
- * elgamal.c
+ * \file elgamal.c
  *
  * ElGamal signature scheme, code
  *
diff --git a/beecrypt/endianness.c b/beecrypt/endianness.c
index a91d3acb0..b42e1dfc4 100644
--- a/beecrypt/endianness.c
+++ b/beecrypt/endianness.c
@@ -347,14 +347,14 @@ int decodeChars(javachar* c, const byte* data, int count)
 	return rc;
 }
 
-int readByte(javabyte* b, FILE* in)
+int readByte(javabyte* b, FILE* ifp)
 {
-	return fread(b, 1, 1, in);
+	return fread(b, 1, 1, ifp);
 }
 
-int readShort(javashort* s, FILE* in)
+int readShort(javashort* s, FILE* ifp)
 {
-	register int rc = fread(s, 2, 1, in);
+	register int rc = fread(s, 2, 1, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == 1)
 	{
@@ -365,9 +365,9 @@ int readShort(javashort* s, FILE* in)
 	return rc;
 }
 
-int readInt(javaint* i, FILE* in)
+int readInt(javaint* i, FILE* ifp)
 {
-	register int rc = fread(i, 4, 1, in);
+	register int rc = fread(i, 4, 1, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == 1)
 	{
@@ -378,9 +378,9 @@ int readInt(javaint* i, FILE* in)
 	return rc;
 }
 
-int readLong(javalong* l, FILE* in)
+int readLong(javalong* l, FILE* ifp)
 {
-	register int rc = fread(l, 8, 1, in);
+	register int rc = fread(l, 8, 1, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == 1)
 	{
@@ -391,9 +391,9 @@ int readLong(javalong* l, FILE* in)
 	return rc;
 }
 
-int readChar(javachar* c, FILE* in)
+int readChar(javachar* c, FILE* ifp)
 {
-	register int rc = fread(c, 2, 1, in);
+	register int rc = fread(c, 2, 1, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == 1)
 	{
@@ -404,9 +404,9 @@ int readChar(javachar* c, FILE* in)
 	return rc;
 }
 
-int readInts(javaint* i, FILE* in, int count)
+int readInts(javaint* i, FILE* ifp, int count)
 {
-	register int rc = fread(i, 4, count, in);
+	register int rc = fread(i, 4, count, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == count)
 	{
@@ -421,9 +421,9 @@ int readInts(javaint* i, FILE* in, int count)
 	return rc;
 }
 
-int readChars(javachar* c, FILE* in, int count)
+int readChars(javachar* c, FILE* ifp, int count)
 {
-	register int rc = fread(c, 2, count, in);
+	register int rc = fread(c, 2, count, ifp);
 	#if !(WORDS_BIGENDIAN)
 	if (rc == count)
 	{
@@ -438,52 +438,52 @@ int readChars(javachar* c, FILE* in, int count)
 	return rc;
 }
 
-int writeByte(javabyte b, FILE* out)
+int writeByte(javabyte b, FILE* ofp)
 {
-	return fwrite(&b, 1, 1, out);
+	return fwrite(&b, 1, 1, ofp);
 }
 
-int writeShort(javashort s, FILE* out)
+int writeShort(javashort s, FILE* ofp)
 {
 	#if !(WORDS_BIGENDIAN)
 	s = swap16(s);
 	#endif
-	return fwrite(&s, 2, 1, out);
+	return fwrite(&s, 2, 1, ofp);
 }
 
-int writeInt(javaint i, FILE* out)
+int writeInt(javaint i, FILE* ofp)
 {
 	#if !(WORDS_BIGENDIAN)
 	i = swap32(i);
 	#endif
-	return fwrite(&i, 4, 1, out);
+	return fwrite(&i, 4, 1, ofp);
 }
 
-int writeLong(javalong l, FILE* out)
+int writeLong(javalong l, FILE* ofp)
 {
 	#if !(WORDS_BIGENDIAN)
 	l = swap64(l);
 	#endif
-	return fwrite(&l, 8, 1, out);
+	return fwrite(&l, 8, 1, ofp);
 }
 
-int writeChar(javachar c, FILE* out)
+int writeChar(javachar c, FILE* ofp)
 {
 	#if !(WORDS_BIGENDIAN)
 	c = swap16(c);
 	#endif
-	return fwrite(&c, 2, 1, out);
+	return fwrite(&c, 2, 1, ofp);
 }
 
-int writeInts(const javaint* i, FILE* out, int count)
+int writeInts(const javaint* i, FILE* ofp, int count)
 {
 	#if WORDS_BIGENDIAN
-	return fwrite(i, 4, count, out);
+	return fwrite(i, 4, count, ofp);
 	#else
 	register int total = 0;
 	while (count-- > 0)
 	{
-		register int rc = writeInt(*(i++), out);
+		register int rc = writeInt(*(i++), ofp);
 		if (rc < 0)
 			break;
 		total += rc;
@@ -492,15 +492,15 @@ int writeInts(const javaint* i, FILE* out, int count)
 	#endif
 }
 
-int writeChars(const javachar* c, FILE* out, int count)
+int writeChars(const javachar* c, FILE* ofp, int count)
 {
 	#if WORDS_BIGENDIAN
-	return fwrite(c, 2, count, out);
+	return fwrite(c, 2, count, ofp);
 	#else
 	register int total = 0;
 	while (count-- > 0)
 	{
-		register int rc = writeChar(*(c++), out);
+		register int rc = writeChar(*(c++), ofp);
 		if (rc < 0)
 			break;
 		total += rc;
diff --git a/beecrypt/endianness.h b/beecrypt/endianness.h
index be43260fb..6a89f5387 100644
--- a/beecrypt/endianness.h
+++ b/beecrypt/endianness.h
@@ -96,131 +96,246 @@ inline int64 swap64(int64 n)
 	#endif
 }
 #else
+/*@-exportlocal@*/
+
+/**
+ */
  int16 swap16 (int16 n)
 	/*@*/;
+
+/**
+ */
 uint16 swapu16(uint16 n)
 	/*@*/;
+
+/**
+ */
  int32 swap32 (int32 n)
 	/*@*/;
+
+/**
+ */
 uint32 swapu32(uint32 n)
 	/*@*/;
+
+/**
+ */
  int64 swap64 (int64 n)
 	/*@*/;
+/*@=exportlocal@*/
 #endif
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-BEEDLLAPI
-int encodeByte(javabyte b, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeByte(javabyte b, /*@out@*/ byte* data)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeShort(javashort s, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeShort(javashort s, /*@out@*/ byte* data)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeInt(javaint i, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeInt(javaint i, /*@out@*/ byte* data)
 	/*@modifies data */;
 
-BEEDLLAPI
-int encodeLong(javalong l, byte* data)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeLong(javalong l, /*@out@*/ byte* data)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeChar(javachar c, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeChar(javachar c, /*@out@*/ byte* data)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeFloat(javafloat f, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeFloat(javafloat f, /*@out@*/ byte* data)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeDouble(javadouble d, byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeDouble(javadouble d, /*@out@*/ byte* data)
 	/*@modifies data */;
 
+/**
+ */
 BEEDLLAPI
-int encodeInts(const javaint* i, byte* data, int count)
+int encodeInts(const javaint* i, /*@out@*/ byte* data, int count)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeIntsPartial(const javaint* i, byte* data, int bytecount)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeIntsPartial(const javaint* i, /*@out@*/ byte* data, int bytecount)
 	/*@modifies data */;
-BEEDLLAPI
-int encodeChars(const javachar* c, byte* data, int count)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int encodeChars(const javachar* c, /*@out@*/ byte* data, int count)
 	/*@modifies data */;
 
-BEEDLLAPI
-int decodeByte(javabyte* b, const byte* data)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeByte(/*@out@*/ javabyte* b, const byte* data)
 	/*@modifies b */;
-BEEDLLAPI
-int decodeShort(javashort* s, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeShort(/*@out@*/ javashort* s, const byte* data)
 	/*@modifies s */;
-BEEDLLAPI
-int decodeInt(javaint* i, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeInt(/*@out@*/ javaint* i, const byte* data)
 	/*@modifies i */;
-BEEDLLAPI
-int decodeLong(javalong* l, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeLong(/*@out@*/ javalong* l, const byte* data)
 	/*@modifies l */;
-BEEDLLAPI
-int decodeChar(javachar* c, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeChar(/*@out@*/ javachar* c, const byte* data)
 	/*@modifies c */;
-BEEDLLAPI
-int decodeFloat(javafloat* f, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeFloat(/*@out@*/ javafloat* f, const byte* data)
 	/*@modifies f */;
-BEEDLLAPI
-int decodeDouble(javadouble* d, const byte* data)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeDouble(/*@out@*/ javadouble* d, const byte* data)
 	/*@modifies d */;
 
-BEEDLLAPI
-int decodeInts(javaint* i, const byte* data, int count)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeInts(/*@out@*/ javaint* i, const byte* data, int count)
 	/*@modifies i */;
+
+/**
+ */
 BEEDLLAPI
-int decodeIntsPartial(javaint* i, const byte* data, int bytecount)
+int decodeIntsPartial(/*@out@*/ javaint* i, const byte* data, int bytecount)
 	/*@modifies i */;
-BEEDLLAPI
-int decodeChars(javachar* c, const byte* data, int count)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int decodeChars(/*@out@*/ javachar* c, const byte* data, int count)
 	/*@modifies c */;
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int writeByte(javabyte b, FILE* ofp)
 	/*@modifies ofp, fileSystem */;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int writeShort(javashort s, FILE* ofp)
 	/*@modifies ofp, fileSystem */;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int writeInt(javaint i, FILE* ofp)
 	/*@modifies ofp, fileSystem */;
-BEEDLLAPI
+/*@=exportlocal@*/
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int writeLong(javalong l, FILE* ofp)
 	/*@modifies ofp, fileSystem */;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int writeChar(javachar c, FILE* ofp)
 	/*@modifies ofp, fileSystem */;
+/*@=exportlocal@*/
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int writeInts(const javaint* i, FILE* ofp, int count)
 	/*@modifies ofp, fileSystem */;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int writeChars(const javachar* c, FILE* ofp, int count)
 	/*@modifies ofp, fileSystem */;
 
-BEEDLLAPI
-int readByte(javabyte* b, FILE* ifp)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readByte(/*@out@*/ javabyte* b, FILE* ifp)
 	/*@modifies b, ifp, fileSystem */;
-BEEDLLAPI
-int readShort(javashort* s, FILE* ifp)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readShort(/*@out@*/ javashort* s, FILE* ifp)
 	/*@modifies s, ifp, fileSystem */;
-BEEDLLAPI
-int readInt(javaint* i, FILE* ifp)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readInt(/*@out@*/ javaint* i, FILE* ifp)
 	/*@modifies i, ifp, fileSystem */;
-BEEDLLAPI
-int readLong(javalong* l, FILE* ifp)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readLong(/*@out@*/ javalong* l, FILE* ifp)
 	/*@modifies l, ifp, fileSystem */;
-BEEDLLAPI
-int readChar(javachar* c, FILE* ifp)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readChar(/*@out@*/ javachar* c, FILE* ifp)
 	/*@modifies c, ifp, fileSystem */;
 
-BEEDLLAPI
-int readInts(javaint* i, FILE* ifp, int count)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readInts(/*@out@*/ javaint* i, FILE* ifp, int count)
 	/*@modifies i, ifp, fileSystem */;
-BEEDLLAPI
-int readChars(javachar* c, FILE* ifp, int count)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+int readChars(/*@out@*/ javachar* c, FILE* ifp, int count)
 	/*@modifies c, ifp, fileSystem */;
 
 #ifdef __cplusplus
diff --git a/beecrypt/entropy.c b/beecrypt/entropy.c
index 88f852093..eb61720e2 100644
--- a/beecrypt/entropy.c
+++ b/beecrypt/entropy.c
@@ -402,7 +402,9 @@ static int entropy_noise_gather(int fd, int samplesize, int channels, int swap,
 			if (errno == EAGAIN)
 			{
 				/* certain linux glibc versions are buggy and don't aio_suspend properly */
+				/*@-unrecog -noeffectuncon @*/
 				nanosleep(&my_aiocb_timeout, (struct timespec*) 0);
+				/*@=unrecog =noeffectuncon @*/
 
 				my_aiocb_timeout.tv_sec = (timeout / 1000);
 				my_aiocb_timeout.tv_nsec = (timeout % 1000) * 1000000;
@@ -425,7 +427,9 @@ static int entropy_noise_gather(int fd, int samplesize, int channels, int swap,
 					my_aiocb_timeout.tv_sec = (timeout / 1000);
 					my_aiocb_timeout.tv_nsec = (timeout % 1000) * 1000000;
 
+					/*@-unrecog -noeffectuncon @*/
 					nanosleep(&my_aiocb_timeout, (struct timespec*) 0);
+					/*@=unrecog =noeffectuncon @*/
 				}
 
 				if (rc < 0)
@@ -618,7 +622,7 @@ int entropy_wavein(uint32* data, int size)
 	rc = waveInOpen(&wavein, WAVE_MAPPER, &waveformatex, (DWORD) entropy_wavein_event, (DWORD) 0, CALLBACK_EVENT);
 	if (rc != MMSYSERR_NOERROR)
 	{
-		fprintf(stderr, "waveInOpen failed!\n"); fflush(stderr);
+		fprintf(stderr, "waveInOpen failed!\n"); (void) fflush(stderr);
 		ReleaseMutex(entropy_wavein_lock);
 		return -1;
 	}
@@ -649,21 +653,21 @@ int entropy_console(uint32* data, int size)
 		return -1;
 	}
 
-	printf("please press random keys on your keyboard\n"); fflush(stdout);
+	printf("please press random keys on your keyboard\n"); (void) fflush(stdout);
 
 	while (randombits)
 	{
 		if (!ReadConsoleInput(hStdin, &inEvent, 1, &inRet))
 		{
-			fprintf(stderr, "ReadConsoleInput failed\n"); fflush(stderr);
+			fprintf(stderr, "ReadConsoleInput failed\n"); (void) fflush(stderr);
 			return -1;
 		}
 		if ((inRet == 1) && (inEvent.EventType == KEY_EVENT) && inEvent.Event.KeyEvent.bKeyDown)
 		{
-			printf("."); fflush(stdout);
+			printf("."); (void) fflush(stdout);
 			if (!QueryPerformanceCounter(&hrtsample))
 			{
-				fprintf(stderr, "QueryPerformanceCounter failed\n"); fflush(stderr);
+				fprintf(stderr, "QueryPerformanceCounter failed\n"); (void) fflush(stderr);
 				return -1;
 			}
 
@@ -684,7 +688,7 @@ int entropy_console(uint32* data, int size)
 	
 	if (!FlushConsoleInputBuffer(hStdin))
 	{
-		fprintf(stderr, "FlushConsoleInputBuffer failed\n"); fflush(stderr);
+		fprintf(stderr, "FlushConsoleInputBuffer failed\n"); (void) fflush(stderr);
 		return -1;
 	}
 
@@ -888,10 +892,10 @@ static int opendevice(const char *device)
  * @return
  */
 static int entropy_randombits(int fd, int timeout, uint32* data, int size)
-	/*@modifies data @*/
+	/*@modifies fileSystem @*/
 {
 	register byte* bytedata = (byte*) data;
-	register int   bytesize = (size << 2);
+	register int   bytesize = (((unsigned)size) << 2);
 	register int rc;
 
 	#if ENABLE_AIO
@@ -904,9 +908,12 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
 	# endif
 
 	memset(&my_aiocb, 0, sizeof(struct aiocb));
+	memset(&my_aiocb_timeout, 0, sizeof(struct timespec));
 
 	my_aiocb.aio_fildes = fd;
+	/*@-unrecog@*/
 	my_aiocb.aio_sigevent.sigev_notify = SIGEV_NONE;
+	/*@=unrecog@*/
 	#endif
 
 	while (bytesize)
@@ -915,7 +922,9 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
 		my_aiocb.aio_buf = bytedata;
 		my_aiocb.aio_nbytes = bytesize;
 
+		/*@-moduncon@*/
 		rc = aio_read(&my_aiocb);
+		/*@=moduncon@*/
 		#else
 		rc = read(fd, bytedata, bytesize);
 		#endif
@@ -927,7 +936,9 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
 		my_aiocb_timeout.tv_sec = (timeout / 1000);
 		my_aiocb_timeout.tv_nsec = (timeout % 1000) * 1000000;
 
+		/*@-compdef -moduncon @*/
 		rc = aio_suspend(&my_aiocb_list, 1, &my_aiocb_timeout);
+		/*@=compdef =moduncon @*/
 
 		if (rc < 0)
 		{
@@ -935,13 +946,17 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
 			if (errno == EAGAIN)
 			{
 				/* certain linux glibc versions are buggy and don't aio_suspend properly */
+				/*@-unrecog -noeffectuncon @*/
 				nanosleep(&my_aiocb_timeout, (struct timespec*) 0);
+				/*@=unrecog =noeffectuncon @*/
 
 				my_aiocb_timeout.tv_sec = 0;
 				my_aiocb_timeout.tv_nsec = 0;
 
 				/* and try again */
+				/*@-compdef -moduncon @*/
 				rc = aio_suspend(&my_aiocb_list, 1, &my_aiocb_timeout);
+				/*@=compdef =moduncon @*/
 			}
 			#endif
 		}
@@ -951,29 +966,37 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
 			/* cancel any remaining reads */
 			while (rc != AIO_ALLDONE)
 			{
+				/*@-nullpass -moduncon @*/
 				rc = aio_cancel(fd, (struct aiocb*) 0);
+				/*@=nullpass =moduncon @*/
 
 				if (rc == AIO_NOTCANCELED)
 				{
 					my_aiocb_timeout.tv_sec = (timeout / 1000);
 					my_aiocb_timeout.tv_nsec = (timeout % 1000) * 1000000;
 
+					/*@-unrecog -noeffectuncon @*/
 					nanosleep(&my_aiocb_timeout, (struct timespec*) 0);
+					/*@=unrecog =noeffectuncon @*/
 				}
 
 				if (rc < 0)
-					break;
+					/*@innerbreak@*/ break;
 			}
 
 			return -1;
 		}
 
+		/*@-moduncon@*/
 		rc = aio_error(&my_aiocb);
+		/*@=moduncon@*/
 
 		if (rc < 0)
 			return -1;
 
+		/*@-moduncon@*/
 		rc = aio_return(&my_aiocb);
+		/*@=moduncon@*/
 
 		if (rc < 0)
 			return -1;
@@ -994,9 +1017,9 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
  * @return
  */
 static int entropy_ttybits(int fd, uint32* data, int size)
-	/*@modifies data @*/
+	/*@modifies fileSystem @*/
 {
-	uint32 randombits = size << 5;
+	uint32 randombits = ((uint32)size) << 5;
 	uint32 temp = 0;
 	byte dummy;
 
@@ -1027,8 +1050,10 @@ static int entropy_ttybits(int fd, uint32* data, int size)
 	}
 
 	tio_set = tio_save;
+	/*@-noeffect@*/	/* LCL: dunno @*/
 	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@*/
 	tio_set.c_iflag |= IGNBRK;			/* ignore <ctrl>-c */
 	tio_set.c_lflag &= ~(ECHO|ICANON);	/* don't echo characters */
 
@@ -1076,7 +1101,7 @@ static int entropy_ttybits(int fd, uint32* data, int size)
 			#endif
 			return -1;
 		}
-		printf("."); fflush(stdout);
+		printf("."); (void) fflush(stdout);
 		#if HAVE_GETHRTIME
 		hrtsample = gethrtime();
 		/* get 16 bits from the sample */
@@ -1086,10 +1111,10 @@ static int entropy_ttybits(int fd, uint32* data, int size)
 		randombits -= 16;
 		#elif HAVE_GETTIMEOFDAY
 		/* discard the 4 lowest bits i.e. 4 microseconds */
-		gettimeofday(&tvsample, 0);
+		(void) gettimeofday(&tvsample, 0);
 		/* get 8 bits from the sample */
 		temp <<= 8;
-		temp |= (uint8)(tvsample.tv_usec >> 2);
+		temp |= (uint8)(((unsigned)tvsample.tv_usec) >> 2);
 		randombits -= 8;
 		#else
 		# error Need alternative high-precision timer sample
@@ -1101,7 +1126,7 @@ static int entropy_ttybits(int fd, uint32* data, int size)
 	printf("\nthanks\n");
 
 	/* give the user 1 second to stop typing */
-	sleep(1);
+	(void) sleep(1);
 
 	#if HAVE_TERMIOS_H
 	/* change the tty settings, and flush input characters */
@@ -1183,7 +1208,7 @@ int entropy_dev_audio(uint32 *data, int size)
 					#if HAVE_ERRNO_H
 					perror("ioctl AUDIO_SETINFO failed");
 					#endif
-					close(dev_audio_fd);
+					(void) close(dev_audio_fd);
 
 					goto dev_audio_end;
 				}
@@ -1193,7 +1218,7 @@ int entropy_dev_audio(uint32 *data, int size)
 				#if HAVE_ERRNO_H
 				perror("ioctl AUDIO_SETINFO failed");
 				#endif
-				close(dev_audio_fd);
+				(void) close(dev_audio_fd);
 
 				goto dev_audio_end;
 			}
@@ -1205,7 +1230,7 @@ int entropy_dev_audio(uint32 *data, int size)
 	# error Unknown type of /dev/audio interface
 	#endif
 
-	close(dev_audio_fd);
+	(void) close(dev_audio_fd);
 
 dev_audio_end:
 	#ifdef _REENTRANT
@@ -1221,6 +1246,7 @@ dev_audio_end:
 
 #if HAVE_DEV_DSP
 int entropy_dev_dsp(uint32 *data, int size)
+	/*@modifies dev_dsp_fd @*/
 {
 	const char* timeout_env = getenv("BEECRYPT_ENTROPY_DSP_TIMEOUT");
 
@@ -1253,7 +1279,7 @@ int entropy_dev_dsp(uint32 *data, int size)
 			#if HAVE_ERRNO_H
 			perror("ioctl SNDCTL_DSP_GETFMTS failed");
 			#endif
-			close (dev_dsp_fd);
+			(void) close (dev_dsp_fd);
 
 			goto dev_dsp_end;
 		}
@@ -1296,7 +1322,7 @@ int entropy_dev_dsp(uint32 *data, int size)
 			/* No linear audio format available */
 			rc = -1;
 
-			close(dev_dsp_fd);
+			(void) close(dev_dsp_fd);
 
 			goto dev_dsp_end;
 		}
@@ -1306,7 +1332,7 @@ int entropy_dev_dsp(uint32 *data, int size)
 			#if HAVE_ERRNO_H
 			perror("ioctl SNDCTL_DSP_SETFMT failed");
 			#endif
-			close(dev_dsp_fd);
+			(void) close(dev_dsp_fd);
 
 			goto dev_dsp_end;
 		}
@@ -1324,7 +1350,7 @@ int entropy_dev_dsp(uint32 *data, int size)
 	# error Unknown type of /dev/dsp interface
 	#endif
 
-	close(dev_dsp_fd);
+	(void) close(dev_dsp_fd);
 
 dev_dsp_end:
 	#ifdef _REENTRANT
@@ -1341,6 +1367,7 @@ dev_dsp_end:
 
 #if HAVE_DEV_RANDOM
 int entropy_dev_random(uint32* data, int size)
+	/*@modifies dev_random_fd @*/
 {
 	const char* timeout_env = getenv("BEECRYPT_ENTROPY_RANDOM_TIMEOUT");
 
@@ -1367,7 +1394,7 @@ int entropy_dev_random(uint32* data, int size)
 	/* collect entropy, with timeout */
 	rc = entropy_randombits(dev_random_fd, timeout_env ? atoi(timeout_env) : 1000, data, size);
 
-	close(dev_random_fd);
+	(void) close(dev_random_fd);
 
 dev_random_end:
 	#ifdef _REENTRANT
@@ -1383,6 +1410,7 @@ dev_random_end:
 
 #if HAVE_DEV_URANDOM
 int entropy_dev_urandom(uint32* data, int size)
+	/*@modifies dev_urandom_fd @*/
 {
 	const char* timeout_env = getenv("BEECRYPT_ENTROPY_URANDOM_TIMEOUT");
 
@@ -1409,7 +1437,7 @@ int entropy_dev_urandom(uint32* data, int size)
 	/* collect entropy, with timeout */
 	rc = entropy_randombits(dev_urandom_fd, timeout_env ? atoi(timeout_env) : 1000, data, size);
 
-	close(dev_urandom_fd);
+	(void) close(dev_urandom_fd);
 
 dev_urandom_end:
 	#ifdef _REENTRANT
@@ -1425,6 +1453,7 @@ dev_urandom_end:
 
 #if HAVE_DEV_TTY
 int entropy_dev_tty(uint32* data, int size)
+	/*@modifies dev_tty_fd @*/
 {
 	register int rc;
 
@@ -1448,7 +1477,7 @@ int entropy_dev_tty(uint32* data, int size)
 
 	rc = entropy_ttybits(dev_tty_fd, data, size);
 
-	close(dev_tty_fd);
+	(void) close(dev_tty_fd);
 
 dev_tty_end:
 	#ifdef _REENTRANT
diff --git a/beecrypt/entropy.h b/beecrypt/entropy.h
index cca37c05c..1e1f2f1ed 100644
--- a/beecrypt/entropy.h
+++ b/beecrypt/entropy.h
@@ -63,28 +63,28 @@ int entropy_dev_audio (uint32* data, int size)
 /** \ingroup ES_dsp_m ES_m
  */
 int entropy_dev_dsp   (uint32* data, int size)
-	/*@modifies data */;
+	/*@modifies data, internalState @*/;
 #endif
 
 #if HAVE_DEV_RANDOM
 /** \ingroup ES_random_m ES_m
  */
 int entropy_dev_random(uint32* data, int size)
-	/*@modifies data */;
+	/*@modifies data, internalState @*/;
 #endif
 
 #if HAVE_DEV_URANDOM
 /** \ingroup ES_urandom_m ES_m
  */
 int entropy_dev_urandom(uint32* data, int size)
-	/*@modifies data */;
+	/*@modifies data, internalState @*/;
 #endif
 
 #if HAVE_DEV_TTY
 /** \ingroup ES_tty_m ES_m
  */
 int entropy_dev_tty   (uint32* data, int size)
-	/*@modifies data */;
+	/*@modifies data, internalState @*/;
 #endif
 #endif
 
diff --git a/beecrypt/fips180opt.h b/beecrypt/fips180opt.h
index f2f495df5..ff955701a 100644
--- a/beecrypt/fips180opt.h
+++ b/beecrypt/fips180opt.h
@@ -1,8 +1,10 @@
-/*
- * fips180opt.h
- *
- * SHA-1 assembler-optimized routines, header
+/** \ingroup HASH_sha1_m HASH_m
+ * \file fips180opt.h
  *
+ * SHA-1 assembler-optimized routines, header.
+ */
+
+/*
  * Copyright (c) 2000 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
@@ -34,15 +36,23 @@ extern "C" {
 #endif
 
 #if WIN32
-#if __INTEL__ && __MWERKS__
-#define ASM_SHA1PROCESS
-#endif
+# if defined(_MSC_VER) && defined(_M_IX86)
+#  define ASM_SHA1PROCESS
+# elif __INTEL__ && __MWERKS__
+#  define ASM_SHA1PROCESS
+# endif
 #endif
 
 #ifdef __GNUC__
-#if defined(i586) || defined(i686)
-#define ASM_SHA1PROCESS
+# if defined(OPTIMIZE_I586) || defined(OPTIMIZE_I686)
+#  define ASM_SHA1PROCESS
+# endif
 #endif
+
+#if defined(__SUNPRO_C) || defined(__SUNPRO_CC)
+# if defined(OPTIMIZE_I586) || defined(OPTIMIZE_I686)
+#  define ASM_SHA1PROCESS
+# endif
 #endif
 
 #ifdef __cplusplus
diff --git a/beecrypt/fips186.c b/beecrypt/fips186.c
index c8252a914..c90b7a2c5 100644
--- a/beecrypt/fips186.c
+++ b/beecrypt/fips186.c
@@ -1,7 +1,7 @@
 /** \ingroup PRNG_fips186_m DSA_m
  * \file fips186.c
  *
- * NIST FIPS 186 pseudo-random generator, code.
+ * NIST FIPS-186 pseudo-random generator, code.
  */
 
 /*
diff --git a/beecrypt/fips186.h b/beecrypt/fips186.h
index 77428443e..8d77433a7 100644
--- a/beecrypt/fips186.h
+++ b/beecrypt/fips186.h
@@ -1,7 +1,7 @@
 /** \ingroup PRNG_fips186_m DSA_m
  * \file fips186.h
  *
- * FIPS186 pseudo-random generator, with SHA-1 as H function, header.
+ * NIST FIPS-186 pseudo-random generator, with SHA-1 as H function, header.
  */
 
 /*
@@ -78,31 +78,39 @@ extern "C" {
 
 /**
  */
-/*@unused@*/ extern BEEDLLAPI const randomGenerator fips186prng;
+extern BEEDLLAPI const randomGenerator fips186prng;
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int fips186Setup  (fips186Param* fp)
 	/*@modifies fp */;
+/*@=exportlocal@*/
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int fips186Seed   (fips186Param* fp, const uint32* data, int size)
 	/*@modifies fp */;
+/*@=exportlocal@*/
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int fips186Next   (fips186Param* fp, uint32* data, int size)
 	/*@modifies fp, data */;
+/*@=exportlocal@*/
 
 /**
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int fips186Cleanup(fips186Param* fp)
 	/*@modifies fp */;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/hmac.c b/beecrypt/hmac.c
index 2f0d5b48a..ae51c290d 100644
--- a/beecrypt/hmac.c
+++ b/beecrypt/hmac.c
@@ -92,7 +92,9 @@ int hmacDigest(hmacParam* hp, const hashFunction* hash, hashFunctionParam* param
 		return -1;
 
 	/* digestsize is in bytes; divide by 4 to get the number of words */
+	/*@-compdef@*/ /* FIX: *data undef ??? Code looks bogus ... */
 	(void) encodeInts((const javaint*) data, (byte*) data, hash->digestsize >> 2);
+	/*@=compdef@*/
 
 	if (hash->update(param, (const byte*) data, hash->digestsize))
 		return -1;
diff --git a/beecrypt/hmacmd5.h b/beecrypt/hmacmd5.h
index 28bf4d6c9..30737bb16 100644
--- a/beecrypt/hmacmd5.h
+++ b/beecrypt/hmacmd5.h
@@ -46,31 +46,43 @@ extern "C" {
 
 /** \ingroup HMAC_md5_m
  */
-/*@unused@*/ extern BEEDLLAPI const keyedHashFunction hmacmd5;
+extern BEEDLLAPI const keyedHashFunction hmacmd5;
 
 /** \ingroup HMAC_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacmd5Setup (hmacmd5Param* sp, const uint32* key, int keybits)
+	/*@globals md5 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacmd5Reset (hmacmd5Param* sp)
+	/*@globals md5 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacmd5Update(hmacmd5Param* sp, const byte* data, int size)
+	/*@globals md5 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacmd5Digest(hmacmd5Param* sp, uint32* data)
+	/*@globals md5 @*/
 	/*@modifies sp, data @*/;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/hmacsha1.h b/beecrypt/hmacsha1.h
index e69bcf51a..1b613a465 100644
--- a/beecrypt/hmacsha1.h
+++ b/beecrypt/hmacsha1.h
@@ -46,31 +46,43 @@ extern "C" {
 
 /** \ingroup HMAC_sha1_m
  */
-/*@unused@*/ extern BEEDLLAPI const keyedHashFunction hmacsha1;
+extern BEEDLLAPI const keyedHashFunction hmacsha1;
 
 /** \ingroup HMAC_sha1_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha1Setup (hmacsha1Param* sp, const uint32* key, int keybits)
+	/*@globals sha1 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha1_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha1Reset (hmacsha1Param* sp)
+	/*@globals sha1 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha1_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha1Update(hmacsha1Param* sp, const byte* data, int size)
+	/*@globals sha1 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha1_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha1Digest(hmacsha1Param* sp, uint32* data)
+	/*@globals sha1 @*/
 	/*@modifies sp, data @*/;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/hmacsha256.h b/beecrypt/hmacsha256.h
index 91923f872..d0f06eb52 100644
--- a/beecrypt/hmacsha256.h
+++ b/beecrypt/hmacsha256.h
@@ -46,31 +46,43 @@ extern "C" {
 
 /** \ingroup HMAC_sha256_m
  */
-/*@unused@*/ extern BEEDLLAPI const keyedHashFunction hmacsha256;
+/*@observer@*/ /*@checkedstrict@*/ extern BEEDLLAPI const keyedHashFunction hmacsha256;
 
 /** \ingroup HMAC_sha256_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha256Setup (hmacsha256Param* sp, const uint32* key, int keybits)
+	/*@globals sha256 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha256_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha256Reset (hmacsha256Param* sp)
+	/*@globals sha256 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha256_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha256Update(hmacsha256Param* sp, const byte* data, int size)
+	/*@globals sha256 @*/
 	/*@modifies sp @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HMAC_sha256_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int hmacsha256Digest(hmacsha256Param* sp, uint32* data)
+	/*@globals sha256 @*/
 	/*@modifies sp, data @*/;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/javaglue.c b/beecrypt/javaglue.c
index 1585dca4a..60988a301 100644
--- a/beecrypt/javaglue.c
+++ b/beecrypt/javaglue.c
@@ -1,5 +1,14 @@
+/** \ingroup JAVA_m
+ * \file javaglue.c
+ */
+
 #define BEECRYPT_DLL_EXPORT
 
+#if defined(__LCLINT__)
+#endif
+#define	JNIEXPORT /*@unused@*/
+#define	JNICALL
+
 #include "beecrypt.h"
 #include "blockmode.h"
 
@@ -8,20 +17,38 @@
 #if HAVE_STDLIB_H
 # include <stdlib.h>
 #endif
+#if HAVE_MALLOC_H
+# include <malloc.h>
+#endif
 
 #include "javaglue.h"
 
+/* For now, I'm lazy ... */
+/*@-nullpass -nullret -shiftsigned -usedef -temptrans -freshtrans @*/
+/*@-noeffectuncon -globs -globnoglobs -modunconnomods -modnomods @*/
+
+#ifndef WORDS_BIGENDIAN
+# define WORDS_BIGENDIAN	0
+#endif
+
+/*@observer@*/
 static const char* JAVA_OUT_OF_MEMORY_ERROR = "java/lang/OutOfMemoryError";
+/*@observer@*/
 static const char* JAVA_PROVIDER_EXCEPTION = "java/security/ProviderException";
+/*@observer@*/
 static const char* JAVA_INVALID_KEY_EXCEPTION = "java/security/InvalidKeyException";
+/*@observer@*/
 static const char* MSG_OUT_OF_MEMORY = "out of memory";
+/*@observer@*/
 static const char* MSG_NO_SUCH_ALGORITHM = "algorithm not available";
+/*@observer@*/
 static const char* MSG_NO_ENTROPY_SOURCE = "no entropy source";
+/*@observer@*/
 static const char* MSG_INVALID_KEY = "invalid key";
 
 /* NativeMessageDigest */
 
-jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_find(JNIEnv* env, jclass dummy, jstring algorithm)
+jlong JNICALL Java_beecrypt_security_NativeMessageDigest_find(JNIEnv* env, /*@unused@*/ jclass dummy, jstring algorithm)
 {
 	const char* name = (*env)->GetStringUTFChars(env, algorithm, (jboolean*) 0);
 	const hashFunction* hash = hashFunctionFind(name);
@@ -30,24 +57,24 @@ jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_find(JNIEnv* env, jc
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_PROVIDER_EXCEPTION);
 		if (ex != (jclass) 0)
-			(*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
+			(void) (*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
 	}
 	return (jlong) hash;
 }
 
-jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_allocParam(JNIEnv* env, jclass dummy, jlong hash)
+jlong JNICALL Java_beecrypt_security_NativeMessageDigest_allocParam(JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash)
 {
 	void *param = malloc(((const hashFunction*) hash)->paramsize);
 	if (param == (void*) 0)
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex != (jclass) 0)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 	}
 	return (jlong) param;
 }
 
-jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_cloneParam(JNIEnv* env, jclass dummy, jlong hash, jlong param)
+jlong JNICALL Java_beecrypt_security_NativeMessageDigest_cloneParam(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash, jlong param)
 {
 	unsigned int paramsize = ((const hashFunction*) hash)->paramsize;
 	void *clone = malloc(paramsize);
@@ -55,23 +82,23 @@ jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_cloneParam(JNIEnv* e
 	return (jlong) clone;
 }
 
-void JNICALL Java_com_beeyond_security_NativeMessageDigest_freeParam(JNIEnv* env, jclass dummy, jlong param)
+void JNICALL Java_beecrypt_security_NativeMessageDigest_freeParam(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong param)
 {
 	if (param)
 		free((void*) param);
 }
 
-void JNICALL Java_com_beeyond_security_NativeMessageDigest_reset(JNIEnv* env, jclass dummy, jlong hash, jlong param)
+void JNICALL Java_beecrypt_security_NativeMessageDigest_reset(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash, jlong param)
 {
-	((const hashFunction*) hash)->reset((hashFunctionParam*) param);
+	(void) ((const hashFunction*) hash)->reset((hashFunctionParam*) param);
 }
 
-void JNICALL Java_com_beeyond_security_NativeMessageDigest_update(JNIEnv* env, jclass dummy, jlong hash, jlong param, jbyte input)
+void JNICALL Java_beecrypt_security_NativeMessageDigest_update(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash, jlong param, jbyte input)
 {
-	((const hashFunction*) hash)->update((hashFunctionParam*) param, (const byte*) &input, 1);
+	(void) ((const hashFunction*) hash)->update((hashFunctionParam*) param, (const byte*) &input, 1);
 }
 
-void JNICALL Java_com_beeyond_security_NativeMessageDigest_updateBlock(JNIEnv* env, jclass dummy, jlong hash, jlong param, jbyteArray input, jint offset, jint len)
+void JNICALL Java_beecrypt_security_NativeMessageDigest_updateBlock(JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash, jlong param, jbyteArray input, jint offset, jint len)
 {
 	jbyte* data = (*env)->GetByteArrayElements(env, input, (jboolean*) 0);
 	if (data == (jbyte*) 0)
@@ -79,14 +106,14 @@ void JNICALL Java_com_beeyond_security_NativeMessageDigest_updateBlock(JNIEnv* e
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		(*env)->ReleaseByteArrayElements(env, input, data, JNI_ABORT);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
-	((const hashFunction*) hash)->update((hashFunctionParam*) param, (const byte*) data+offset, len);
+	(void) ((const hashFunction*) hash)->update((hashFunctionParam*) param, (const byte*) data+offset, len);
 	(*env)->ReleaseByteArrayElements(env, input, data, JNI_ABORT);
 }
 
-jbyteArray JNICALL Java_com_beeyond_security_NativeMessageDigest_digest(JNIEnv* env, jclass dummy, jlong hash, jlong param)
+jbyteArray JNICALL Java_beecrypt_security_NativeMessageDigest_digest(JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash, jlong param)
 {
 	jbyteArray digestArray;
 	jbyte* digest;
@@ -101,7 +128,7 @@ jbyteArray JNICALL Java_com_beeyond_security_NativeMessageDigest_digest(JNIEnv*
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return (jbyteArray) 0;
 	}
 
@@ -114,17 +141,17 @@ jbyteArray JNICALL Java_com_beeyond_security_NativeMessageDigest_digest(JNIEnv*
 			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 			(*env)->ReleaseByteArrayElements(env, digestArray, digest, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return (jbyteArray) 0;
 		}
 
-		((const hashFunction*) hash)->digest((hashFunctionParam*) param, data);
-		encodeInts((const javaint*) data, digest, digestwords);
+		(void) ((const hashFunction*) hash)->digest((hashFunctionParam*) param, data);
+		(void) encodeInts((const javaint*) data, digest, digestwords);
 		free(data);
 	}
 	else
 	{	/* aligned */
-		((const hashFunction*) hash)->digest((hashFunctionParam*) param, (uint32*) digest);
+		(void) ((const hashFunction*) hash)->digest((hashFunctionParam*) param, (uint32*) digest);
 	}
 
 	(*env)->ReleaseByteArrayElements(env, digestArray, digest, 0);
@@ -132,14 +159,14 @@ jbyteArray JNICALL Java_com_beeyond_security_NativeMessageDigest_digest(JNIEnv*
 	return digestArray;
 }
 
-jint JNICALL Java_com_beeyond_security_NativeMessageDigest_digestLength(JNIEnv* env, jclass dummy, jlong hash)
+jint JNICALL Java_beecrypt_security_NativeMessageDigest_digestLength(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong hash)
 {
 	return (jint) ((const hashFunction*) hash)->digestsize;
 }
 
 /* NativeSecureRandom */
 
-jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_find(JNIEnv* env, jclass dummy, jstring algorithm)
+jlong JNICALL Java_beecrypt_security_NativeSecureRandom_find(JNIEnv* env, /*@unused@*/ jclass dummy, jstring algorithm)
 {
 	const char* name = (*env)->GetStringUTFChars(env, algorithm, (jboolean*) 0);
 	const randomGenerator* prng = randomGeneratorFind(name);
@@ -148,24 +175,24 @@ jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_find(JNIEnv* env, jcl
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_PROVIDER_EXCEPTION);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
+			(void) (*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
 	}
 	return (jlong) prng;
 }
 
-jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_allocParam(JNIEnv* env, jclass dummy, jlong prng)
+jlong JNICALL Java_beecrypt_security_NativeSecureRandom_allocParam(JNIEnv* env, /*@unused@*/ jclass dummy, jlong prng)
 {
 	void *param = malloc(((const randomGenerator*) prng)->paramsize);
 	if (param == (void*) 0)
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 	}
 	return (jlong) param;
 }
 
-jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_cloneParam(JNIEnv* env, jclass dummy, jlong prng, jlong param)
+jlong JNICALL Java_beecrypt_security_NativeSecureRandom_cloneParam(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong prng, jlong param)
 {
 	unsigned int paramsize = ((const randomGenerator*) prng)->paramsize;
 	void *clone = malloc(paramsize);
@@ -173,18 +200,18 @@ jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_cloneParam(JNIEnv* en
 	return (jlong) clone;
 }
 
-void JNICALL Java_com_beeyond_security_NativeSecureRandom_freeParam(JNIEnv* env, jclass dummy, jlong param)
+void JNICALL Java_beecrypt_security_NativeSecureRandom_freeParam(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong param)
 {
 	if (param)
 		free((void*) param);
 }
 
-void JNICALL Java_com_beeyond_security_NativeSecureRandom_setup(JNIEnv* env, jclass dummy, jlong prng, jlong param)
+void JNICALL Java_beecrypt_security_NativeSecureRandom_setup(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong prng, jlong param)
 {
-	((const randomGenerator*) prng)->setup((randomGeneratorParam*) param);
+	(void) ((const randomGenerator*) prng)->setup((randomGeneratorParam*) param);
 }
 
-void JNICALL Java_com_beeyond_security_NativeSecureRandom_setSeed(JNIEnv* env, jclass dummy, jlong prng, jlong param, jbyteArray seedArray)
+void JNICALL Java_beecrypt_security_NativeSecureRandom_setSeed(JNIEnv* env, /*@unused@*/ jclass dummy, jlong prng, jlong param, jbyteArray seedArray)
 {
 	/* BeeCrypt takes size in words */
 	jsize seedSize = (*env)->GetArrayLength(env, seedArray);
@@ -195,7 +222,7 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_setSeed(JNIEnv* env, j
 		{
 			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		/* check memory alignment of seed and seedSize */
@@ -209,23 +236,23 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_setSeed(JNIEnv* env, j
 				jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 				(*env)->ReleaseByteArrayElements(env, seedArray, seed, JNI_ABORT);
 				if (ex)
-					(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+					(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 				return;
 			}
-			decodeIntsPartial(data, seed, seedSize);
-			((const randomGenerator*) prng)->seed((randomGeneratorParam*) param, data, size);
+			(void) decodeIntsPartial(data, seed, seedSize);
+			(void) ((const randomGenerator*) prng)->seed((randomGeneratorParam*) param, data, size);
 			free(data);
 		}
 		else
 		{	/* aligned and properly sized */
-			((const randomGenerator*) prng)->seed((randomGeneratorParam*) param, (uint32*) seed, seedSize >> 2);
+			(void) ((const randomGenerator*) prng)->seed((randomGeneratorParam*) param, (uint32*) seed, seedSize >> 2);
 		}
 
 		(*env)->ReleaseByteArrayElements(env, seedArray, seed, JNI_ABORT);
 	}
 }
 
-void JNICALL Java_com_beeyond_security_NativeSecureRandom_nextBytes(JNIEnv* env, jclass dummy, jlong prng, jlong param, jbyteArray bytesArray)
+void JNICALL Java_beecrypt_security_NativeSecureRandom_nextBytes(JNIEnv* env, /*@unused@*/ jclass dummy, jlong prng, jlong param, jbyteArray bytesArray)
 {
 	/* BeeCrypt takes size in words */
 	jsize bytesSize = (*env)->GetArrayLength(env, bytesArray);
@@ -236,7 +263,7 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_nextBytes(JNIEnv* env,
 		{
 			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 
@@ -251,24 +278,24 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_nextBytes(JNIEnv* env,
 				jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 				(*env)->ReleaseByteArrayElements(env, bytesArray, bytes, JNI_ABORT);
 				if (ex)
-					(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+					(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 				return;
 			}
 
-			((const randomGenerator*) prng)->next((randomGeneratorParam*) param, data, size);
+			(void) ((const randomGenerator*) prng)->next((randomGeneratorParam*) param, data, size);
 			memcpy(bytes, data, bytesSize);
 			free(data);
 		}
 		else
 		{	/* aligned and properly sized */
-			((const randomGenerator*) prng)->next((randomGeneratorParam*) param, (uint32*) bytes, bytesSize >> 2);
+			(void) ((const randomGenerator*) prng)->next((randomGeneratorParam*) param, (uint32*) bytes, bytesSize >> 2);
 		}
 
 		(*env)->ReleaseByteArrayElements(env, bytesArray, bytes, 0);
 	}
 }
 
-void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed(JNIEnv* env, jclass dummy, jbyteArray seedArray)
+void JNICALL Java_beecrypt_security_NativeSecureRandom_generateSeed(JNIEnv* env, /*@unused@*/ jclass dummy, jbyteArray seedArray)
 {
 	/* BeeCrypt takes size in words */
 	jsize seedSize = (*env)->GetArrayLength(env, seedArray);
@@ -283,7 +310,7 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed(JNIEnv* e
 		{
 			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 
@@ -292,7 +319,7 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed(JNIEnv* e
 			jclass ex = (*env)->FindClass(env, JAVA_PROVIDER_EXCEPTION);
 			(*env)->ReleaseByteArrayElements(env, seedArray, seed, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_NO_ENTROPY_SOURCE);
+				(void) (*env)->ThrowNew(env, ex, MSG_NO_ENTROPY_SOURCE);
 			return;
 		}
 
@@ -301,13 +328,13 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed(JNIEnv* e
 		{	/* unaligned */
 			int size = (seedSize+3) >> 2;
 			uint32* data = (uint32*) malloc(size * sizeof(uint32));
-			ents->next(data, size);
+			(void) ents->next(data, size);
 			memcpy(seed, data, seedSize);
 			free(data);
 		}
 		else
 		{	/* aligned */
-			ents->next((uint32*) seed, seedSize >> 2);
+			(void) ents->next((uint32*) seed, seedSize >> 2);
 		}
 
 		(*env)->ReleaseByteArrayElements(env, seedArray, seed, 0);
@@ -316,7 +343,7 @@ void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed(JNIEnv* e
 
 /* NativeBlockCipher */
 
-jlong JNICALL Java_com_beeyond_crypto_NativeBlockCipher_find(JNIEnv* env, jclass dummy, jstring algorithm)
+jlong JNICALL Java_beecrypt_crypto_NativeBlockCipher_find(JNIEnv* env, /*@unused@*/ jclass dummy, jstring algorithm)
 {
 	const char* name = (*env)->GetStringUTFChars(env, algorithm, (jboolean*) 0);
 	const blockCipher* ciph = blockCipherFind(name);
@@ -325,35 +352,35 @@ jlong JNICALL Java_com_beeyond_crypto_NativeBlockCipher_find(JNIEnv* env, jclass
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_PROVIDER_EXCEPTION);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
+			(void) (*env)->ThrowNew(env, ex, MSG_NO_SUCH_ALGORITHM);
 	}
 	return (jlong) ciph;
 }
 
-jlong JNICALL Java_com_beeyond_crypto_NativeBlockCipher_allocParam(JNIEnv* env, jclass dummy, jlong ciph)
+jlong JNICALL Java_beecrypt_crypto_NativeBlockCipher_allocParam(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph)
 {
 	void *param = malloc(((const blockCipher*) ciph)->paramsize);
 	if (param == (void*) 0)
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 	}
 	return (jlong) param;
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_freeParam(JNIEnv* env, jclass dummy, jlong param)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_freeParam(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong param)
 {
 	if (param)
 		free((void*) param);
 }
 
-jint JNICALL Java_com_beeyond_crypto_NativeBlockCipher_getBlockSize(JNIEnv* env, jclass dummy, jlong ciph)
+jint JNICALL Java_beecrypt_crypto_NativeBlockCipher_getBlockSize(/*@unused@*/ JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph)
 {
 	return ((const blockCipher*) ciph)->blocksize;
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setup(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jint mode, jbyteArray keyArray)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_setup(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jint mode, jbyteArray keyArray)
 {
 	/* BeeCrypt takes key in 32 bit words with size in bits */
 	jsize keysize = (*env)->GetArrayLength(env, keyArray);
@@ -379,7 +406,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setup(JNIEnv* env, jclass
 		{
 			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 
@@ -393,11 +420,11 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setup(JNIEnv* env, jclass
 				jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 				(*env)->ReleaseByteArrayElements(env, keyArray, key, JNI_ABORT);
 				if (ex)
-					(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+					(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 				return;
 			}
 
-			decodeIntsPartial(data, key, keysize);
+			(void) decodeIntsPartial(data, key, keysize);
 			rc = ((const blockCipher*) ciph)->setup((blockCipherParam*) param, data, keysize << 3, nativeop);
 			free(data);
 		}
@@ -410,56 +437,63 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setup(JNIEnv* env, jclass
 		{
 			jclass ex = (*env)->FindClass(env, JAVA_INVALID_KEY_EXCEPTION);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_INVALID_KEY);
+				(void) (*env)->ThrowNew(env, ex, MSG_INVALID_KEY);
 		}
 
 		(*env)->ReleaseByteArrayElements(env, keyArray, key, JNI_ABORT);
 	}
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setIV(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jbyteArray ivArray)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_setIV(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jbyteArray ivArray)
 {
-	jsize ivsize = (*env)->GetArrayLength(env, ivArray);
-
-	if (ivsize > 0)
+	if (ivArray == (jbyteArray) 0)
 	{
-		jbyte* iv = (*env)->GetByteArrayElements(env, ivArray, (jboolean*) 0);
-	
-		if (iv == (jbyte*) 0)
-		{
-			jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
-			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
-			return;
-		}
-	
-		if (!WORDS_BIGENDIAN || ((int) iv & 0x3) || (ivsize & 0x3))
-		{	/* unaligned */
-			int size = (ivsize + 3) >> 2;
-			uint32* data = (uint32*) malloc(size * sizeof(uint32));
+		(void) ((const blockCipher*) ciph)->setiv((blockCipherParam*) param, 0);
+	}
+	else
+	{
+		jsize ivsize = (*env)->GetArrayLength(env, ivArray);
 
-			if (data == (uint32*) 0)
+		if (ivsize > 0)
+		{
+			jbyte* iv = (*env)->GetByteArrayElements(env, ivArray, (jboolean*) 0);
+		
+			if (iv == (jbyte*) 0)
 			{
 				jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
-				(*env)->ReleaseByteArrayElements(env, ivArray, iv, JNI_ABORT);
 				if (ex)
-					(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+					(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 				return;
 			}
-
-			decodeIntsPartial(data, iv, ivsize);
-			((const blockCipher*) ciph)->setiv((blockCipherParam*) param, data);
-			free(data);
-		}
-		else
-		{	/* aligned */
-			((const blockCipher*) ciph)->setiv((blockCipherParam*) param, (uint32*) iv);
+		
+			if (!WORDS_BIGENDIAN || ((int) iv & 0x3) || (ivsize & 0x3))
+			{	/* unaligned */
+				int size = (ivsize + 3) >> 2;
+				uint32* data = (uint32*) malloc(size * sizeof(uint32));
+
+				if (data == (uint32*) 0)
+				{
+					jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
+					(*env)->ReleaseByteArrayElements(env, ivArray, iv, JNI_ABORT);
+					if (ex)
+						(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+					return;
+				}
+
+				(void) decodeIntsPartial(data, iv, ivsize);
+				(void) ((const blockCipher*) ciph)->setiv((blockCipherParam*) param, data);
+				free(data);
+			}
+			else
+			{	/* aligned */
+				(void) ((const blockCipher*) ciph)->setiv((blockCipherParam*) param, (uint32*) iv);
+			}
+			(*env)->ReleaseByteArrayElements(env, ivArray, iv, JNI_ABORT);
 		}
-		(*env)->ReleaseByteArrayElements(env, ivArray, iv, JNI_ABORT);
 	}
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
 {
 	jbyte* input;
 	jbyte* output;
@@ -469,7 +503,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, j
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 	output = (*env)->GetByteArrayElements(env, outputArray, (jboolean*) 0);
@@ -478,7 +512,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, j
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 
@@ -494,7 +528,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		dataout = (uint32*) malloc(blocks * sizeof(uint32));
@@ -505,23 +539,23 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		memcpy(datain, input+inputOffset, blocks * sizeof(uint32));
-		blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, dataout, datain);
+		(void) blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, dataout, datain);
 		memcpy(output+outputOffset, dataout, blocks * sizeof(uint32));
 	}
 	else
 	{	/* aligned */
-		blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
+		(void) blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
 	}
 
 	(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 	(*env)->ReleaseByteArrayElements(env, outputArray, output, 0);
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
 {
 	jbyte* input;
 	jbyte* output;
@@ -531,7 +565,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, j
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 	output = (*env)->GetByteArrayElements(env, outputArray, (jboolean*) 0);
@@ -540,7 +574,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, j
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 
@@ -556,7 +590,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		dataout = (uint32*) malloc(blocks * sizeof(uint32));
@@ -567,23 +601,23 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		memcpy(datain, input+inputOffset, blocks * sizeof(uint32));
-		blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, dataout, datain);
+		(void) blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, dataout, datain);
 		memcpy(output+outputOffset, dataout, blocks * sizeof(uint32));
 	}
 	else
 	{	/* aligned */
-		blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
+		(void) blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, ECB, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
 	}
 
 	(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 	(*env)->ReleaseByteArrayElements(env, outputArray, output, 0);
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
 {
 	jbyte* input;
 	jbyte* output;
@@ -593,7 +627,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, j
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 	output = (*env)->GetByteArrayElements(env, outputArray, (jboolean*) 0);
@@ -602,7 +636,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, j
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 
@@ -618,7 +652,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		dataout = (uint32*) malloc(blocks * sizeof(uint32));
@@ -629,23 +663,23 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		memcpy(datain, input+inputOffset, blocks * sizeof(uint32));
-		blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, dataout, datain);
+		(void) blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, dataout, datain);
 		memcpy(output+outputOffset, dataout, blocks * sizeof(uint32));
 	}
 	else
 	{	/* aligned */
-		blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
+		(void) blockEncrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
 	}
 
 	(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 	(*env)->ReleaseByteArrayElements(env, outputArray, output, 0);
 }
 
-void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
+void JNICALL Java_beecrypt_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, /*@unused@*/ jclass dummy, jlong ciph, jlong param, jbyteArray inputArray, jint inputOffset, jbyteArray outputArray, jint outputOffset, jint blocks)
 {
 	jbyte* input;
 	jbyte* output;
@@ -655,7 +689,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, j
 	{
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 	output = (*env)->GetByteArrayElements(env, outputArray, (jboolean*) 0);
@@ -664,7 +698,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, j
 		jclass ex = (*env)->FindClass(env, JAVA_OUT_OF_MEMORY_ERROR);
 		(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 		if (ex)
-			(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+			(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 		return;
 	}
 
@@ -680,7 +714,7 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		dataout = (uint32*) malloc(blocks * sizeof(uint32));
@@ -691,20 +725,23 @@ void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, j
 			(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 			(*env)->ReleaseByteArrayElements(env, outputArray, output, JNI_ABORT);
 			if (ex)
-				(*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
+				(void) (*env)->ThrowNew(env, ex, MSG_OUT_OF_MEMORY);
 			return;
 		}
 		memcpy(datain, input+inputOffset, blocks * sizeof(uint32));
-		blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, dataout, datain);
+		(void) blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, dataout, datain);
 		memcpy(output+outputOffset, dataout, blocks * sizeof(uint32));
 	}
 	else
 	{	/* aligned */
-		blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
+		(void) blockDecrypt((const blockCipher*) ciph, (blockCipherParam*) param, CBC, blocks, (uint32*)(output+outputOffset), (uint32*) (input+inputOffset));
 	}
 
 	(*env)->ReleaseByteArrayElements(env, inputArray, input, JNI_ABORT);
 	(*env)->ReleaseByteArrayElements(env, outputArray, output, 0);
 }
 
+/*@=noeffectuncon =globs =globnoglobs =modunconnomods =modnomods @*/
+/*@=nullpass =nullret =shiftsigned =usedef =temptrans =freshtrans @*/
+
 #endif
diff --git a/beecrypt/javaglue.h b/beecrypt/javaglue.h
index 883b199ca..b7c43d328 100644
--- a/beecrypt/javaglue.h
+++ b/beecrypt/javaglue.h
@@ -1,3 +1,7 @@
+/** \ingroup JAVA_m
+ * \file javaglue.h
+ */
+
 /* DO NOT EDIT THIS FILE - it is machine generated */
 #include <jni.h>
 /* Header for class javax_crypto_Cipher */
@@ -7,268 +11,281 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+#undef javax_crypto_Cipher_UNINITIALIZED
+#define javax_crypto_Cipher_UNINITIALIZED 0L
 #undef javax_crypto_Cipher_ENCRYPT_MODE
 #define javax_crypto_Cipher_ENCRYPT_MODE 1L
 #undef javax_crypto_Cipher_DECRYPT_MODE
 #define javax_crypto_Cipher_DECRYPT_MODE 2L
+#undef javax_crypto_Cipher_WRAP_MODE
+#define javax_crypto_Cipher_WRAP_MODE 3L
+#undef javax_crypto_Cipher_UNWRAP_MODE
+#define javax_crypto_Cipher_UNWRAP_MODE 4L
+#undef javax_crypto_Cipher_PUBLIC_KEY
+#define javax_crypto_Cipher_PUBLIC_KEY 1L
+#undef javax_crypto_Cipher_PRIVATE_KEY
+#define javax_crypto_Cipher_PRIVATE_KEY 2L
+#undef javax_crypto_Cipher_SECRET_KEY
+#define javax_crypto_Cipher_SECRET_KEY 3L
 #ifdef __cplusplus
 }
 #endif
 #endif
-/* Header for class com_beeyond_security_NativeMessageDigest */
+/* Header for class beecrypt_security_NativeMessageDigest */
 
-#ifndef _Included_com_beeyond_security_NativeMessageDigest
-#define _Included_com_beeyond_security_NativeMessageDigest
+#ifndef _Included_beecrypt_security_NativeMessageDigest
+#define _Included_beecrypt_security_NativeMessageDigest
 #ifdef __cplusplus
 extern "C" {
 #endif
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    find
  * Signature: (Ljava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_find
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeMessageDigest_find
   (JNIEnv *, jclass, jstring);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    allocParam
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_allocParam
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeMessageDigest_allocParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    cloneParam
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeMessageDigest_cloneParam
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeMessageDigest_cloneParam
   (JNIEnv *, jclass, jlong, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    freeParam
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeMessageDigest_freeParam
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeMessageDigest_freeParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    reset
  * Signature: (JJ)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeMessageDigest_reset
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeMessageDigest_reset
   (JNIEnv *, jclass, jlong, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    update
  * Signature: (JJB)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeMessageDigest_update
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeMessageDigest_update
   (JNIEnv *, jclass, jlong, jlong, jbyte);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    updateBlock
  * Signature: (JJ[BII)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeMessageDigest_updateBlock
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeMessageDigest_updateBlock
   (JNIEnv *, jclass, jlong, jlong, jbyteArray, jint, jint);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    digest
  * Signature: (JJ)[B
  */
-JNIEXPORT jbyteArray JNICALL Java_com_beeyond_security_NativeMessageDigest_digest
+JNIEXPORT jbyteArray JNICALL Java_beecrypt_security_NativeMessageDigest_digest
   (JNIEnv *, jclass, jlong, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeMessageDigest
+ * Class:     beecrypt_security_NativeMessageDigest
  * Method:    digestLength
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_com_beeyond_security_NativeMessageDigest_digestLength
+JNIEXPORT jint JNICALL Java_beecrypt_security_NativeMessageDigest_digestLength
   (JNIEnv *, jclass, jlong);
 
 #ifdef __cplusplus
 }
 #endif
 #endif
-/* Header for class com_beeyond_security_NativeSecureRandom */
+/* Header for class beecrypt_security_NativeSecureRandom */
 
-#ifndef _Included_com_beeyond_security_NativeSecureRandom
-#define _Included_com_beeyond_security_NativeSecureRandom
+#ifndef _Included_beecrypt_security_NativeSecureRandom
+#define _Included_beecrypt_security_NativeSecureRandom
 #ifdef __cplusplus
 extern "C" {
 #endif
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    find
  * Signature: (Ljava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_find
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeSecureRandom_find
   (JNIEnv *, jclass, jstring);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    allocParam
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_allocParam
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeSecureRandom_allocParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    cloneParam
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_security_NativeSecureRandom_cloneParam
+JNIEXPORT jlong JNICALL Java_beecrypt_security_NativeSecureRandom_cloneParam
   (JNIEnv *, jclass, jlong, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    freeParam
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeSecureRandom_freeParam
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeSecureRandom_freeParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    setup
  * Signature: (JJ)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeSecureRandom_setup
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeSecureRandom_setup
   (JNIEnv *, jclass, jlong, jlong);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    setSeed
  * Signature: (JJ[B)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeSecureRandom_setSeed
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeSecureRandom_setSeed
   (JNIEnv *, jclass, jlong, jlong, jbyteArray);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    nextBytes
  * Signature: (JJ[B)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeSecureRandom_nextBytes
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeSecureRandom_nextBytes
   (JNIEnv *, jclass, jlong, jlong, jbyteArray);
 
 /*
- * Class:     com_beeyond_security_NativeSecureRandom
+ * Class:     beecrypt_security_NativeSecureRandom
  * Method:    generateSeed
  * Signature: ([B)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_security_NativeSecureRandom_generateSeed
+JNIEXPORT void JNICALL Java_beecrypt_security_NativeSecureRandom_generateSeed
   (JNIEnv *, jclass, jbyteArray);
 
 #ifdef __cplusplus
 }
 #endif
 #endif
-/* Header for class com_beeyond_crypto_NativeBlockCipher */
+/* Header for class beecrypt_crypto_NativeBlockCipher */
 
-#ifndef _Included_com_beeyond_crypto_NativeBlockCipher
-#define _Included_com_beeyond_crypto_NativeBlockCipher
+#ifndef _Included_beecrypt_crypto_NativeBlockCipher
+#define _Included_beecrypt_crypto_NativeBlockCipher
 #ifdef __cplusplus
 extern "C" {
 #endif
-#undef com_beeyond_crypto_NativeBlockCipher_MODE_ECB
-#define com_beeyond_crypto_NativeBlockCipher_MODE_ECB 0L
-#undef com_beeyond_crypto_NativeBlockCipher_MODE_CBC
-#define com_beeyond_crypto_NativeBlockCipher_MODE_CBC 1L
+#undef beecrypt_crypto_NativeBlockCipher_MODE_ECB
+#define beecrypt_crypto_NativeBlockCipher_MODE_ECB 0L
+#undef beecrypt_crypto_NativeBlockCipher_MODE_CBC
+#define beecrypt_crypto_NativeBlockCipher_MODE_CBC 1L
 /* Inaccessible static: MODES */
-#undef com_beeyond_crypto_NativeBlockCipher_PADDING_NOPADDING
-#define com_beeyond_crypto_NativeBlockCipher_PADDING_NOPADDING 0L
-#undef com_beeyond_crypto_NativeBlockCipher_PADDING_PKCS5
-#define com_beeyond_crypto_NativeBlockCipher_PADDING_PKCS5 1L
+#undef beecrypt_crypto_NativeBlockCipher_PADDING_NOPADDING
+#define beecrypt_crypto_NativeBlockCipher_PADDING_NOPADDING 0L
+#undef beecrypt_crypto_NativeBlockCipher_PADDING_PKCS5
+#define beecrypt_crypto_NativeBlockCipher_PADDING_PKCS5 1L
 /* Inaccessible static: PADDINGS */
+/* Inaccessible static: class_00024javax_00024crypto_00024spec_00024PBEParameterSpec */
 /* Inaccessible static: class_00024javax_00024crypto_00024spec_00024IvParameterSpec */
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    find
  * Signature: (Ljava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_crypto_NativeBlockCipher_find
+JNIEXPORT jlong JNICALL Java_beecrypt_crypto_NativeBlockCipher_find
   (JNIEnv *, jclass, jstring);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    allocParam
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_com_beeyond_crypto_NativeBlockCipher_allocParam
+JNIEXPORT jlong JNICALL Java_beecrypt_crypto_NativeBlockCipher_allocParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    freeParam
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_freeParam
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_freeParam
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    getBlockSize
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_com_beeyond_crypto_NativeBlockCipher_getBlockSize
+JNIEXPORT jint JNICALL Java_beecrypt_crypto_NativeBlockCipher_getBlockSize
   (JNIEnv *, jclass, jlong);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    setup
  * Signature: (JJI[B)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setup
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_setup
   (JNIEnv *, jclass, jlong, jlong, jint, jbyteArray);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    setIV
  * Signature: (JJ[B)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_setIV
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_setIV
   (JNIEnv *, jclass, jlong, jlong, jbyteArray);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    encryptECB
  * Signature: (JJ[BI[BII)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptECB
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_encryptECB
   (JNIEnv *, jclass, jlong, jlong, jbyteArray, jint, jbyteArray, jint, jint);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    decryptECB
  * Signature: (JJ[BI[BII)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptECB
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_decryptECB
   (JNIEnv *, jclass, jlong, jlong, jbyteArray, jint, jbyteArray, jint, jint);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    encryptCBC
  * Signature: (JJ[BI[BII)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_encryptCBC
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_encryptCBC
   (JNIEnv *, jclass, jlong, jlong, jbyteArray, jint, jbyteArray, jint, jint);
 
 /*
- * Class:     com_beeyond_crypto_NativeBlockCipher
+ * Class:     beecrypt_crypto_NativeBlockCipher
  * Method:    decryptCBC
  * Signature: (JJ[BI[BII)V
  */
-JNIEXPORT void JNICALL Java_com_beeyond_crypto_NativeBlockCipher_decryptCBC
+JNIEXPORT void JNICALL Java_beecrypt_crypto_NativeBlockCipher_decryptCBC
   (JNIEnv *, jclass, jlong, jlong, jbyteArray, jint, jbyteArray, jint, jint);
 
 #ifdef __cplusplus
diff --git a/beecrypt/md5.h b/beecrypt/md5.h
index 240e6a4c0..8f2fb42ff 100644
--- a/beecrypt/md5.h
+++ b/beecrypt/md5.h
@@ -50,27 +50,35 @@ extern BEEDLLAPI const hashFunction md5;
 
 /** \ingroup HASH_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 void md5Process(md5Param* p)
 	/*@modifies p @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int md5Reset   (md5Param* p)
 	/*@modifies p @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 int md5Update  (md5Param* p, const byte* data, int size)
 	/*@modifies p @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_md5_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
-int md5Digest  (md5Param* p, uint32* data)
+int md5Digest  (md5Param* p, /*@out@*/ uint32* data)
 	/*@modifies p, data @*/;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/memchunk.c b/beecrypt/memchunk.c
index 22a8662a0..fb68c510a 100644
--- a/beecrypt/memchunk.c
+++ b/beecrypt/memchunk.c
@@ -34,6 +34,7 @@
 # include <malloc.h>
 #endif
 
+/*@-compdef@*/	/* tmp-?data is undefined */
 memchunk* memchunkAlloc(int size)
 {
 	memchunk* tmp = (memchunk*) calloc(1, sizeof(memchunk));
@@ -52,6 +53,7 @@ memchunk* memchunkAlloc(int size)
 
 	return tmp;
 }
+/*@=compdef@*/
 
 void memchunkFree(memchunk* m)
 {
@@ -88,7 +90,7 @@ memchunk* memchunkResize(memchunk* m, int size)
 			/*@=nullderef@*/
 	}
 
-	/*@-nullret@*/	/* LCL: m->data might ve NULL */
+	/*@-nullret -compdef @*/	/* LCL: m->data might be NULL */
 	return m;
-	/*@=nullret@*/
+	/*@=nullret =compdef@*/
 }
diff --git a/beecrypt/memchunk.h b/beecrypt/memchunk.h
index a37fbbd3f..85fa9a185 100644
--- a/beecrypt/memchunk.h
+++ b/beecrypt/memchunk.h
@@ -39,14 +39,22 @@ typedef struct
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI /*@only@*/ /*@null@*/
-memchunk*	memchunkAlloc(int size)
+memchunk* memchunkAlloc(int size)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
-void		memchunkFree(/*@only@*/ /*@null@*/memchunk* m)
+/*@unused@*/ void memchunkFree(/*@only@*/ /*@null@*/memchunk* m)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI /*@only@*/ /*@null@*/
-memchunk*	memchunkResize(/*@only@*/ /*@null@*/memchunk* m, int size)
+memchunk* memchunkResize(/*@only@*/ /*@null@*/memchunk* m, int size)
 	/*@*/;
 
 #ifdef __cplusplus
diff --git a/beecrypt/mp32.c b/beecrypt/mp32.c
index f2e993c05..8e8a6a64f 100644
--- a/beecrypt/mp32.c
+++ b/beecrypt/mp32.c
@@ -965,9 +965,9 @@ void mp32gcd_w(uint32 size, const uint32* xdata, const uint32* ydata, uint32* re
 #endif
 
 #ifndef ASM_MP32NMODW
-uint32 mp32nmodw(uint32* result, uint32 xsize, const uint32* xdata, uint32 y, uint32* workspace)
+uint32 mp32nmodw(uint32* result, uint32 xsize, const uint32* xdata, uint32 y, uint32* wksp)
 {
-	/* result size xsize, workspace size xsize+1 */
+	/* result size xsize, wksp size xsize+1 */
 	register uint64 temp;
 	register uint32 q;
 	uint32 qsize = xsize-1;
@@ -994,26 +994,26 @@ uint32 mp32nmodw(uint32* result, uint32 xsize, const uint32* xdata, uint32 y, ui
 		temp /= y;
 		/*
 			temp *= y;
-			workspace[0] = (uint32) (temp >> 32);
-			workspace[1] = (uint32) (temp);
+			wksp[0] = (uint32) (temp >> 32);
+			wksp[1] = (uint32) (temp);
 		*/
 		q = (uint32) temp;
 
 		/* printf("q = %08x\n", q); */
 		/*@-evalorder@*/
-		*workspace = mp32setmul(1, workspace+1, &y, q);
+		*wksp = mp32setmul(1, wksp+1, &y, q);
 		/*@=evalorder@*/
 
-		/* printf("mplt "); mp32print(2, rdata); printf(" < "); mp32println(2, workspace); */
-		while (mp32lt(2, rdata, workspace))
+		/* printf("mplt "); mp32print(2, rdata); printf(" < "); mp32println(2, wksp); */
+		while (mp32lt(2, rdata, wksp))
 		{
-			/* printf("mp32lt! "); mp32print(2, rdata); printf(" < "); mp32println(2, workspace); */
+			/* printf("mp32lt! "); mp32print(2, rdata); printf(" < "); mp32println(2, wksp); */
 			/* printf("decreasing q\n"); */
-			(void) mp32subx(2, workspace, 1, &y);
+			(void) mp32subx(2, wksp, 1, &y);
 			/* q--; */
 		}
 		/* printf("subtracting\n"); */
-		(void) mp32sub(2, rdata, workspace);
+		(void) mp32sub(2, rdata, wksp);
 		rdata++;
 	}
 
@@ -1022,9 +1022,9 @@ uint32 mp32nmodw(uint32* result, uint32 xsize, const uint32* xdata, uint32 y, ui
 #endif
 
 #ifndef ASM_MP32NMOD
-void mp32nmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* workspace)
+void mp32nmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* wksp)
 {
-	/* result size xsize, workspace size xsize+1 */
+	/* result size xsize, wksp size xsize+1 */
 	register uint64 temp;
 	register uint32 q;
 	uint32 msw = *ydata;
@@ -1050,29 +1050,29 @@ void mp32nmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, c
 
 		/* printf("q = %08x\n", q); */
 		/*@-evalorder@*/
-		*workspace = mp32setmul(ysize, workspace+1, ydata, q);
+		*wksp = mp32setmul(ysize, wksp+1, ydata, q);
 		/*@=evalorder@*/
 
-		/* printf("mp32lt "); mp32print(ysize+1, rdata); printf(" < "); mp32println(ysize+1, workspace); */
-		while (mp32lt(ysize+1, rdata, workspace))
+		/* printf("mp32lt "); mp32print(ysize+1, rdata); printf(" < "); mp32println(ysize+1, wksp); */
+		while (mp32lt(ysize+1, rdata, wksp))
 		{
-			/* printf("mp32lt! "); mp32print(ysize+1, rdata); printf(" < "); mp32println(ysize+1, workspace); */
+			/* printf("mp32lt! "); mp32print(ysize+1, rdata); printf(" < "); mp32println(ysize+1, wksp); */
 			/* printf("decreasing q\n"); */
-			(void) mp32subx(ysize+1, workspace, ysize, ydata);
+			(void) mp32subx(ysize+1, wksp, ysize, ydata);
 			q--;
 		}
 		/* printf("subtracting\n"); */
-		(void) mp32sub(ysize+1, rdata, workspace);
+		(void) mp32sub(ysize+1, rdata, wksp);
 		rdata++;
 	}
 }
 #endif
 
 #ifndef ASM_MP32NDIVMOD
-void mp32ndivmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, register uint32* workspace)
+void mp32ndivmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, register uint32* wksp)
 {
 	/* result must be xsize+1 in length */
-	/* workspace must be ysize+1 in length */
+	/* wksp must be ysize+1 in length */
 	/* expect ydata to be normalized */
 	register uint64 temp;
 	register uint32 q;
@@ -1080,6 +1080,7 @@ void mp32ndivmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize
 	uint32 qsize = xsize-ysize;
 
 	mp32copy(xsize, result+1, xdata);
+	/*@-compdef@*/ /* LCL: result+1 undefined */
 	if (mp32ge(ysize, result+1, ydata))
 	{
 		/* printf("subtracting\n"); */
@@ -1088,6 +1089,7 @@ void mp32ndivmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize
 	}
 	else
 		*(result++) = 0;
+	/*@=compdef@*/
 
 	/*@-usedef@*/	/* LCL: result[0] is set */
 	while (qsize--)
@@ -1106,19 +1108,19 @@ void mp32ndivmod(uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize
 		/* printf("q = %08x\n", q); */
 
 		/*@-evalorder@*/
-		*workspace = mp32setmul(ysize, workspace+1, ydata, q);
+		*wksp = mp32setmul(ysize, wksp+1, ydata, q);
 		/*@=evalorder@*/
 
-		/* printf("mp32lt "); mp32print(ysize+1, result); printf(" < "); mp32println(ysize+1, workspace); */
-		while (mp32lt(ysize+1, result, workspace))
+		/* printf("mp32lt "); mp32print(ysize+1, result); printf(" < "); mp32println(ysize+1, wksp); */
+		while (mp32lt(ysize+1, result, wksp))
 		{
-			/* printf("mp32lt! "); mp32print(ysize+1, result); printf(" < "); mp32println(ysize+1, workspace); */
+			/* printf("mp32lt! "); mp32print(ysize+1, result); printf(" < "); mp32println(ysize+1, wksp); */
 			/* printf("decreasing q\n"); */
-			(void) mp32subx(ysize+1, workspace, ysize, ydata);
+			(void) mp32subx(ysize+1, wksp, ysize, ydata);
 			q--;
 		}
 		/* printf("subtracting\n"); */
-		(void) mp32sub(ysize+1, result, workspace);
+		(void) mp32sub(ysize+1, result, wksp);
 		*(result++) = q;
 	}
 	/*@=usedef@*/
diff --git a/beecrypt/mp32.h b/beecrypt/mp32.h
index f7271407e..7eb13139c 100644
--- a/beecrypt/mp32.h
+++ b/beecrypt/mp32.h
@@ -40,227 +40,404 @@
 extern "C" {
 #endif
 
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32copy(uint32 size, /*@out@*/ uint32* dst, const uint32* src)
+	/*@modifies dst @*/;
 #ifndef ASM_MP32COPY
 #ifdef	__LCLINT__
-#define mp32copy(size, dst, src) memmove(dst, src, (size) << 2)
+#define mp32copy(size, dst, src) memmove(dst, src, ((unsigned)(size)) << 2)
 #else
 #define mp32copy(size, dst, src) memcpy(dst, src, (size) << 2)
 #endif
-#else
-BEEDLLAPI
-void mp32copy(uint32 size, uint32* dst, const uint32* src)
-	/*@modifies dst @*/;
 #endif
 
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32move(uint32 size, /*@out@*/ uint32* dst, const uint32* src)
+	/*@modifies dst @*/;
 #ifndef ASM_MP32MOVE
-#define mp32move(size, dst, src) memmove(dst, src, (size) << 2)
+#ifdef	__LCLINT__
+#define mp32move(size, dst, src) memmove(dst, src, ((unsigned)(size)) << 2)
 #else
-BEEDLLAPI
-void mp32move(uint32 size, uint32* dst, const uint32* src)
-	/*@modifies dst @*/;
+#define mp32move(size, dst, src) memmove(dst, src, (size) << 2)
+#endif
 #endif
 
+/**
+ */
 BEEDLLAPI
-void mp32zero(uint32 xsize, uint32* xdata)
+void mp32zero(uint32 xsize, /*@out@*/ uint32* xdata)
 	/*@modifies xdata @*/;
-BEEDLLAPI
-void mp32fill(uint32 xsize, uint32* xdata, uint32 val)
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32fill(uint32 xsize, /*@out@*/ uint32* xdata, uint32 val)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 int mp32odd (uint32 xsize, const uint32* xdata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32even(uint32 xsize, const uint32* xdata)
 	/*@*/;
 
+/**
+ */
 BEEDLLAPI
 int mp32z  (uint32 xsize, const uint32* xdata)
 	/*@*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mp32nz (uint32 xsize, const uint32* xdata)
 	/*@*/;
+/*@=exportlocal@*/
 
+/**
+ */
 BEEDLLAPI
 int mp32eq (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mp32ne (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
+/*@=exportlocal@*/
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mp32gt (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
+/*@=exportlocal@*/
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mp32lt (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
+/*@=exportlocal@*/
+
+/**
+ */
 BEEDLLAPI
 int mp32ge (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32le (uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
 
+/**
+ */
 BEEDLLAPI
 int mp32eqx(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int mp32nex(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int mp32gtx(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int mp32ltx(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32gex(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32lex(uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@*/;
 
+/**
+ */
 BEEDLLAPI
 int mp32isone(uint32 xsize, const uint32* xdata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32istwo(uint32 xsize, const uint32* xdata)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
 int mp32leone(uint32 xsize, const uint32* xdata)
 	/*@*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int mp32eqmone(uint32 size, const uint32* xdata, const uint32* ydata)
 	/*@*/;
 
+/**
+ */
 BEEDLLAPI
 int mp32msbset(uint32 xsize, const uint32* xdata)
 	/*@*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int mp32lsbset(uint32 xsize, const uint32* xdata)
 	/*@*/;
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32setmsb(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32setlsb(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32clrmsb(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32clrlsb(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32xor(uint32 size, uint32* xdata, const uint32* ydata)
 	/*@modifies xdata @*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 void mp32not(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
+/*@=exportlocal@*/
 
+/**
+ */
 BEEDLLAPI
-void mp32setw(uint32 xsize, uint32* xdata, uint32 y)
+void mp32setw(uint32 xsize, /*@out@*/ uint32* xdata, uint32 y)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
-void mp32setx(uint32 xsize, uint32* xdata, uint32 ysize, const uint32* ydata)
+void mp32setx(uint32 xsize, /*@out@*/ uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32addw(uint32 xsize, uint32* xdata, uint32 y)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32add (uint32 size, uint32* xdata, const uint32* ydata)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32addx(uint32 xsize, uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32subw(uint32 xsize, uint32* xdata, uint32 y)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32sub (uint32 size, uint32* xdata, const uint32* ydata)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32subx(uint32 xsize, uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32multwo(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32neg(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 uint32 mp32size(uint32 xsize, const uint32* xdata)
 	/*@*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32mszcnt(uint32 xsize, const uint32* xdata)
 	/*@*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 uint32 mp32lszcnt(uint32 xsize, const uint32* xdata)
 	/*@*/;
+/*@=exportlocal@*/
 
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 void mp32lshift(uint32 xsize, uint32* xdata, uint32 count)
 	/*@modifies xdata @*/;
+/*@=exportlocal@*/
+
+/**
+ */
 BEEDLLAPI
 void mp32rshift(uint32 xsize, uint32* xdata, uint32 count)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32norm(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32divpowtwo(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32divtwo (uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32sdivtwo(uint32 xsize, uint32* xdata)
 	/*@modifies xdata @*/;
 
+/**
+ */
 BEEDLLAPI
 uint32 mp32setmul   (uint32 size, /*@out@*/ uint32* result, const uint32* xdata, uint32 y)
 	/*@modifies result @*/;
+
+/**
+ */
 BEEDLLAPI
 uint32 mp32addmul   (uint32 size, /*@out@*/ uint32* result, const uint32* xdata, uint32 y)
 	/*@modifies result @*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 uint32 mp32addsqrtrc(uint32 size, /*@out@*/ uint32* result, const uint32* xdata)
 	/*@modifies result @*/;
+/*@=exportlocal@*/
 
+/**
+ */
 BEEDLLAPI
 void mp32mul(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata)
 	/*@modifies result @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32sqr(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata)
 	/*@modifies result @*/;
 
+/**
+ */
 BEEDLLAPI
-void mp32gcd_w(uint32 size, const uint32* xdata, const uint32* ydata, /*@out@*/ uint32* result, uint32* wksp)
+void mp32gcd_w(uint32 size, const uint32* xdata, const uint32* ydata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
-BEEDLLAPI
-uint32 mp32nmodw(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 y, uint32* wksp)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+uint32 mp32nmodw(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 y, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
-BEEDLLAPI
-void mp32nmod(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* wksp)
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32nmod(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
 BEEDLLAPI
-void mp32ndivmod(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* wksp)
+void mp32ndivmod(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32print(uint32 xsize, const uint32* xdata)
 	/*@modifies fileSystem @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32println(uint32 xsize, const uint32* xdata)
 	/*@modifies fileSystem @*/;
diff --git a/beecrypt/mp32barrett.c b/beecrypt/mp32barrett.c
index cd38b35f5..37890e80e 100644
--- a/beecrypt/mp32barrett.c
+++ b/beecrypt/mp32barrett.c
@@ -92,7 +92,7 @@ void mp32bfree(mp32barrett* b)
 }
 /*@=nullstate@*/
 
-/*@-nullstate@*/	/* b->mu may be null @*/
+/*@-nullstate -compdef @*/	/* b->mu may be null @*/
 void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
 {
 	register uint32 size = copy->size;
@@ -126,10 +126,12 @@ void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
 		b->modl = (uint32*) 0;
 		b->mu = (uint32*) 0;
 	}
+	else
+		{};
 }
-/*@=nullstate@*/
+/*@=nullstate =compdef @*/
 
-/*@-nullstate@*/	/* b->mu may be null @*/
+/*@-nullstate -compdef @*/	/* b->mu may be null @*/
 /**
  * mp32bset
  */
@@ -165,9 +167,9 @@ void mp32bset(mp32barrett* b, uint32 size, const uint32 *data)
 		}
 	}
 }
-/*@=nullstate@*/
+/*@=nullstate =compdef @*/
 
-/*@-nullstate@*/	/* b->mu may be null @*/
+/*@-nullstate -compdef @*/	/* b->mu may be null @*/
 void mp32bsethex(mp32barrett* b, const char* hex)
 {
 	uint32 length = strlen(hex);
@@ -202,6 +204,8 @@ void mp32bsethex(mp32barrett* b, const char* hex)
 				val += (ch - 'A') + 10;
 			else if (ch >= 'a' && ch <= 'f')
 				val += (ch - 'a') + 10;
+			else
+				{};
 
 			if ((length & 0x7) == 0)
 			{
@@ -224,11 +228,10 @@ void mp32bsethex(mp32barrett* b, const char* hex)
 		b->mu = 0;
 	}
 }
-/*@=nullstate@*/
+/*@=nullstate =compdef @*/
 
 /**
- * mp32bmu_w
- *  computes the Barrett 'mu' coefficient
+ *  Computes the Barrett 'mu' coefficient.
  *  needs workspace of (6*size+4) words
  */
 void mp32bmu_w(mp32barrett* b, uint32* wksp)
@@ -251,8 +254,7 @@ void mp32bmu_w(mp32barrett* b, uint32* wksp)
 }
 
 /**
- * mp32brnd_w
- *  generates a random number in the range 1 < r < b-1
+ *  Generates a random number in the range 1 < r < b-1.
  *  need workspace of (size) words
  */
 void mp32brnd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* result, uint32* wksp)
@@ -264,7 +266,9 @@ void mp32brnd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* result
 
 	do
 	{
+		/*@-noeffectuncon@*/ /* LCL: ??? */
 		(void) rc->rng->next(rc->param, result, b->size);
+		/*@=noeffectuncon@*/
 
 		/*@-shiftsigned -usedef@*/
 		result[0] &= (0xffffffff >> msz);
@@ -276,8 +280,7 @@ void mp32brnd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* result
 }
 
 /**
- * mp32brndodd_w
- *  generates a random odd number in the range 1 < r < b-1
+ *  Generates a random odd number in the range 1 < r < b-1.
  *  needs workspace of (size) words
  */
 void mp32brndodd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* result, uint32* wksp)
@@ -289,7 +292,9 @@ void mp32brndodd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* res
 
 	do
 	{
+		/*@-noeffectuncon@*/ /* LCL: ??? */
 		(void) rc->rng->next(rc->param, result, b->size);
+		/*@=noeffectuncon@*/
 
 		/*@-shiftsigned -usedef@*/
 		result[0] &= (0xffffffff >> msz);
@@ -305,8 +310,7 @@ void mp32brndodd_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* res
 }
 
 /**
- * mp32brndinv_w
- *  generates a random invertible (modulo b) in the range 1 < r < b-1
+ *  Generates a random invertible (modulo b) in the range 1 < r < b-1.
  *  needs workspace of (6*size+6) words
  */
 void mp32brndinv_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* result, uint32* inverse, uint32* wksp)
@@ -324,8 +328,7 @@ void mp32brndinv_w(const mp32barrett* b, randomGeneratorContext* rc, uint32* res
 }
 
 /**
- * mp32bmod_w
- *  computes the barrett modular reduction of a number x, which has twice the size of b
+ *  Computes the barrett modular reduction of a number x, which has twice the size of b.
  *  needs workspace of (2*size+2) words
  */
 void mp32bmod_w(const mp32barrett* b, const uint32* xdata, uint32* result, uint32* wksp)
@@ -386,8 +389,7 @@ void mp32bmod_w(const mp32barrett* b, const uint32* xdata, uint32* result, uint3
 }
 
 /**
- * mp32bsubone
- *  copies (b-1) into result
+ *  Copies (b-1) into result.
  */
 void mp32bsubone(const mp32barrett* b, uint32* result)
 {
@@ -398,8 +400,7 @@ void mp32bsubone(const mp32barrett* b, uint32* result)
 }
 
 /**
- * mp32bneg
- *  computes the negative (modulo b) of x, where x must contain a value between 0 and b-1
+ *  Computes the negative (modulo b) of x, where x must contain a value between 0 and b-1.
  */
 void mp32bneg(const mp32barrett* b, const uint32* xdata, uint32* result)
 {
@@ -411,8 +412,7 @@ void mp32bneg(const mp32barrett* b, const uint32* xdata, uint32* result)
 }
 
 /**
- * mp32baddmod_w
- *  computes the sum (modulo b) of x and y
+ *  Computes the sum (modulo b) of x and y.
  *  needs a workspace of (4*size+2) words
  */
 void mp32baddmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* result, uint32* wksp)
@@ -428,8 +428,7 @@ void mp32baddmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
 }
 
 /**
- * mp32bsubmod_w
- *  computes the difference (modulo b) of x and y
+ *  Computes the difference (modulo b) of x and y.
  *  needs a workspace of (4*size+2) words
  */
 void mp32bsubmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* result, uint32* wksp)
@@ -446,8 +445,7 @@ void mp32bsubmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
 }
 
 /**
- * mp32mulmod_w
- *  computes the product (modulo b) of x and y
+ *  Computes the product (modulo b) of x and y.
  *  needs a workspace of (4*size+2) words
  */
 void mp32bmulmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, uint32* result, uint32* wksp)
@@ -465,8 +463,7 @@ void mp32bmulmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
 }
 
 /**
- * mp32bsqrmod_w
- *  computes the square (modulo b) of x
+ *  Computes the square (modulo b) of x.
  *  needs a workspace of (4*size+2) words
  */
 void mp32bsqrmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32* result, uint32* wksp)
@@ -483,7 +480,10 @@ void mp32bsqrmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
 	mp32bmod_w(b, temp, result, wksp);
 }
 
-/*
+/**
+ *  Precomputes the sliding window table for computing powers of x modulo b.
+ *  needs workspace (4*size+2)
+ *
  * Sliding Window Exponentiation technique, slightly altered from the method Applied Cryptography:
  *
  * First of all, the table with the powers of g can be reduced by about half; the even powers don't
@@ -496,31 +496,29 @@ void mp32bsqrmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
  *
  * This table can be used for K=2,3,4 and can be extended
  *  
- *     0 : - | -       | -
- *     1 : 1 |  g1 @ 0 | 0
- *    10 : 1 |  g1 @ 0 | 1
- *    11 : 2 |  g3 @ 1 | 0
- *   100 : 1 |  g1 @ 0 | 2
- *   101 : 3 |  g5 @ 2 | 0
- *   110 : 2 |  g3 @ 1 | 1
- *   111 : 3 |  g7 @ 3 | 0
- *  1000 : 1 |  g1 @ 0 | 3
- *  1001 : 4 |  g9 @ 4 | 0
- *  1010 : 3 |  g5 @ 2 | 1
- *  1011 : 4 | g11 @ 5 | 0
- *  1100 : 2 |  g3 @ 1 | 2
- *  1101 : 4 | g13 @ 6 | 0
- *  1110 : 3 |  g7 @ 3 | 1
- *  1111 : 4 | g15 @ 7 | 0
+ *
+\verbatim
+	   0 : - | -       | -
+	   1 : 1 |  g1 @ 0 | 0
+	  10 : 1 |  g1 @ 0 | 1
+	  11 : 2 |  g3 @ 1 | 0
+	 100 : 1 |  g1 @ 0 | 2
+	 101 : 3 |  g5 @ 2 | 0
+	 110 : 2 |  g3 @ 1 | 1
+	 111 : 3 |  g7 @ 3 | 0
+	1000 : 1 |  g1 @ 0 | 3
+	1001 : 4 |  g9 @ 4 | 0
+	1010 : 3 |  g5 @ 2 | 1
+	1011 : 4 | g11 @ 5 | 0
+	1100 : 2 |  g3 @ 1 | 2
+	1101 : 4 | g13 @ 6 | 0
+	1110 : 3 |  g7 @ 3 | 1
+	1111 : 4 | g15 @ 7 | 0
+\endverbatim
  *
  */
-
-/**
- * mp32bslide_w
- *  precomputes the sliding window table for computing powers of x modulo b
- *  needs workspace (4*size+2)
- */
-void mp32bslide_w(const mp32barrett* b, const uint32 xsize, const uint32* xdata, uint32* slide, uint32* wksp)
+static void mp32bslide_w(const mp32barrett* b, const uint32 xsize, const uint32* xdata, /*@out@*/ uint32* slide, /*@out@*/ uint32* wksp)
+	/*@modifies slide, wksp @*/
 {
 	register uint32 size = b->size;
 	mp32bsqrmod_w(b, xsize, xdata,                     slide       , wksp); /* x^2 mod b, temp */
@@ -544,6 +542,7 @@ void mp32bslide_w(const mp32barrett* b, const uint32 xsize, const uint32* xdata,
 { 0, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0 };
 
 /**
+ * mp32bpowmod_w
  * needs workspace of 4*size+2 words
  */
 void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 psize, const uint32* pdata, uint32* result, uint32* wksp)
@@ -631,6 +630,8 @@ void mp32bpowmodsld_w(const mp32barrett* b, const uint32* slide, uint32 psize, c
 						l++;
 					else if (bit != 0)
 						l = 1;
+					else
+						{};
 
 					if (l == 4)
 					{
@@ -747,10 +748,9 @@ void mp32btwopowmod_w(const mp32barrett* b, uint32 psize, const uint32* pdata, u
 }
 
 /**
- * mp32binv_w
- *  computes the inverse (modulo b) of x, and returns 1 if x was invertible
+ *  Computes the inverse (modulo b) of x, and returns 1 if x was invertible.
  *  needs workspace of (6*size+6) words
- *  note: xdata and result cannot point to the same area
+ *  @note xdata and result cannot point to the same area
  */
 int mp32binv_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32* result, uint32* wksp)
 {
@@ -901,7 +901,7 @@ int mp32binv_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32*
 /**
  * needs workspace of (7*size+2) words
  */
-int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* r, int t, uint32* wksp)
+int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* rc, int t, uint32* wksp)
 {
 	/*
 	 * This test works for candidate probable primes >= 3, which are also not small primes.
@@ -929,7 +929,9 @@ int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* r, int t, uint32
 		if (size > SMALL_PRIMES_PRODUCT_MAX)
 		{
 			mp32setx(size, wksp+size, SMALL_PRIMES_PRODUCT_MAX, mp32spprod[SMALL_PRIMES_PRODUCT_MAX-1]);
+			/*@-compdef@*/ /* LCL: wksp+size */
 			mp32gcd_w(size, b->modl, wksp+size, wksp, wksp+2*size);
+			/*@=compdef@*/
 		}
 		else
 		{
@@ -938,7 +940,7 @@ int mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* r, int t, uint32
 
 		if (mp32isone(size, wksp))
 		{
-			return mp32pmilrab_w(b, r, t, wksp);
+			return mp32pmilrab_w(b, rc, t, wksp);
 		}
 	}
 
diff --git a/beecrypt/mp32barrett.h b/beecrypt/mp32barrett.h
index 96bcbd978..0b9231e19 100644
--- a/beecrypt/mp32barrett.h
+++ b/beecrypt/mp32barrett.h
@@ -42,108 +42,188 @@ typedef struct
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI
 void mp32bzero(/*@out@*/ mp32barrett* b)
 	/*@modifies b @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32binit(mp32barrett* b, uint32 size)
 	/*@modifies b @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32bfree(mp32barrett* b)
 	/*@modifies b @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
 	/*@modifies b @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32bset(mp32barrett* b, uint32 size, const uint32* data)
 	/*@modifies b @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32bsethex(mp32barrett* b, const char* hex)
 	/*@modifies b @*/;
 
+/**
+ */
 BEEDLLAPI
-void mp32bsubone(const mp32barrett* b, /*@out@*/ uint32* result)
+void mp32bsubone(const mp32barrett* b, uint32* result)
+	/*@modifies result @*/;
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32bneg(const mp32barrett* b, const uint32* xdata, uint32* result)
 	/*@modifies result @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32bmu_w(mp32barrett* b, /*@out@*/ uint32* wksp)
 	/*@modifies b, wksp @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32brnd_w   (const mp32barrett* b, randomGeneratorContext* rc, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 void mp32brndodd_w(const mp32barrett* b, randomGeneratorContext* rc, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+/*@=exportlocal@*/
+
+/**
+ */
 BEEDLLAPI
-void mp32brndinv_w(const mp32barrett* b, randomGeneratorContext* rc, /*@out@*/ uint32* result, uint32* inverse, /*@out@*/ uint32* wksp)
+void mp32brndinv_w(const mp32barrett* b, randomGeneratorContext* rc, /*@out@*/ uint32* result, /*@out@*/ uint32* inverse, /*@out@*/ uint32* wksp)
 	/*@modifies result, inverse, wksp @*/;
 
-BEEDLLAPI
-void mp32bneg_w(const mp32barrett* b, const uint32* xdata, uint32* result)
-	/*@modifies result @*/;
+/**
+ */
 BEEDLLAPI
 void mp32bmod_w(const mp32barrett* b, const uint32* xdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32baddmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32bsubmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32bmulmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 ysize, const uint32* ydata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32bsqrmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint32 psize, const uint32* pdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 void mp32bpowmodsld_w(const mp32barrett* b, const uint32* slide, uint32 psize, const uint32* pdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
-	/*@modifies result, wksp @*/;
+	/*@modifies result, wksp, internalState @*/;
+/*@=exportlocal@*/
+
+/**
+ */
 BEEDLLAPI
 void mp32btwopowmod_w(const mp32barrett* b, uint32 psize, const uint32* pdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
+/**
+ */
 BEEDLLAPI
 int  mp32binv_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
 	/*@modifies result, wksp @*/;
 
-
-/* To be added:
- * simultaneous multiple exponentiation, for use in dsa and elgamal signature verification
+#ifdef	NOTYET
+/**
+ * @todo Simultaneous multiple exponentiation, for use in dsa and elgamal
+ * signature verification.
  */
-BEEDLLAPI
+BEEDLLAPI /*@unused@*/
 void mp32bsm2powmod(const mp32barrett* b, const uint32*, const uint32*, const uint32*, const uint32*);
-BEEDLLAPI
-void mp32bsm3powmod(const mp32barrett* b, const uint32*, const uint32*, const uint32*, const uint32*, const uint32*, const uint32*);
 
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32bsm3powmod(const mp32barrett* b, const uint32*, const uint32*, const uint32*, const uint32*, const uint32*, const uint32*);
+#endif	/* NOTYET */
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int  mp32bpprime_w(const mp32barrett* b, randomGeneratorContext* rc, int t, /*@out@*/ uint32* wksp)
 	/*@modifies wksp @*/;
 
-/* the next routines take mp32numbers as parameters */
-
+/**
+ * @note Takes mp32number as parameter.
+ */
 BEEDLLAPI
-void mp32bnrnd(const mp32barrett* b, randomGeneratorContext* rc, /*@out@*/ mp32number* result)
+void mp32bnrnd(const mp32barrett* b, randomGeneratorContext* rc, mp32number* result)
 	/*@modifies result @*/;
 
-BEEDLLAPI
-void mp32bnmulmod(const mp32barrett* b, const mp32number* x, const mp32number* y, /*@out@*/ mp32number* result)
+/**
+ * @note Takes mp32number as parameter.
+ */
+BEEDLLAPI /*@unused@*/
+void mp32bnmulmod(const mp32barrett* b, const mp32number* x, const mp32number* y, mp32number* result)
 	/*@modifies result @*/;
-BEEDLLAPI
-void mp32bnsqrmod(const mp32barrett* b, const mp32number* x, /*@out@*/ mp32number* result)
+
+/**
+ * @note Takes mp32number as parameter.
+ */
+BEEDLLAPI /*@unused@*/
+void mp32bnsqrmod(const mp32barrett* b, const mp32number* x, mp32number* result)
 	/*@modifies result @*/;
 
+/**
+ * @note Takes mp32number as parameter.
+ */
 BEEDLLAPI
 void mp32bnpowmod   (const mp32barrett* b, const mp32number* x, const mp32number* pow, mp32number* y)
 	/*@modifies y @*/;
-BEEDLLAPI
+
+/**
+ * @note Takes mp32number as parameter.
+ */
+BEEDLLAPI /*@unused@*/
 void mp32bnpowmodsld(const mp32barrett* b, const uint32* slide, const mp32number* pow, mp32number* y)
 	/*@modifies y @*/;
 
diff --git a/beecrypt/mp32number.c b/beecrypt/mp32number.c
index c3d54b1b8..881e030cf 100644
--- a/beecrypt/mp32number.c
+++ b/beecrypt/mp32number.c
@@ -46,7 +46,7 @@ void mp32nzero(mp32number* n)
 }
 /*@=nullstate@*/
 
-/*@-nullstate@*/	/* n->data may be NULL */
+/*@-nullstate -compdef @*/	/* n->data may be NULL */
 void mp32nsize(mp32number* n, uint32 size)
 {
 	if (size)
@@ -59,20 +59,25 @@ void mp32nsize(mp32number* n, uint32 size)
 		else
 			n->data = (uint32*) malloc(size * sizeof(uint32));
 
-		if (n->data == (uint32*) 0)
-			n->size = 0;
-		else
+		if (n->data)
 			n->size = size;
+		else
+		{
+			n->size = 0;
+			n->data = (uint32*) 0;
+		}
 
 	}
 	else if (n->data)
 	{
 		free(n->data);
-		n->data = (uint32*) 0;
 		n->size = 0;
+		n->data = (uint32*) 0;
 	}
+	else
+		{};
 }
-/*@=nullstate@*/
+/*@=nullstate =compdef @*/
 
 /*@-nullstate@*/	/* n->data may be NULL */
 void mp32ninit(mp32number* n, uint32 size, const uint32* data)
@@ -99,7 +104,9 @@ void mp32nfree(mp32number* n)
 
 void mp32ncopy(mp32number* n, const mp32number* copy)
 {
+	/*@-compdef@*/
 	mp32nset(n, copy->size, copy->data);
+	/*@=compdef@*/
 }
 
 void mp32nwipe(mp32number* n)
@@ -126,7 +133,10 @@ void mp32nset(mp32number* n, uint32 size, const uint32* data)
 			mp32copy(n->size = size, n->data, data);
 			/*@=nullpass@*/
 		else
+		{
 			n->size = 0;
+			n->data = (uint32*) 0;
+		}
 	}
 	else if (n->data)
 	{
@@ -134,6 +144,8 @@ void mp32nset(mp32number* n, uint32 size, const uint32* data)
 		n->data = (uint32*) 0;
 		n->size = 0;
 	}
+	else
+		{};
 }
 /*@=nullstate@*/
 
@@ -154,11 +166,14 @@ void mp32nsetw(mp32number* n, uint32 val)
 		n->data[0] = val;
 	}
 	else
+	{
 		n->size = 0;
+		n->data = (uint32*) 0;
+	}
 }
 /*@=nullstate@*/
 
-/*@-nullstate@*/	/* n->data may be NULL */
+/*@-nullstate -compdef @*/	/* n->data may be NULL */
 void mp32nsethex(mp32number* n, const char* hex)
 {
 	uint32 length = strlen(hex);
@@ -191,6 +206,8 @@ void mp32nsethex(mp32number* n, const char* hex)
 				val += (ch - 'A') + 10;
 			else if (ch >= 'a' && ch <= 'f')
 				val += (ch - 'a') + 10;
+			else
+				{};
 
 			if ((length & 0x7) == 0)
 			{
@@ -201,7 +218,9 @@ void mp32nsethex(mp32number* n, const char* hex)
 		if (rem != 0)
 			*dst = val;
 	}
-	else
+	else {
 		n->size = 0;
+		n->data = (uint32*)0;
+	}
 }
-/*@=nullstate@*/
+/*@=nullstate =compdef @*/
diff --git a/beecrypt/mp32number.h b/beecrypt/mp32number.h
index a9621691a..4998935bf 100644
--- a/beecrypt/mp32number.h
+++ b/beecrypt/mp32number.h
@@ -32,6 +32,8 @@
 # include "config.h"
 #endif
 
+/**
+ */
 typedef struct
 {
 	uint32  size;
@@ -42,34 +44,59 @@ typedef struct
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI
-void mp32nzero(mp32number* n)
-	/*@modifies n @*/;
+void mp32nzero(/*@out@*/ mp32number* n)
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32nsize(mp32number* n, uint32 size)
-	/*@modifies n @*/;
-BEEDLLAPI
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 void mp32ninit(mp32number* n, uint32 size, const uint32* data)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32nfree(mp32number* n)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
-void mp32ncopy(mp32number* n, const mp32number* copy)
-	/*@modifies n @*/;
+void mp32ncopy(/*@out@*/ mp32number* n, const mp32number* copy)
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32nwipe(mp32number* n)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
 
+/**
+ */
 BEEDLLAPI
 void mp32nset   (mp32number* n, uint32 size, /*@null@*/ const uint32* data)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32nsetw  (mp32number* n, uint32 val)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
+
+/**
+ */
 BEEDLLAPI
 void mp32nsethex(mp32number* n, const char* hex)
-	/*@modifies n @*/;
+	/*@modifies n->size, n->data @*/;
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/mp32prime.c b/beecrypt/mp32prime.c
index 0953f7a70..deb892fe4 100644
--- a/beecrypt/mp32prime.c
+++ b/beecrypt/mp32prime.c
@@ -998,7 +998,7 @@ int mp32ptrials(uint32 bits)
 /**
  */
 static void mp32prndbits(mp32barrett* p, uint8 msbclr, uint8 lsbset, randomGeneratorContext* rc)
-	/*@modifies p, rc @*/
+	/*@modifies p @*/
 {
 	register uint32 size;
 
@@ -1006,7 +1006,9 @@ static void mp32prndbits(mp32barrett* p, uint8 msbclr, uint8 lsbset, randomGener
 		return;
 
 	size = p->size;
+	/*@-noeffectuncon@*/ /* LCL: ??? */
 	(void) rc->rng->next(rc->param, p->modl, size);
+	/*@=noeffectuncon@*/
 
 	if (msbclr != 0)
 		p->modl[0] &= (((uint32)0xffffffff) >> msbclr);
@@ -1021,7 +1023,9 @@ static void mp32prndbits(mp32barrett* p, uint8 msbclr, uint8 lsbset, randomGener
  * mp32psppdiv_w
  *  needs workspace of (3*size) words
  */
-int mp32psppdiv_w(const mp32barrett* p, uint32* wksp)
+static int mp32psppdiv_w(const mp32barrett* p, /*@out@*/ uint32* wksp)
+	/*@globals mp32spprod @*/
+	/*@modifies wksp @*/
 {
 	/* small prime product trial division test */
 	register uint32 size = p->size;
@@ -1029,7 +1033,9 @@ int mp32psppdiv_w(const mp32barrett* p, uint32* wksp)
 	if (size > SMALL_PRIMES_PRODUCT_MAX)
 	{
 		mp32setx(size, wksp+size, SMALL_PRIMES_PRODUCT_MAX, mp32spprod[SMALL_PRIMES_PRODUCT_MAX-1]);
+		/*@-compdef@*/ /* LCL: wksp+size undef */
 		mp32gcd_w(size, p->modl, wksp+size, wksp, wksp+2*size);
+		/*@=compdef@*/
 	}
 	else
 	{
@@ -1040,9 +1046,11 @@ int mp32psppdiv_w(const mp32barrett* p, uint32* wksp)
 }
 
 /**
+ * mp32pmilrabtwo_w
  * needs workspace of (5*size+2)
  */
-int mp32pmilrabtwo_w(const mp32barrett* p, uint32 s, const uint32* rdata, const uint32* ndata, uint32* wksp)
+static int mp32pmilrabtwo_w(const mp32barrett* p, uint32 s, const uint32* rdata, const uint32* ndata, /*@out@*/ uint32* wksp)
+	/*@modifies wksp @*/
 {
 	register uint32 size = p->size;
 	register uint32 j = 0;
@@ -1065,9 +1073,11 @@ int mp32pmilrabtwo_w(const mp32barrett* p, uint32 s, const uint32* rdata, const
 }
 
 /**
+ * mp32pmilraba_w
  * needs workspace of (5*size+2) words
  */
-int mp32pmilraba_w(const mp32barrett* p, const uint32* adata, uint32 s, const uint32* rdata, const uint32* ndata, uint32* wksp)
+static int mp32pmilraba_w(const mp32barrett* p, const uint32* adata, uint32 s, const uint32* rdata, const uint32* ndata, /*@out@*/ uint32* wksp)
+	/*@modifies wksp @*/
 {
 	register uint32 size = p->size;
 	register uint32 j = 0;
@@ -1246,6 +1256,8 @@ void mp32prndconone_w(mp32barrett* p, randomGeneratorContext* rc, uint32 size, i
 			{
 				mp32setlsb(s.size, s.modl);
 			}
+			else
+				{};
 
 			if (cofactor == 2)
 			{
diff --git a/beecrypt/mp32prime.h b/beecrypt/mp32prime.h
index 6051ca976..e8c1d2898 100644
--- a/beecrypt/mp32prime.h
+++ b/beecrypt/mp32prime.h
@@ -32,30 +32,52 @@
 
 #define SMALL_PRIMES_PRODUCT_MAX	64
 
+/**
+ */
+/*@-exportlocal@*/
 extern uint32* mp32spprod[SMALL_PRIMES_PRODUCT_MAX];
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI
 int  mp32ptrials     (uint32 bits)
 	/*@*/;
+
+/**
+ */
 BEEDLLAPI
-int  mp32pmilrab_w   (const mp32barrett* p, randomGeneratorContext* rc, int t, uint32* wksp)
+int  mp32pmilrab_w   (const mp32barrett* p, randomGeneratorContext* rc, int t, /*@out@*/ uint32* wksp)
 	/*@modifies wksp @*/;
 
+/**
+ */
 BEEDLLAPI
-void mp32prnd_w      (mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, /*@null@*/ const mp32number* f, uint32* wksp)
+void mp32prnd_w      (mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, /*@null@*/ const mp32number* f, /*@out@*/ uint32* wksp)
 	/*@modifies p, rc, wksp @*/;
+
+/**
+ */
 BEEDLLAPI
-void mp32prndsafe_w  (mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, uint32* wksp)
+void mp32prndsafe_w  (mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, /*@out@*/ uint32* wksp)
 	/*@modifies p, rc, wksp @*/;
-BEEDLLAPI
-void mp32prndcon_w   (mp32barrett* p, randomGeneratorContext* rc, uint32, int, const mp32number*, const mp32number*, const mp32number*, mp32number*, uint32* wksp)
+
+#ifdef	NOTYET
+/**
+ */
+BEEDLLAPI /*@unused@*/
+void mp32prndcon_w   (mp32barrett* p, randomGeneratorContext* rc, uint32, int, const mp32number*, const mp32number*, const mp32number*, mp32number*, /*@out@*/ uint32* wksp)
 	/*@modifies wksp @*/;
+#endif
+
+/**
+ */
 BEEDLLAPI
-void mp32prndconone_w(mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, const mp32barrett* q, /*@null@*/ const mp32number* f, mp32number* r, int cofactor, uint32* wksp)
+void mp32prndconone_w(mp32barrett* p, randomGeneratorContext* rc, uint32 size, int t, const mp32barrett* q, /*@null@*/ const mp32number* f, mp32number* r, int cofactor, /*@out@*/ uint32* wksp)
 	/*@modifies p, rc, r, wksp @*/;
 
 #ifdef __cplusplus
diff --git a/beecrypt/mtprng.c b/beecrypt/mtprng.c
index 25739f341..03b39c861 100644
--- a/beecrypt/mtprng.c
+++ b/beecrypt/mtprng.c
@@ -1,7 +1,7 @@
-/*
- * mtprng.c
+/**
+ * \file mtprng.c
  *
- * Mersenne Twister pseudo-random number generator
+ * Mersenne Twister pseudo-random number generator, code.
  *
  * Developed by Makoto Matsumoto and Takuji Nishimura
  *
@@ -13,7 +13,9 @@
  * Note: this generator has a very long period, passes statistical test, but
  * needs more study to determine whether it is cryptographically strong enough.
  *
- * Copyright (c) 1998, 1999, 2000, 2001 Virtual Unlimited B.V.
+ */
+
+/* Copyright (c) 1998, 1999, 2000, 2001 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
  *
@@ -53,12 +55,16 @@
 
 const randomGenerator mtprng = { "Mersenne Twister", sizeof(mtprngParam), (randomGeneratorSetup) mtprngSetup, (randomGeneratorSeed) mtprngSeed, (randomGeneratorNext) mtprngNext, (randomGeneratorCleanup) mtprngCleanup };
 
+/**
+ */
 static void mtprngReload(mtprngParam* mp)
 	/*@modifies mp @*/
 {
-    register uint32* p0 = mp->state, *p2=p0+2, *pM = p0+M, s0, s1;
+    register uint32* p0 = mp->state;
+    register uint32* p2=p0+2, *pM = p0+M, s0, s1;
     register int j;
 
+    /*@-shiftsigned@*/
     for (s0=mp->state[0], s1=mp->state[1], j=N-M+1; --j; s0=s1, s1=*(p2++))
         *(p0++) = *(pM++) ^ (mixBits(s0, s1) >> 1) ^ (loBit(s1) ? K : 0);
 
@@ -66,6 +72,7 @@ static void mtprngReload(mtprngParam* mp)
         *(p0++) = *(pM++) ^ (mixBits(s0, s1) >> 1) ^ (loBit(s1) ? K : 0);
 
     s1 = mp->state[0], *p0 = *pM ^ (mixBits(s0, s1) >> 1) ^ (loBit(s1) ? K : 0);
+    /*@=shiftsigned@*/
 
     mp->left = N;
     mp->nextw = mp->state;
diff --git a/beecrypt/mtprng.h b/beecrypt/mtprng.h
index bc73cbb9f..e9242a39b 100644
--- a/beecrypt/mtprng.h
+++ b/beecrypt/mtprng.h
@@ -1,8 +1,10 @@
-/*
- * mtprng.h
- *
- * Mersenne twister pseudo-random number generator, header
+/**
+ * \file mtprng.h
  *
+ * Mersenne twister pseudo-random number generator, header.
+ */
+
+/*
  * Copyright (c) 1998, 1999, 2000 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
@@ -41,12 +43,12 @@
 # endif
 #endif
 
-#include "beecrypt.h"
-
 #define N	624
 #define M	397
 #define K	0x9908B0DF
 
+/**
+ */
 typedef struct
 {
 	#ifdef _REENTRANT
@@ -64,27 +66,48 @@ typedef struct
 	#endif
 	uint32	state[N+1];
 	uint32	left;
-	uint32*	nextw;
+/*@kept@*/ uint32*	nextw;
 } mtprngParam;
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
+/**
+ */
 extern BEEDLLAPI const randomGenerator mtprng;
 
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mtprngSetup  (mtprngParam* mp)
 	/*@modifies mp @*/;
+/*@=exportlocal@*/
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mtprngSeed   (mtprngParam* mp, const uint32* data, int size)
 	/*@modifies mp @*/;
+/*@=exportlocal@*/
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mtprngNext   (mtprngParam* mp, uint32* data, int size)
 	/*@modifies mp, data @*/;
+/*@=exportlocal@*/
+
+/**
+ */
+/*@-exportlocal@*/
 BEEDLLAPI
 int mtprngCleanup(mtprngParam* mp)
 	/*@modifies mp @*/;
+/*@=exportlocal@*/
 
 #ifdef __cplusplus
 }
diff --git a/beecrypt/rsa.c b/beecrypt/rsa.c
index 0484083e3..845dba774 100644
--- a/beecrypt/rsa.c
+++ b/beecrypt/rsa.c
@@ -54,7 +54,7 @@ int rsapri(const rsakp* kp, const mp32number* m, mp32number* c)
 	return -1;
 }
 
-/*@-nullpass@*/
+/*@-nullpass -nullptrarith @*/ /* temp may be NULL */
 /* this routine doesn't work yet: needs debugging! */
 int rsapricrt(const rsakp* kp, const mp32number* m, mp32number* c)
 {
@@ -68,7 +68,9 @@ int rsapricrt(const rsakp* kp, const mp32number* m, mp32number* c)
 	if (mp32gex(psize, kp->p.modl, m->size, m->data))
 	{
 		mp32setx(nsize, temp+psize+qsize, m->size, m->data);
+		/*@-compdef@*/ /* LCL: temp+psize+qsize */
 		mp32bmod_w(&kp->p, temp+psize+qsize, temp, wksp);
+		/*@=compdef@*/
 	}
 	else
 		mp32setx(psize, temp, m->size, m->data);
@@ -79,7 +81,9 @@ int rsapricrt(const rsakp* kp, const mp32number* m, mp32number* c)
 	if (mp32gex(qsize, kp->q.modl, m->size, m->data))
 	{
 		mp32setx(nsize, temp+psize+qsize, m->size, m->data);
+		/*@-compdef@*/ /* LCL: temp+psize+qsize */
 		mp32bmod_w(&kp->q, temp+psize+qsize, temp+psize, wksp);
+		/*@=compdef@*/
 	}
 	else
 		mp32setx(qsize, temp+psize, m->size, m->data);
@@ -103,7 +107,7 @@ int rsapricrt(const rsakp* kp, const mp32number* m, mp32number* c)
 
 	return -1;
 }
-/*@=nullpass@*/
+/*@=nullpass =nullptrarith @*/
 
 /**
  * returns: 1 if signature verifies
diff --git a/beecrypt/rsa.h b/beecrypt/rsa.h
index 9e559a22c..9e80427e1 100644
--- a/beecrypt/rsa.h
+++ b/beecrypt/rsa.h
@@ -34,13 +34,20 @@
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI
 int rsapri   (const rsakp* kp, const mp32number* m, mp32number* c)
 	/*@modifies c */;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int rsapricrt(const rsakp* kp, const mp32number* m, mp32number* c)
 	/*@modifies c */;
 
+/**
+ */
 BEEDLLAPI
 int rsavrfy  (const rsapk* pk, const mp32number* m, const mp32number* c)
 	/*@*/;
diff --git a/beecrypt/rsakp.h b/beecrypt/rsakp.h
index dd8ff28c5..403d97219 100644
--- a/beecrypt/rsakp.h
+++ b/beecrypt/rsakp.h
@@ -48,16 +48,27 @@ typedef struct
 extern "C" {
 #endif
 
+/**
+ */
 BEEDLLAPI
 int rsakpMake(rsakp* kp, randomGeneratorContext* rgc, int nsize)
 	/*@modifies kp, rgc @*/;
+
+/**
+ */
 BEEDLLAPI
 int rsakpInit(rsakp* kp)
 	/*@modifies kp @*/;
+
+/**
+ */
 BEEDLLAPI
 int rsakpFree(rsakp* kp)
 	/*@modifies kp @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int rsakpCopy(rsakp* dst, const rsakp* src)
 	/*@modifies dst @*/;
 
diff --git a/beecrypt/rsapk.h b/beecrypt/rsapk.h
index 2a527afa0..908584ae7 100644
--- a/beecrypt/rsapk.h
+++ b/beecrypt/rsapk.h
@@ -30,6 +30,8 @@
 
 #include "mp32barrett.h"
 
+/**
+ */
 typedef struct
 {
 	mp32barrett n;
@@ -40,13 +42,21 @@ typedef struct
 extern "C" {
 #endif
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int rsapkInit(rsapk* pk)
 	/*@modifies pk @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int rsapkFree(rsapk* pk)
 	/*@modifies pk @*/;
-BEEDLLAPI
+
+/**
+ */
+BEEDLLAPI /*@unused@*/
 int rsapkCopy(rsapk* dst, const rsapk* src)
 	/*@modifies dst @*/;
 
diff --git a/beecrypt/sha256.h b/beecrypt/sha256.h
index 9aaaf8ed5..637ba3339 100644
--- a/beecrypt/sha256.h
+++ b/beecrypt/sha256.h
@@ -46,13 +46,15 @@ extern "C" {
 
 /** \ingroup HASH_sha256_m
  */
-extern BEEDLLAPI const hashFunction sha256;
+/*@observer@*/ /*@checkedstrict@*/ extern BEEDLLAPI const hashFunction sha256;
 
 /** \ingroup HASH_sha256_m
  */
+/*@-exportlocal@*/
 BEEDLLAPI
 void sha256Process(sha256Param* p)
-	/*@modifies p @*/;
+	/*@modifies p, internalState @*/;
+/*@=exportlocal@*/
 
 /** \ingroup HASH_sha256_m
  */
@@ -69,7 +71,7 @@ int  sha256Update (sha256Param* p, const byte* data, int size)
 /** \ingroup HASH_sha256_m
  */
 BEEDLLAPI
-int  sha256Digest (sha256Param* p, uint32* data)
+int  sha256Digest (sha256Param* p, /*@out@*/ uint32* data)
 	/*@modifies p, data @*/;
 
 #ifdef __cplusplus
diff --git a/beecrypt/tests/beetest.c b/beecrypt/tests/beetest.c
index a443ece5e..b89e59570 100644
--- a/beecrypt/tests/beetest.c
+++ b/beecrypt/tests/beetest.c
@@ -51,24 +51,36 @@
 
 #include <stdio.h>
 
+/*@unused@*/ /*@observer@*/
 static const char* dsa_p = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8324f0d7882e5d0762fc5b7210eafc2e9adac32ab7aac49693dfbf83724c2ec0736ee31c80291";
+/*@unused@*/ /*@observer@*/
 static const char* dsa_q = "c773218c737ec8ee993b4f2ded30f48edace915f";
+/*@unused@*/ /*@observer@*/
 static const char* dsa_g = "626d027839ea0a13413163a55b4cb500299d5522956cefcb3bff10f399ce2c2e71cb9de5fa24babf58e5b79521925c9cc42e9f6f464b088cc572af53e6d78802";
+/*@unused@*/ /*@observer@*/
 static const char* dsa_x = "2070b3223dba372fde1c0ffc7b2e3b498b260614";
+/*@unused@*/ /*@observer@*/
 static const char* dsa_y = "19131871d75b1612a819f29d78d1b0d7346f7aa77bb62a859bfd6c5675da9d212d3a36ef1672ef660b8c7c255cc0ec74858fba33f44c06699630a76b030ee333";
+/*@unused@*/ /*@observer@*/
 static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8324f0d7882e5d0762fc5b7210eafc2e9adac32ab7aac49693dfbf83724c2ec0736ee31c80290";
 
-int testVectorInvMod(const dlkp_p* keypair)
+/*@unused@*/ static int testVectorInvMod(const dlkp_p* keypair)
+	/*@*/
 {
 	randomGeneratorContext rngc;
 
+	memset(&rngc, 0, sizeof(randomGeneratorContext));
+
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		register int rc;
 
 		register uint32  size = keypair->param.p.size;
 		register uint32* temp = (uint32*) malloc((8*size+6) * sizeof(uint32));
 
+		/*@-nullpass -nullptrarith @*/ /* temp may be NULL */
 		mp32brndinv_w(&keypair->param.n, &rngc, temp, temp+size, temp+2*size);
 
 		mp32bmulmod_w(&keypair->param.n, size, temp, size, temp+size, temp, temp+2*size);
@@ -76,15 +88,17 @@ int testVectorInvMod(const dlkp_p* keypair)
 		rc = mp32isone(size, temp);
 
 		free(temp);
+		/*@=nullpass =nullptrarith @*/
 
-		randomGeneratorContextFree(&rngc);
+		(void) randomGeneratorContextFree(&rngc);
 
 		return rc;
 	}
 	return -1;
 }
 
-int testVectorExpMod(const dlkp_p* keypair)
+/*@unused@*/ static int testVectorExpMod(const dlkp_p* keypair)
+	/*@*/
 {
 	int rc;
 	mp32number y;
@@ -100,13 +114,18 @@ int testVectorExpMod(const dlkp_p* keypair)
 	return rc;
 }
 
-int testVectorElGamalV1(const dlkp_p* keypair)
+/*@unused@*/ static int testVectorElGamalV1(const dlkp_p* keypair)
+	/*@*/
 {
 	int rc = 0;
 
 	randomGeneratorContext rngc;
 
+	memset(&rngc, 0, sizeof(randomGeneratorContext));
+
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		mp32number digest, r, s;
 
@@ -116,9 +135,11 @@ int testVectorElGamalV1(const dlkp_p* keypair)
 
 		mp32nsize(&digest, 5);
 
-		rngc.rng->next(rngc.param, digest.data, digest.size);
+		/*@-noeffectuncon@*/ /* LCL: ??? */
+		(void) rngc.rng->next(rngc.param, digest.data, digest.size);
+		/*@=noeffectuncon@*/
 
-		elgv1sign(&keypair->param.p, &keypair->param.n, &keypair->param.g, &rngc, &digest, &keypair->x, &r, &s);
+		(void) elgv1sign(&keypair->param.p, &keypair->param.n, &keypair->param.g, &rngc, &digest, &keypair->x, &r, &s);
 
 		rc = elgv1vrfy(&keypair->param.p, &keypair->param.n, &keypair->param.g, &digest, &keypair->y, &r, &s);
 
@@ -126,18 +147,23 @@ int testVectorElGamalV1(const dlkp_p* keypair)
 		mp32nfree(&r);
 		mp32nfree(&s);
 
-		randomGeneratorContextFree(&rngc);
+		(void) randomGeneratorContextFree(&rngc);
 	}
 	return rc;
 }
 
-int testVectorElGamalV3(const dlkp_p* keypair)
+/*@unused@*/ static int testVectorElGamalV3(const dlkp_p* keypair)
+	/*@*/
 {
 	int rc = 0;
 
 	randomGeneratorContext rngc;
 
+	memset(&rngc, 0, sizeof(randomGeneratorContext));
+
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		mp32number digest, r, s;
 
@@ -147,9 +173,11 @@ int testVectorElGamalV3(const dlkp_p* keypair)
 
 		mp32nsize(&digest, 5);
 
-		rngc.rng->next(rngc.param, digest.data, digest.size);
+		/*@-noeffectuncon@*/ /* LCL: ??? */
+		(void) rngc.rng->next(rngc.param, digest.data, digest.size);
+		/*@=noeffectuncon@*/
 
-		elgv3sign(&keypair->param.p, &keypair->param.n, &keypair->param.g, &rngc, &digest, &keypair->x, &r, &s);
+		(void) elgv3sign(&keypair->param.p, &keypair->param.n, &keypair->param.g, &rngc, &digest, &keypair->x, &r, &s);
 
 		rc = elgv3vrfy(&keypair->param.p, &keypair->param.n, &keypair->param.g, &digest, &keypair->y, &r, &s);
 
@@ -157,13 +185,14 @@ int testVectorElGamalV3(const dlkp_p* keypair)
 		mp32nfree(&r);
 		mp32nfree(&s);
 
-		randomGeneratorContextFree(&rngc);
+		(void) randomGeneratorContextFree(&rngc);
 	}
 	return rc;
 }
 
 #if 0
-int testVectorDHAES(const dlkp_p* keypair)
+static int testVectorDHAES(const dlkp_p* keypair)
+	/*@*/
 {
 	/* try encrypting and decrypting a randomly generated message */
 
@@ -181,6 +210,7 @@ int testVectorDHAES(const dlkp_p* keypair)
 		/* make a random message of 2K size */
 		src.size = 2048;
 		src.data = (byte*) malloc(src.size);
+		/*@-nullpass@*/	/* malloc can return NULL */
 		memset(src.data, 1, src.size);
 
 		/* initialize the message key and mac */
@@ -207,6 +237,7 @@ int testVectorDHAES(const dlkp_p* keypair)
 		free(dst->data);
 		free(dst);
 		free(src.data);
+		/*@=nullpass@*/
 
 		dhaes_pFree(&dh);
 
@@ -217,20 +248,27 @@ int testVectorDHAES(const dlkp_p* keypair)
 }
 #endif
 
-int testVectorRSA()
+/*@unused@*/ static int testVectorRSA(void)
+	/*@*/
 {
 	int rc = 0;
 
 	randomGeneratorContext rngc;
 
+	memset(&rngc, 0, sizeof(randomGeneratorContext));
+
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		rsakp kp;
 		mp32number digest, s;
 
-		rsakpInit(&kp);
+		memset(&kp, 0, sizeof(rsakp));
+
+		(void) rsakpInit(&kp);
 		printf("making RSA CRT keypair\n");
-		rsakpMake(&kp, &rngc, 32);
+		(void) rsakpMake(&kp, &rngc, 32);
 		printf("RSA CRT keypair generated\n");
 
 		mp32nzero(&digest);
@@ -238,93 +276,106 @@ int testVectorRSA()
 
 		mp32bnrnd(&kp.n, &rngc, &digest);
 
-		rsapri(&kp, &digest, &s);
+		(void) rsapri(&kp, &digest, &s);
 
 		rc = rsavrfy((rsapk*) &kp, &digest, &s);
 
 		mp32nfree(&digest);
 		mp32nfree(&s);
 
-		rsakpFree(&kp);
+		(void) rsakpFree(&kp);
 
-		randomGeneratorContextFree(&rngc);
+		(void) randomGeneratorContextFree(&rngc);
 
 		return rc;
 	}
 	return -1;
 }
 
-int testVectorDLDP()
+/*@unused@*/ static int testVectorDLDP(void)
+	/*@*/
 {
 	/* try generating dldp_p parameters, then see if the order of the generator is okay */
 	randomGeneratorContext rc;
 	dldp_p dp;
 
+	memset(&rc, 0, sizeof(randomGeneratorContext));
 	memset(&dp, 0, sizeof(dldp_p));
 
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		register int result;
 		mp32number gq;
 
 		mp32nzero(&gq);
 
-		dldp_pgoqMake(&dp, &rc, 768 >> 5, 512 >> 5, 1);
+		(void) dldp_pgoqMake(&dp, &rc, 768 >> 5, 512 >> 5, 1);
 
 		/* we have the parameters, now see if g^q == 1 */
 		mp32bnpowmod(&dp.p, &dp.g, (mp32number*) &dp.q, &gq);
 		result = mp32isone(gq.size, gq.data);
 
 		mp32nfree(&gq);
-		dldp_pFree(&dp);
+		(void) dldp_pFree(&dp);
 
-		randomGeneratorContextFree(&rc);
+		(void) randomGeneratorContextFree(&rc);
 
 		return result;
 	}
 	return 0;
 }
 
-int testVectorMD5()
+/*@unused@*/ static int testVectorMD5(void)
+	/*@*/
 {
 	uint32 expect[4] = { 0x90015098, 0x3cd24fb0, 0xd6963f7d, 0x28e17f72 };
 	uint32 digest[4];
 	md5Param param;
 
-	md5Reset(&param);
-	md5Update(&param, (const unsigned char*) "abc", 3);
-	md5Digest(&param, digest);
+	memset(&param, 0, sizeof(param));
+
+	(void) md5Reset(&param);
+	(void) md5Update(&param, (const unsigned char*) "abc", 3);
+	(void) md5Digest(&param, digest);
 
 	return mp32eq(4, expect, digest);
 }
 
-int testVectorSHA1()
+/*@unused@*/ static int testVectorSHA1(void)
+	/*@*/
 {
 	uint32 expect[5] = { 0xA9993E36, 0x4706816A, 0xBA3E2571, 0x7850C26C, 0x9CD0D89D };
 	uint32 digest[5];
 	sha1Param param;
 	
-	sha1Reset(&param);
-	sha1Update(&param, (const unsigned char*) "abc", 3);
-	sha1Digest(&param, digest);
+	memset(&param, 0, sizeof(param));
+
+	(void) sha1Reset(&param);
+	(void) sha1Update(&param, (const unsigned char*) "abc", 3);
+	(void) sha1Digest(&param, digest);
 
 	return mp32eq(5, expect, digest);
 }
 
-int testVectorSHA256()
+/*@unused@*/ static int testVectorSHA256(void)
+	/*@*/
 {
 	uint32 expect[8] = { 0xba7816bf, 0x8f01cfea, 0x414140de, 0x5dae2223, 0xb00361a3, 0x96177a9c, 0xb410ff61, 0xf20015ad };
 	uint32 digest[8];
 	sha256Param param;
 	
-	sha256Reset(&param);
-	sha256Update(&param, (const unsigned char*) "abc", 3);
-	sha256Digest(&param, digest);
+	memset(&param, 0, sizeof(param));
+
+	(void) sha256Reset(&param);
+	(void) sha256Update(&param, (const unsigned char*) "abc", 3);
+	(void) sha256Digest(&param, digest);
 
 	return mp32eq(8, expect, digest);
 }
 
-uint32 keyValue[] = 
+static uint32 keyValue[] = 
 {
 	0x00010203,
 	0x04050607,
@@ -344,14 +395,19 @@ uint32 keyValue[] =
 	0x3c3d3e3f
 };
 	
-void testBlockInit(uint8* block, int length)
+static void testBlockInit(/*@out@*/ uint8* block, int length)
+	/*@modifies *block @*/
 {
 	register int i;
-	for (i = 1; i <= length; i++)
-		*(block++) = (uint8) i;
+	for (i = 1; i <= length; i++) {
+		block++;
+		*block = (uint8) i;
+	}
 }
 
-void testBlockCiphers()
+static void testBlockCiphers(void)
+	/*@globals keyValue @*/
+	/*@modifies internalState @*/
 {
 	int i, k;
 
@@ -373,34 +429,40 @@ void testBlockCiphers()
 			void* encrypt_param = (void*) malloc(tmp->paramsize);
 			void* decrypt_param = (void*) malloc(tmp->paramsize);
 
+			if (encrypt_param)
+				memset(encrypt_param, 0, tmp->paramsize);
+			if (decrypt_param)
+				memset(decrypt_param, 0, tmp->paramsize);
+
 			printf("  %s:\n", tmp->name);
 
+			/*@-nullpass@*/ /* malloc can return NULL */
 			for (k = tmp->keybitsmin; k <= tmp->keybitsmax; k += tmp->keybitsinc)
 			{
 				printf("    setup encrypt (%d bits key): ", k);
 				if (tmp->setup(encrypt_param, keyValue, k, ENCRYPT) < 0)
 				{
 					printf("failed\n");
-					continue;
+					/*@innercontinue@*/ continue;
 				}
 				printf("ok\n");
 				printf("    setup decrypt (%d bits key): ", k);
 				if (tmp->setup(decrypt_param, keyValue, k, DECRYPT) < 0)
 				{
 					printf("failed\n");
-					continue;
+					/*@innercontinue@*/ continue;
 				}
 				printf("ok\n");
 				printf("    encrypt/decrypt test block: ");
 				testBlockInit((uint8*) src_block, tmp->blocksize >> 2);
 
-				blockEncrypt(tmp, encrypt_param, CBC, 2, enc_block, src_block);
-				blockDecrypt(tmp, decrypt_param, CBC, 2, dec_block, enc_block);
+				(void) blockEncrypt(tmp, encrypt_param, CBC, 2, enc_block, src_block);
+				(void) blockDecrypt(tmp, decrypt_param, CBC, 2, dec_block, enc_block);
 
 				if (memcmp(dec_block, src_block, tmp->blocksize >> 2))
 				{
 					printf("failed\n");
-					continue;
+					/*@innercontinue@*/ continue;
 				}
 				printf("ok\n");
 				printf("    speed measurement:\n");
@@ -413,38 +475,40 @@ void testBlockCiphers()
 					#if HAVE_TIME_H
 					tstart = clock();
 					#endif
-					blockEncrypt(tmp, encrypt_param, ECB, 1024 * 1024, spd_block, spd_block);
+					/*@-compdef@*/ /* spd_block undefined */
+					(void) blockEncrypt(tmp, encrypt_param, ECB, 1024 * 1024, spd_block, spd_block);
+					/*@=compdef@*/
 					#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 %d bits in %.3f seconds (%.3f MB/s)\n", (int)(tmp->blocksize << 3), ttime, (tmp->blocksize) / ttime);
 					#endif
 					#if HAVE_TIME_H
 					tstart = clock();
 					#endif
-					blockDecrypt(tmp, decrypt_param, ECB, 1024 * 1024, spd_block, spd_block);
+					(void) blockDecrypt(tmp, decrypt_param, ECB, 1024 * 1024, spd_block, spd_block);
 					#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 %d bits in %.3f seconds (%.3f MB/s)\n", (int)(tmp->blocksize << 3), ttime, (tmp->blocksize) / ttime);
 					#endif
 					#if HAVE_TIME_H
 					tstart = clock();
 					#endif
-					blockEncrypt(tmp, encrypt_param, CBC, 1024 * 1024, spd_block, spd_block);
+					(void) blockEncrypt(tmp, encrypt_param, CBC, 1024 * 1024, spd_block, spd_block);
 					#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 %d bits in %.3f seconds (%.3f MB/s)\n", (int)(tmp->blocksize << 3), ttime, (tmp->blocksize) / ttime);
 					#endif
 					#if HAVE_TIME_H
 					tstart = clock();
 					#endif
-					blockDecrypt(tmp, decrypt_param, CBC, 1024 * 1024, spd_block, spd_block);
+					(void) blockDecrypt(tmp, decrypt_param, CBC, 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 %d bits in %.3f seconds (%.3f MB/s)\n", (int)(tmp->blocksize << 3), ttime, (tmp->blocksize) / ttime);
 					#endif
 				}
 			}
@@ -454,11 +518,13 @@ void testBlockCiphers()
 			free(src_block);
 			free(decrypt_param);
 			free(encrypt_param);
+			/*@=nullpass@*/
 		}
 	}
 }
 
-void testHashFunctions()
+static void testHashFunctions(void)
+	/*@modifies internalState */
 {
 	int i, j;
 
@@ -468,6 +534,7 @@ void testHashFunctions()
 	{
 		hashFunctionContext hfc;
 
+		memset(&hfc, 0, sizeof(hashFunctionContext));
 		printf("  Testing the hash functions:\n");
 
 		for (i = 0; i < hashFunctionCount(); i++)
@@ -494,8 +561,10 @@ void testHashFunctions()
 						tstart = clock();
 						#endif
 
-						hashFunctionContextUpdate(&hfc, data, 32 * 1024 * 1024);
-						hashFunctionContextDigest(&hfc, &digest);
+						/*@-compdef@*/ /* data undefined */
+						(void) hashFunctionContextUpdate(&hfc, data, 32 * 1024 * 1024);
+						/*@=compdef@*/
+						(void) hashFunctionContextDigest(&hfc, &digest);
 
 						#if HAVE_TIME_H
 						tstop = clock();
@@ -504,7 +573,7 @@ void testHashFunctions()
 						#endif
 					}
 
-					hashFunctionContextFree(&hfc);
+					(void) hashFunctionContextFree(&hfc);
 				}
 
 				mp32nfree(&digest);
@@ -513,13 +582,14 @@ void testHashFunctions()
 	}
 }
 
-void testExpMods()
+static void testExpMods(void)
+	/*@modifies internalState */
 {
-	static const char* p_512 = "ffcf0a0767f18f9b659d92b9550351430737c3633dc6ae7d52445d937d8336e07a7ccdb119e9ab3e011a8f938151230e91187f84ac05c3220f335193fc5e351b";
+	/*@observer@*/ static const char* p_512 = "ffcf0a0767f18f9b659d92b9550351430737c3633dc6ae7d52445d937d8336e07a7ccdb119e9ab3e011a8f938151230e91187f84ac05c3220f335193fc5e351b";
 
-	static const char* p_768 = "f9c3dc0b8e199094e3e69386e01de863908348196d6ad2557065e6ba36d10412579f394d1114c954ee647c84551d52f214e1e1682a75e7074b91085cfaf20b2888aa056bf760948a0b678bc253633eccfca86556ddb90f000ef93041b0d53171";
+	/*@observer@*/ static const char* p_768 = "f9c3dc0b8e199094e3e69386e01de863908348196d6ad2557065e6ba36d10412579f394d1114c954ee647c84551d52f214e1e1682a75e7074b91085cfaf20b2888aa056bf760948a0b678bc253633eccfca86556ddb90f000ef93041b0d53171";
 
-	static const char* p_1024 = "c615c47a56b47d869010256171ab164525f2ef4b887a4e0cdfc87043a9dd8894f2a18fa56729448e700f4b7420470b61257d11ecefa9ff518dc9fed5537ec6a9665ba73c948674320ff61b29c4cfa61e5baf47dfc1b80939e1bffb51787cc3252c4d1190a7f13d1b0f8d4aa986571ce5d4de5ecede1405e9bc0b5bf040a46d99";
+	/*@observer@*/ static const char* p_1024 = "c615c47a56b47d869010256171ab164525f2ef4b887a4e0cdfc87043a9dd8894f2a18fa56729448e700f4b7420470b61257d11ecefa9ff518dc9fed5537ec6a9665ba73c948674320ff61b29c4cfa61e5baf47dfc1b80939e1bffb51787cc3252c4d1190a7f13d1b0f8d4aa986571ce5d4de5ecede1405e9bc0b5bf040a46d99";
 
 	randomGeneratorContext rngc;
 
@@ -529,13 +599,17 @@ void testExpMods()
 	mp32number x;
 	mp32number y;
 
+	memset(&rngc, 0, sizeof(randomGeneratorContext));
+
 	mp32bzero(&p);
 	mp32nzero(&g);
 	mp32nzero(&x);
 	mp32nzero(&y);
 	mp32nzero(&tmp);
 
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		int i;
 		#if HAVE_TIME_H
@@ -597,7 +671,9 @@ void testExpMods()
 		#endif
 		/* now run a test with x having 160 bits */
 		mp32nsize(&x, 5);
-		rngc.rng->next(rngc.param, x.data, x.size);
+		/*@-noeffectuncon@*/ /* LCL: ??? */
+		(void) rngc.rng->next(rngc.param, x.data, x.size);
+		/*@=noeffectuncon@*/
 		printf("  (1024 bits ^ 160 bits) mod 1024 bits:");
 		#if HAVE_TIME_H
 		tstart = clock();
@@ -615,20 +691,24 @@ void testExpMods()
 		mp32nfree(&y);
 		mp32nfree(&tmp);
 
-		randomGeneratorContextFree(&rngc);
+		(void) randomGeneratorContextFree(&rngc);
 	}
 	else
 		printf("random generator setup problem\n");
 }
 
-void testDLParams()
+static void testDLParams(void)
+	/*@modifies internalState */
 {
 	randomGeneratorContext rc;
 	dldp_p dp;
 
+	memset(&rc, 0, sizeof(randomGeneratorContext));
 	memset(&dp, 0, sizeof(dldp_p));
 
+	/*@-nullpass@*/
 	if (randomGeneratorContextInit(&rc, randomGeneratorDefault()) == 0)
+	/*@=nullpass@*/
 	{
 		#if HAVE_TIME_H
 		double ttime;
@@ -638,39 +718,39 @@ void testDLParams()
 		#if HAVE_TIME_H
 		tstart = clock();
 		#endif
-		dldp_pgoqMake(&dp, &rc, 768 >> 5, 512 >> 5, 1);
+		(void) dldp_pgoqMake(&dp, &rc, 768 >> 5, 512 >> 5, 1);
 		#if HAVE_TIME_H
 		tstop = clock();
 		ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
 		printf("  done in %.3f seconds\n", ttime);
 		#endif
-		printf("P = "); fflush(stdout); mp32println(dp.p.size, dp.p.modl);
-		printf("Q = "); fflush(stdout); mp32println(dp.q.size, dp.q.modl);
-		printf("G = "); fflush(stdout); mp32println(dp.g.size, dp.g.data);
-		dldp_pFree(&dp);
+		printf("P = "); (void) fflush(stdout); mp32println(dp.p.size, dp.p.modl);
+		printf("Q = "); (void) fflush(stdout); mp32println(dp.q.size, dp.q.modl);
+		printf("G = "); (void) fflush(stdout); mp32println(dp.g.size, dp.g.data);
+		(void) dldp_pFree(&dp);
 
 		printf("Generating P (768 bits) Q (512 bits) G with order (P-1)\n");
 		#if HAVE_TIME_H
 		tstart = clock();
 		#endif
-		dldp_pgonMake(&dp, &rc, 768 >> 5, 512 >> 5);
+		(void) dldp_pgonMake(&dp, &rc, 768 >> 5, 512 >> 5);
 		#if HAVE_TIME_H
 		tstop = clock();
 		ttime = ((double)(tstop - tstart)) / CLOCKS_PER_SEC;
 		printf("  done in %.3f seconds\n", ttime);
 		#endif
-		printf("P = "); fflush(stdout); mp32println(dp.p.size, dp.p.modl);
-		printf("Q = "); fflush(stdout); mp32println(dp.q.size, dp.q.modl);
-		printf("G = "); fflush(stdout); mp32println(dp.g.size, dp.g.data);
-		printf("N = "); fflush(stdout); mp32println(dp.n.size, dp.n.modl);
-		dldp_pFree(&dp);
+		printf("P = "); (void) fflush(stdout); mp32println(dp.p.size, dp.p.modl);
+		printf("Q = "); (void) fflush(stdout); mp32println(dp.q.size, dp.q.modl);
+		printf("G = "); (void) fflush(stdout); mp32println(dp.g.size, dp.g.data);
+		printf("N = "); (void) fflush(stdout); mp32println(dp.n.size, dp.n.modl);
+		(void) dldp_pFree(&dp);
 
-		randomGeneratorContextFree(&rc);
+		(void) randomGeneratorContextFree(&rc);
 	}
 }
 
 #if 0
-int main()
+int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
 {
 	dlkp_p keypair;
 
@@ -741,7 +821,7 @@ int main()
 	return 0;
 }
 #else
-int main()
+int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
 {
 	int i, j;
 
@@ -801,10 +881,12 @@ int main()
 		else
 			printf("*** error: library corrupt\n");
 	}
+	/*@-modnomods@*/ /* LCL: ??? */
 	testBlockCiphers();
 	testHashFunctions();
 	testExpMods();
 	testDLParams();
+	/*@=modnomods@*/
 
 	printf("done\n");
 
diff --git a/beecrypt/timestamp.h b/beecrypt/timestamp.h
index 364273d91..75b289123 100644
--- a/beecrypt/timestamp.h
+++ b/beecrypt/timestamp.h
@@ -1,8 +1,10 @@
-/*
- * timestamp.h
- *
- * Java-compatible 64 bit timestamp, header
+/** \ingroup JAVA_m
+ * \file timestamp.h
  *
+ * Java-compatible 64 bit timestamp, header.
+ */
+
+/*
  * Copyright (c) 1999, 2000 Virtual Unlimited B.V.
  *
  * Author: Bob Deblier <bob@virtualunlimited.com>
@@ -46,7 +48,9 @@
 extern "C" {
 #endif
 
-BEEDLLAPI
+/**
+ */
+BEEDLLAPI /*@unused@*/
 javalong timestamp(void);
 
 #ifdef __cplusplus
author	jbj <devnull@localhost>	2001-09-23 12:09:48 +0000
committer	jbj <devnull@localhost>	2001-09-23 12:09:48 +0000
commit	0f7777894493527a5672d0ce09c4855e2b69495f (patch)
tree	af5511490946ca59d1abc0ae69696437bd73eac8 /beecrypt
parent	1eef0782f60f9d8d80be273ace982ad4c2a56d98 (diff)
download	librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.tar.gz librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.tar.bz2 librpm-tizen-0f7777894493527a5672d0ce09c4855e2b69495f.zip