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); @*/ ;
30 This is defined in ansi.h
31 We include it here for reference
37 typedef /*@concrete@*/ struct
46 extern div_t div (int num, int denom) /*@*/ ;
48 double drand48 (void) /*@modifies internalState@*/ ;
51 char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign)
54 char *fcvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/int *sign);
56 char *gcvt(double value, int ndigit, char *buf)
57 /*@requires maxSet(buf) >= ndigit @*/
60 extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ;
62 extern int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep)
63 /*@modifies optionp, valuep @*/ ;
65 extern int grantpt(int fildes)
66 /*@modifies fileSystem, errno @*/
68 char *initstate(unsigned int seed, char *state, size_t size)
69 /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
72 /*drl 1/4/2002: specifying the array sizes is meaningless but we include
73 them to be consistent with the unix specification at opengroup.org */
74 /*@-fixedformalarray@*/
75 long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ;
77 char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ;
78 extern long int labs (long int n) /*@*/ ;
80 /*@-fixedformalarray@*/
81 extern void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ;
83 /*@=fixedformalarray@*/
86 This is already defined in ansi.h
87 We include it here for reference but
88 comment it out to avoid a warning
93 typedef /*@concrete@*/ struct
100 extern ldiv_t ldiv (long num, long denom) /*@*/ ;
102 long int lrand48 (void) /*@modifies internalState@*/ ;
105 extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/
106 /*drl 09-20-001 added errno*/
107 /*@ensures MaxSet(result) == (size - 1); @*/ ;
109 extern int mblen (char *s, size_t n)
111 /*@requires maxRead(s) >= (n - 1) @*/
112 /*drl 09-20-001 added errno*/ ;
114 size_t mbstowcs(/*@null@*/ /*@out@*/ wchar_t *pwcs, const char *s, size_t n)
115 /*@requires maxSet(pwcs) >= (n - 1) @*/
116 /*drl 09-20-001 added errno*/ ;
118 extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
119 /*@modifies *pwc, errno@*/ /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/;
122 extern char *mktemp(char *template) /*@modifies template @*/
123 /*drl added 09-20-001*/ /*warn use mkstemp */
126 int mkstemp(char *template)
127 /*@modifies template, fileSystem @*/
129 /*drl added 09-20-001*/
132 long int mrand48 (void) /*@modifies internalState@*/ ;
135 /*drl 1/4/2002: specifying the array size is meaningless but we include
136 it to be consistent with the unix specification at opengroup.org */
137 /*@-fixedformalarray@*/
138 long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/
140 /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/
142 /*@=fixedformalarray@*/
144 extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ;
147 putenv (/*@kept@*/ const char *string)
148 /*@globals environ@*/
149 /*@modifies *environ, errno@*/
150 /*drl 09-20-01 added kept */
153 extern void qsort (void *base, size_t nel, size_t size,
154 int (*compar)(const void *, const void *) )
155 /*@requires maxRead(base) >= (nel - 1) @*/
156 /*@modifies *base, errno@*/ ;
160 /*@constant int RAND_MAX; @*/
161 extern int rand (void) /*@modifies internalState@*/ ;
163 extern int rand_r(unsigned int *seed) /*@modifies seed@*/ /*drl 09-20-01 added*/
167 long random(void) /*@modifies internalState@*/ ;
169 extern /*@null@*/ /*@only@*/ void *
170 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;
172 extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name)
173 // *@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/
176 /*drl 1/4/2002: specifying the array sizes is meaningless but we include
177 them to be consistent with the unix specification at opengroup.org */
178 /*@-fixedformalarray@*/
179 unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
180 /*@requires maxRead(seed16v) >= 2 @*/
182 /*@=fixedformalarray@*/
184 void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/
185 /*@modifies internalState, errno@*/
188 /*@only@*/ char *setstate(/*@kept@*/ const char *state) /*@modifies internalState, errno@*/ ;
190 extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
192 extern void srand48 (long int seedval) /*@modifies internalState@*/ ;
194 extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */
196 extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp)
197 /*@modifies *endp, errno@*/ ;
199 extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
200 /*@modifies *endp, errno@*/ ;
203 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
204 /*@modifies *endp, errno@*/ ;
207 extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/
208 /*drl 09-20-01 added errno */
211 extern int ttyslot(void) /*@*/
212 /*drl added 09-20-001 */ /*legacy*/ ;
215 extern int unlockpt(int fildes)
216 /*@modifies fileSystem, internalState @*/
217 /*drl added 09-20-001 */
220 extern void *valloc(size_t size)/*@modifies errno@*/
222 /*@ensures MaxSet(result) == (size - 1); @*/
225 extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
226 /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ;
228 extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)