extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
/*@ensures MaxSet(result) == (nobj - 1); @*/ ;
+ /*
+ This is defined in ansi.h
+ We include it here for reference
+
+ drl 1/4/2002
+ */
+
+ /*@-redef@*/
typedef /*@concrete@*/ struct
{
int quot;
int rem;
} div_t ;
+/*@=redef@*/
+
+
extern div_t div (int num, int denom) /*@*/ ;
/*@modifies fileSystem, errno @*/
;
char *initstate(unsigned int seed, char *state, size_t size)
- /*@modifies interalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
+ /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
;
- long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ;
+ /*drl 1/4/2002: specifying the array sizes is meaningless but we include
+ them to be consistent with the unix specification at opengroup.org */
+ /*@-fixedformalarray@*/
+ long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ;
+
char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ;
extern long int labs (long int n) /*@*/ ;
+ /*@-fixedformalarray@*/
extern void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ;
+ /*@=fixedformalarray@*/
+
+ /*
+ This is already defined in ansi.h
+ We include it here for reference but
+ comment it out to avoid a warning
+ drl 1/4/2002
+ */
+
+/*@-redef@*/
typedef /*@concrete@*/ struct
{
long int quot;
long int rem;
} ldiv_t ;
+/*@=redef@*/
extern ldiv_t ldiv (long num, long denom) /*@*/ ;
long int lrand48 (void) /*@modifies internalState@*/ ;
-extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifes errno@*/
+extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/
/*drl 09-20-001 added errno*/
/*@ensures MaxSet(result) == (size - 1); @*/ ;
extern int mblen (char *s, size_t n)
- /*@modifes errno@*/
+ /*@modifies errno@*/
/*@requires maxRead(s) >= (n - 1) @*/
/*drl 09-20-001 added errno*/ ;
long int mrand48 (void) /*@modifies internalState@*/ ;
+
+ /*drl 1/4/2002: specifying the array size is meaningless but we include
+ it to be consistent with the unix specification at opengroup.org */
+ /*@-fixedformalarray@*/
long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/
/*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/
;
+ /*@=fixedformalarray@*/
- extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*@drl added 09-20-01@*/ ;
-
+ extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ;
extern int
putenv (/*@kept@*/ const char *string)
realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;
extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name)
- // /*@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/
+ // *@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/
;
+ /*drl 1/4/2002: specifying the array sizes is meaningless but we include
+ them to be consistent with the unix specification at opengroup.org */
+ /*@-fixedformalarray@*/
unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
/*@requires maxRead(seed16v) >= 2 @*/
;
-
+ /*@=fixedformalarray@*/
void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/
/*@modifies internalState, errno@*/
extern int unlockpt(int fildes)
- /*@modifes fileSystem, internalState @*/
+ /*@modifies fileSystem, internalState @*/
/*drl added 09-20-001 */
;
-extern void *valloc(size_t size)/*@modifes errno@*/
+extern void *valloc(size_t size)/*@modifies errno@*/
/*drl 09-20-001 */
/*@ensures MaxSet(result) == (size - 1); @*/
/*legacy*/ ;