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