]>
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 | ||
4aadc959 | 29 | /*@-redef@*/ |
345671f3 | 30 | typedef /*@concrete@*/ struct |
31 | { | |
32 | int quot; | |
33 | int rem; | |
34 | } div_t ; | |
4aadc959 | 35 | /*@=redef@*/ |
36 | ||
345671f3 | 37 | |
38 | extern div_t div (int num, int denom) /*@*/ ; | |
39 | ||
40 | double drand48 (void) /*@modifies internalState@*/ ; | |
41 | ||
42 | ||
43 | char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign) | |
44 | ; | |
45 | ||
46 | char *fcvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/int *sign); | |
47 | ||
48 | char *gcvt(double value, int ndigit, char *buf) | |
49 | /*@requires maxSet(buf) >= ndigit @*/ | |
50 | ; | |
51 | ||
52 | extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ; | |
53 | ||
54 | extern int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep) | |
55 | /*@modifies optionp, valuep @*/ ; | |
56 | ||
57 | extern int grantpt(int fildes) | |
58 | /*@modifies fileSystem, errno @*/ | |
59 | ; | |
60 | char *initstate(unsigned int seed, char *state, size_t size) | |
61 | /*@modifies interalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/ | |
62 | ; | |
4aadc959 | 63 | |
64 | /*@-fixedformalarray@*/ | |
345671f3 | 65 | long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ; |
4aadc959 | 66 | /*@=fixedformalarray@*/ |
67 | ||
345671f3 | 68 | char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ; |
69 | extern long int labs (long int n) /*@*/ ; | |
70 | ||
4aadc959 | 71 | /*@-fixedformalarray@*/ |
345671f3 | 72 | extern void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ; |
73 | ||
4aadc959 | 74 | /*@=fixedformalarray@*/ |
75 | ||
76 | /*also in ansi.h */ | |
77 | ||
78 | /*@-redef@*/ | |
345671f3 | 79 | typedef /*@concrete@*/ struct |
80 | { | |
81 | long int quot; | |
82 | long int rem; | |
83 | } ldiv_t ; | |
4aadc959 | 84 | /*@=redef@*/ |
345671f3 | 85 | |
86 | extern ldiv_t ldiv (long num, long denom) /*@*/ ; | |
87 | ||
88 | long int lrand48 (void) /*@modifies internalState@*/ ; | |
89 | ||
90 | ||
6c9a3167 | 91 | extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/ |
345671f3 | 92 | /*drl 09-20-001 added errno*/ |
93 | /*@ensures MaxSet(result) == (size - 1); @*/ ; | |
94 | ||
95 | extern int mblen (char *s, size_t n) | |
6c9a3167 | 96 | /*@modifies errno@*/ |
345671f3 | 97 | /*@requires maxRead(s) >= (n - 1) @*/ |
98 | /*drl 09-20-001 added errno*/ ; | |
99 | ||
100 | size_t mbstowcs(/*@null@*/ /*@out@*/ wchar_t *pwcs, const char *s, size_t n) | |
101 | /*@requires maxSet(pwcs) >= (n - 1) @*/ | |
102 | /*drl 09-20-001 added errno*/ ; | |
103 | ||
104 | extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) | |
105 | /*@modifies *pwc, errno@*/ /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/; | |
106 | ||
107 | ||
108 | extern char *mktemp(char *template) /*@modifies template @*/ | |
109 | /*drl added 09-20-001*/ /*warn use mkstemp */ | |
110 | ; | |
111 | ||
112 | int mkstemp(char *template) | |
113 | /*@modifies template, fileSystem @*/ | |
114 | ||
115 | /*drl added 09-20-001*/ | |
116 | ; | |
117 | ||
118 | long int mrand48 (void) /*@modifies internalState@*/ ; | |
119 | ||
4aadc959 | 120 | /*@-fixedformalarray@*/ |
345671f3 | 121 | long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/ |
122 | ||
123 | /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/ | |
124 | ; | |
4aadc959 | 125 | |
126 | /*@=fixedformalarray@*/ | |
345671f3 | 127 | |
4aadc959 | 128 | extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ; |
345671f3 | 129 | |
130 | ||
131 | extern int | |
132 | putenv (/*@kept@*/ const char *string) | |
133 | /*@globals environ@*/ | |
134 | /*@modifies *environ, errno@*/ | |
135 | /*drl 09-20-01 added kept */ | |
136 | ; | |
137 | ||
138 | extern void qsort (void *base, size_t nel, size_t size, | |
139 | int (*compar)(const void *, const void *) ) | |
140 | /*@requires maxRead(base) >= (nel - 1) @*/ | |
141 | /*@modifies *base, errno@*/ ; | |
142 | ||
143 | ||
144 | ||
145 | /*@constant int RAND_MAX; @*/ | |
146 | extern int rand (void) /*@modifies internalState@*/ ; | |
147 | ||
148 | extern int rand_r(unsigned int *seed) /*@modifies seed@*/ /*drl 09-20-01 added*/ | |
149 | ; | |
150 | ||
151 | ||
152 | long random(void) /*@modifies internalState@*/ ; | |
153 | ||
154 | extern /*@null@*/ /*@only@*/ void * | |
155 | realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/; | |
156 | ||
157 | extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name) | |
4aadc959 | 158 | // *@requires maxSet(resolved_name) >= (PATH_MAX - 1) @*/ |
345671f3 | 159 | ; |
160 | ||
4aadc959 | 161 | /*@-fixedformalarray@*/ |
345671f3 | 162 | unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/ |
163 | /*@requires maxRead(seed16v) >= 2 @*/ | |
164 | ; | |
165 | ||
4aadc959 | 166 | /*@=fixedformalarray@*/ |
345671f3 | 167 | void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/ |
168 | /*@modifies internalState, errno@*/ | |
169 | ; | |
170 | ||
171 | /*@only@*/ char *setstate(/*@kept@*/ const char *state) /*@modifies internalState, errno@*/ ; | |
172 | ||
173 | extern void srand (unsigned int seed) /*@modifies internalState@*/ ; | |
174 | ||
175 | extern void srand48 (long int seedval) /*@modifies internalState@*/ ; | |
176 | ||
ccf415d0 | 177 | extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */ |
345671f3 | 178 | ; |
179 | extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp) | |
180 | /*@modifies *endp, errno@*/ ; | |
181 | ||
182 | extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) | |
183 | /*@modifies *endp, errno@*/ ; | |
184 | ||
185 | extern unsigned long | |
186 | strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base) | |
187 | /*@modifies *endp, errno@*/ ; | |
188 | ||
189 | ||
190 | extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/ | |
191 | /*drl 09-20-01 added errno */ | |
192 | ; | |
193 | ||
194 | extern int ttyslot(void) /*@*/ | |
195 | /*drl added 09-20-001 */ /*legacy*/ ; | |
196 | ||
197 | ||
198 | extern int unlockpt(int fildes) | |
6c9a3167 | 199 | /*@modifies fileSystem, internalState @*/ |
345671f3 | 200 | /*drl added 09-20-001 */ |
201 | ; | |
202 | ||
6c9a3167 | 203 | extern void *valloc(size_t size)/*@modifies errno@*/ |
345671f3 | 204 | /*drl 09-20-001 */ |
ccf415d0 | 205 | /*@ensures MaxSet(result) == (size - 1); @*/ |
345671f3 | 206 | /*legacy*/ ; |
207 | ||
208 | extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) | |
209 | /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ; | |
210 | ||
211 | extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) | |
212 | /*@modifies *s@*/ ; | |
213 |