/*@constant int EXIT_FAILURE; @*/ /*@constant int EXIT_SUCCESS; @*/ /*@constant null anytype NULL = 0;@*/ /*@constant int RAND_MAX; @*/ /*@constant size_t MB_CUR_MAX; @*/ // div_t Structure type returned by div() function. // ldiv_t // Structure type returned by ldiv() function. long a64l(const char *s) ; /*@exits@*/ void abort (void) /*@*/ ; extern int abs (int n) /*@*/ ; int atexit(void (*func)(void)); extern double atof (char *s) /*@*/ ; extern int atoi (char *s) /*@*/ ; extern long int atol (char *s) /*@*/ ; void * bsearch (const void *key, const void *base, size_t nel, size_t size, int (*compar)(const void *, const void *)) /*@*/ /*@requires maxSet(base) >= (nel - 1) @*/ ; 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) /*@*/ ; double drand48 (void) /*@modifies internalState@*/ ; char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign) ; char *fcvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/int *sign); char *gcvt(double value, int ndigit, char *buf) /*@requires maxSet(buf) >= ndigit @*/ ; extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ; extern int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep) /*@modifies optionp, valuep @*/ ; extern int grantpt(int fildes) /*@modifies fileSystem, errno @*/ ; char *initstate(unsigned int seed, char *state, size_t size) /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/ ; /*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) /*@modifies errno@*/ /*drl 09-20-001 added errno*/ /*@ensures MaxSet(result) == (size - 1); @*/ ; extern int mblen (char *s, size_t n) /*@modifies errno@*/ /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/ ; size_t mbstowcs(/*@null@*/ /*@out@*/ wchar_t *pwcs, const char *s, size_t n) /*@requires maxSet(pwcs) >= (n - 1) @*/ /*drl 09-20-001 added errno*/ ; extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) /*@modifies *pwc, errno@*/ /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/; extern char *mktemp(char *template) /*@modifies template @*/ /*drl added 09-20-001*/ /*warn use mkstemp */ ; int mkstemp(char *template) /*@modifies template, fileSystem @*/ /*drl added 09-20-001*/ ; 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 int putenv (/*@kept@*/ const char *string) /*@globals environ@*/ /*@modifies *environ, errno@*/ /*drl 09-20-01 added kept */ ; extern void qsort (void *base, size_t nel, size_t size, int (*compar)(const void *, const void *) ) /*@requires maxRead(base) >= (nel - 1) @*/ /*@modifies *base, errno@*/ ; /*@constant int RAND_MAX; @*/ extern int rand (void) /*@modifies internalState@*/ ; extern int rand_r(unsigned int *seed) /*@modifies seed@*/ /*drl 09-20-01 added*/ ; long random(void) /*@modifies internalState@*/ ; extern /*@null@*/ /*@only@*/ void * 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) @*/ ; /*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@*/ ; /*@only@*/ char *setstate(/*@kept@*/ const char *state) /*@modifies internalState, errno@*/ ; extern void srand (unsigned int seed) /*@modifies internalState@*/ ; extern void srand48 (long int seedval) /*@modifies internalState@*/ ; extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */ ; extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp) /*@modifies *endp, errno@*/ ; extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) /*@modifies *endp, errno@*/ ; extern unsigned long strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base) /*@modifies *endp, errno@*/ ; extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/ /*drl 09-20-01 added errno */ ; extern int ttyslot(void) /*@*/ /*drl added 09-20-001 */ /*legacy*/ ; extern int unlockpt(int fildes) /*@modifies fileSystem, internalState @*/ /*drl added 09-20-001 */ ; extern void *valloc(size_t size)/*@modifies errno@*/ /*drl 09-20-001 */ /*@ensures MaxSet(result) == (size - 1); @*/ /*legacy*/ ; extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ; extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) /*@modifies *s@*/ ;