More lclint fiddles.

CVS patchset: 5070
CVS date: 2001/09/23 15:47:37

diff --git a/beecrypt/.lclintrc b/beecrypt/.lclintrc
index 3be6606..53e47f0 100644 (file)
--- a/beecrypt/.lclintrc
+++ b/beecrypt/.lclintrc
@@ -13,61 +13,40 @@
 +strict                        # lclint level
 
 # --- not-yet at strict level
--exportconst
--exportfcn
--exporttype
--exportvar
--warnmissingglobs
--internalglobs
+-exportconst           # 4 occurences
+-exportfcn             # 317 occurences
+-exporttype            # 52 occurences
+-exportvar             # 10 occurences
 -protoparamname
 
 -ansi-reserved-internal        # goofy
 
--ptrarith
--bitwisesigned
--strictops
--sizeoftype
-
--mod-file-sys
+-ptrarith              # 217 occurences
+-bitwisesigned         # 69 occurences
+-strictops             # 37 occurences
+-sizeoftype            # 124 occurences
 
 -impcheckedstrictglobs
 -impcheckedstrictstatics
 -strictbranchstate
--strictdestroy
+-strictdestroy         # 18 occurences
 
--forblock
--ifblock
--whileblock
+-forblock              # 10 occurences
+-ifblock               # 406 occurences
+-whileblock            # 23 occurences
 -sys-dir-errors                # 30 occurences
 
 # --- not-yet at checks level
--predboolptr   
-+enumint
--allglobs              # painful
+-predboolptr           # 121 occurences
+-allglobs              # 219 occurences, painful
 -ansi-reserved         # goofy
--infloopsuncon         # goofy
 
 # don't-bother-me-yet parameters
 -branchstate           # 6 occurences
--mustfree              # alloca is painful
 
 # --- not-yet at standard level
--boolops
--predboolint
--type
+-boolops               # 58 occurences
+-predboolint           # 203 occurences
+-type                  # 844 occurences
 
 # --- not-yet at weak level
-#+boolint
-#-boolops
-#+ignorequals
-#+ignoresigns
-#-mustfree
-#+longintegral
-#+matchanyintegral
-#-nullpass
-#-observertrans
-#-predboolint
-#-predboolothers
-#-retvalint
-#-retvalother
-#-shiftsigned

diff --git a/beecrypt/Makefile.in b/beecrypt/Makefile.in
index 295ab5f..da4a713 100644 (file)
--- a/beecrypt/Makefile.in
+++ b/beecrypt/Makefile.in
@@ -139,8 +139,6 @@ 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
 
-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
 mkinstalldirs = $(SHELL) $(top_srcdir)/mkinstalldirs

