]>
Commit | Line | Data |
---|---|---|
345671f3 | 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; @*/ | |
6 | ||
ccf415d0 | 7 | // div_t Structure type returned by div() function. |
8 | // ldiv_t | |
9 | // Structure type returned by ldiv() function. | |
345671f3 | 10 | |
11 | ||
12 | long a64l(const char *s) ; | |
13 | ||
14 | /*@exits@*/ void abort (void) /*@*/ ; | |
15 | extern int abs (int n) /*@*/ ; | |
16 | int atexit(void (*func)(void)); | |
17 | ||
18 | extern double atof (char *s) /*@*/ ; | |
19 | extern int atoi (char *s) /*@*/ ; | |
20 | extern long int atol (char *s) /*@*/ ; | |
21 | ||
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) @*/ | |
25 | ; | |
26 | extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/ | |
27 | /*@ensures MaxSet(result) == (nobj - 1); @*/ ; | |
28 | ||
86d93ed3 | 29 | /* |
30 | This is defined in ansi.h | |
31 | We include it here for reference | |
32 | ||
33 | drl 1/4/2002 | |
34 | */ | |
35 | ||
4aadc959 | 36 | /*@-redef@*/ |
345671f3 | 37 | typedef /*@concrete@*/ struct |
38 | { | |
39 | int quot; | |
40 | int rem; | |
41 | } div_t ; | |
4aadc959 | 42 | /*@=redef@*/ |
43 | ||
345671f3 | 44 | |
86d93ed3 | 45 | |
345671f3 | 46 | extern div_t div (int num, int denom) /*@*/ ; |
47 | ||
48 | double drand48 (void) /*@modifies internalState@*/ ; | |
49 | ||
50 | ||
51 | char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign) | |
52 | ; | |
53 | ||
54 | char *fcvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/int *sign); | |
55 | ||
56 | char *gcvt(double value, int ndigit, char *buf) | |
57 | /*@requires maxSet(buf) >= ndigit @*/ | |
58 | ; | |
59 | ||
60 | extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ; | |
61 | ||
62 | extern int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep) | |
63 | /*@modifies optionp, valuep @*/ ; | |
64 | ||
65 | extern int grantpt(int fildes) | |
66 | /*@modifies fileSystem, errno @*/ | |
67 | ; | |
68 | char *initstate(unsigned int seed, char *state, size_t size) | |
86d93ed3 | 69 | /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/ |
345671f3 | 70 | ; |
86d93ed3 | 71 | |
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 */ | |
4aadc959 | 74 | /*@-fixedformalarray@*/ |
345671f3 | 75 | long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ; |
4aadc959 | 76 | |
345671f3 | 77 | char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ; |
78 | extern long int labs (long int n) /*@*/ ; | |
79 | ||
4aadc959 | 80 | /*@-fixedformalarray@*/ |
345671f3 | 81 | extern void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ; |
82 | ||
86d93ed3 | 83 | /*@=fixedformalarray@*/ |
4aadc959 | 84 | |
86d93ed3 | 85 | /* |
86 | This is already defined in ansi.h | |
87 | We include it here for reference but | |
88 | comment it out to avoid a warning | |
89 | drl 1/4/2002 | |
90 | */ | |
4aadc959 | 91 | |
92 | /*@-redef@*/ | |
345671f3 | 93 | typedef /*@concrete@*/ struct |
94 | { | |
95 | long int quot; | |
96 | long int rem; | |
97 | } ldiv_t ; | |
4aadc959 | 98 | /*@=redef@*/ |
345671f3 | 99 | |
100 | extern ldiv_t ldiv (long num, long denom) /*@*/ ; | |
101 | ||
102 | long int lrand48 (void) /*@modifies internalState@*/ ; | |
103 | ||
104 | ||
6c9a3167 | 105 | extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/ |
345671f3 | 106 | /*drl 09-20-001 added errno*/ |
107 | /*@ensures MaxSet(result) == (size - 1); @*/ ; | |
108 | ||
109 | extern int mblen (char *s, size_t n) | |
6c9a3167 | 110 | /*@modifies errno@*/ |
345671f3 | 111 | /*@requires maxRead(s) >= (n - 1) @*/ |
112 | /*drl 09-20-001 added errno*/ ; | |
113 | ||
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*/ ; | |
117 | ||
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*/; | |
120 | ||
121 | ||
122 | extern char *mktemp(char *template) /*@modifies template @*/ | |
123 | /*drl added 09-20-001*/ /*warn use mkstemp */ | |
124 | ; | |
125 | ||
126 | int mkstemp(char *template) | |
127 | /*@modifies template, fileSystem @*/ | |
128 | ||
129 | /*drl added 09-20-001*/ | |
130 | ; | |
131 | ||
132 | long int mrand48 (void) /*@modifies internalState@*/ ; | |
133 | ||
86d93ed3 | 134 | |
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 */ | |
4aadc959 | 137 | /*@-fixedformalarray@*/ |
345671f3 | 138 | long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/ |
139 | ||
140 | /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/ | |
141 | ; | |
86d93ed3 | 142 | /*@=fixedformalarray@*/ |
345671f3 | 143 | |
4aadc959 | 144 | extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ; |
345671f3 | 145 | |
146 | extern int | |
147 | putenv (/*@kept@*/ const char *string) | |
148 | /*@globals environ@*/ | |
149 | /*@modifies *environ, errno@*/ | |
150 | /*drl 09-20-01 added kept */ | |
151 | ; | |
152 | ||
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@*/ ; | |
157 | ||
158 | ||
159 | ||
160 | /*@constant int RAND_MAX; @*/ | |
161 | extern int rand (void) /*@modifies internalState@*/ ; | |
162 | ||
163 | extern int rand_r(unsigned int *seed) /*@modifies seed@*/ /*drl 09-20-01 added*/ | |
164 | ; | |
165 | ||
166 | ||
167 | long random(void) /*@modifies internalState@*/ ; | |
168 | ||
169 | extern /*@null@*/ /*@only@*/ void * | |
170 | realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/; | |
171 | ||
172 | extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name) | |
4aadc959 | 173 | // *@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/ |
345671f3 | 174 | ; |
175 | ||
86d93ed3 | 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@*/ | |
345671f3 | 179 | unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/ |
180 | /*@requires maxRead(seed16v) >= 2 @*/ | |
181 | ; | |
86d93ed3 | 182 | /*@=fixedformalarray@*/ |
345671f3 | 183 | |
345671f3 | 184 | void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/ |
185 | /*@modifies internalState, errno@*/ | |
186 | ; | |
187 | ||
188 | /*@only@*/ char *setstate(/*@kept@*/ const char *state) /*@modifies internalState, errno@*/ ; | |
189 | ||
190 | extern void srand (unsigned int seed) /*@modifies internalState@*/ ; | |
191 | ||
192 | extern void srand48 (long int seedval) /*@modifies internalState@*/ ; | |
193 | ||
ccf415d0 | 194 | extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */ |
345671f3 | 195 | ; |
196 | extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp) | |
197 | /*@modifies *endp, errno@*/ ; | |
198 | ||
199 | extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) | |
200 | /*@modifies *endp, errno@*/ ; | |
201 | ||
202 | extern unsigned long | |
203 | strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base) | |
204 | /*@modifies *endp, errno@*/ ; | |
205 | ||
206 | ||
207 | extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/ | |
208 | /*drl 09-20-01 added errno */ | |
209 | ; | |
210 | ||
211 | extern int ttyslot(void) /*@*/ | |
212 | /*drl added 09-20-001 */ /*legacy*/ ; | |
213 | ||
214 | ||
215 | extern int unlockpt(int fildes) | |
6c9a3167 | 216 | /*@modifies fileSystem, internalState @*/ |
345671f3 | 217 | /*drl added 09-20-001 */ |
218 | ; | |
219 | ||
6c9a3167 | 220 | extern void *valloc(size_t size)/*@modifies errno@*/ |
345671f3 | 221 | /*drl 09-20-001 */ |
ccf415d0 | 222 | /*@ensures MaxSet(result) == (size - 1); @*/ |
345671f3 | 223 | /*legacy*/ ; |
224 | ||
225 | extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) | |
226 | /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ; | |
227 | ||
228 | extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) | |
229 | /*@modifies *s@*/ ; | |
230 |