1 /*@constant int EXIT_FAILURE; @*/
2 /*@constant int EXIT_SUCCESS; @*/
3 /*@constant null anytype NULL = 0;@*/
4 /*@constant int RAND_MAX; @*/
5 /*@constant size_t MB_CUR_MAX; @*/
7 // div_t Structure type returned by div() function.
9 // Structure type returned by ldiv() function.
12 long a64l(const char *s) ;
14 /*@exits@*/ void abort (void) /*@*/ ;
15 extern int abs (int n) /*@*/ ;
16 int atexit(void (*func)(void));
18 extern double atof (char *s) /*@*/ ;
19 extern int atoi (char *s) /*@*/ ;
20 extern long int atol (char *s) /*@*/ ;
22 void * bsearch (const void *key, const void *base, size_t nel, size_t size,
23 int (*compar)(const void *, const void *)) /*@*/
24 /*@requires maxSet(base) >= (nel - 1) @*/
26 extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
27 /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
29 typedef /*@concrete@*/ struct
35 extern div_t div (int num, int denom) /*@*/ ;
37 double drand48 (void) /*@modifies internalState@*/ ;
40 char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign)
43 char *fcvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/int *sign);
45 char *gcvt(double value, int ndigit, char *buf)
46 /*@requires maxSet(buf) >= ndigit @*/
49 extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ;
51 extern int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep)
52 /*@modifies optionp, valuep @*/ ;
54 extern int grantpt(int fildes)
55 /*@modifies fileSystem, errno @*/
57 char *initstate(unsigned int seed, char *state, size_t size)
58 /*@modifies interalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
60 long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ;
62 char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ;
63 extern long int labs (long int n) /*@*/ ;
65 extern void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ;
67 typedef /*@concrete@*/ struct
73 extern ldiv_t ldiv (long num, long denom) /*@*/ ;
75 long int lrand48 (void) /*@modifies internalState@*/ ;
78 extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifes errno@*/
79 /*drl 09-20-001 added errno*/
80 /*@ensures MaxSet(result) == (size - 1); @*/ ;
82 extern int mblen (char *s, size_t n)
84 /*@requires maxRead(s) >= (n - 1) @*/
85 /*drl 09-20-001 added errno*/ ;
87 size_t mbstowcs(/*@null@*/ /*@out@*/ wchar_t *pwcs, const char *s, size_t n)
88 /*@requires maxSet(pwcs) >= (n - 1) @*/
89 /*drl 09-20-001 added errno*/ ;
91 extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
92 /*@modifies *pwc, errno@*/ /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/;
95 extern char *mktemp(char *template) /*@modifies template @*/
96 /*drl added 09-20-001*/ /*warn use mkstemp */
99 int mkstemp(char *template)
100 /*@modifies template, fileSystem @*/
102 /*drl added 09-20-001*/
105 long int mrand48 (void) /*@modifies internalState@*/ ;
107 long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/
109 /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/
112 extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*@drl added 09-20-01@*/ ;
116 putenv (/*@kept@*/ const char *string)
117 /*@globals environ@*/
118 /*@modifies *environ, errno@*/
119 /*drl 09-20-01 added kept */
122 extern void qsort (void *base, size_t nel, size_t size,
123 int (*compar)(const void *, const void *) )
124 /*@requires maxRead(base) >= (nel - 1) @*/
125 /*@modifies *base, errno@*/ ;
129 /*@constant int RAND_MAX; @*/
130 extern int rand (void) /*@modifies internalState@*/ ;
132 extern int rand_r(unsigned int *seed) /*@modifies seed@*/ /*drl 09-20-01 added*/
136 long random(void) /*@modifies internalState@*/ ;
138 extern /*@null@*/ /*@only@*/ void *
139 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;
141 extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name)
142 // /*@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/
145 unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
146 /*@requires maxRead(seed16v) >= 2 @*/
150 void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/
151 /*@modifies internalState, errno@*/
154 /*@only@*/ char *setstate(/*@kept@*/ const char *state) /*@modifies internalState, errno@*/ ;
156 extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
158 extern void srand48 (long int seedval) /*@modifies internalState@*/ ;
160 extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */
162 extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp)
163 /*@modifies *endp, errno@*/ ;
165 extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
166 /*@modifies *endp, errno@*/ ;
169 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
170 /*@modifies *endp, errno@*/ ;
173 extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/
174 /*drl 09-20-01 added errno */
177 extern int ttyslot(void) /*@*/
178 /*drl added 09-20-001 */ /*legacy*/ ;
181 extern int unlockpt(int fildes)
182 /*@modifes fileSystem, internalState @*/
183 /*drl added 09-20-001 */
186 extern void *valloc(size_t size)/*@modifes errno@*/
188 /*@ensures MaxSet(result) == (size - 1); @*/
191 extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
192 /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ;
194 extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)