diff --git a/beecrypt/beecrypt.c b/beecrypt/beecrypt.c
index 8c8002b..e482f9c 100644 (file)
--- a/beecrypt/beecrypt.c
+++ b/beecrypt/beecrypt.c
@@ -209,9 +209,9 @@ int randomGeneratorContextInit(randomGeneratorContext* ctxt, const randomGenerat
        if (rng == (randomGenerator*) 0)
                return -1;
 
-       /*@-temptrans@*/
        ctxt->rng = rng;
-       /*@=temptrans@*/
+       if (ctxt->param)        /* XXX error? */
+               free(ctxt->param);
        ctxt->param = (randomGeneratorParam*) calloc(rng->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -226,6 +226,7 @@ int randomGeneratorContextFree(randomGeneratorContext* ctxt)
 {
        register int rc;
 
+       /*@-mustfree@*/
        if (ctxt == (randomGeneratorContext*) 0)
                return -1;
 
@@ -234,6 +235,7 @@ int randomGeneratorContextFree(randomGeneratorContext* ctxt)
 
        if (ctxt->param == (randomGeneratorParam*) 0)
                return -1;
+       /*@=mustfree@*/
 
        rc = ctxt->rng->cleanup(ctxt->param);
 
@@ -302,9 +304,9 @@ int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
        if (hash == (hashFunction*) 0)
                return -1;
 
-       /*@-temptrans@*/
        ctxt->algo = hash;
-       /*@=temptrans@*/
+       if (ctxt->param)        /* XXX error? */
+               free(ctxt->param);
        ctxt->param = (hashFunctionParam*) calloc(hash->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -317,11 +319,13 @@ int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
 
 int hashFunctionContextFree(hashFunctionContext* ctxt)
 {
+       /*@-mustfree@*/
        if (ctxt == (hashFunctionContext*) 0)
                return -1;
 
        if (ctxt->param == (hashFunctionParam*) 0)
                return -1;
+       /*@=mustfree@*/
 
        free(ctxt->param);
 
@@ -450,7 +454,9 @@ int hashFunctionContextDigestMatch(hashFunctionContext* ctxt, const mp32number*
 
        mp32nfree(&dig);
 
+       /*@-mustfree@*/ /* dig.data is OK */
        return rc;
+       /*@=mustfree@*/
 }
 
 /*@observer@*/ static const keyedHashFunction* keyedHashFunctionList[] =
@@ -509,9 +515,9 @@ int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHash
        if (mac == (keyedHashFunction*) 0)
                return -1;
 
-       /*@-temptrans@*/
        ctxt->algo = mac;
-       /*@=temptrans@*/
+       if (ctxt->param)        /* XXX error? */
+               free(ctxt->param);
        ctxt->param = (keyedHashFunctionParam*) calloc(mac->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -524,6 +530,7 @@ int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHash
 
 int keyedHashFunctionContextFree(keyedHashFunctionContext* ctxt)
 {
+       /*@-mustfree@*/
        if (ctxt == (keyedHashFunctionContext*) 0)
                return -1;
 
@@ -532,6 +539,7 @@ int keyedHashFunctionContextFree(keyedHashFunctionContext* ctxt)
 
        if (ctxt->param == (keyedHashFunctionParam*) 0)
                return -1;
+       /*@=mustfree@*/
 
        free(ctxt->param);
 
@@ -678,7 +686,9 @@ int keyedHashFunctionContextDigestMatch(keyedHashFunctionContext* ctxt, const mp
 
        mp32nfree(&dig);
 
+       /*@-mustfree@*/ /* dig.data is OK */
        return rc;
+       /*@=mustfree@*/
 }
 
 
@@ -737,9 +747,9 @@ int blockCipherContextInit(blockCipherContext* ctxt, const blockCipher* ciph)
        if (ciph == (blockCipher*) 0)
                return -1;
 
-       /*@-temptrans@*/
        ctxt->algo = ciph;
-       /*@=temptrans@*/
+       if (ctxt->param)        /* XXX error? */
+               free(ctxt->param);
        ctxt->param = (blockCipherParam*) calloc(ciph->paramsize, 1);
 
        /*@-nullstate@*/ /* FIX: ctxt->param may be NULL */
@@ -785,11 +795,13 @@ int blockCipherContextSetIV(blockCipherContext* ctxt, const uint32* iv)
 
 int blockCipherContextFree(blockCipherContext* ctxt)
 {
+       /*@-mustfree@*/
        if (ctxt == (blockCipherContext*) 0)
                return -1;
 
        if (ctxt->param == (blockCipherParam*) 0)
                return -1;
+       /*@=mustfree@*/
 
        free(ctxt->param);
 

diff --git a/beecrypt/beecrypt.h b/beecrypt/beecrypt.h
index 76f1b25..ed0fda2 100644 (file)
--- a/beecrypt/beecrypt.h
+++ b/beecrypt/beecrypt.h
@@ -239,7 +239,7 @@ const randomGenerator* randomGeneratorDefault(void)
  */
 typedef struct
 {
-    const randomGenerator* rng;                /*!< global functions and parameters */
+/*@observer@*/ /*@dependent@*/ const randomGenerator* rng; /*!< global functions and parameters */
 /*@only@*/ randomGeneratorParam* param;        /*!< specific parameters */
 } randomGeneratorContext;
 
@@ -251,14 +251,16 @@ extern "C" {
  * Initialize a randomGenerator instance.
  */
 BEEDLLAPI
-int randomGeneratorContextInit(randomGeneratorContext* ctxt, const randomGenerator* rng)
+int randomGeneratorContextInit(randomGeneratorContext* ctxt, /*@observer@*/ /*@dependent@*/ const randomGenerator* rng)
        /*@modifies ctxt->rng, ctxt->param @*/;
 
 /** \ingroup PRNG_m
  * Destroy a randomGenerator instance.
  */
 BEEDLLAPI
-int randomGeneratorContextFree(randomGeneratorContext* ctxt)
+int randomGeneratorContextFree(/*@special@*/ randomGeneratorContext* ctxt)
+       /*@uses ctxt->rng @*/
+       /*@releases ctxt->param @*/
        /*@modifies ctxt->rng, ctxt->param @*/;
 
 #ifdef __cplusplus
@@ -377,8 +379,8 @@ const hashFunction* hashFunctionDefault(void)
  */
 typedef struct
 {
-/*@unused@*/ const hashFunction* algo; /*!< global functions and parameters */
-/*@unused@*/ hashFunctionParam* param; /*!< specific parameters */
+/*@observer@*/ /*@dependent@*/ const hashFunction* algo;/*!< global functions and parameters */
+/*@only@*/ hashFunctionParam* param;   /*!< specific parameters */
 } hashFunctionContext;
 
 #ifdef __cplusplus
@@ -389,15 +391,16 @@ extern "C" {
  * Initialize a hashFunction instance.
  */
 BEEDLLAPI
-int hashFunctionContextInit(hashFunctionContext* ctxt, const hashFunction* hash)
-       /*@modifies ctxt */;
+int hashFunctionContextInit(hashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const hashFunction* hash)
+       /*@modifies ctxt->algo, ctxt->param */;
 
 /** \ingroup HASH_m
  * Destroy a hashFunction instance.
  */
 BEEDLLAPI
-int hashFunctionContextFree(hashFunctionContext* ctxt)
-       /*@modifies ctxt */;
+int hashFunctionContextFree(/*@special@*/ hashFunctionContext* ctxt)
+       /*@releases ctxt->param @*/
+       /*@modifies ctxt->algo, ctxt->param */;
 
 /** \ingroup HASH_m
  */
@@ -569,8 +572,8 @@ const keyedHashFunction* keyedHashFunctionDefault(void)
  */
 typedef struct
 {
-/*@unused@*/ const keyedHashFunction* algo;    /*!< global functions and parameters */
-/*@unused@*/ keyedHashFunctionParam* param;    /*!< specific parameters */
+/*@observer@*/ /*@dependent@*/ const keyedHashFunction* algo;  /*!< global functions and parameters */
+/*@only@*/ keyedHashFunctionParam* param;      /*!< specific parameters */
 } keyedHashFunctionContext;
 
 #ifdef __cplusplus
@@ -581,15 +584,17 @@ extern "C" {
  * Initialize a keyedHashFunction instance.
  */
 BEEDLLAPI
-int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, const keyedHashFunction* mac)
-       /*@modifies ctxt @*/;
+int keyedHashFunctionContextInit(keyedHashFunctionContext* ctxt, /*@observer@*/ /*@dependent@*/ const keyedHashFunction* mac)
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup HMAC_m
  * Destroy a keyedHashFunction instance.
  */
 BEEDLLAPI
-int keyedHashFunctionContextFree(keyedHashFunctionContext* ctxt)
-       /*@modifies ctxt @*/;
+int keyedHashFunctionContextFree(/*@special@*/ keyedHashFunctionContext* ctxt)
+       /*@uses ctxt->algo @*/
+       /*@releases ctxt->param @*/
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup HMAC_m
  */
@@ -659,9 +664,7 @@ typedef enum
  */
 typedef enum
 {
-       /*@-enummemuse@*/
        ECB,
-       /*@=enummemuse@*/
        CBC
 } cipherMode;
 
@@ -812,8 +815,8 @@ const blockCipher* blockCipherDefault(void)
  */
 typedef struct
 {
-    const blockCipher* algo;   /*!< global functions and parameters */
-    blockCipherParam* param;   /*!< specific parameters */
+/*@observer@*/ /*@dependent@*/ const blockCipher* algo;        /*!< global functions and parameters */
+/*@only@*/ blockCipherParam* param;    /*!< specific parameters */
 } blockCipherContext;
 
 #ifdef __cplusplus
@@ -824,8 +827,8 @@ extern "C" {
  * Initialize a blockCipher instance.
  */
 BEEDLLAPI
-int blockCipherContextInit(blockCipherContext* ctxt, const blockCipher* ciph)
-       /*@modifies ctxt @*/;
+int blockCipherContextInit(blockCipherContext* ctxt, /*@observer@*/ /*@dependent@*/ const blockCipher* ciph)
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 /** \ingroup BC_m
  */
@@ -843,8 +846,9 @@ int blockCipherContextSetIV(blockCipherContext* ctxt, const uint32* iv)
  * Destroy a blockCipher instance.
  */
 BEEDLLAPI
-int blockCipherContextFree(blockCipherContext* ctxt)
-       /*@modifies ctxt @*/;
+int blockCipherContextFree(/*@special@*/ blockCipherContext* ctxt)
+       /*@releases ctxt->param @*/
+       /*@modifies ctxt->algo, ctxt->param @*/;
 
 #ifdef __cplusplus
 }

diff --git a/beecrypt/dhaes.c b/beecrypt/dhaes.c
index 676c715..98e6ea9 100644 (file)
--- a/beecrypt/dhaes.c
+++ b/beecrypt/dhaes.c
@@ -132,6 +132,7 @@ int dhaes_pContextInit(dhaes_pContext* ctxt, const dhaes_pParameters* params)
        mp32nzero(&ctxt->pub);
        mp32nzero(&ctxt->pri);
 
+       /*@-modobserver@*/
        if (hashFunctionContextInit(&ctxt->hash, params->hash))
                return -1;
 
@@ -140,6 +141,7 @@ int dhaes_pContextInit(dhaes_pContext* ctxt, const dhaes_pParameters* params)
 
        if (keyedHashFunctionContextInit(&ctxt->mac, params->mac))
                return -1;
+       /*@=modobserver@*/
 
        ctxt->cipherkeybits = params->cipherkeybits;
        ctxt->mackeybits = params->mackeybits;
@@ -174,6 +176,7 @@ int dhaes_pContextFree(dhaes_pContext* ctxt)
        mp32nfree(&ctxt->pub);
        mp32nfree(&ctxt->pri);
 
+       /*@-mustfree -modobserver @*/ /* ctxt is OK */
        if (hashFunctionContextFree(&ctxt->hash))
                return -1;
 
@@ -184,6 +187,7 @@ int dhaes_pContextFree(dhaes_pContext* ctxt)
                return -1;
 
        return 0;
+       /*@=mustfree =modobserver @*/
 }
 
 /**
@@ -199,7 +203,9 @@ static int dhaes_pContextSetup(dhaes_pContext* ctxt, const mp32number* privkey,
        /* compute the shared secret, Diffie-Hellman style */
        mp32nzero(&secret);
        if (dlsvdp_pDHSecret(&ctxt->param, privkey, pubkey, &secret))
+               /*@-mustfree@*/ /* FIX: secret.data leak? */
                return -1;
+               /*@=mustfree@*/
 
        /* compute the hash of the message (ephemeral public) key and the shared secret */
        mp32nzero(&digest);
@@ -245,7 +251,9 @@ setup_end:
        mp32nwipe(&digest);
        mp32nfree(&digest);
 
+       /*@-mustfree@*/ /* {secret,digest}.data are OK */
        return rc;
+       /*@=mustfree@*/
 }
 
 memchunk* dhaes_pContextEncrypt(dhaes_pContext* ctxt, mp32number* ephemeralPublicKey, mp32number* mac, const memchunk* cleartext, randomGeneratorContext* rng)
@@ -297,7 +305,9 @@ encrypt_end:
        mp32nwipe(&ephemeralPrivateKey);
        mp32nfree(&ephemeralPrivateKey);
 
+       /*@-mustfree@*/ /* ephemeralPrivateKey.data is OK */
        return ciphertext;
+       /*@=mustfree@*/
 }
 
 memchunk* dhaes_pContextDecrypt(dhaes_pContext* ctxt, const mp32number* ephemeralPublicKey, const mp32number* mac, const memchunk* ciphertext)
@@ -323,7 +333,9 @@ memchunk* dhaes_pContextDecrypt(dhaes_pContext* ctxt, const mp32number* ephemera
                goto decrypt_end;
 
        paddedtext->size = ciphertext->size;
+       /*@-mustfree@*/ /* paddedtext->data is OK */
        paddedtext->data = (byte*) malloc(ciphertext->size);
+       /*@=mustfree@*/
 
        if (paddedtext->data == (byte*) 0)
        {

diff --git a/beecrypt/dldp.c b/beecrypt/dldp.c
index cee920a..d96db15 100644 (file)
--- a/beecrypt/dldp.c
+++ b/beecrypt/dldp.c
@@ -43,12 +43,12 @@
 /**
  */
 static int dldp_pgoqGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, /*@out@*/ uint32* wksp)
-       /*@modifies dp, wksp @*/;
+       /*@modifies dp->g, wksp @*/;
 
 /**
  */
 static int dldp_pgonGenerator_w(dldp_p* dp, randomGeneratorContext* rgc, /*@out@*/ uint32* wksp)
-       /*@modifies dp, wksp @*/;
+       /*@modifies dp->g, wksp @*/;
 
 int dldp_pPrivate(const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x)
 {
@@ -157,11 +157,13 @@ int dldp_pInit(dldp_p* dp)
 
 int dldp_pFree(dldp_p* dp)
 {
+       /*@-usedef -compdef@*/
        mp32bfree(&dp->p);
        mp32bfree(&dp->q);
        mp32nfree(&dp->g);
        mp32nfree(&dp->r);
        mp32bfree(&dp->n);
+       /*@=usedef =compdef@*/
 
        return 0;
 }

diff --git a/beecrypt/dldp.h b/beecrypt/dldp.h
index 03c0e30..d93d391 100644 (file)
--- a/beecrypt/dldp.h
+++ b/beecrypt/dldp.h
@@ -65,19 +65,20 @@ extern "C" {
  */
 BEEDLLAPI
 int dldp_pInit(dldp_p* dp)
-       /*@modifies dp */;
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n @*/;
 
 /**
  */
 BEEDLLAPI
-int dldp_pFree(dldp_p* dp)
-       /*@modifies dp */;
+int dldp_pFree(/*@special@*/ dldp_p* dp)
+       /*@releases dp->p.modl, dp->q.modl, dp->n.modl @*/
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n @*/;
 
 /**
  */
 BEEDLLAPI
 int dldp_pCopy(dldp_p* dst, const dldp_p* src)
-       /*@modifies dst */;
+       /*@modifies dst @*/;
 
 /*
  * Functions for generating keys
@@ -87,19 +88,19 @@ int dldp_pCopy(dldp_p* dst, const dldp_p* src)
  */
 BEEDLLAPI /*@unused@*/
 int dldp_pPrivate(const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x)
-       /*@modifies rgc, x */;
+       /*@modifies rgc, x @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
-int dldp_pPublic (const dldp_p* dp, const mp32number* x, mp32number* y)
-       /*@modifies y */;
+int dldp_pPublic(const dldp_p* dp, const mp32number* x, mp32number* y)
+       /*@modifies y @*/;
 
 /**
  */
 BEEDLLAPI
-int dldp_pPair   (const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x, mp32number* y)
-       /*@modifies rgc, x, y */;
+int dldp_pPair(const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x, mp32number* y)
+       /*@modifies rgc, x, y @*/;
 
 /*
  * Function for comparing domain parameters
@@ -109,7 +110,7 @@ int dldp_pPair   (const dldp_p* dp, randomGeneratorContext* rgc, mp32number* x,
 /**
  */
 BEEDLLAPI
-int  dldp_pEqual  (const dldp_p* a, const dldp_p* b)
+int  dldp_pEqual(const dldp_p* a, const dldp_p* b)
        /*@*/;
 
 /*
@@ -120,25 +121,25 @@ int  dldp_pEqual  (const dldp_p* a, const dldp_p* b)
 /**
  */
 BEEDLLAPI
-int dldp_pgoqMake     (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, uint32 qsize, int cofactor)
-       /*@modifies dp, rgc */;
+int dldp_pgoqMake(dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, uint32 qsize, int cofactor)
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
-int dldp_pgoqMakeSafe (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
-       /*@modifies dp, rgc */;
+int dldp_pgoqMakeSafe(dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int dldp_pgoqGenerator(dldp_p* dp, randomGeneratorContext* rgc)
-       /*@modifies dp, rgc */;
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI
-int  dldp_pgoqValidate (const dldp_p*, randomGeneratorContext* rgc, int cofactor)
+int  dldp_pgoqValidate(const dldp_p*, randomGeneratorContext* rgc, int cofactor)
        /*@modifies rgc @*/;
 
 /*
@@ -149,25 +150,25 @@ int  dldp_pgoqValidate (const dldp_p*, randomGeneratorContext* rgc, int cofactor
 /**
  */
 BEEDLLAPI
-int dldp_pgonMake     (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, uint32 qsize)
-       /*@modifies dp, rgc */;
+int dldp_pgonMake(dldp_p* dp, randomGeneratorContext* rgc, uint32 psize, uint32 qsize)
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
-int dldp_pgonMakeSafe (dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
-       /*@modifies dp, rgc */;
+int dldp_pgonMakeSafe(dldp_p* dp, randomGeneratorContext* rgc, uint32 psize)
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int dldp_pgonGenerator(dldp_p* dp, randomGeneratorContext* rgc)
-       /*@modifies dp, rgc */;
+       /*@modifies dp->p, dp->q, dp->r, dp->g, dp->n, rgc @*/;
 
 /**
  */
 BEEDLLAPI
-int  dldp_pgonValidate (const dldp_p* dp, randomGeneratorContext* rgc)
+int  dldp_pgonValidate(const dldp_p* dp, randomGeneratorContext* rgc)
        /*@modifies rgc @*/;
 
 #ifdef __cplusplus

diff --git a/beecrypt/dlkp.c b/beecrypt/dlkp.c
index 24aafdb..3229ae0 100644 (file)
--- a/beecrypt/dlkp.c
+++ b/beecrypt/dlkp.c
@@ -56,12 +56,15 @@ int dlkp_pInit(dlkp_p* kp)
 
 int dlkp_pFree(dlkp_p* kp)
 {
+       /*@-usereleased -compdef @*/ /* kp->param.{p,q,n}.modl is OK */
        if (dldp_pFree(&kp->param) < 0)
+               return -1;
 
        mp32nfree(&kp->y);
        mp32nfree(&kp->x);
 
        return 0;
+       /*@=usereleased =compdef @*/
 }
 
 int dlkp_pCopy(dlkp_p* dst, const dlkp_p* src)

diff --git a/beecrypt/dlpk.c b/beecrypt/dlpk.c
index 339297e..78b64bd 100644 (file)
--- a/beecrypt/dlpk.c
+++ b/beecrypt/dlpk.c
@@ -42,12 +42,14 @@ int dlpk_pInit(dlpk_p* pk)
 
 int dlpk_pFree(dlpk_p* pk)
 {
+       /*@-usereleased -compdef @*/ /* pk->param.{p,q,n}.modl is OK */
        if (dldp_pFree(&pk->param) < 0)
                return -1;
 
        mp32nfree(&pk->y);
 
        return 0;
+       /*@=usereleased =compdef @*/
 }
 
 int dlpk_pCopy(dlpk_p* dst, const dlpk_p* src)

diff --git a/beecrypt/endianness.h b/beecrypt/endianness.h
index 6a89f53..22c1c28 100644 (file)
--- a/beecrypt/endianness.h
+++ b/beecrypt/endianness.h
@@ -254,12 +254,14 @@ int decodeChars(/*@out@*/ javachar* c, const byte* data, int count)
  */
 BEEDLLAPI /*@unused@*/
 int writeByte(javabyte b, FILE* ofp)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int writeShort(javashort s, FILE* ofp)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 
 /**
@@ -267,6 +269,7 @@ int writeShort(javashort s, FILE* ofp)
 /*@-exportlocal@*/
 BEEDLLAPI
 int writeInt(javaint i, FILE* ofp)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 /*@=exportlocal@*/
 
@@ -274,6 +277,7 @@ int writeInt(javaint i, FILE* ofp)
  */
 BEEDLLAPI /*@unused@*/
 int writeLong(javalong l, FILE* ofp)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 
 /**
@@ -281,6 +285,7 @@ int writeLong(javalong l, FILE* ofp)
 /*@-exportlocal@*/
 BEEDLLAPI
 int writeChar(javachar c, FILE* ofp)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 /*@=exportlocal@*/
 
@@ -288,54 +293,63 @@ int writeChar(javachar c, FILE* ofp)
  */
 BEEDLLAPI /*@unused@*/
 int writeInts(const javaint* i, FILE* ofp, int count)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int writeChars(const javachar* c, FILE* ofp, int count)
+       /*@globals fileSystem @*/
        /*@modifies ofp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readByte(/*@out@*/ javabyte* b, FILE* ifp)
+       /*@globals fileSystem @*/
        /*@modifies b, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readShort(/*@out@*/ javashort* s, FILE* ifp)
+       /*@globals fileSystem @*/
        /*@modifies s, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readInt(/*@out@*/ javaint* i, FILE* ifp)
+       /*@globals fileSystem @*/
        /*@modifies i, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readLong(/*@out@*/ javalong* l, FILE* ifp)
+       /*@globals fileSystem @*/
        /*@modifies l, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readChar(/*@out@*/ javachar* c, FILE* ifp)
+       /*@globals fileSystem @*/
        /*@modifies c, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readInts(/*@out@*/ javaint* i, FILE* ifp, int count)
+       /*@globals fileSystem @*/
        /*@modifies i, ifp, fileSystem */;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 int readChars(/*@out@*/ javachar* c, FILE* ifp, int count)
+       /*@globals fileSystem @*/
        /*@modifies c, ifp, fileSystem */;
 
 #ifdef __cplusplus

diff --git a/beecrypt/entropy.c b/beecrypt/entropy.c
index eb61720..87df1a6 100644 (file)
--- a/beecrypt/entropy.c
+++ b/beecrypt/entropy.c
@@ -843,6 +843,7 @@ static pthread_mutex_t dev_tty_lock = PTHREAD_MUTEX_INITIALIZER;
  * @return
  */
 static int statdevice(const char *device)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/
 {
        struct stat s;
@@ -868,6 +869,7 @@ static int statdevice(const char *device)
  * @return
  */
 static int opendevice(const char *device)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/
 {
        register int fd;
@@ -891,8 +893,11 @@ static int opendevice(const char *device)
  * @param size
  * @return
  */
+/*@-globuse@*/ /* aio_foo annotations aren't correct */
 static int entropy_randombits(int fd, int timeout, uint32* data, int size)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/
+/*@=globuse@*/
 {
        register byte* bytedata = (byte*) data;
        register int   bytesize = (((unsigned)size) << 2);
@@ -919,7 +924,9 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
        while (bytesize)
        {
                #if ENABLE_AIO
+               /*@-mustfree@*/ /* my_aiocb.aio_buf is OK */
                my_aiocb.aio_buf = bytedata;
+               /*@=mustfree@*/
                my_aiocb.aio_nbytes = bytesize;
 
                /*@-moduncon@*/
@@ -1017,6 +1024,7 @@ static int entropy_randombits(int fd, int timeout, uint32* data, int size)
  * @return
  */
 static int entropy_ttybits(int fd, uint32* data, int size)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/
 {
        uint32 randombits = ((uint32)size) << 5;
@@ -1367,6 +1375,7 @@ dev_dsp_end:
 
 #if HAVE_DEV_RANDOM
 int entropy_dev_random(uint32* data, int size)
+       /*@globals dev_random_fd @*/
        /*@modifies dev_random_fd @*/
 {
        const char* timeout_env = getenv("BEECRYPT_ENTROPY_RANDOM_TIMEOUT");
@@ -1410,6 +1419,7 @@ dev_random_end:
 
 #if HAVE_DEV_URANDOM
 int entropy_dev_urandom(uint32* data, int size)
+       /*@globals dev_urandom_fd @*/
        /*@modifies dev_urandom_fd @*/
 {
        const char* timeout_env = getenv("BEECRYPT_ENTROPY_URANDOM_TIMEOUT");
@@ -1453,6 +1463,7 @@ dev_urandom_end:
 
 #if HAVE_DEV_TTY
 int entropy_dev_tty(uint32* data, int size)
+       /*@globals dev_tty_fd @*/
        /*@modifies dev_tty_fd @*/
 {
        register int rc;

diff --git a/beecrypt/entropy.h b/beecrypt/entropy.h
index 1e1f2f1..fd204bc 100644 (file)
--- a/beecrypt/entropy.h
+++ b/beecrypt/entropy.h
@@ -56,35 +56,40 @@ int entropy_wincrypt(uint32* data, int size);
 /** \ingroup ES_audio_m ES_m
  */
 int entropy_dev_audio (uint32* data, int size)
-       /*@*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 #endif
 
 #if HAVE_DEV_DSP
 /** \ingroup ES_dsp_m ES_m
  */
 int entropy_dev_dsp   (uint32* data, int size)
-       /*@modifies data, internalState @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 #endif
 
 #if HAVE_DEV_RANDOM
 /** \ingroup ES_random_m ES_m
  */
 int entropy_dev_random(uint32* data, int size)
-       /*@modifies data, internalState @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 #endif
 
 #if HAVE_DEV_URANDOM
 /** \ingroup ES_urandom_m ES_m
  */
 int entropy_dev_urandom(uint32* data, int size)
-       /*@modifies data, internalState @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 #endif
 
 #if HAVE_DEV_TTY
 /** \ingroup ES_tty_m ES_m
  */
 int entropy_dev_tty   (uint32* data, int size)
-       /*@modifies data, internalState @*/;
+       /*@globals fileSystem, internalState @*/
+       /*@modifies data, fileSystem, internalState @*/;
 #endif
 #endif
 

diff --git a/beecrypt/javaglue.c b/beecrypt/javaglue.c
index 60988a3..aa408be 100644 (file)
--- a/beecrypt/javaglue.c
+++ b/beecrypt/javaglue.c
@@ -26,6 +26,7 @@
 /* For now, I'm lazy ... */
 /*@-nullpass -nullret -shiftsigned -usedef -temptrans -freshtrans @*/
 /*@-noeffectuncon -globs -globnoglobs -modunconnomods -modnomods @*/
+/*@-mustfree@*/
 
 #ifndef WORDS_BIGENDIAN
 # define WORDS_BIGENDIAN       0
@@ -741,6 +742,7 @@ void JNICALL Java_beecrypt_crypto_NativeBlockCipher_decryptCBC(JNIEnv* env, /*@u
        (*env)->ReleaseByteArrayElements(env, outputArray, output, 0);
 }
 
+/*@=mustfree@*/
 /*@=noeffectuncon =globs =globnoglobs =modunconnomods =modnomods @*/
 /*@=nullpass =nullret =shiftsigned =usedef =temptrans =freshtrans @*/
 

diff --git a/beecrypt/memchunk.c b/beecrypt/memchunk.c
index fb68c51..bc1a519 100644 (file)
--- a/beecrypt/memchunk.c
+++ b/beecrypt/memchunk.c
@@ -34,7 +34,7 @@
 # include <malloc.h>
 #endif
 
-/*@-compdef@*/ /* tmp-?data is undefined */
+/*@-compdef@*/ /* tmp->data is undefined */
 memchunk* memchunkAlloc(int size)
 {
        memchunk* tmp = (memchunk*) calloc(1, sizeof(memchunk));
@@ -42,7 +42,9 @@ memchunk* memchunkAlloc(int size)
        if (tmp)
        {
                tmp->size = size;
+               /*@-mustfree@*/ /* tmp->data is OK */
                tmp->data = (byte*) malloc(size);
+               /*@=mustfree@*/
 
                if (tmp->data == (byte*) 0)
                {

diff --git a/beecrypt/mp32.h b/beecrypt/mp32.h
index 7eb1313..2e716c5 100644 (file)
--- a/beecrypt/mp32.h
+++ b/beecrypt/mp32.h
@@ -434,12 +434,14 @@ void mp32ndivmod(/*@out@*/ uint32* result, uint32 xsize, const uint32* xdata, ui
  */
 BEEDLLAPI /*@unused@*/
 void mp32print(uint32 xsize, const uint32* xdata)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/;
 
 /**
  */
 BEEDLLAPI
 void mp32println(uint32 xsize, const uint32* xdata)
+       /*@globals fileSystem @*/
        /*@modifies fileSystem @*/;
 
 #ifdef __cplusplus

diff --git a/beecrypt/mp32barrett.c b/beecrypt/mp32barrett.c
index 37890e8..86c8982 100644 (file)
--- a/beecrypt/mp32barrett.c
+++ b/beecrypt/mp32barrett.c
@@ -46,7 +46,6 @@
 
 #include <stdio.h>
 
-/*@-nullstate@*/       /* b->mu may be null @*/
 /**
  * mp32bzero
  */
@@ -56,17 +55,17 @@ void mp32bzero(mp32barrett* b)
        b->modl = (uint32*) 0;
        b->mu = (uint32*) 0;
 }
-/*@=nullstate@*/
 
-/*@-nullstate@*/       /* b->mu may be null @*/
+/*@-nullstate@*/       /* b->modl may be null @*/
 /**
- * mp32binit
- *  allocates the data words for an mp32barrett structure
+ *  Allocates the data words for an mp32barrett structure.
  *  will allocate 2*size+1 words
  */
 void mp32binit(mp32barrett* b, uint32 size)
 {
        b->size = size;
+       if (b->modl)
+               free(b->modl);
        b->modl = (uint32*) calloc(2*size+1, sizeof(uint32));
 
        if (b->modl != (uint32*) 0)
@@ -76,7 +75,6 @@ void mp32binit(mp32barrett* b, uint32 size)
 }
 /*@=nullstate@*/
 
-/*@-nullstate@*/       /* b->mu may be null @*/
 /**
  * mp32bfree
  */
@@ -90,9 +88,8 @@ void mp32bfree(mp32barrett* b)
        }
        b->size = 0;
 }
-/*@=nullstate@*/
 
-/*@-nullstate -compdef @*/     /* b->mu may be null @*/
+/*@-nullstate -compdef @*/     /* b->modl may be null @*/
 void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
 {
        register uint32 size = copy->size;
@@ -131,7 +128,7 @@ void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
 }
 /*@=nullstate =compdef @*/
 
-/*@-nullstate -compdef @*/     /* b->mu may be null @*/
+/*@-nullstate -compdef @*/     /* b->modl may be null @*/
 /**
  * mp32bset
  */
@@ -169,7 +166,7 @@ void mp32bset(mp32barrett* b, uint32 size, const uint32 *data)
 }
 /*@=nullstate =compdef @*/
 
-/*@-nullstate -compdef @*/     /* b->mu may be null @*/
+/*@-nullstate -compdef @*/     /* b->modl may be null @*/
 void mp32bsethex(mp32barrett* b, const char* hex)
 {
        uint32 length = strlen(hex);
@@ -248,7 +245,9 @@ void mp32bmu_w(mp32barrett* b, uint32* wksp)
        *dividend = (uint32) (1 << shift);
        mp32zero(size*2, dividend+1);
        mp32ndivmod(divmod, size*2+1, dividend, size, b->modl, workspace);
+       /*@-nullpass@*/ /* b->mu may be NULL */
        mp32copy(size+1, b->mu, divmod+1);
+       /*@=nullpass@*/
        /* de-normalize */
        mp32rshift(size, b->modl, shift);
 }
@@ -338,6 +337,7 @@ void mp32bmod_w(const mp32barrett* b, const uint32* xdata, uint32* result, uint3
        register const uint32* src = xdata+b->size+1;
        register       uint32* dst = wksp +b->size+1;
 
+       /*@-nullpass@*/ /* b->mu may be NULL */
        rc = mp32setmul(sp, dst, b->mu, *(--src));
        *(--dst) = rc;
 
@@ -359,6 +359,7 @@ void mp32bmod_w(const mp32barrett* b, const uint32* xdata, uint32* result, uint3
        }
        else
                *(--dst) = 0;
+       /*@=nullpass@*/
 
        /* q3 is one word larger than b->modl */
        /* r2 is (2*size+1) words, of which we only needs the (size+1) lsw's */
@@ -574,7 +575,9 @@ void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
                /*@-nullpass@*/         /* slide may be NULL */
                mp32bslide_w(b, xsize, xdata, slide, wksp);
 
+               /*@-internalglobs -mods@*/ /* noisy */
                mp32bpowmodsld_w(b, slide, psize, pdata-1, result, wksp);
+               /*@=internalglobs =mods@*/
 
                free(slide);
                /*@=nullpass@*/
@@ -1037,7 +1040,9 @@ void mp32bnpowmodsld(const mp32barrett* b, const uint32* slide, const mp32number
        mp32nsize(y, size);
 
        /*@-nullpass@*/         /* temp may be NULL */
+       /*@-internalglobs -mods@*/ /* noisy */
        mp32bpowmodsld_w(b, slide, pow->size, pow->data, y->data, temp);
+       /*@=internalglobs =mods@*/
 
        free(temp);
        /*@=nullpass@*/

diff --git a/beecrypt/mp32barrett.h b/beecrypt/mp32barrett.h
index 0b9231e..8b8a566 100644 (file)
--- a/beecrypt/mp32barrett.h
+++ b/beecrypt/mp32barrett.h
@@ -35,7 +35,7 @@ typedef struct
 {
        uint32  size;
 /*@owned@*/ uint32* modl;      /* (size) words */
-/*@dependent@*/ uint32* mu;    /* (size+1) words */
+/*@dependent@*/ /*@null@*/ uint32* mu; /* (size+1) words */
 } mp32barrett;
 
 #ifdef __cplusplus
@@ -46,37 +46,39 @@ extern "C" {
  */
 BEEDLLAPI
 void mp32bzero(/*@out@*/ mp32barrett* b)
-       /*@modifies b @*/;
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
 BEEDLLAPI
 void mp32binit(mp32barrett* b, uint32 size)
-       /*@modifies b @*/;
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
 BEEDLLAPI
-void mp32bfree(mp32barrett* b)
-       /*@modifies b @*/;
+void mp32bfree(/*@special@*/ mp32barrett* b)
+       /*@uses b->size, b->modl @*/
+       /*@releases b->modl @*/
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
 BEEDLLAPI
 void mp32bcopy(mp32barrett* b, const mp32barrett* copy)
-       /*@modifies b @*/;
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
 BEEDLLAPI
 void mp32bset(mp32barrett* b, uint32 size, const uint32* data)
-       /*@modifies b @*/;
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
 BEEDLLAPI /*@unused@*/
 void mp32bsethex(mp32barrett* b, const char* hex)
-       /*@modifies b @*/;
+       /*@modifies b->size, b->modl, b->mu @*/;
 
 /**
  */
@@ -94,7 +96,7 @@ void mp32bneg(const mp32barrett* b, const uint32* xdata, uint32* result)
  */
 BEEDLLAPI
 void mp32bmu_w(mp32barrett* b, /*@out@*/ uint32* wksp)
-       /*@modifies b, wksp @*/;
+       /*@modifies b->size, b->modl, b->mu, wksp @*/;
 
 /**
  */
@@ -157,6 +159,7 @@ void mp32bpowmod_w(const mp32barrett* b, uint32 xsize, const uint32* xdata, uint
 /*@-exportlocal@*/
 BEEDLLAPI
 void mp32bpowmodsld_w(const mp32barrett* b, const uint32* slide, uint32 psize, const uint32* pdata, /*@out@*/ uint32* result, /*@out@*/ uint32* wksp)
+       /*@globals internalState @*/
        /*@modifies result, wksp, internalState @*/;
 /*@=exportlocal@*/
 

diff --git a/beecrypt/mp32number.c b/beecrypt/mp32number.c
index 881e030..a4c766d 100644 (file)
--- a/beecrypt/mp32number.c
+++ b/beecrypt/mp32number.c
@@ -83,6 +83,11 @@ void mp32nsize(mp32number* n, uint32 size)
 void mp32ninit(mp32number* n, uint32 size, const uint32* data)
 {
        n->size = size;
+       if (n->data)
+       {
+               free(n->data);
+               n->data = (uint32*) 0;
+       }
        n->data = (uint32*) malloc(size * sizeof(uint32));
 
        if (n->data && data)

diff --git a/beecrypt/mp32number.h b/beecrypt/mp32number.h
index 4998935..f3fdae4 100644 (file)
--- a/beecrypt/mp32number.h
+++ b/beecrypt/mp32number.h
@@ -37,7 +37,7 @@
 typedef struct
 {
        uint32  size;
-/*@only@*/ uint32* data;
+/*@owned@*/ uint32* data;
 } mp32number;
 
 #ifdef __cplusplus

diff --git a/beecrypt/rsakp.c b/beecrypt/rsakp.c
index 717fec6..89e55fa 100644 (file)
--- a/beecrypt/rsakp.c
+++ b/beecrypt/rsakp.c
@@ -172,6 +172,7 @@ int rsakpInit(rsakp* kp)
 
 int rsakpFree(rsakp* kp)
 {
+       /*@-usereleased -compdef @*/ /* kp->param.{n,p,q}.modl is OK */
        mp32bfree(&kp->n);
        mp32nfree(&kp->e);
        mp32nfree(&kp->d);
@@ -182,6 +183,7 @@ int rsakpFree(rsakp* kp)
        mp32nfree(&kp->c);
 
        return 0;
+       /*@=usereleased =compdef @*/
 }
 
 int rsakpCopy(rsakp* dst, const rsakp* src)

diff --git a/beecrypt/rsapk.c b/beecrypt/rsapk.c
index 8d4dd07..4dcfbe1 100644 (file)
--- a/beecrypt/rsapk.c
+++ b/beecrypt/rsapk.c
@@ -48,10 +48,12 @@ int rsapkInit(rsapk* pk)
 
 int rsapkFree(rsapk* pk)
 {
+       /*@-usereleased -compdef @*/ /* pk->n.modl is OK */
        mp32bfree(&pk->n);
        mp32nfree(&pk->e);
 
        return 0;
+       /*@=usereleased =compdef @*/
 }
 
 int rsapkCopy(rsapk* dst, const rsapk* src)

diff --git a/beecrypt/sha256.c b/beecrypt/sha256.c
index ddac5d6..c40443a 100644 (file)
--- a/beecrypt/sha256.c
+++ b/beecrypt/sha256.c
@@ -208,7 +208,8 @@ int sha256Update(register sha256Param *p, const byte *data, int size)
 /**
  */
 static void sha256Finish(register sha256Param *p)
-       /*@modifies p @*/
+       /*@globals internalState @*/
+       /*@modifies p, internalState @*/
 {
        register byte *ptr = ((byte *) p->data) + p->offset++;
 

diff --git a/beecrypt/sha256.h b/beecrypt/sha256.h
index 637ba33..8d49b27 100644 (file)
--- a/beecrypt/sha256.h
+++ b/beecrypt/sha256.h
@@ -53,6 +53,7 @@ extern "C" {
 /*@-exportlocal@*/
 BEEDLLAPI
 void sha256Process(sha256Param* p)
+       /*@globals internalState @*/
        /*@modifies p, internalState @*/;
 /*@=exportlocal@*/
 
@@ -66,13 +67,15 @@ int  sha256Reset  (sha256Param* p)
  */
 BEEDLLAPI
 int  sha256Update (sha256Param* p, const byte* data, int size)
-       /*@modifies p @*/;
+       /*@globals internalState @*/
+       /*@modifies p, internalState @*/;
 
 /** \ingroup HASH_sha256_m
  */
 BEEDLLAPI
 int  sha256Digest (sha256Param* p, /*@out@*/ uint32* data)
-       /*@modifies p, data @*/;
+       /*@globals internalState @*/
+       /*@modifies p, data, internalState @*/;
 
 #ifdef __cplusplus
 }

diff --git a/beecrypt/tests/beetest.c b/beecrypt/tests/beetest.c
index b89e595..3d69ea6 100644 (file)
--- a/beecrypt/tests/beetest.c
+++ b/beecrypt/tests/beetest.c
@@ -71,9 +71,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
 
        memset(&rngc, 0, sizeof(randomGeneratorContext));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                register int rc;
 
@@ -90,7 +90,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
                free(temp);
                /*@=nullpass =nullptrarith @*/
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver@*/
 
                return rc;
        }
@@ -123,9 +125,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
 
        memset(&rngc, 0, sizeof(randomGeneratorContext));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                mp32number digest, r, s;
 
@@ -147,7 +149,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
                mp32nfree(&r);
                mp32nfree(&s);
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver@*/
        }
        return rc;
 }
@@ -161,9 +165,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
 
        memset(&rngc, 0, sizeof(randomGeneratorContext));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                mp32number digest, r, s;
 
@@ -185,7 +189,9 @@ static const char* elg_n = "8df2a494492276aa3d25759bb06869cbeac0d83afb8d0cf7cbb8
                mp32nfree(&r);
                mp32nfree(&s);
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver@*/
        }
        return rc;
 }
@@ -249,7 +255,8 @@ static int testVectorDHAES(const dlkp_p* keypair)
 #endif
 
 /*@unused@*/ static int testVectorRSA(void)
-       /*@*/
+       /*@globals fileSystem @*/
+       /*@modifies fileSystem @*/
 {
        int rc = 0;
 
@@ -257,9 +264,9 @@ static int testVectorDHAES(const dlkp_p* keypair)
 
        memset(&rngc, 0, sizeof(randomGeneratorContext));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                rsakp kp;
                mp32number digest, s;
@@ -285,7 +292,9 @@ static int testVectorDHAES(const dlkp_p* keypair)
 
                (void) rsakpFree(&kp);
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver@*/
 
                return rc;
        }
@@ -302,9 +311,9 @@ static int testVectorDHAES(const dlkp_p* keypair)
        memset(&rc, 0, sizeof(randomGeneratorContext));
        memset(&dp, 0, sizeof(dldp_p));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                register int result;
                mp32number gq;
@@ -320,7 +329,9 @@ static int testVectorDHAES(const dlkp_p* keypair)
                mp32nfree(&gq);
                (void) dldp_pFree(&dp);
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rc);
+               /*@=modobserver@*/
 
                return result;
        }
@@ -369,8 +380,10 @@ static int testVectorDHAES(const dlkp_p* keypair)
        memset(&param, 0, sizeof(param));
 
        (void) sha256Reset(&param);
+       /*@-internalglobs -mods @*/ /* noisy */
        (void) sha256Update(&param, (const unsigned char*) "abc", 3);
        (void) sha256Digest(&param, digest);
+       /*@=internalglobs =mods @*/
 
        return mp32eq(8, expect, digest);
 }
@@ -406,8 +419,8 @@ static void testBlockInit(/*@out@*/ uint8* block, int length)
 }
 
 static void testBlockCiphers(void)
-       /*@globals keyValue @*/
-       /*@modifies internalState @*/
+       /*@globals fileSystem, internalState, keyValue @*/
+       /*@modifies fileSystem, internalState @*/
 {
        int i, k;
 
@@ -524,7 +537,8 @@ static void testBlockCiphers(void)
 }
 
 static void testHashFunctions(void)
-       /*@modifies internalState */
+       /*@globals fileSystem, internalState */
+       /*@modifies fileSystem, internalState */
 {
        int i, j;
 
@@ -553,7 +567,9 @@ static void testHashFunctions(void)
 
                                printf("  %s:\n", tmp->name);
 
+                               /*@-nullpass -modobserver @*/
                                if (hashFunctionContextInit(&hfc, tmp) == 0)
+                               /*@=nullpass =modobserver @*/
                                {
                                        for (j = 0; j < 4; j++)
                                        {
@@ -573,17 +589,21 @@ static void testHashFunctions(void)
                                                #endif
                                        }
 
+                                       /*@-modobserver@*/
                                        (void) hashFunctionContextFree(&hfc);
+                                       /*@=modobserver@*/
                                }
 
                                mp32nfree(&digest);
                        }
                }
+               free(data);
        }
 }
 
 static void testExpMods(void)
-       /*@modifies internalState */
+       /*@globals fileSystem, internalState */
+       /*@modifies fileSystem, internalState */
 {
        /*@observer@*/ static const char* p_512 = "ffcf0a0767f18f9b659d92b9550351430737c3633dc6ae7d52445d937d8336e07a7ccdb119e9ab3e011a8f938151230e91187f84ac05c3220f335193fc5e351b";
 
@@ -607,9 +627,9 @@ static void testExpMods(void)
        mp32nzero(&y);
        mp32nzero(&tmp);
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rngc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                int i;
                #if HAVE_TIME_H
@@ -691,14 +711,17 @@ static void testExpMods(void)
                mp32nfree(&y);
                mp32nfree(&tmp);
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rngc);
+               /*@=modobserver@*/
        }
        else
                printf("random generator setup problem\n");
 }
 
 static void testDLParams(void)
-       /*@modifies internalState */
+       /*@globals fileSystem, internalState */
+       /*@modifies fileSystem, internalState */
 {
        randomGeneratorContext rc;
        dldp_p dp;
@@ -706,9 +729,9 @@ static void testDLParams(void)
        memset(&rc, 0, sizeof(randomGeneratorContext));
        memset(&dp, 0, sizeof(dldp_p));
 
-       /*@-nullpass@*/
+       /*@-nullpass -modobserver @*/
        if (randomGeneratorContextInit(&rc, randomGeneratorDefault()) == 0)
-       /*@=nullpass@*/
+       /*@=nullpass =modobserver @*/
        {
                #if HAVE_TIME_H
                double ttime;
@@ -733,6 +756,8 @@ static void testDLParams(void)
                #if HAVE_TIME_H
                tstart = clock();
                #endif
+
+               /*@-usereleased -compdef @*/ /* annotate dldp_pgonMake correctly */
                (void) dldp_pgonMake(&dp, &rc, 768 >> 5, 512 >> 5);
                #if HAVE_TIME_H
                tstop = clock();
@@ -744,8 +769,11 @@ static void testDLParams(void)
                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);
+               /*@=usereleased =compdef @*/
 
+               /*@-modobserver@*/
                (void) randomGeneratorContextFree(&rc);
+               /*@=modobserver@*/
        }
 }
 
@@ -822,6 +850,8 @@ int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
 }
 #else
 int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
+       /*@globals fileSystem, internalState @*/
+       /*@modifies fileSystem, internalState @*/
 {
        int i, j;