More lclint fiddles.

CVS patchset: 5070
CVS date: 2001/09/23 15:47:37
This commit is contained in:
jbj 2001-09-23 15:47:37 +00:00
parent 0f77778944
commit 039162ac61
24 changed files with 244 additions and 144 deletions

View File

@ -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

View File

@ -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

View File

@ -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);

View File

@ -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
}

View File

@ -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)
{

View File

@ -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;
}

View File

@ -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

View File

@ -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)

View File

@ -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)

View File

@ -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

View File

@ -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;

View File

@ -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

View File

@ -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 @*/

View File

@ -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)
{

View File

@ -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

View File

@ -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@*/

View File

@ -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@*/

View File

@ -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)

View File

@ -37,7 +37,7 @@
typedef struct
{
uint32 size;
/*@only@*/ uint32* data;
/*@owned@*/ uint32* data;
} mp32number;
#ifdef __cplusplus

View File

@ -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)

View File

@ -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)

View File

@ -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++;

View File

@ -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
}

View File

@ -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;