]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** unix.h | |
3 | */ | |
4 | ||
5 | /*@-nextlinemacros@*/ | |
6 | ||
345671f3 | 7 | /* |
8 | ** sys/types.h | |
9 | ** | |
10 | ** evans - 2001-08-27: from http://www.opengroup.org/onlinepubs/007908799/xsh/systypes.h.html | |
11 | */ | |
12 | ||
13 | typedef /*@integraltype@*/ blkcnt_t; | |
14 | typedef /*@integraltype@*/ blksize_t; | |
8fe44445 | 15 | |
16 | /*@-redef@*/ /* These are also defined by ansi.h: */ | |
345671f3 | 17 | typedef /*@integraltype@*/ clock_t; |
345671f3 | 18 | typedef /*@integraltype@*/ dev_t; |
345671f3 | 19 | typedef /*@integraltype@*/ gid_t; |
345671f3 | 20 | typedef /*@unsignedintegraltype@*/ ino_t; |
345671f3 | 21 | typedef /*@integraltype@*/ mode_t; |
22 | typedef /*@integraltype@*/ nlink_t; | |
23 | typedef /*@integraltype@*/ off_t; | |
24 | typedef /*@integraltype@*/ pid_t; | |
8fe44445 | 25 | typedef /*@integraltype@*/ time_t; |
26 | typedef /*@integraltype@*/ uid_t; | |
27 | ||
28 | /*@=redef@*/ | |
29 | ||
30 | typedef /*@integraltype@*/ clockid_t; | |
31 | typedef /*@unsignedintegraltype@*/ fsblkcnt_t; | |
32 | typedef /*@unsignedintegraltype@*/ fsfilcnt_t; | |
33 | typedef /*@integraltype@*/ id_t; | |
34 | ||
35 | typedef /*@integraltype@*/ key_t; | |
345671f3 | 36 | typedef /*@integraltype@*/ pthread_attr_t; |
37 | typedef /*@integraltype@*/ pthread_cond_t; | |
38 | typedef /*@integraltype@*/ pthread_condattr_t; | |
39 | typedef /*@integraltype@*/ pthread_key_t; | |
40 | typedef /*@integraltype@*/ pthread_mutex_t; | |
41 | typedef /*@integraltype@*/ pthread_mutexattr_t; | |
42 | typedef /*@integraltype@*/ pthread_once_t; | |
43 | typedef /*@integraltype@*/ pthread_rwlock_t; | |
44 | typedef /*@integraltype@*/ pthread_rwlockattr_t; | |
45 | typedef /*@integraltype@*/ pthread_t; | |
46 | typedef /*@signedintegraltype@*/ suseconds_t; | |
345671f3 | 47 | typedef /*@integraltype@*/ timer_t; |
345671f3 | 48 | typedef /*@unsignedintegraltype@*/ useconds_t; |
49 | ||
885824d3 | 50 | /* |
51 | ** Extra stuff in some unixen, not in posix. | |
52 | */ | |
53 | ||
8fe44445 | 54 | extern /*@unchecked@*/ int signgam; |
885824d3 | 55 | |
8fe44445 | 56 | /*@-redef@*/ /* Defined by ansi: */ |
885824d3 | 57 | typedef /*@integraltype@*/ clockid_t; |
8fe44445 | 58 | /*@=redef@*/ |
885824d3 | 59 | |
60 | extern void bcopy (char *b1, /*@out@*/ char *b2, int length) | |
61 | /*@modifies *b2@*/ ; /* Yes, the second parameter is the out param! */ | |
62 | ||
63 | extern int /*@alt lltX_bool@*/ bcmp (char *b1, char *b2, int length) /*@*/ ; | |
64 | /* Return value is NOT like strcmp! */ | |
65 | ||
66 | extern void bzero (/*@out@*/ char *b1, int length) /*@modifies *b1@*/ ; | |
67 | extern int ffs (int i) /*@*/ ; | |
68 | extern int symlink (char *name1, char *name2) /*@modifies fileSystem@*/ ; | |
69 | ||
70 | extern int | |
71 | setvbuf_unlocked (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, | |
72 | int mode, size_t size) | |
73 | /*@modifies internalState@*/ ; | |
74 | ||
75 | extern void | |
76 | setbuffer (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, int size) | |
77 | /*@modifies internalState@*/ ; | |
78 | ||
79 | extern void setlinebuf (FILE *stream) /*@modifies internalState@*/ ; | |
80 | ||
81 | extern int strerror_r (int errnum, /*@out@*/ char *strerrbuf, int buflen) | |
82 | /*@modifies strerrbuf@*/ ; | |
83 | ||
84 | extern size_t | |
85 | fread_unlocked (/*@out@*/ void *ptr, size_t size, size_t nitems, | |
86 | FILE *stream) | |
87 | /*@modifies *stream, *ptr;@*/ ; | |
88 | ||
89 | extern size_t | |
90 | fwrite_unlocked (void *pointer, size_t size, size_t num_items, FILE *stream) | |
91 | /*@modifies *stream;@*/ ; | |
92 | ||
885824d3 | 93 | extern void /*@alt void * @*/ |
94 | memccpy (/*@returned@*/ /*@out@*/ void *s1, | |
95 | /*@unique@*/ void *s2, int c, size_t n) | |
96 | /*@modifies *s1@*/ ; | |
97 | ||
98 | extern int strcasecmp (char *s1, char *s2) /*@*/ ; | |
99 | extern int strncasecmp (char *s1, char *s2, int n) /*@*/ ; | |
1d239d69 | 100 | extern /*@null@*/ /*@only@*/ char *strdup (char *s) /*@*/ ; |
885824d3 | 101 | |
885824d3 | 102 | extern /*@null@*/ /*@dependent@*/ char * |
103 | index (/*@returned@*/ char *s, char c) /*@*/ ; | |
104 | ||
105 | extern /*@null@*/ /*@dependent@*/ char * | |
106 | rindex (/*@returned@*/ char *s, char c) /*@*/ ; | |
107 | ||
885824d3 | 108 | |
109 | extern double cbrt (double x) /*@modifies errno@*/ ; | |
110 | extern double rint (double x) /*@*/ ; | |
111 | extern double trunc (double x) /*@*/ ; | |
112 | ||
113 | /*@constant int ENOTBLK@*/ | |
114 | /*@constant int ETXTBSY@*/ | |
115 | /*@constant int EWOULDBLOCK@*/ | |
116 | /*@constant int EINPROGRESS@*/ | |
117 | /*@constant int EALREADY@*/ | |
118 | /*@constant int ENOTSOCK@*/ | |
119 | /*@constant int EDESTADDRREQ@*/ | |
120 | /*@constant int EMSGSIZE@*/ | |
121 | /*@constant int EPROTOTYPE@*/ | |
122 | /*@constant int ENOPROTOOPT@*/ | |
123 | /*@constant int EPROTONOSUPPORT@*/ | |
124 | /*@constant int ESOCKTNOSUPPORT@*/ | |
125 | /*@constant int EOPNOTSUPP@*/ | |
126 | /*@constant int EPFNOSUPPORT@*/ | |
127 | /*@constant int EAFNOSUPPORT@*/ | |
128 | /*@constant int EADDRINUSE@*/ | |
129 | /*@constant int EADDRNOTAVAIL@*/ | |
130 | /*@constant int ENETDOWN@*/ | |
131 | /*@constant int ENETUNREACH@*/ | |
132 | /*@constant int ENETRESET@*/ | |
133 | /*@constant int ECONNABORTED@*/ | |
134 | /*@constant int ECONNRESET@*/ | |
135 | /*@constant int ENOBUFS@*/ | |
136 | /*@constant int EISCONN@*/ | |
137 | /*@constant int ENOTCONN@*/ | |
138 | /*@constant int ESHUTDOWN@*/ | |
139 | /*@constant int ETOOMANYREFS@*/ | |
140 | /*@constant int ETIMEDOUT@*/ | |
141 | /*@constant int ECONNREFUSED@*/ | |
142 | /*@constant int ENAMETOOLONG@*/ | |
143 | /*@constant int EHOSTDOWN@*/ | |
144 | /*@constant int EHOSTUNREACH@*/ | |
145 | /*@constant int ENOTEMPTY@*/ | |
146 | /*@constant int EPROCLIM@*/ | |
147 | /*@constant int EUSERS@*/ | |
148 | /*@constant int EDQUOT@*/ | |
149 | /*@constant int ESTALE@*/ | |
150 | /*@constant int EREMOTE@*/ | |
151 | /*@constant int ENOMSG@*/ | |
152 | /*@constant int EIDRM@*/ | |
153 | /*@constant int EALIGN@*/ | |
154 | /*@constant int EDEADLK@*/ | |
155 | /*@constant int ENOLCK@*/ | |
156 | /*@constant int ENOSYS@*/ | |
157 | /*@constant int EACTIVE@*/ | |
158 | /*@constant int ENOACTIVE@*/ | |
159 | /*@constant int ENORESOURCES@*/ | |
160 | /*@constant int ENOSYSTEM@*/ | |
161 | /*@constant int ENODUST@*/ | |
162 | /*@constant int EDUPNOCONN@*/ | |
163 | /*@constant int EDUPNODISCONN@*/ | |
164 | /*@constant int EDUPNOTCNTD@*/ | |
165 | /*@constant int EDUPNOTIDLE@*/ | |
166 | /*@constant int EDUPNOTWAIT@*/ | |
167 | /*@constant int EDUPNOTRUN@*/ | |
168 | /*@constant int EDUPBADOPCODE@*/ | |
169 | /*@constant int EDUPINTRANSIT@*/ | |
170 | /*@constant int EDUPTOOMANYCPUS@*/ | |
171 | /*@constant int ELOOP@*/ | |
172 | ||
173 | /*@constant int LOCK_MAX@*/ | |
174 | /*@constant int FCHR_MAX@*/ | |
175 | /*@constant int USI_MAX@*/ | |
176 | /*@constant int WORD_BIT@*/ | |
177 | /*@constant int LONG_BIT@*/ | |
4aadc959 | 178 | |
86d93ed3 | 179 | /*@-incondefs@*/ /* some constant are also declared in posix.h*/ |
180 | ||
181 | /*@constant long NAME_MAX@*/ | |
182 | ||
885824d3 | 183 | /*@constant long NGROUPS_MAX@*/ |
4aadc959 | 184 | |
885824d3 | 185 | /*@constant long MAX_CANON@*/ |
186 | /*@constant int MAX_CHAR@*/ | |
187 | /*@constant long OPEN_MAX@*/ | |
188 | /*@constant int PASS_MAX@*/ | |
4aadc959 | 189 | |
885824d3 | 190 | /*@constant int PID_MAX@*/ |
191 | /*@constant int SYSPID_MAX@*/ | |
86d93ed3 | 192 | /*@constant long PIPE_BUF@*/ |
193 | /*@=incondefs@*/ | |
885824d3 | 194 | /*@constant int PIPE_MAX@*/ |
195 | /*@constant int PROC_MAX@*/ | |
196 | /*@constant int STD_BLK@*/ | |
197 | /*@constant int SYS_NMLN@*/ | |
198 | /*@constant int SYS_OPEN@*/ | |
199 | /*@constant int NZERO@*/ | |
200 | /*@constant int UID_MAX@*/ | |
201 | /*@constant long MB_LEN_MAX@*/ | |
202 | /*@constant int NL_ARGMAX@*/ | |
203 | /*@constant int NL_MSGMAX@*/ | |
204 | /*@constant int NL_NMAX@*/ | |
205 | /*@constant int NL_SETMAX@*/ | |
206 | /*@constant int NL_TEXTMAX@*/ | |
207 | /*@constant int NL_LBLMAX@*/ | |
208 | /*@constant int NL_LANGMAX @*/ | |
209 | ||
210 | /*@constant double M_E@*/ | |
211 | /*@constant double M_LOG2E@*/ | |
212 | /*@constant double M_LOG10E@*/ | |
213 | /*@constant double M_LN2@*/ | |
214 | /*@constant double M_LN10@*/ | |
215 | /*@constant double M_PI@*/ | |
216 | /*@constant double M_PI_2@*/ | |
217 | /*@constant double M_PI_4@*/ | |
218 | /*@constant double M_1_PI@*/ | |
219 | /*@constant double M_2_PI@*/ | |
220 | /*@constant double M_2_SQRTPI@*/ | |
221 | /*@constant double M_SQRT2@*/ | |
222 | /*@constant double M_SQRT1_2@*/ | |
223 | ||
224 | /*@constant double MAXFLOAT@*/ | |
225 | /*@constant double HUGE@*/ | |
226 | ||
227 | /*@constant int DOMAIN@*/ | |
228 | /*@constant int SING@*/ | |
229 | /*@constant int OVERFLOW@*/ | |
230 | /*@constant int UNDERFLOW@*/ | |
231 | /*@constant int TLOSS@*/ | |
232 | /*@constant int PLOSS@*/ | |
233 | ||
234 | extern /*@unchecked@*/ int daylight; | |
235 | extern /*@unchecked@*/ long timezone; | |
236 | extern /*@unchecked@*/ char *tzname[]; | |
237 | ||
238 | /*@-incondefs@*/ | |
239 | extern void tzset(void) /*@modifies daylight, timezone, tzname@*/ ; | |
240 | /*@=incondefs@*/ | |
241 | ||
8fe44445 | 242 | /*@-redef@*/ /* Defined by ansi: */ |
243 | typedef /*@integraltype@*/ key_t; | |
244 | /*@-incondefs@*/ typedef long timer_t; /*@=incondefs@*/ | |
245 | /*@=redef@*/ | |
246 | ||
885824d3 | 247 | typedef unsigned char uchar_t; |
248 | typedef unsigned short ushort_t; | |
249 | typedef unsigned int uint_t; | |
250 | typedef unsigned long ulong_t; | |
251 | typedef volatile unsigned char vuchar_t; | |
252 | typedef volatile unsigned short vushort_t; | |
253 | typedef volatile unsigned int vuint_t; | |
254 | typedef volatile unsigned long vulong_t; | |
255 | typedef long label_t; | |
256 | typedef int level_t; | |
257 | typedef /*@integraltype@*/ daddr_t; | |
258 | typedef char *caddr_t; | |
259 | typedef long *qaddr_t; | |
260 | typedef char *addr_t; | |
261 | typedef long physadr_t; | |
262 | typedef short cnt_t; | |
263 | typedef int chan_t; | |
264 | typedef unsigned long rlim_t; | |
265 | typedef int paddr_t; | |
885824d3 | 266 | typedef void *mid_t; |
267 | typedef char slab_t[12]; | |
268 | typedef ulong_t shmatt_t; | |
269 | typedef ulong_t msgqnum_t; | |
270 | typedef ulong_t msglen_t; | |
885824d3 | 271 | typedef uchar_t uchar; |
272 | typedef ushort_t ushort; | |
273 | typedef uint_t uint; | |
274 | typedef ulong_t ulong; | |
275 | typedef uchar_t u_char; | |
276 | typedef ushort_t u_short; | |
277 | typedef uint_t u_int; | |
278 | typedef ulong_t u_long; | |
279 | typedef vuchar_t vu_char; | |
280 | typedef vushort_t vu_short; | |
281 | typedef vuint_t vu_int; | |
282 | typedef vulong_t vu_long; | |
283 | typedef long swblk_t; | |
284 | typedef u_long fixpt_t; | |
285 | typedef long segsz_t; | |
286 | typedef /*@abstract@*/ fd_set; | |
287 | ||
885824d3 | 288 | int ioctl (int d, int /*@alt long@*/ request, /*@out@*/ void *arg) |
289 | /*@modifies *arg, errno@*/ ; /* depends on request! */ | |
290 | ||
885824d3 | 291 | pid_t vfork (void) /*@modifies fileSystem@*/ ; |
292 | ||
140c27a8 | 293 | /* |
294 | ** sys/uio.h | |
295 | */ | |
885824d3 | 296 | |
15b3d2b2 | 297 | struct iovec { |
140c27a8 | 298 | void *iov_base; |
299 | size_t iov_len; /*: maxSet(iov_base) = iov_len */ | |
885824d3 | 300 | }; |
301 | ||
140c27a8 | 302 | /* from limits.h */ |
885824d3 | 303 | /*@constant int UIO_MAXIOV@*/ /* BSD */ |
304 | /*@constant int IOV_MAX@*/ /* supposedly SVR4 */ | |
305 | ||
140c27a8 | 306 | ssize_t readv (int fd, const struct iovec *iov, int iovcnt) |
307 | /*@modifies iov->iov_base, fileSystem, errno@*/; | |
885824d3 | 308 | |
140c27a8 | 309 | ssize_t writev (int fd, const struct iovec *iov, int iovcnt) |
310 | /*@modifies errno@*/; | |
885824d3 | 311 | |
312 | /*________________________________________________________________________ | |
313 | * poll.h | |
314 | */ | |
315 | ||
316 | struct poll { | |
317 | int fd; | |
318 | short events; | |
319 | short revents; | |
320 | }; | |
321 | ||
322 | /*@constant short POLLIN@*/ | |
323 | /*@constant short POLLRDNORM@*/ | |
324 | /*@constant short POLLRDBAND@*/ | |
325 | /*@constant short POLLPRI@*/ | |
326 | /*@constant short POLLOUT@*/ | |
327 | /*@constant short POLLWRNORM@*/ | |
328 | /*@constant short POLLWRBAND@*/ | |
329 | /*@constant short POLLERR@*/ | |
330 | /*@constant short POLLHUP@*/ | |
331 | /*@constant short POLLNVAL@*/ | |
332 | ||
333 | extern int poll (struct poll pollfd[], unsigned long nfds, int timeout) | |
334 | /*@modifies pollfd[].revents, errno@*/ ; | |
335 | ||
336 | /* | |
337 | ** free does not take null | |
338 | */ | |
339 | ||
340 | /*@-incondefs@*/ | |
341 | extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ ; | |
342 | /*@=incondefs@*/ | |
343 | ||
344 | /*________________________________________________________________________ | |
345 | * sys/socket.h | |
346 | */ | |
347 | ||
140c27a8 | 348 | |
349 | ||
350 | ||
885824d3 | 351 | /*@constant int SOCK_RDM@*/ |
140c27a8 | 352 | |
353 | ||
354 | ||
355 | ||
356 | ||
357 | ||
358 | ||
885824d3 | 359 | /*@constant int SO_USELOOPBACK@*/ |
140c27a8 | 360 | |
361 | ||
885824d3 | 362 | /*@constant int SO_REUSEPORT@*/ |
140c27a8 | 363 | |
364 | ||
365 | ||
366 | ||
367 | ||
368 | ||
369 | ||
370 | ||
371 | ||
372 | ||
885824d3 | 373 | /*@constant int AF_LOCAL@*/ |
140c27a8 | 374 | |
375 | ||
885824d3 | 376 | /*@constant int AF_IMPLINK@*/ |
377 | /*@constant int AF_PUP@*/ | |
378 | /*@constant int AF_CHAOS@*/ | |
379 | /*@constant int AF_NS@*/ | |
380 | /*@constant int AF_ISO@*/ | |
381 | /*@constant int AF_OSI@*/ | |
382 | /*@constant int AF_ECMA@*/ | |
383 | /*@constant int AF_DATAKIT@*/ | |
384 | /*@constant int AF_CCITT@*/ | |
385 | /*@constant int AF_SNA@*/ | |
386 | /*@constant int AF_DECnet@*/ | |
387 | /*@constant int AF_DLI@*/ | |
388 | /*@constant int AF_LAT@*/ | |
389 | /*@constant int AF_HYLINK@*/ | |
390 | /*@constant int AF_APPLETALK@*/ | |
391 | /*@constant int AF_ROUTE@*/ | |
392 | /*@constant int AF_LINK@*/ | |
393 | /*@constant int pseudo_AF_XTP@*/ | |
394 | /*@constant int AF_COIP@*/ | |
395 | /*@constant int AF_CNT@*/ | |
396 | /*@constant int pseudo_AF_RTIP@*/ | |
397 | /*@constant int AF_IPX@*/ | |
398 | /*@constant int AF_SIP@*/ | |
399 | /*@constant int pseudo_AF_PIP@*/ | |
400 | /*@constant int AF_ISDN@*/ | |
401 | /*@constant int AF_E164@*/ | |
402 | /*@constant int AF_MAX@*/ | |
140c27a8 | 403 | |
404 | ||
405 | ||
406 | ||
407 | ||
408 | ||
885824d3 | 409 | /*@constant int MSG_DONTWAIT@*/ |
410 | /*@constant int MSG_EOF@*/ | |
411 | /*@constant int MSG_COMPAT@*/ | |
412 | /*@constant int PF_UNSPEC@*/ | |
413 | /*@constant int PF_LOCAL@*/ | |
414 | /*@constant int PF_UNIX@*/ | |
415 | /*@constant int PF_INET@*/ | |
416 | /*@constant int PF_IMPLINK@*/ | |
417 | /*@constant int PF_PUP@*/ | |
418 | /*@constant int PF_CHAOS@*/ | |
419 | /*@constant int PF_NS@*/ | |
420 | /*@constant int PF_ISO@*/ | |
421 | /*@constant int PF_OSI@*/ | |
422 | /*@constant int PF_ECMA@*/ | |
423 | /*@constant int PF_DATAKIT@*/ | |
424 | /*@constant int PF_CCITT@*/ | |
425 | /*@constant int PF_SNA@*/ | |
426 | /*@constant int PF_DECnet@*/ | |
427 | /*@constant int PF_DLI@*/ | |
428 | /*@constant int PF_LAT@*/ | |
429 | /*@constant int PF_HYLINK@*/ | |
430 | /*@constant int PF_APPLETALK@*/ | |
431 | /*@constant int PF_ROUTE@*/ | |
432 | /*@constant int PF_LINK@*/ | |
433 | /*@constant int PF_XTP@*/ | |
434 | /*@constant int PF_COIP@*/ | |
435 | /*@constant int PF_CNT@*/ | |
436 | /*@constant int PF_SIP@*/ | |
437 | /*@constant int PF_IPX@*/ | |
438 | /*@constant int PF_RTIP@*/ | |
439 | /*@constant int PF_PIP@*/ | |
440 | /*@constant int PF_ISDN@*/ | |
441 | /*@constant int PF_MAX@*/ | |
442 | /*@constant int NET_MAXID@*/ | |
443 | /*@constant int NET_RT_DUMP@*/ | |
444 | /*@constant int NET_RT_FLAGS@*/ | |
445 | /*@constant int NET_RT_IFLIST@*/ | |
446 | /*@constant int NET_RT_MAXID@*/ | |
885824d3 | 447 | |
885824d3 | 448 | |
eed3d8ac | 449 | /*moved this to before socket.h to get splint to parse the header*/ |
450 | typedef /*@unsignedintegraltype@*/ sa_family_t; | |
451 | ||
885824d3 | 452 | |
140c27a8 | 453 | /* |
454 | ** sys/socket.h | |
455 | ** (updated 26 May 2002) | |
456 | */ | |
457 | ||
458 | typedef /*@unsignedintegraltype@*/ socklen_t; | |
459 | ||
460 | struct sockaddr { | |
461 | sa_family_t sa_family; /* address family */ | |
462 | char sa_data[]; /* variable length */ | |
885824d3 | 463 | }; |
140c27a8 | 464 | |
465 | struct sockaddr_storage { | |
466 | sa_family_t ss_family; | |
467 | } ; | |
468 | ||
469 | struct msghdr { | |
470 | void *msg_name; | |
471 | socklen_t msg_namelen; /*: maxSet (msg_name) >= msg_namelen */ | |
472 | struct iovec *msg_iov; /* scatter/gather array */ | |
473 | int msg_iovlen; /* # elements in msg_iov */ /*: maxSet (msg_iov) >= msg_iovlen */ | |
474 | void *msg_control; /* ancillary data, see below */ | |
475 | socklen_t msg_controllen; /*: maxSet (msg_control) >= msg_controllen */ | |
476 | int msg_flags; /* flags on received message */ | |
477 | } ; | |
478 | ||
479 | struct cmsghdr { | |
480 | socklen_t cmsg_len; /* data byte count, including hdr */ | |
481 | int cmsg_level; /* originating protocol */ | |
482 | int cmsg_type; /* protocol-specific type */ | |
483 | } ; | |
484 | ||
485 | /*@constant int SCM_RIGHTS@*/ | |
486 | ||
487 | /*@exposed@*/ unsigned char *CMSG_DATA (/*@sef@*/ struct cmsghdr *) /*@*/ ; | |
488 | /*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_NXTHDR (struct msghdr *, struct cmsghdr *) /*@*/ ; | |
489 | /*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_FIRSTHDR (struct msghdr *) /*@*/ ; | |
490 | ||
491 | struct linger { | |
492 | int l_onoff; | |
493 | int l_linger; | |
885824d3 | 494 | }; |
495 | ||
140c27a8 | 496 | /*@constant int SOCK_DGRAM@*/ |
497 | /*@constant int SOCK_RAW@*/ | |
498 | /*@constant int SOCK_SEQPACKET@*/ | |
499 | /*@constant int SOCK_STREAM@*/ | |
500 | ||
501 | /*@constant int SOL_SOCKET@*/ | |
502 | ||
503 | /*@constant int SO_ACCEPTCONN@*/ | |
504 | /*@constant int SO_BROADCAST@*/ | |
505 | /*@constant int SO_DEBUG@*/ | |
506 | /*@constant int SO_DONTROUTE@*/ | |
507 | /*@constant int SO_ERROR@*/ | |
508 | /*@constant int SO_KEEPALIVE@*/ | |
509 | /*@constant int SO_LINGER@*/ | |
510 | /*@constant int SO_OOBINLINE@*/ | |
511 | /*@constant int SO_RCVBUF@*/ | |
512 | /*@constant int SO_RCVLOWAT@*/ | |
513 | /*@constant int SO_RCVTIMEO@*/ | |
514 | /*@constant int SO_REUSEADDR@*/ | |
515 | /*@constant int SO_SNDBUF@*/ | |
516 | /*@constant int SO_SNDLOWAT@*/ | |
517 | /*@constant int SO_SNDTIMEO@*/ | |
518 | /*@constant int SO_TYPE@*/ | |
519 | ||
520 | /*@constant int SOMAXCONN@*/ | |
521 | ||
522 | /*@constant int MSG_CTRUNC@*/ | |
523 | /*@constant int MSG_DONTROUTE@*/ | |
524 | /*@constant int MSG_EOR@*/ | |
525 | /*@constant int MSG_OOB@*/ | |
526 | /*@constant int MSG_PEEK@*/ | |
527 | /*@constant int MSG_TRUNC@*/ | |
528 | /*@constant int MSG_WAITALL@*/ | |
529 | ||
530 | /*@constant int AF_INET@*/ | |
531 | /*@constant int AF_INET6@*/ | |
532 | /*@constant int AF_UNIX@*/ | |
533 | /*@constant int AF_UNSPEC@*/ | |
534 | ||
535 | /*@constant int SHUT_RD@*/ | |
536 | /*@constant int SHUT_RDWR@*/ | |
537 | /*@constant int SHUT_WR@*/ | |
538 | ||
539 | # if 0 | |
540 | /* | |
541 | ** These were in the old unix.h spec, but are not in SUS6 | |
542 | */ | |
543 | ||
544 | struct sockproto { | |
545 | u_short sp_family; /* address family */ | |
546 | u_short sp_protocol; /* protocol */ | |
885824d3 | 547 | }; |
548 | ||
140c27a8 | 549 | # endif |
885824d3 | 550 | |
140c27a8 | 551 | int accept (int s, struct sockaddr *addr, int *addrlen) |
552 | /*@modifies *addrlen, errno@*/; | |
885824d3 | 553 | |
140c27a8 | 554 | int bind (int s, const struct sockaddr *name, int namelen) |
555 | /*@modifies errno, fileSystem@*/; | |
885824d3 | 556 | |
140c27a8 | 557 | int connect (int s, const struct sockaddr *name, int namelen) |
558 | /*@modifies errno, internalState@*/; | |
86d93ed3 | 559 | |
eed3d8ac | 560 | /*drl splint doesn't handle restrict yet*/ |
561 | int getpeername (int s, /*@out@*/ struct sockaddr * | |
562 | #if 0 | |
563 | restrict | |
564 | #endif | |
565 | name, socklen_t * | |
566 | #if 0 | |
567 | restrict | |
568 | #endif | |
569 | namelen) | |
140c27a8 | 570 | /*@modifies *name, *namelen, errno@*/; |
571 | ||
86d93ed3 | 572 | #ifdef STRICT |
885824d3 | 573 | |
86d93ed3 | 574 | int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t *address_len) |
575 | /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/ | |
7272a1c1 | 576 | /*@modifies *address, *address_len, errno@*/; |
885824d3 | 577 | |
86d93ed3 | 578 | #else |
579 | int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t /*@alt size_t@*/ *address_len) | |
155af98d | 580 | /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/ |
86d93ed3 | 581 | /*@modifies *address, *address_len, errno@*/; |
582 | ||
583 | #endif | |
584 | ||
7272a1c1 | 585 | int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen) |
885824d3 | 586 | /*@modifies *optval, *optlen, errno@*/; |
587 | ||
588 | extern int | |
589 | listen (int s, int backlog) | |
590 | /*@modifies errno, internalState@*/; | |
591 | ||
592 | extern ssize_t | |
593 | recv (int s, /*@out@*/ void *buf, size_t len, int flags) | |
594 | /*@modifies *buf, errno@*/; | |
595 | ||
596 | extern ssize_t | |
597 | recvfrom (int s, void *buf, size_t len, int flags, /*@null@*/ struct sockaddr *from, int *fromlen) | |
598 | /*@modifies *buf, *from, *fromlen, errno@*/; | |
599 | ||
600 | extern ssize_t | |
601 | recvmsg (int s, struct msghdr *msg, int flags) | |
602 | /*@modifies msg->msg_iov->iov_base[], errno@*/; | |
603 | ||
604 | extern ssize_t | |
605 | send (int s, const void *msg, size_t len, int flags) | |
606 | /*@modifies errno@*/; | |
607 | ||
608 | extern ssize_t | |
609 | sendto (int s, const void *msg, size_t len, int flags, const struct sockaddr *to, int tolen) | |
610 | /*@modifies errno@*/; | |
611 | ||
612 | extern ssize_t | |
613 | sendmsg (int s, const struct msghdr *msg, int flags) | |
614 | /*@modifies errno@*/; | |
615 | ||
616 | extern int | |
617 | setsockopt (int s, int level, int optname, const void *optval, int optlen) | |
618 | /*@modifies internalState, errno@*/; | |
619 | ||
620 | extern int | |
621 | shutdown (int s, int how) | |
622 | /*@modifies errno@*/; | |
623 | ||
624 | extern int | |
625 | socket (int domain, int type, int protocol) | |
626 | /*@modifies errno@*/; | |
627 | ||
628 | extern int | |
629 | socketpair (int d, int type, int protocol, /*@out@*/ int *sv) | |
630 | /*@modifies errno@*/; | |
631 | ||
632 | /*@constant int BADSIG@*/ | |
633 | /*@constant int SA_ONSTACK@*/ | |
634 | /*@constant int SA_RESTART@*/ | |
635 | /*@constant int SA_DISABLE@*/ | |
636 | /*@constant int SIGBUS@*/ | |
637 | /*@constant int SIGEMT@*/ | |
638 | /*@constant int SIGINFO@*/ | |
639 | /*@constant int SIGIO@*/ | |
640 | /*@constant int SIGIOT@*/ | |
641 | /*@constant int SIGPOLL@*/ | |
642 | /*@constant int SIGPROF@*/ | |
643 | /*@constant int SIGPWR@*/ | |
644 | /*@constant int SIGSYS@*/ | |
645 | /*@constant int SIGTRAP@*/ | |
646 | /*@constant int SIGURG@*/ | |
647 | /*@constant int SIGVTALRM@*/ | |
648 | /*@constant int SIGWINCH@*/ | |
649 | /*@constant int SIGXCPU@*/ | |
650 | /*@constant int SIGXFSZ@*/ | |
651 | ||
652 | extern void psignal (int sig, const char *msg) | |
653 | /*@modifies fileSystem@*/; | |
654 | ||
885824d3 | 655 | extern int |
656 | setenv (const char *name, const char *value, int overwrite) | |
657 | /*@globals environ@*/ | |
658 | /*@modifies *environ, errno@*/; | |
659 | ||
885824d3 | 660 | extern void |
661 | unsetenv (const char *name) | |
662 | /*@globals environ@*/ | |
663 | /*@modifies *environ@*/; | |
664 | ||
665 | /*________________________________________________________________________ | |
666 | * sys/wait.h | |
667 | */ | |
668 | ||
669 | extern int | |
670 | WCOREDUMP (int x) | |
671 | /*@*/; | |
672 | ||
673 | extern int | |
674 | W_EXITCODE (int ret, int sig) | |
675 | /*@*/; | |
676 | ||
677 | extern int | |
678 | W_STOPCODE (int sig) | |
679 | /*@*/; | |
680 | ||
681 | /*@constant int WAIT_ANY@*/ | |
682 | /*@constant int WAIT_MYPGRP@*/ | |
683 | /*@constant int WSTOPPED@*/ | |
684 | ||
685 | extern pid_t | |
686 | wait3 (int *statloc, int options, /*@null@*/ /*@out@*/ struct rusage *rusage) | |
687 | /*@modifies *statloc, *rusage, errno@*/; | |
688 | ||
689 | extern pid_t | |
690 | wait4 (pid_t p, int *statloc, int opt, /*@null@*/ /*@out@*/ struct rusage *r) | |
691 | /*@modifies *statloc, *r, errno@*/; | |
692 | ||
693 | struct timeval { | |
694 | long tv_sec; | |
695 | long tv_usec; | |
696 | } ; | |
697 | ||
698 | struct timespec { | |
699 | long ts_sec; | |
700 | long ts_nsec; | |
701 | } ; | |
702 | ||
703 | struct timezone { | |
704 | int tz_minuteswest; | |
705 | int tz_dsttime; | |
706 | } ; | |
707 | ||
708 | /*@constant int DST_NONE@*/ | |
709 | /*@constant int DST_USA@*/ | |
710 | /*@constant int DST_AUST@*/ | |
711 | /*@constant int DST_WET@*/ | |
712 | /*@constant int DST_MET@*/ | |
713 | /*@constant int DST_EET@*/ | |
714 | /*@constant int DST_CAN@*/ | |
715 | ||
716 | /*@constant int ITIMER_PROF@*/ | |
717 | /*@constant int ITIMER_REAL@*/ | |
718 | /*@constant int ITIMER_VIRTUAL@*/ | |
719 | ||
720 | struct itimerval { | |
721 | struct timeval it_interval; | |
722 | struct timeval it_value; | |
723 | }; | |
724 | ||
725 | struct clockinfo { | |
726 | int hz; | |
727 | int tick; | |
728 | int stathz; | |
729 | int profhz; | |
730 | }; | |
731 | ||
732 | extern int | |
733 | adjtime (const struct timeval *delta, /*@null@*/ /*@out@*/ struct timeval *olddelta) | |
734 | /*@modifies internalState, *olddelta, errno@*/; | |
735 | ||
736 | extern int | |
737 | getitimer (int which, /*@out@*/ struct itimerval *value) | |
738 | /*@modifies errno, *value*/; | |
739 | ||
740 | extern int | |
741 | gettimeofday (/*@null@*/ /*@out@*/ struct timeval *tp, /*@null@*/ /*@out@*/ struct timezone *tzp) | |
742 | /*@modifies *tp, *tzp, errno@*/; | |
743 | ||
744 | extern int | |
745 | setitimer (int which, struct itimerval *val, /*@null@*/ /*@out@*/ struct itimerval *oval) | |
746 | /*@modifies *oval, errno, internalState*/; | |
747 | ||
748 | extern int | |
749 | settimeofday (const struct timeval *t, const struct timezone *z) | |
750 | /*@modifies internalState, errno@*/; | |
751 | ||
752 | extern int | |
753 | utimes (const char *file, /*@null@*/ const struct timeval *times) | |
754 | /*@modifies fileSystem, errno*/; | |
755 | ||
756 | /*________________________________________________________________________ | |
757 | * sys/mman.h | |
758 | */ | |
759 | ||
760 | /*@constant int PROT_READ@*/ | |
761 | /*@constant int PROT_WRITE@*/ | |
762 | /*@constant int PROT_EXEC@*/ | |
763 | /*@constant int MAP_SHARED@*/ | |
764 | /*@constant int MAP_PRIVATE@*/ | |
765 | /*@constant int MAP_COPY@*/ | |
766 | /*@constant int MAP_FIXED@*/ | |
767 | /*@constant int MAP_RENAME@*/ | |
768 | /*@constant int MAP_NORESERVE@*/ | |
769 | /*@constant int MAP_INHERIT@*/ | |
770 | /*@constant int MAP_NOEXTEND@*/ | |
771 | /*@constant int MAP_HASSEMAPHORE@*/ | |
772 | /*@constant int MS_ASYNC@*/ | |
773 | /*@constant int MS_INVALIDATE@*/ | |
774 | /*@constant int MAP_FILE@*/ | |
775 | /*@constant int MAP_ANON@*/ | |
776 | /*@constant int MADV_NORMAL@*/ | |
777 | /*@constant int MADV_RANDOM@*/ | |
778 | /*@constant int MADV_SEQUENTIAL@*/ | |
779 | /*@constant int MADV_WILLNEED@*/ | |
780 | /*@constant int MADV_DONTNEED@*/ | |
781 | ||
782 | extern caddr_t | |
783 | mmap (/*@null@*/ /*@returned@*/ caddr_t addr, size_t len, int prot, int flags, int fd, off_t offset) | |
784 | /*@modifies addr@*/; | |
785 | ||
786 | extern int | |
787 | madvise (caddr_t addr, int len, int behav) | |
788 | /*@*/; | |
789 | ||
790 | extern int | |
791 | mprotect (caddr_t addr, int len, int prot) | |
792 | /*@*/; | |
793 | ||
794 | extern int | |
345671f3 | 795 | int munmap (/*@only@*/ caddr_t addr, size_t len) |
796 | /*@modifies fileSystem, *addr, errno @*/; | |
797 | ||
885824d3 | 798 | extern int |
799 | msync (caddr_t addr, int len, int flags) | |
800 | /*@*/; | |
801 | ||
802 | extern int | |
803 | mlock (caddr_t addr, size_t len) | |
804 | /*@*/; | |
805 | ||
806 | extern int | |
807 | munlock (caddr_t addr, size_t len) | |
808 | /*@*/; | |
809 | ||
810 | ||
811 | /*________________________________________________________________________ | |
812 | * sys/ioctl.h | |
813 | */ | |
814 | ||
815 | struct winsize { | |
816 | unsigned short ws_row; | |
817 | unsigned short ws_col; | |
818 | unsigned short ws_xpixel; | |
819 | unsigned short ws_ypixel; | |
820 | }; | |
821 | ||
822 | /*@constant int TIOCMODG@*/ | |
823 | /*@constant int TIOCMODS@*/ | |
824 | /*@constant int TIOCM_LE@*/ | |
825 | /*@constant int TIOCM_DTR@*/ | |
826 | /*@constant int TIOCM_RTS@*/ | |
827 | /*@constant int TIOCM_ST@*/ | |
828 | /*@constant int TIOCM_SR@*/ | |
829 | /*@constant int TIOCM_CTS@*/ | |
830 | /*@constant int TIOCM_CAR@*/ | |
831 | /*@constant int TIOCM_CD@*/ | |
832 | /*@constant int TIOCM_RNG@*/ | |
833 | /*@constant int TIOCM_RI@*/ | |
834 | /*@constant int TIOCM_DSR@*/ | |
835 | /*@constant int TIOCEXCL@*/ | |
836 | /*@constant int TIOCNXCL@*/ | |
837 | /*@constant int TIOCFLUSH@*/ | |
838 | /*@constant int TIOCGETA@*/ | |
839 | /*@constant int TIOCSETA@*/ | |
840 | /*@constant int TIOCSETAW@*/ | |
841 | /*@constant int TIOCSETAF@*/ | |
842 | /*@constant int TIOCGETD@*/ | |
843 | /*@constant int TIOCSETD@*/ | |
844 | /*@constant int TIOCSBRK@*/ | |
845 | /*@constant int TIOCCBRK@*/ | |
846 | /*@constant int TIOCSDTR@*/ | |
847 | /*@constant int TIOCCDTR@*/ | |
848 | /*@constant int TIOCGPGRP@*/ | |
849 | /*@constant int TIOCSPGRP@*/ | |
850 | /*@constant int TIOCOUTQ@*/ | |
851 | /*@constant int TIOCSTI@*/ | |
852 | /*@constant int TIOCNOTTY@*/ | |
853 | /*@constant int TIOCPKT@*/ | |
854 | /*@constant int TIOCPKT_DATA@*/ | |
855 | /*@constant int TIOCPKT_FLUSHREAD@*/ | |
856 | /*@constant int TIOCPKT_FLUSHWRITE@*/ | |
857 | /*@constant int TIOCPKT_STOP@*/ | |
858 | /*@constant int TIOCPKT_START@*/ | |
859 | /*@constant int TIOCPKT_NOSTOP@*/ | |
860 | /*@constant int TIOCPKT_DOSTOP@*/ | |
861 | /*@constant int TIOCPKT_IOCTL@*/ | |
862 | /*@constant int TIOCSTOP@*/ | |
863 | /*@constant int TIOCSTART@*/ | |
864 | /*@constant int TIOCMSET@*/ | |
865 | /*@constant int TIOCMBIS@*/ | |
866 | /*@constant int TIOCMBIC@*/ | |
867 | /*@constant int TIOCMGET@*/ | |
868 | /*@constant int TIOCREMOTE@*/ | |
869 | /*@constant int TIOCGWINSZ@*/ | |
870 | /*@constant int TIOCSWINSZ@*/ | |
871 | /*@constant int TIOCUCNTL@*/ | |
872 | /*@constant int TIOCSTAT@*/ | |
873 | /*@constant int TIOCCONS@*/ | |
874 | /*@constant int TIOCSCTTY@*/ | |
875 | /*@constant int TIOCEXT@*/ | |
876 | /*@constant int TIOCSIG@*/ | |
877 | /*@constant int TIOCDRAIN@*/ | |
878 | /*@constant int TIOCMSDTRWAIT@*/ | |
879 | /*@constant int TIOCMGDTRWAIT@*/ | |
880 | /*@constant int TIOCTIMESTAMP@*/ | |
881 | /*@constant int TIOCSDRAINWAIT@*/ | |
882 | /*@constant int TIOCGDRAINWAIT@*/ | |
883 | /*@constant int TTYDISC@*/ | |
884 | /*@constant int TABLDISC@*/ | |
885 | /*@constant int SLIPDISC@*/ | |
886 | /*@constant int PPPDISC@*/ | |
887 | ||
888 | /*@constant int MAXHOSTNAMELEN@*/ | |
889 | ||
890 | extern void | |
891 | FD_CLR (int n, fd_set *p) | |
892 | /*@modifies *p@*/; | |
893 | ||
894 | extern void | |
895 | FD_COPY (fd_set *f, /*@out@*/ fd_set *t) | |
896 | /*@modifies *t@*/; | |
897 | ||
898 | extern int /*@alt lltX_bool@*/ | |
899 | FD_ISSET (int n, fd_set *p) | |
900 | /*@*/; | |
901 | ||
902 | extern void | |
903 | FD_SET (int n, fd_set *p) | |
904 | /*@modifies *p@*/; | |
905 | ||
906 | extern void | |
907 | FD_ZERO (fd_set /*@out@*/ *p) | |
908 | /*@modifies *p@*/; | |
909 | ||
910 | extern int | |
911 | fchdir (int fd) | |
912 | /*@modifies internalState, errno@*/; | |
913 | ||
914 | extern int | |
915 | fchown (int fd, uid_t owner, gid_t group) | |
916 | /*@modifies errno, fileSystem@*/; | |
917 | ||
918 | extern int | |
919 | fsync (int fd) | |
920 | /*@modifies errno, fileSystem@*/; | |
921 | ||
922 | extern int | |
923 | ftruncate (int fd, off_t length) | |
924 | /*@modifies errno, fileSystem@*/; | |
925 | ||
b072092f | 926 | int gethostname (/*@out@*/ char *address, size_t address_len) |
927 | /*:errorstatus@*/ | |
928 | /*@modifies address@*/ ; | |
885824d3 | 929 | |
b072092f | 930 | int initgroups (const char *name, int basegid) |
931 | /*@modifies internalState@*/; | |
885824d3 | 932 | |
140c27a8 | 933 | int lchown (const char *path, uid_t owner, gid_t group) |
934 | /*@modifies errno, fileSystem@*/; | |
935 | ||
936 | int select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, fd_set /*@null@*/ *e, /*@null@*/ struct timeval *t) | |
937 | /*@modifies *r, *w, *e, *t, errno@*/; | |
938 | /* evans - 2002-05-26: added null for t, bug reported by Enrico Scholz */ | |
939 | ||
940 | int setegid (gid_t egid) | |
941 | /*@modifies errno, internalState@*/; | |
942 | ||
943 | int seteuid (uid_t euid) | |
944 | /*@modifies errno, internalState@*/; | |
945 | ||
946 | int setgroups (int ngroups, const gid_t *gidset) | |
947 | /*@modifies errno, internalState@*/; | |
948 | ||
949 | int setregid (gid_t rgid, gid_t egid) | |
950 | /*@modifies errno, internalState@*/; | |
951 | ||
952 | int setreuid (gid_t ruid, gid_t euid) | |
953 | /*@modifies errno, internalState@*/; | |
954 | ||
955 | void sync (void) | |
956 | /*@modifies fileSystem@*/; | |
957 | ||
958 | int symlink (const char *path, const char *path2) | |
959 | /*@modifies fileSystem@*/; | |
960 | ||
961 | int truncate (const char *name, off_t length) | |
962 | /*@modifies errno, fileSystem@*/; | |
963 | ||
885824d3 | 964 | /*@constant int EBADRPC@*/ |
965 | /*@constant int ERPCMISMATCH@*/ | |
966 | /*@constant int EPROGUNAVAIL@*/ | |
967 | /*@constant int EPROGMISMATCH@*/ | |
968 | /*@constant int EPROCUNAVAIL@*/ | |
969 | /*@constant int EFTYPE@*/ | |
970 | /*@constant int EAUTH@*/ | |
971 | /*@constant int ENEEDAUTH@*/ | |
972 | /*@constant int ELAST@*/ | |
973 | ||
79127b5d | 974 | /* |
975 | ** tar.h | |
976 | */ | |
885824d3 | 977 | |
978 | /*@unchecked@*/ extern char *TMAGIC; | |
979 | /*@constant int TMAGLEN@*/ | |
980 | /*@unchecked@*/ extern char *TVERSION; | |
981 | /*@constant int TVERSLEN@*/ | |
982 | ||
983 | /*@constant int REGTYPE@*/ | |
984 | /*@constant int AREGTYPE@*/ | |
985 | /*@constant int LNKTYPE@*/ | |
986 | /*@constant int SYMTYPE@*/ | |
987 | /*@constant int CHRTYPE@*/ | |
988 | /*@constant int BLKTYPE@*/ | |
989 | /*@constant int DIRTYPE@*/ | |
990 | /*@constant int FIFOTYPE@*/ | |
991 | /*@constant int CONTTYPE@*/ | |
992 | ||
993 | /*@constant int TSUID@*/ | |
994 | /*@constant int TSGID@*/ | |
995 | /*@constant int TSVTX@*/ | |
996 | ||
997 | /*@constant int TUREAD@*/ | |
998 | /*@constant int TUWRITE@*/ | |
999 | /*@constant int TUEXEC@*/ | |
1000 | /*@constant int TGREAD@*/ | |
1001 | /*@constant int TGWRITE@*/ | |
1002 | /*@constant int TGEXEC@*/ | |
1003 | /*@constant int TOREAD@*/ | |
1004 | /*@constant int TOWRITE@*/ | |
1005 | /*@constant int TOEXEC@*/ | |
1006 | ||
1007 | struct ipc_perm { | |
1008 | uid_t uid; /* user id */ | |
1009 | gid_t gid; /* group id */ | |
1010 | uid_t cuid; /* creator user id */ | |
1011 | gid_t cgid; /* creator group id */ | |
1012 | mode_t mode; /* r/w permission */ | |
1013 | ulong seq; /* slot usage sequence number */ | |
1014 | key_t key; /* user specified msg/sem/shm key */ | |
1015 | } ; | |
1016 | ||
1017 | /*@constant int IPC_R@*/ | |
1018 | /*@constant int IPC_W@*/ | |
1019 | /*@constant int IPC_M@*/ | |
1020 | /*@constant int IPC_CREAT@*/ | |
1021 | /*@constant int IPC_EXCL@*/ | |
1022 | /*@constant int IPC_NOWAIT@*/ | |
1023 | /*@constant key_t IPC_PRIVATE@*/ | |
1024 | /*@constant int IPC_RMID@*/ | |
1025 | /*@constant int IPC_SET@*/ | |
1026 | /*@constant int IPC_STAT@*/ | |
1027 | ||
79127b5d | 1028 | /* |
1029 | ** sys/msg.h | |
1030 | */ | |
885824d3 | 1031 | |
1032 | struct msqid_ds { | |
1033 | struct ipc_perm msg_perm; /* msg queue permission bits */ | |
1034 | struct msg *msg_first; /* first message in the queue */ | |
1035 | struct msg *msg_last; /* last message in the queue */ | |
1036 | u_long msg_cbytes; /* number of bytes in use on the queue */ | |
1037 | u_long msg_qnum; /* number of msgs in the queue */ | |
1038 | u_long msg_qbytes; /* max # of bytes on the queue */ | |
1039 | pid_t msg_lspid; /* pid of last msgsnd() */ | |
1040 | pid_t msg_lrpid; /* pid of last msgrcv() */ | |
1041 | time_t msg_stime; /* time of last msgsnd() */ | |
1042 | time_t msg_rtime; /* time of last msgrcv() */ | |
1043 | time_t msg_ctime; /* time of last msgctl() */ | |
1044 | }; | |
1045 | ||
1046 | struct mymesg { | |
1047 | long mtype; /* message type (+ve integer) */ | |
1048 | char mtext[]; /* message body */ | |
1049 | }; | |
1050 | ||
1051 | /*@constant int MSG_NOERROR@*/ | |
1052 | /*@constant int MSGMAX@*/ | |
1053 | /*@constant int MSGMNB@*/ | |
1054 | /*@constant int MSGMNI@*/ | |
1055 | /*@constant int MSGTQL@*/ | |
1056 | ||
1057 | extern int | |
1058 | msgctl (int id , int cmd, /*@out@*/ struct msqid_ds *buf) | |
1059 | /*@modifies errno, *buf@*/; | |
1060 | ||
1061 | extern int | |
1062 | msgget (key_t key, int flag) | |
1063 | /*@modifies errno@*/; | |
1064 | ||
1065 | extern int | |
1066 | msgrcv (int id, /*@out@*/ void *ptr, size_t nbytes, long type, int flags) | |
1067 | /*@modifies errno, *ptr@*/; | |
1068 | ||
1069 | extern int | |
1070 | msgsnd (int id, const void *ptr, size_t nbytes, int flag) | |
1071 | /*@modifies errno@*/; | |
1072 | ||
79127b5d | 1073 | /* |
1074 | ** sys/sem.h | |
1075 | */ | |
885824d3 | 1076 | |
1077 | struct semid_ds { | |
1078 | struct ipc_perm sem_perm; | |
1079 | struct sem *sem_base; | |
1080 | ushort sem_nsems; | |
1081 | time_t sem_otime; | |
1082 | time_t sem_ctime; | |
1083 | }; | |
1084 | ||
1085 | struct sem { | |
1086 | ushort semval; | |
1087 | pid_t sempid; | |
1088 | ushort semncnt; | |
1089 | ushort semzcnt; | |
1090 | }; | |
1091 | ||
1092 | union semun { | |
1093 | int val; | |
1094 | struct semid_ds *buf; | |
1095 | ushort *array; | |
1096 | }; | |
1097 | ||
1098 | struct sembuf { | |
1099 | ushort sem_num; | |
1100 | short sem_op; | |
1101 | short sem_flg; | |
1102 | }; | |
1103 | ||
1104 | /*@constant int SEM_A@*/ | |
1105 | /*@constant int SEMAEM@*/ | |
1106 | /*@constant int SEMMNI@*/ | |
1107 | /*@constant int SEMMNS@*/ | |
1108 | /*@constant int SEMMNU@*/ | |
1109 | /*@constant int SEMMSL@*/ | |
1110 | /*@constant int SEMOPN@*/ | |
1111 | /*@constant int SEM_R@*/ | |
1112 | /*@constant int SEMUME@*/ | |
1113 | /*@constant int SEM_UNDO@*/ | |
1114 | /*@constant int SEMVMX@*/ | |
1115 | /*@constant int GETVAL@*/ | |
1116 | /*@constant int SETVAL@*/ | |
1117 | /*@constant int GETPID@*/ | |
1118 | /*@constant int GETNCNT@*/ | |
1119 | /*@constant int GETZCNT@*/ | |
1120 | /*@constant int GETALL@*/ | |
1121 | /*@constant int SETALL@*/ | |
1122 | ||
1123 | /*@constant int ERMID@*/ | |
1124 | ||
1125 | extern int | |
1126 | semctl (int id, int semnum, int cmd, union semun arg) | |
1127 | /*@modifies errno@*/; | |
1128 | ||
1129 | extern int | |
1130 | semget (key_t key, int nsems, int flag) | |
1131 | /*@modifies errno@*/; | |
1132 | ||
1133 | extern int | |
1134 | semop (int id, struct sembuf *semoparray, size_t nops) | |
1135 | /*@modifies errno@*/; | |
1136 | ||
79127b5d | 1137 | /* |
1138 | ** sys/shm.h | |
1139 | */ | |
885824d3 | 1140 | |
1141 | struct shmid_ds { | |
1142 | struct ipc_perm shm_perm; | |
1143 | int shm_segsz; | |
1144 | ushort shm_lkcnt; | |
1145 | pid_t shm_lpid; | |
1146 | pid_t shm_cpid; | |
1147 | ulong shm_nattch; | |
1148 | ulong shm_cnattch; | |
1149 | time_t shm_atime; | |
1150 | time_t shm_dtime; | |
1151 | time_t shm_ctime; | |
1152 | }; | |
1153 | ||
1154 | /*@constant int SHMLBA@*/ | |
1155 | /*@constant int SHM_LOCK@*/ | |
1156 | /*@constant int SHMMAX@*/ | |
1157 | /*@constant int SHMMIN@*/ | |
1158 | /*@constant int SHMMNI@*/ | |
1159 | /*@constant int SHM_R@*/ | |
1160 | /*@constant int SHM_RDONLY@*/ | |
1161 | /*@constant int SHM_RND@*/ | |
1162 | /*@constant int SHMSEG@*/ | |
1163 | /*@constant int SHM_W@*/ | |
1164 | /*@constant int SHM_UNLOCK@*/ | |
1165 | ||
79127b5d | 1166 | void * shmat (int id, /*@null@*/ void *addr, int flag) |
1167 | /*@modifies errno@*/ ; | |
1168 | ||
1169 | extern int shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf) | |
1170 | /*@modifies errno, *buf@*/ ; | |
885824d3 | 1171 | |
79127b5d | 1172 | extern int shmdt (void *addr) |
1173 | /*@modifies errno@*/ ; | |
885824d3 | 1174 | |
79127b5d | 1175 | extern int shmget (key_t key, int size, int flag) |
1176 | /*@modifies errno@*/ ; | |
885824d3 | 1177 | |
79127b5d | 1178 | # if 0 |
1179 | /* | |
1180 | ** this is in stdio.h! | |
1181 | */ | |
885824d3 | 1182 | |
79127b5d | 1183 | /* |
1184 | ** stdio.h | |
1185 | */ | |
1186 | ||
1187 | /* | |
1188 | ** evans 2001-12-30: added from http://www.opengroup.org/onlinepubs/007908799/xsh/stdio.h.html | |
1189 | */ | |
1190 | ||
1191 | /*@constant unsignedintegraltype BUFSIZ@*/ | |
1192 | /*@constant unsignedintegraltype FILENAME_MAX@*/ | |
1193 | /*@constant unsignedintegraltype FOPEN_MAX@*/ | |
1194 | /*@constant bool _IOFBF@*/ | |
1195 | /*@constant bool _IOLBF@*/ | |
1196 | /*@constant bool _IONBF@*/ | |
1197 | /*@constant unsignedintegraltype L_ctermid@*/ | |
1198 | /*@constant unsignedintegraltype L_cuserid@*/ | |
1199 | /*@constant unsignedintegraltype L_tmpnam@*/ | |
1200 | /*@constant unsignedintegraltype SEEK_CUR@*/ | |
1201 | /*@constant unsignedintegraltype SEEK_END@*/ | |
1202 | /*@constant unsignedintegraltype SEEK_SET@*/ | |
1203 | /*@constant unsignedintegraltype TMP_MAX@*/ | |
1204 | ||
1205 | /* EOF */ | |
1206 | /* NULL */ | |
1207 | ||
1208 | /*@constant observer char *P_tmpdir@*/ | |
1209 | ||
d5047b91 | 1210 | void clearerr (FILE *s) |
1211 | /*@modifies s@*/ ; | |
1212 | ||
79127b5d | 1213 | /*@dependent@*/ char *ctermid (/*@returned@*/ /*@null@*/ char *) /*@*/ ; |
1214 | /* Result may be static pointer if parameter is NULL, otherwise is fresh. */ | |
1215 | ||
1216 | char *cuserid (/*@null@*/ /*@returned@*/ char *) | |
1217 | /*@warn legacy "cuserid is obsolete"@*/ /*@*/ ; | |
1218 | ||
d5047b91 | 1219 | /* fclose in standard.h */ |
1220 | ||
79127b5d | 1221 | /*@null@*/ FILE *fdopen (int, const char *) |
1222 | /*@modifies errno, fileSystem@*/ ; | |
1223 | ||
d5047b91 | 1224 | /* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */ |
1225 | ||
79127b5d | 1226 | int fileno (/*@notnull@*/ FILE *) |
1227 | /*:errorcode -1:*/ | |
1228 | /*@modifies errno@*/ ; | |
1229 | ||
1230 | void flockfile (/*@notnull@*/ FILE *f) | |
1231 | /*@modifies f, fileSystem@*/ ; | |
1232 | ||
1233 | int fseeko (FILE *stream, off_t offset, int whence) | |
1234 | /*:errorcode -1:*/ | |
1235 | /*@modifies stream, errno@*/ ; | |
1236 | ||
1237 | off_t ftello(FILE *stream) | |
1238 | /*:errorcode -1:*/ /*@modifies errno*/ ; | |
1239 | ||
1240 | int ftrylockfile(FILE *stream) | |
1241 | /*:errorcode !0:*/ | |
1242 | /*@modifies stream, fileSystem, errno*/ ; | |
1243 | ||
1244 | void funlockfile (FILE *stream) | |
1245 | /*@modifies stream, fileSystem*/ ; | |
1246 | ||
1247 | int getc_unlocked(FILE *stream) | |
1248 | /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/ | |
1249 | /*@modifies *stream, fileSystem, errno@*/ ; | |
1250 | ||
1251 | int getchar_unlocked (void) | |
1252 | /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/ | |
1253 | /*@globals stdin@*/ | |
1254 | /*@modifies *stdin, fileSystem@*/ ; | |
1255 | ||
1256 | int getopt (int, char * const[], const char) | |
1257 | /*@warn legacy@*/ ; | |
1258 | ||
1259 | int getw (FILE *stream) | |
1260 | /*:errorcode EOF:*/ | |
1261 | /*@modifies fileSystem, *stream, errno@*/ ; | |
1262 | ||
1263 | int pclose(FILE *stream) | |
1264 | /*:errorcode -1:*/ | |
1265 | /*@modifies *stream, errno@*/ ; | |
1266 | ||
1267 | /*@null@*/ FILE *popen (const char *command, const char *mode) | |
1268 | /*:errorcode NULL:*/ | |
1269 | /*@modifies fileSystem, errno@*/ ; | |
1270 | ||
1271 | int putc_unlocked (int, FILE *stream) | |
1272 | /*@warn multithreaded "putc_unlocked is a thread unsafe version of putc"@*/ | |
1273 | /*:errorcode EOF:*/ | |
1274 | /*@modifies fileSystem, *stream, errno@*/ ; | |
1275 | ||
1276 | int putchar_unlocked(int) | |
1277 | /*@warn multithreaded "putchar_unlocked is a thread unsafe version of putchar"@*/ | |
1278 | /*:errorcode EOF:*/ | |
1279 | /*@modifies fileSystem, *stdout, errno@*/ ; | |
1280 | ||
1281 | int putw(int, FILE *stream) | |
1282 | /*:errorcode EOF:*/ | |
1283 | /*@modifies fileSystem, *stdout, errno@*/ ; | |
1284 | ||
1285 | int remove (const char *) | |
1286 | /*@modifies fileSystem@*/ ; | |
1287 | ||
1288 | int rename (const char *, const char *) | |
1289 | /*@modifies fileSystem@*/ ; | |
1290 | ||
1291 | void rewind (FILE *stream) | |
1292 | /*@modifies *stream@*/ ; | |
1293 | ||
d5047b91 | 1294 | void setbuf (FILE *stream, /*@null@*/ /*@dependent@*/ /*@exposed@*/ char *buf) |
1295 | /*@modifies stream@*/ | |
1296 | ||
1297 | int setvbuf (FILE *stream, /*@null@*/ /*@dependent@*/ /*@exposed@*/ char *buf, int type, size_t size) | |
1298 | /*@modifies stream@*/ | |
1299 | /*:errorcode !0:*/ ; | |
1300 | ||
1301 | int snprintf (char *s, size_t n, const char *format, ...); | |
1302 | ||
79127b5d | 1303 | int sprintf(char *, const char *, ...); |
1304 | int sscanf(const char *, const char *, int ...); | |
1305 | char *tempnam(const char *, const char *); | |
1306 | FILE *tmpfile(void); | |
1307 | char *tmpnam(char *); | |
1308 | int ungetc(int, FILE *); | |
1309 | int vfprintf(FILE *, const char *, va_list); | |
1310 | int vprintf(const char *, va_list); | |
1311 | int vsnprintf(char *, size_t, const char *, va_list); | |
1312 | int vsprintf(char *, const char *, va_list); | |
1313 | ||
1314 | ||
1315 | The following external variables are defined: | |
1316 | ||
1317 | ||
1318 | extern char *optarg; ) | |
1319 | extern int opterr; ) | |
1320 | extern int optind; ) (LEGACY) | |
1321 | extern int optopt; ) | |
1322 | ||
1323 | # endif | |
1324 | ||
1325 | /* | |
1326 | ** syslog.h | |
1327 | */ | |
885824d3 | 1328 | |
1329 | /*@constant int LOG_EMERG@*/ | |
1330 | /*@constant int LOG_ALERT@*/ | |
1331 | /*@constant int LOG_CRIT@*/ | |
1332 | /*@constant int LOG_ERR@*/ | |
1333 | /*@constant int LOG_WARNING@*/ | |
1334 | /*@constant int LOG_NOTICE@*/ | |
1335 | /*@constant int LOG_INFO@*/ | |
1336 | /*@constant int LOG_DEBUG@*/ | |
1337 | ||
1338 | /*@constant int LOG_KERN@*/ | |
1339 | /*@constant int LOG_USER@*/ | |
1340 | /*@constant int LOG_MAIL@*/ | |
1341 | /*@constant int LOG_DAEMON@*/ | |
1342 | /*@constant int LOG_AUTH@*/ | |
1343 | /*@constant int LOG_SYSLOG@*/ | |
1344 | /*@constant int LOG_LPR@*/ | |
1345 | /*@constant int LOG_NEWS@*/ | |
1346 | /*@constant int LOG_UUCP@*/ | |
1347 | /*@constant int LOG_CRON@*/ | |
1348 | /*@constant int LOG_AUTHPRIV@*/ | |
1349 | /*@constant int LOG_FTP@*/ | |
1350 | /*@constant int LOG_LOCAL0@*/ | |
1351 | /*@constant int LOG_LOCAL1@*/ | |
1352 | /*@constant int LOG_LOCAL2@*/ | |
1353 | /*@constant int LOG_LOCAL3@*/ | |
1354 | /*@constant int LOG_LOCAL4@*/ | |
1355 | /*@constant int LOG_LOCAL5@*/ | |
1356 | /*@constant int LOG_LOCAL6@*/ | |
1357 | /*@constant int LOG_LOCAL7@*/ | |
1358 | ||
1359 | /*@constant int LOG_PID@*/ | |
1360 | /*@constant int LOG_CONS@*/ | |
1361 | /*@constant int LOG_ODELAY@*/ | |
1362 | /*@constant int LOG_NDELAY@*/ | |
1363 | /*@constant int LOG_NOWAIT@*/ | |
1364 | /*@constant int LOG_PERROR@*/ | |
1365 | ||
d5047b91 | 1366 | int LOG_MASK (int pri) |
1367 | /*@*/; | |
1368 | ||
1369 | int LOG_UPTO (int pri) | |
1370 | /*@*/; | |
1371 | ||
1372 | void closelog (void) | |
1373 | /*@modifies fileSystem@*/; | |
1374 | ||
1375 | void openlog (const char *ident, int logopt, int facility) | |
1376 | /*@modifies fileSystem@*/; | |
1377 | ||
1378 | int setlogmask (int maskpri) | |
1379 | /*@modifies internalState@*/; | |
1380 | ||
1381 | void /*@printflike@*/ syslog (int priority, const char *message, ...) | |
1382 | /*@modifies fileSystem@*/; | |
1383 | ||
1384 | void vsyslog (int priority, const char *message, va_list args) | |
1385 | /*@modifies fileSystem@*/; | |
885824d3 | 1386 | |
1387 | /*________________________________________________________________________ | |
1388 | * pwd.h | |
1389 | */ | |
1390 | ||
1391 | extern extern void | |
1392 | endpwent (void) | |
1393 | /*@modifies internalState@*/; | |
1394 | ||
1395 | extern /*@null@*/ struct passwd * | |
1396 | getpwent (void) | |
1397 | /*@modifies internalState@*/; | |
1398 | ||
1399 | extern int | |
1400 | setpassent (int stayopen) | |
1401 | /*@modifies internalState@*/; | |
1402 | ||
1403 | extern int | |
1404 | setpwent (void) | |
1405 | /*@modifies internalState@*/; | |
1406 | ||
1407 | /*________________________________________________________________________ | |
1408 | * grp.h | |
1409 | */ | |
1410 | ||
1411 | extern void | |
1412 | endgrent (void) | |
1413 | /*@modifies internalState@*/; | |
1414 | ||
1415 | extern /*@null@*/ struct group * | |
1416 | getgrent (void) | |
1417 | /*@modifies internalState@*/; | |
1418 | ||
1419 | extern int | |
1420 | setgrent (void) | |
1421 | /*@modifies internalState@*/; | |
1422 | ||
1423 | extern void | |
1424 | setgrfile (const char *name) | |
1425 | /*@modifies internalState@*/; | |
1426 | ||
1427 | extern int | |
1428 | setgroupent (int stayopen) | |
1429 | /*@modifies internalState@*/; | |
1430 | ||
1d239d69 | 1431 | /* |
1432 | ** sys/stat.h | |
1433 | ** | |
1434 | ** evans 2001-08-26 - updated from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstat.h.html | |
1435 | */ | |
1436 | ||
1437 | /* | |
1438 | ** struct stat replaces POSIX version - more required fields in Unix | |
1439 | */ | |
1440 | ||
8fe44445 | 1441 | /*@-redef@*/ /*@-matchfields@*/ |
1d239d69 | 1442 | struct stat { |
1443 | dev_t st_dev; /* ID of device containing file */ | |
1444 | ino_t st_ino; /* file serial number */ | |
1445 | mode_t st_mode; /* mode of file (see below) */ | |
1446 | nlink_t st_nlink; /* number of links to the file */ | |
1447 | uid_t st_uid; /* user ID of file */ | |
1448 | gid_t st_gid; /* group ID of file */ | |
1449 | dev_t st_rdev; /* device ID (if file is character or block special) */ | |
1450 | off_t st_size; /* file size in bytes (if file is a regular file) */ | |
1451 | time_t st_atime; /* time of last access */ | |
1452 | time_t st_mtime; /* time of last data modification */ | |
1453 | time_t st_ctime; /* time of last status change */ | |
1454 | blksize_t st_blksize; /* a filesystem-specific preferred I/O block size for | |
1455 | this object. In some filesystem types, this may | |
1456 | vary from file to file */ | |
1457 | blkcnt_t st_blocks; /* number of blocks allocated for this object */ | |
8fe44445 | 1458 | } ; |
1459 | /*@=redef@*/ /*@=matchfields@*/ | |
885824d3 | 1460 | |
1d239d69 | 1461 | /*@constant mode_t S_IWUSR@*/ |
1462 | /*@constant mode_t S_IXUSR@*/ | |
1463 | /*@constant mode_t S_IRWXG@*/ | |
1464 | /*@constant mode_t S_IRGRP@*/ | |
1465 | /*@constant mode_t S_IWGRP@*/ | |
1466 | /*@constant mode_t S_IXGRP@*/ | |
1467 | /*@constant mode_t S_IRWXO@*/ | |
1468 | /*@constant mode_t S_IROTH@*/ | |
1469 | /*@constant mode_t S_IWOTH@*/ | |
1470 | /*@constant mode_t S_IXOTH@*/ | |
1471 | /*@constant mode_t S_ISUID@*/ | |
1472 | /*@constant mode_t S_ISGID@*/ | |
1473 | /*@constant mode_t S_ISVTX@*/ | |
1474 | ||
1475 | # if 0 | |
345671f3 | 1476 | /*These are the old definitions - they don't appear to be in the Single UNIX Specification */ |
1477 | ||
885824d3 | 1478 | /*@constant int S_ISTXT@*/ |
1479 | /*@constant int S_IREAD@*/ | |
1480 | /*@constant int S_IWRITE@*/ | |
1481 | /*@constant int S_IEXEC@*/ | |
1482 | /*@constant int S_IFMT@*/ | |
1483 | /*@constant int S_IFIFO@*/ | |
1484 | /*@constant int S_IFCHR@*/ | |
1485 | /*@constant int S_IFDIR@*/ | |
1486 | /*@constant int S_IFBLK@*/ | |
1487 | /*@constant int S_IFREG@*/ | |
1488 | /*@constant int S_IFLNK@*/ | |
1489 | /*@constant int S_IFSOCK@*/ | |
1490 | /*@constant int S_ISVTX@*/ | |
1491 | /*@constant int S_ISVTX@*/ | |
1492 | /*@constant int SF_SETTABLE@*/ | |
1493 | /*@constant int SF_ARCHIVED@*/ | |
1494 | /*@constant int ACCESSPERMS@*/ | |
1495 | /*@constant int ALLPERMS@*/ | |
1496 | /*@constant int DEFFILEMODE@*/ | |
1497 | /*@constant int S_BLKSIZE@*/ | |
1498 | /*@constant int SF_IMMUTABLE@*/ | |
1499 | /*@constant int SF_APPEND@*/ | |
1500 | /*@constant int UF_NODUMP@*/ | |
1501 | /*@constant int UF_IMMUTABLE@*/ | |
1502 | /*@constant int UF_APPEND@*/ | |
1d239d69 | 1503 | # endif |
885824d3 | 1504 | |
1d239d69 | 1505 | int /*@alt lltX_bool@*/ S_ISBLK (/*@sef@*/ mode_t m) /*@*/; |
1506 | int /*@alt lltX_bool@*/ S_ISCHR (/*@sef@*/ mode_t m) /*@*/; | |
1507 | int /*@alt lltX_bool@*/ S_ISDIR (/*@sef@*/ mode_t m) /*@*/; | |
1508 | int /*@alt lltX_bool@*/ S_ISFIFO (/*@sef@*/ mode_t m) /*@*/; | |
1509 | int /*@alt lltX_bool@*/ S_ISREG (/*@sef@*/ mode_t m) /*@*/; | |
1510 | int /*@alt lltX_bool@*/ S_ISLNK (/*@sef@*/ mode_t m) /*@*/; | |
885824d3 | 1511 | |
1d239d69 | 1512 | int /*@alt lltX_bool@*/ S_TYPEISMQ (/*@sef@*/ struct stat *buf) /*@*/ ; |
1513 | int /*@alt lltX_bool@*/ S_TYPEISSEM (/*@sef@*/ struct stat *buf) /*@*/ ; | |
1514 | int /*@alt lltX_bool@*/ S_TYPEISSHM (/*@sef@*/ struct stat *buf) /*@*/ ; | |
885824d3 | 1515 | |
1d239d69 | 1516 | /* in POSIX: chmod, fstat, mkdir, mkfifo, stat, umask */ |
885824d3 | 1517 | |
1d239d69 | 1518 | int lstat(const char *, /*@out@*/ struct stat *) |
b87215ab | 1519 | /*:errorcode -1:*/ |
1520 | /*@modifies errno@*/ ; | |
1521 | ||
1d239d69 | 1522 | int mknod (const char *, mode_t, dev_t) |
1523 | /*@warn portability "The only portable use of mknod is to create FIFO-special file. If mode is not S_IFIFO or dev is not 0, the behaviour of mknod() is unspecified."@*/ | |
1524 | /*:errorcode -1:*/ | |
1525 | /*@modifies errno@*/ ; | |
885824d3 | 1526 | |
1d239d69 | 1527 | int chflags (const char *path, u_long flags) |
1528 | /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/ | |
1529 | /*@modifies fileSystem, errno@*/; | |
1530 | ||
1531 | int fchflags (int fd, u_long flags) | |
1532 | /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/ | |
1533 | /*@modifies fileSystem, errno@*/; | |
885824d3 | 1534 | |
b87215ab | 1535 | /* evans 2002-03-17: this was missing, reported by Ralf Wildenhues */ |
1536 | int fchmod(int fildes, mode_t mode) | |
1537 | /*@modifies fileSystem, errno@*/ ; | |
1538 | ||
1539 | /* | |
1540 | ** sys/statvfs.h | |
1541 | ** from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstatvfs.h.html | |
1542 | */ | |
1543 | ||
1544 | struct statvfs { | |
1545 | unsigned long f_bsize; | |
1546 | unsigned long f_frsize; | |
1547 | fsblkcnt_t f_blocks; | |
1548 | fsblkcnt_t f_bfree; | |
1549 | fsblkcnt_t f_bavail; | |
1550 | fsfilcnt_t f_files; | |
1551 | fsfilcnt_t f_ffree; | |
1552 | fsfilcnt_t f_favail; | |
1553 | unsigned long f_fsid; | |
1554 | unsigned long f_flag; | |
1555 | unsigned long f_namemax; | |
1556 | } ; | |
1557 | ||
1558 | /*@constant unsigned long ST_RDONLY; @*/ | |
1559 | /*@constant unsigned long ST_NOSUID; @*/ | |
1560 | ||
1561 | int fstatvfs (int fildes, /*@out@*/ struct statvfs *buf) | |
1562 | /*@modifies buf@*/ ; | |
1563 | ||
1564 | int statvfs (const char *path, /*@out@*/ struct statvfs *buf) | |
1565 | /*@modifies buf@*/ ; | |
1566 | ||
1567 | ||
885824d3 | 1568 | /*________________________________________________________________________ |
1569 | * stropts.h | |
1570 | */ | |
1571 | ||
1572 | /*@constant int FMNAMESZ@*/ | |
1573 | /*@constant int MSG_BAND@*/ | |
1574 | /*@constant int MSG_HIPRI@*/ | |
1575 | /*@constant int RS_HIPRI@*/ | |
1576 | /*@constant int S_INPUT@*/ | |
1577 | /*@constant int S_RDNORM@*/ | |
1578 | /*@constant int S_RDBAND@*/ | |
1579 | /*@constant int S_BANDURG@*/ | |
1580 | /*@constant int S_HIPRI@*/ | |
1581 | /*@constant int S_OUTPUT@*/ | |
1582 | /*@constant int S_WRNORM@*/ | |
1583 | /*@constant int S_WRBAND@*/ | |
1584 | /*@constant int S_MSG@*/ | |
1585 | /*@constant int S_ERROR@*/ | |
1586 | /*@constant int S_HANGUP@*/ | |
1587 | ||
1588 | struct strbuf { | |
1589 | int maxlen; | |
1590 | int len; | |
1591 | char *buf; | |
1592 | } | |
1593 | ||
1594 | struct str_mlist { | |
1595 | char l_name[]; | |
1596 | } | |
1597 | ||
1598 | struct str_list { | |
1599 | int sl_nmods; | |
1600 | struct str_mlist *sl_modlist; | |
1601 | } | |
1602 | ||
1603 | extern int | |
1604 | getmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *f) | |
1605 | /*@modifies *c, *d, errno@*/; | |
1606 | ||
1607 | extern int | |
1608 | getpmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *b, int *f) | |
1609 | /*@modifies *b, *c, *d, errno@*/; | |
1610 | ||
1611 | extern int | |
1612 | putmsg (int fd, const struct strbuf *c, const struct strbuf *d, int *f) | |
1613 | /*@modifies internalState, errno@*/; | |
1614 | ||
dfd82dce | 1615 | extern int putpmsg (int fd, const struct strbuf *c, const struct strbuf *d, int b, int *f) |
1616 | /*@modifies internalState, errno@*/; | |
885824d3 | 1617 | |
1618 | /*________________________________________________________________________ | |
1619 | * sys/resource.h | |
1620 | */ | |
1621 | ||
1622 | /*@constant int RLIMIT_CPU@*/ | |
1623 | /*@constant int RLIMIT_FSIZE@*/ | |
1624 | /*@constant int RLIMIT_DATA@*/ | |
1625 | /*@constant int RLIMIT_STACK@*/ | |
1626 | /*@constant int RLIMIT_CORE@*/ | |
1627 | /*@constant int RLIMIT_RSS@*/ | |
1628 | /*@constant int RLIMIT_MEMLOCK@*/ | |
1629 | /*@constant int RLIMIT_NPROC@*/ | |
1630 | /*@constant int RLIMIT_NOFILE@*/ | |
1631 | /*@constant int RLIM_NLIMITS@*/ | |
1632 | /*@constant int RLIM_INFINITY@*/ | |
1633 | /*@constant int PRIO_MIN@*/ | |
1634 | /*@constant int PRIO_MAX@*/ | |
1635 | /*@constant int PRIO_PROCESS@*/ | |
1636 | /*@constant int PRIO_PGRP@*/ | |
1637 | /*@constant int PRIO_USER@*/ | |
1638 | /*@constant int RUSAGE_SELF@*/ | |
1639 | /*@constant int RUSAGE_CHILDREN@*/ | |
1640 | ||
1641 | struct rusage { | |
1642 | struct timeval ru_utime; /* user time used */ | |
1643 | struct timeval ru_stime; /* system time used */ | |
1644 | long ru_maxrss; /* max resident set size */ | |
1645 | long ru_ixrss; /* integral shared memory size */ | |
1646 | long ru_idrss; /* integral unshared data " */ | |
1647 | long ru_isrss; /* integral unshared stack " */ | |
1648 | long ru_minflt; /* page reclaims */ | |
1649 | long ru_majflt; /* page faults */ | |
1650 | long ru_nswap; /* swaps */ | |
1651 | long ru_inblock; /* block input operations */ | |
1652 | long ru_oublock; /* block output operations */ | |
1653 | long ru_msgsnd; /* messages sent */ | |
1654 | long ru_msgrcv; /* messages received */ | |
1655 | long ru_nsignals; /* signals received */ | |
1656 | long ru_nvcsw; /* voluntary context switches */ | |
1657 | long ru_nivcsw; /* involuntary " */ | |
1658 | }; | |
1659 | ||
1660 | struct rlimit { | |
1661 | long rlim_cur; | |
1662 | long rlim_max; | |
1663 | }; | |
1664 | ||
1665 | struct loadavg { | |
1666 | unsigned long ldavg[3]; | |
1667 | long fscale; | |
1668 | }; | |
1669 | ||
1670 | extern int | |
1671 | getpriority (int which, int who) | |
1672 | /*@modifies errno@*/; | |
1673 | ||
1674 | extern int | |
1675 | getrlimit (int res, /*@out@*/ struct rlimit *rlp) | |
1676 | /*@modifies *rlp, errno@*/; | |
1677 | ||
1678 | extern int | |
1679 | getrusage (int who, /*@out@*/ struct rusage *rusage) | |
1680 | /*@modifies *rusage, errno@*/; | |
1681 | ||
1682 | extern int | |
1683 | setpriority (int which, int who, int prio) | |
1684 | /*@modifies errno, internalState@*/; | |
1685 | ||
1686 | extern int | |
1687 | setrlimit (int resource, const struct rlimit *rlp) | |
1688 | /*@modifies errno, internalState@*/; | |
1689 | ||
7272a1c1 | 1690 | |
1691 | /* | |
1692 | ** in <netdb.h> | |
1693 | */ | |
1694 | ||
1695 | struct servent | |
1696 | { | |
1697 | /*@observer@*/ char *s_name; /* Official service name. */ | |
1698 | /*@observer@*/ char **s_aliases; /* Alias list. */ | |
1699 | int s_port; /* Port number. */ | |
1700 | /*@observer@*/ char *s_proto; /* Protocol to use. */ | |
1701 | } ; | |
1702 | ||
1703 | /*@observer@*/ /*@dependent@*/ /*@null@*/ struct servent *getservbyname (const char *name, /*@null@*/ const char *proto) | |
1704 | /*@warn multithreaded "Unsafe in multithreaded applications, use getsrvbyname_r instead"@*/ ; | |
1705 | ||
1706 | struct servent *getservbyname_r (const char *name, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen) | |
1707 | /*@requires maxSet (buffer) >= buflen@*/ ; | |
1708 | ||
1709 | ||
1710 | /*@observer@*/ /*@dependent@*/ struct servent *getservbyport (int port, /*@null@*/ const char *proto) | |
1711 | /*@warn multithreaded "Unsafe in multithreaded applications, use getservbyport_r instead"@*/ ; | |
1712 | ||
1713 | struct servent *getservbyport_r (int port, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen) | |
1714 | /*@requires maxSet (buffer) >= buflen@*/ ; | |
1715 | ||
1716 | /*@null@*/ struct servent *getservent (void); | |
1717 | ||
1718 | /*@null@*/ struct servent *getservent_r (struct servent *result, char *buffer, int buflen); | |
1719 | ||
1720 | int setservent (int stayopen); | |
7272a1c1 | 1721 | int endservent (void); |
1722 | ||
7272a1c1 | 1723 | extern int h_errno; |
1724 | ||
1725 | /*@null@*/ /*@observer@*/ struct hostent *gethostbyname (/*@nullterminated@*/ /*@notnull@*/ const char *name) | |
1726 | /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyname_r instead"@*/ | |
1727 | /*@modifies h_errno@*/ ; | |
1728 | ||
1729 | struct hostent *gethostbyname_r (/*@nullterminated@*/ const char *name, /*@notnull@*/ /*@returned@*/ struct hostent *hent, /*@out@*/ /*@exposed@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop) | |
1730 | /*@requires maxSet(buffer) >= bufsize@*/ ; | |
1731 | ||
1732 | /*@null@*/ /*@observer@*/ struct hostent *gethostbyaddr (/*@notnull@*/ const void *addr, size_t addrlen, int type) | |
8fe44445 | 1733 | /*@requires maxRead(addr) == addrlen@*/ /*:i534 ??? is this right? */ |
7272a1c1 | 1734 | /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyaddr_r instead"@*/ |
1735 | /*@modifies h_errno@*/ ; | |
1736 | ||
1737 | struct hostent *gethostbyaddr_r (/*@notnull@*/ const void *addr, size_t addrlen, int type, | |
1738 | /*@returned@*/ /*@out@*/ struct hostent *hent, | |
1739 | /*@exposed@*/ /*@out@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop) | |
8fe44445 | 1740 | /*@requires maxRead(addr) == addrlen /\ maxSet(buffer) >= bufsize@*/ |
1741 | /*:i534 ??? is this right? */ ; | |
7272a1c1 | 1742 | |
1743 | /*@observer@*/ /*@null@*/ struct hostent *gethostent (void) | |
1744 | /*@warn multithreaded "Unsafe in multithreaded applications, use gethostent_r instead"@*/ ; | |
1745 | ||
1746 | struct hostent *gethostent_r (/*@out@*/ /*@returned@*/ struct hostent *hent, /*@exposed@*/ /*@out@*/ char *buffer, int bufsize) | |
1747 | /*@requires maxSet(buffer) >= bufsize@*/ ; | |
1748 | ||
8fe44445 | 1749 | /*:i534 need to annotate these: */ |
7272a1c1 | 1750 | |
8fe44445 | 1751 | struct hostent *fgethostent(FILE *f); |
7272a1c1 | 1752 | struct hostent *fgethostent_r(FILE*f, struct hostent *hent, char buffer, int bufsize); |
7272a1c1 | 1753 | void sethostent(int stayopen); |
7272a1c1 | 1754 | void endhostent(void); |
7272a1c1 | 1755 | void herror(const char *string); |
7272a1c1 | 1756 | char *hstrerror(int err); |
1757 | ||
1758 | struct hostent { | |
1759 | /*@observer@*/ /*@nullterminated@*/ char *h_name; /* official name of host */ | |
1760 | /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_aliases; /* alias list */ | |
1761 | int h_addrtype; /* host address type*/ | |
1762 | int h_length; /* length ofaddress*/ | |
1763 | /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_addr_list; /* list of addressesfrom name server */ | |
1764 | /*@observer@*/ /*@nullterminated@*/ char *h_addr; /* first address in list (backward compatibility) */ | |
1765 | } ; | |
1766 | ||
7272a1c1 | 1767 | /* |
1768 | ** unistd.h | |
b87215ab | 1769 | ** from http://www.opengroup.org/onlinepubs/007908799/xsh/unistd.h.html |
7272a1c1 | 1770 | */ |
1771 | ||
b87215ab | 1772 | /*@constant int _POSIX_VERSION@*/ |
1773 | /*@constant int _POSIX2_VERSION@*/ | |
1774 | /*@constant int _POSIX2_C_VERSION@*/ | |
1775 | /*@constant int _XOPEN_VERSION@*/ | |
1776 | /*@constant int _XOPEN_XCU_VERSION@*/ | |
1777 | ||
1778 | /* for access: */ | |
1779 | ||
1780 | /*@constant int R_OK@*/ | |
1781 | /*@constant int W_OK@*/ | |
1782 | /*@constant int X_OK@*/ | |
1783 | /*@constant int F_OK@*/ | |
1784 | ||
1785 | /* for confstr: */ | |
1786 | /*@constant int _CS_PATH@*/ | |
1787 | /*@constant int _CS_XBS5_ILP32_OFF32_CFLAGS@*/ | |
1788 | /*@constant int _CS_XBS5_ILP32_OFF32_LDFLAGS@*/ | |
1789 | /*@constant int _CS_XBS5_ILP32_OFF32_LIBS@*/ | |
1790 | /*@constant int _CS_XBS5_ILP32_OFF32_LINTFLAGS@*/ | |
1791 | /*@constant int _CS_XBS5_ILP32_OFFBIG_CFLAGS@*/ | |
1792 | /*@constant int _CS_XBS5_ILP32_OFFBIG_LDFLAGS@*/ | |
1793 | /*@constant int _CS_XBS5_ILP32_OFFBIG_LIBS@*/ | |
1794 | /*@constant int _CS_XBS5_ILP32_OFFBIG_LINTFLAGS@*/ | |
1795 | /*@constant int _CS_XBS5_LP64_OFF64_CFLAGS@*/ | |
1796 | /*@constant int _CS_XBS5_LP64_OFF64_LDFLAGS@*/ | |
1797 | /*@constant int _CS_XBS5_LP64_OFF64_LIBS@*/ | |
1798 | /*@constant int _CS_XBS5_LP64_OFF64_LINTFLAGS@*/ | |
1799 | /*@constant int _CS_XBS5_LPBIG_OFFBIG_CFLAGS@*/ | |
1800 | /*@constant int _CS_XBS5_LPBIG_OFFBIG_LDFLAGS@*/ | |
1801 | /*@constant int _CS_XBS5_LPBIG_OFFBIG_LIBS@*/ | |
1802 | /*@constant int _CS_XBS5_LPBIG_OFFBIG_LINTFLAGS@*/ | |
1803 | ||
1804 | /* name parameters to sysconf: */ | |
1805 | ||
1806 | /*@constant int _SC_2_C_BIND@*/ | |
1807 | /*@constant int _SC_2_C_DEV@*/ | |
1808 | /*@constant int _SC_2_C_VERSION@*/ | |
1809 | /*@constant int _SC_2_FORT_DEV@*/ | |
1810 | /*@constant int _SC_2_FORT_RUN@*/ | |
1811 | /*@constant int _SC_2_LOCALEDEF@*/ | |
1812 | /*@constant int _SC_2_SW_DEV@*/ | |
1813 | /*@constant int _SC_2_UPE@*/ | |
1814 | /*@constant int _SC_2_VERSION@*/ | |
1815 | /*@constant int _SC_ARG_MAX@*/ | |
1816 | /*@constant int _SC_AIO_LISTIO_MAX@*/ | |
1817 | /*@constant int _SC_AIO_MAX@*/ | |
1818 | /*@constant int _SC_AIO_PRIO_DELTA_MAX@*/ | |
1819 | /*@constant int _SC_ASYNCHRONOUS_IO@*/ | |
1820 | /*@constant int _SC_ATEXIT_MAX@*/ | |
1821 | /*@constant int _SC_BC_BASE_MAX@*/ | |
1822 | /*@constant int _SC_BC_DIM_MAX@*/ | |
1823 | /*@constant int _SC_BC_SCALE_MAX@*/ | |
1824 | /*@constant int _SC_BC_STRING_MAX@*/ | |
1825 | /*@constant int _SC_CHILD_MAX@*/ | |
1826 | /*@constant int _SC_CLK_TCK@*/ | |
1827 | /*@constant int _SC_COLL_WEIGHTS_MAX@*/ | |
1828 | /*@constant int _SC_DELAYTIMER_MAX@*/ | |
1829 | /*@constant int _SC_EXPR_NEST_MAX@*/ | |
1830 | /*@constant int _SC_FSYNC@*/ | |
1831 | /*@constant int _SC_GETGR_R_SIZE_MAX@*/ | |
1832 | /*@constant int _SC_GETPW_R_SIZE_MAX@*/ | |
1833 | /*@constant int _SC_IOV_MAX@*/ | |
1834 | /*@constant int _SC_JOB_CONTROL@*/ | |
1835 | /*@constant int _SC_LINE_MAX@*/ | |
1836 | /*@constant int _SC_LOGIN_NAME_MAX@*/ | |
1837 | /*@constant int _SC_MAPPED_FILES@*/ | |
1838 | /*@constant int _SC_MEMLOCK@*/ | |
1839 | /*@constant int _SC_MEMLOCK_RANGE@*/ | |
1840 | /*@constant int _SC_MEMORY_PROTECTION@*/ | |
1841 | /*@constant int _SC_MESSAGE_PASSING@*/ | |
1842 | /*@constant int _SC_MQ_OPEN_MAX@*/ | |
1843 | /*@constant int _SC_MQ_PRIO_MAX@*/ | |
1844 | /*@constant int _SC_NGROUPS_MAX@*/ | |
1845 | /*@constant int _SC_OPEN_MAX@*/ | |
1846 | /*@constant int _SC_PAGESIZE@*/ | |
1847 | /*@constant int _SC_PAGE_SIZE@*/ | |
1848 | /*@constant int _SC_PASS_MAX@*/ | |
1849 | /*@constant int _SC_PRIORITIZED_IO@*/ | |
1850 | /*@constant int _SC_PRIORITY_SCHEDULING@*/ | |
1851 | /*@constant int _SC_RE_DUP_MAX@*/ | |
1852 | /*@constant int _SC_REALTIME_SIGNALS@*/ | |
1853 | /*@constant int _SC_RTSIG_MAX@*/ | |
1854 | /*@constant int _SC_SAVED_IDS@*/ | |
1855 | /*@constant int _SC_SEMAPHORES@*/ | |
1856 | /*@constant int _SC_SEM_NSEMS_MAX@*/ | |
1857 | /*@constant int _SC_SEM_VALUE_MAX@*/ | |
1858 | /*@constant int _SC_SHARED_MEMORY_OBJECTS@*/ | |
1859 | /*@constant int _SC_SIGQUEUE_MAX@*/ | |
1860 | /*@constant int _SC_STREAM_MAX@*/ | |
1861 | /*@constant int _SC_SYNCHRONIZED_IO@*/ | |
1862 | /*@constant int _SC_THREADS@*/ | |
1863 | /*@constant int _SC_THREAD_ATTR_STACKADDR@*/ | |
1864 | /*@constant int _SC_THREAD_ATTR_STACKSIZE@*/ | |
1865 | /*@constant int _SC_THREAD_DESTRUCTOR_ITERATIONS@*/ | |
1866 | /*@constant int _SC_THREAD_KEYS_MAX@*/ | |
1867 | /*@constant int _SC_THREAD_PRIORITY_SCHEDULING@*/ | |
1868 | /*@constant int _SC_THREAD_PRIO_INHERIT@*/ | |
1869 | /*@constant int _SC_THREAD_PRIO_PROTECT@*/ | |
1870 | /*@constant int _SC_THREAD_PROCESS_SHARED@*/ | |
1871 | /*@constant int _SC_THREAD_SAFE_FUNCTIONS@*/ | |
1872 | /*@constant int _SC_THREAD_STACK_MIN@*/ | |
1873 | /*@constant int _SC_THREAD_THREADS_MAX@*/ | |
1874 | /*@constant int _SC_TIMERS@*/ | |
1875 | /*@constant int _SC_TIMER_MAX@*/ | |
1876 | /*@constant int _SC_TTY_NAME_MAX@*/ | |
1877 | /*@constant int _SC_TZNAME_MAX@*/ | |
1878 | /*@constant int _SC_VERSION@*/ | |
1879 | /*@constant int _SC_XOPEN_VERSION@*/ | |
1880 | /*@constant int _SC_XOPEN_CRYPT@*/ | |
1881 | /*@constant int _SC_XOPEN_ENH_I18N@*/ | |
1882 | /*@constant int _SC_XOPEN_SHM@*/ | |
1883 | /*@constant int _SC_XOPEN_UNIX@*/ | |
1884 | /*@constant int _SC_XOPEN_XCU_VERSION@*/ | |
1885 | /*@constant int _SC_XOPEN_LEGACY@*/ | |
1886 | /*@constant int _SC_XOPEN_REALTIME@*/ | |
1887 | /*@constant int _SC_XOPEN_REALTIME_THREADS@*/ | |
1888 | /*@constant int _SC_XBS5_ILP32_OFF32@*/ | |
1889 | /*@constant int _SC_XBS5_ILP32_OFFBIG@*/ | |
1890 | /*@constant int _SC_XBS5_LP64_OFF64@*/ | |
1891 | /*@constant int _SC_XBS5_LPBIG_OFFBIG@*/ | |
1892 | ||
1893 | ||
1894 | int access(const char *, int) /*@modifies errno@*/ /*:errorcode -1:*/ ; | |
1895 | unsigned int alarm (unsigned int) /*@modifies internalState@*/ ; | |
1896 | ||
1897 | int brk(void *) | |
1898 | /*@modifies errno@*/ | |
1899 | /*:errorcode -1:*/ | |
1900 | /*@warn legacy "brk is obsolete"@*/ ; | |
1901 | ||
1902 | int chdir (const char *) | |
1903 | /*@modifies internalState, errno@*/ | |
1904 | /*:errorcode -1:*/ ; | |
1905 | ||
1906 | int chown (const char *, uid_t, gid_t) | |
1907 | /*@modifies internalState, errno@*/ | |
1908 | /*:errorcode -1:*/ ; | |
1909 | ||
1910 | int close (int) | |
1911 | /*@modifies internalState, errno@*/ | |
1912 | /*:errorcode -1:*/ ; | |
1913 | ||
1914 | size_t confstr(int, /*@null@*/ char *, size_t) | |
1915 | /*@globals internalState@*/ | |
1916 | /*@modifies errno@*/ | |
1917 | /*:errorcode 0:*/ ; | |
1918 | ||
1919 | /*@dependent@*/ /*@null@*/ char *crypt(const char *, const char *) | |
1920 | /*@modifies errno, internalState@*/ ; | |
1921 | ||
1922 | /*@dependent@*/ /*@null@*/ char *ctermid(/*@returned@*/ /*@null@*/ /*@out@*/ char *s) | |
1923 | /*@modifies s@*/ ; | |
1924 | ||
1925 | /*@null@*/ /*@dependent@*/ char *cuserid (/*@null@*/ /*@returned@*/ char *s) | |
1926 | /*@warn legacy "cuserid is obsolete"@*/ | |
1927 | /*@modifies s@*/ ; | |
1928 | ||
1929 | int dup(int) | |
1930 | /*@modifies errno, internalState@*/ | |
1931 | /*:errorcode -1:*/ ; | |
1932 | ||
1933 | int dup2(int, int) | |
1934 | /*@modifies errno, internalState@*/ | |
1935 | /*:errorcode -1:*/ ; | |
1936 | ||
1937 | void encrypt(char p_block[], int) | |
1938 | /*@requires maxSet(p_block) == 63@*/ | |
1939 | /*@modifies p_block, errno@*/ ; | |
1940 | ||
1941 | extern char **environ; | |
1942 | ||
1943 | int execl (const char *, const char *, ...) | |
1944 | /*@modifies errno, internalState@*/ | |
1945 | /*:errorcode -1:*/ ; | |
1946 | ||
1947 | int execle(const char *, const char *, ...) | |
1948 | /*@modifies errno, internalState@*/ | |
1949 | /*:errorcode -1:*/ ; | |
1950 | ||
1951 | int execlp(const char *, const char *, ...) | |
1952 | /*@modifies errno, internalState@*/ | |
1953 | /*:errorcode -1:*/ ; | |
1954 | ||
1955 | int execv(const char *, char *const []) | |
1956 | /*@modifies errno, internalState@*/ | |
1957 | /*:errorcode -1:*/ ; | |
1958 | ||
1959 | int execve(const char *, char *const [], char *const []) | |
1960 | /*@modifies errno, internalState@*/ | |
1961 | /*:errorcode -1:*/ ; | |
1962 | ||
1963 | int execvp(const char *, char *const []) | |
1964 | /*@modifies errno, internalState@*/ | |
1965 | /*:errorcode -1:*/ ; | |
1966 | ||
1967 | /*@exits@*/ void _exit (int); | |
1968 | ||
1969 | int fchown (int, uid_t, gid_t) | |
1970 | /*@modifies errno, fileSystem@*/ | |
1971 | /*:errorcode -1:*/ ; | |
1972 | ||
1973 | int fchdir (int) | |
1974 | /*@modifies errno, fileSystem@*/ | |
1975 | /*:errorcode -1:*/ ; | |
1976 | ||
1977 | int fdatasync (int) | |
1978 | /*@modifies errno, fileSystem@*/ | |
1979 | /*:errorcode -1:*/ ; | |
1980 | ||
1981 | pid_t fork (void) | |
1982 | /*@modifies errno, internalState@*/ | |
1983 | /*:errorcode -1:*/ ; | |
1984 | ||
1985 | long int fpathconf(int, int) | |
1986 | /*@modifies errno, internalState@*/ | |
1987 | /*:errorcode -1:*/ ; | |
1988 | ||
1989 | int fsync(int) | |
1990 | /*@modifies errno, fileSystem@*/ | |
1991 | /*:errorcode -1:*/ ; | |
1992 | ||
1993 | int ftruncate(int, off_t) | |
1994 | /*@modifies errno, fileSystem@*/ | |
1995 | /*:errorcode -1:*/ ; | |
1996 | ||
1997 | /*@null@*/ char *getcwd (/*@returned@*/ char *buf, size_t size) | |
1998 | /*@requires maxSet(buf) >= size;@*/ | |
1999 | /*@modifies errno@*/ ; | |
2000 | ||
2001 | int getdtablesize (void) | |
2002 | /*@warn legacy "getdtablesize is obsolete"@*/ ; | |
2003 | ||
2004 | gid_t getegid (void) /*@globals internalState*/ ; | |
2005 | uid_t geteuid (void) /*@globals internalState*/ ; | |
2006 | gid_t getgid (void) /*@globals internalState*/ ; | |
2007 | ||
2008 | int getgroups (int gidsetsize, gid_t grouplist[]) | |
2009 | /*@requires maxSet(grouplist) >= gidsetsize@*/ | |
2010 | /*@modifies errno@*/ | |
2011 | /*:errorcode -1:*/ ; | |
2012 | ||
2013 | long gethostid (void) /*@globals internalState@*/ ; | |
2014 | ||
2015 | /*@null@*/ /*@dependent@*/ char *getlogin (void) | |
2016 | /*@modifies errno@*/ ; | |
2017 | ||
2018 | int getlogin_r (char *name, size_t namesize) | |
2019 | /*@requires maxSet(name) >= namesize@*/ | |
2020 | /*:errorcode !0:*/ ; | |
2021 | ||
2022 | extern char *optarg; | |
2023 | extern int optind; | |
2024 | extern int opterr; | |
2025 | extern int optopt; | |
2026 | ||
2027 | int getopt(int, char * const [], const char *) | |
2028 | /*@modifies optind, opterr, optopt, errno@*/ | |
2029 | /*:errorcode -1:*/ ; | |
2030 | ||
2031 | int getpagesize(void) | |
2032 | /*@warn legacy "getpagesize is obsolete"@*/ ; | |
2033 | ||
2034 | /*@dependent@*/ /*@null@*/ char *getpass(/*@nullterminated@*/ const char *) | |
2035 | /*@warn legacy "getpass is obsolete"@*/ ; | |
2036 | ||
2037 | pid_t getpgid(pid_t) | |
2038 | /*@modifies errno@*/ | |
2039 | /*@globals internalState@*/ | |
2040 | /*:errorcode (pid_t)-1:*/ ; | |
2041 | ||
2042 | pid_t getpgrp(void) /*@globals internalState*/ ; | |
2043 | ||
2044 | pid_t getpid(void) /*@globals internalState*/ ; | |
2045 | pid_t getppid(void) /*@globals internalState*/ ; | |
2046 | ||
2047 | pid_t getsid(pid_t) | |
2048 | /*@modifies errno@*/ | |
2049 | /*@globals internalState@*/ | |
2050 | /*:errorcode (pid_t)-1:*/ ; | |
2051 | ||
2052 | uid_t getuid(void) /*@globals internalState@*/ ; | |
2053 | ||
2054 | /*@null@*/ char *getwd (/*@returned@*/ char *path_name) | |
2055 | /*@modifies path_name@*/ ; | |
2056 | ||
2057 | int isatty(int) | |
2058 | /*@globals internalState@*/ | |
2059 | /*@modifies errno@*/ | |
2060 | /*:errorcode 0:*/ ; | |
2061 | ||
2062 | int lchown(const char *, uid_t, gid_t) | |
2063 | /*@modifies errno, fileSystem@*/ | |
2064 | /*:errorcode -1:*/ ; | |
2065 | ||
2066 | int link(const char *, const char *) | |
2067 | /*@modifies errno, fileSystem@*/ | |
2068 | /*:errorcode -1:*/ ; | |
2069 | ||
2070 | int lockf(int, int, off_t) | |
2071 | /*@modifies errno, fileSystem@*/ | |
2072 | /*:errorcode -1:*/ ; | |
2073 | ||
2074 | off_t lseek(int, off_t, int) | |
2075 | /*@modifies errno, fileSystem@*/ | |
2076 | /*:errorcode (off_t)-1:*/ ; | |
2077 | ||
2078 | int nice(int) | |
2079 | /*@modifies errno, fileSystem@*/ | |
2080 | /*:errorcode -1:*/ ; | |
2081 | ||
2082 | long int pathconf(const char *, int) | |
2083 | /*@modifies errno, internalState@*/ | |
2084 | /*:errorcode -1:*/ ; | |
2085 | ||
2086 | int pause(void) | |
2087 | /*@modifies errno, internalState@*/ | |
2088 | /*:errorcode -1:*/ ; | |
2089 | ||
2090 | int pipe(int p[]) | |
2091 | /*@requires maxRead(p) == 1@*/ | |
2092 | /*@modifies errno, fileSystem@*/ | |
2093 | /*:errorcode -1:*/ ; | |
2094 | ||
2095 | ssize_t pread(int, /*@out@*/ void *buf, size_t nbyte, off_t offset) | |
2096 | /*@modifies errno, fileSystem@*/ | |
2097 | /*@requires maxSet(buf) >= (nbyte - 1) @*/ | |
2098 | /*@ensures maxRead(buf) >= nbyte @*/ | |
2099 | /*:errorcode -1:*/ ; | |
2100 | ||
2101 | int pthread_atfork(void (*)(void), void (*)(void), void(*)(void)) | |
2102 | /*@modifies errno, fileSystem@*/ | |
2103 | /*:errorcode !0:*/ ; | |
2104 | ||
2105 | ssize_t pwrite(int, const void *buf, size_t nbyte, off_t) | |
2106 | /*@requires maxRead(buf) >= nbyte@*/ | |
2107 | /*@modifies errno, fileSystem@*/ | |
2108 | /*:errorcode -1:*/ ; | |
2109 | ||
2110 | /* ssize_t read(int, void *, size_t); in posix.h */ | |
2111 | ||
2112 | int readlink(const char *, char *buf, size_t bufsize) | |
2113 | /*@requires maxSet(buf) >= (bufsize - 1)@*/ | |
2114 | /*@modifies errno, fileSystem, *buf@*/ | |
2115 | /*:errorcode -1:*/ ; | |
2116 | ||
2117 | /* int rmdir(const char *); in posix.h */ | |
2118 | ||
2119 | void *sbrk(intptr_t) | |
2120 | /*@modifies errno@*/ | |
2121 | /*:errorcode (void *)-1:*/ | |
2122 | /*@warn legacy "sbrk is obsolete"@*/ ; | |
2123 | ||
2124 | /* int setgid(gid_t); | |
2125 | int setpgid(pid_t, pid_t); | |
2126 | */ | |
2127 | ||
2128 | pid_t setpgrp(void) /*@modifies internalState@*/ ; | |
2129 | ||
2130 | int setregid(gid_t, gid_t) | |
2131 | /*@modifies errno, internalState@*/ | |
2132 | /*:errorcode -1:*/ ; | |
2133 | ||
2134 | int setreuid(uid_t, uid_t) | |
2135 | /*@modifies errno, internalState@*/ | |
2136 | /*:errorcode -1:*/ ; | |
2137 | ||
2138 | pid_t setsid(void) | |
2139 | /*@modifies errno, internalState@*/ | |
2140 | /*:errorcode (pid_t) -1:*/ ; | |
2141 | ||
2142 | int setuid(uid_t) | |
2143 | /*@modifies errno, internalState@*/ | |
2144 | /*:errorcode -1:*/ ; | |
2145 | ||
2146 | unsigned int sleep(unsigned int) | |
2147 | /*@modifies systemState@*/ ; | |
2148 | ||
2149 | void swab(/*@unique@*/ const void *src, /*@unique@*/ void *dest, ssize_t nbytes) | |
2150 | /*@requires maxSet(dest) >= (nbytes - 1)@*/ ; | |
2151 | ||
2152 | int symlink(const char *, const char *) | |
2153 | /*@modifies errno, fileSystem@*/ | |
2154 | /*:errorcode -1:*/ ; | |
2155 | ||
2156 | void sync(void) /*@modifies systemState@*/ ; | |
2157 | ||
2158 | long int sysconf(int) | |
2159 | /*@modifies errno, systemState@*/ | |
2160 | /*:errorcode -1:*/ ; | |
2161 | ||
2162 | pid_t tcgetpgrp(int) | |
2163 | /*@globals systemState@*/ | |
2164 | /*@modifies errno@*/ | |
2165 | /*:errorcode -1:*/ ; | |
2166 | ||
2167 | int tcsetpgrp(int, pid_t) | |
2168 | /*@modifies errno, systemState@*/ | |
2169 | /*:errorcode -1:*/ ; | |
2170 | ||
2171 | int truncate(const char *, off_t) | |
2172 | /*@modifies errno, fileSystem@*/ | |
2173 | /*:errorcode -1:*/ ; | |
2174 | ||
2175 | /*@dependent@*/ /*@null@*/ char *ttyname(int) | |
2176 | /*@globals systemState@*/ | |
2177 | /*@modifies errno@*/ | |
2178 | /*:errorcode -1:*/ ; | |
2179 | ||
2180 | int ttyname_r(int, char *name, size_t namesize) | |
2181 | /*@requires maxSet(name) >= (namesize - 1)@*/ ; | |
2182 | /*:errorcode !0:*/ ; | |
2183 | ||
2184 | useconds_t ualarm(useconds_t, useconds_t) | |
2185 | /*@modifies systemState@*/ ; | |
2186 | ||
2187 | int unlink(const char *) | |
2188 | /*@modifies fileSystem, errno@*/ | |
2189 | /*:errorcode -1:*/ ; | |
2190 | ||
2191 | int usleep(useconds_t) | |
2192 | /*@modifies fileSystem, errno@*/ | |
2193 | /*:errorcode -1:*/ ; | |
2194 | ||
2195 | pid_t vfork(void) | |
2196 | /*@modifies fileSystem, errno@*/ | |
2197 | /*:errorcode -1:*/ ; | |
2198 | ||
2199 | /* in posix.h ssize_t write(int, const void *, size_t); */ | |
2200 | ||
2201 | ||
7272a1c1 | 2202 | int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path) |
b87215ab | 2203 | /*@modifies internalState, errno@*/ |
2204 | /*:errorcode -1:*/ | |
2205 | /*@warn superuser "Only super-user processes may call chroot."@*/ ; | |
7272a1c1 | 2206 | |
2207 | int fchroot (int fildes) | |
2208 | /*:statusreturn@*/ | |
2209 | /*@warn superuser "Only super-user processes may call fchroot."@*/ ; | |
1d239d69 | 2210 | |
b87215ab | 2211 | |
1d239d69 | 2212 | /* |
2213 | ** ctype.h | |
2214 | ** | |
2215 | ** evans 2001-08-26 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/ctype.h.html | |
2216 | */ | |
2217 | ||
2218 | # ifdef STRICT | |
2219 | lltX_bool isascii(int) /*@*/ ; | |
2220 | lltX_bool toascii(int) /*@*/ ; | |
2221 | char _toupper(/*@sef@*/ int) /*@*/ ; | |
2222 | char _tolower(/*@sef@*/ int) /*@*/ ; | |
2223 | # else | |
2224 | lltX_bool /*@alt int@*/ isascii(int /*@alt unsigned char@*/) /*@*/ ; | |
2225 | lltX_bool /*@alt int@*/ toascii(int /*@alt unsigned char@*/); | |
2226 | char /*@alt int@*/ _toupper(/*@sef@*/ int /*@alt unsigned char@*/); | |
2227 | char /*@alt int@*/ _tolower(/*@sef@*/ int /*@alt unsigned char@*/); | |
2228 | # endif | |
2229 | ||
2230 | /* other ctype.h functions in ansi.h */ | |
345671f3 | 2231 | |
2232 | /* | |
2233 | ** stdlib.h | |
2234 | ** | |
2235 | ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/drand48.html | |
2236 | */ | |
2237 | ||
2238 | double drand48 (void) /*@modifies internalState@*/ ; | |
8fe44445 | 2239 | double erand48 (unsigned short int /*@-fixedformalarray@*/ xsubi[3] /*@=fixedformalarray@*/ ) |
2240 | /*@modifies internalState@*/ ; | |
2241 | ||
345671f3 | 2242 | void srand48 (long int seedval) /*@modifies internalState@*/ ; |
2243 | ||
2244 | /* | |
2245 | ** netinet/in.h | |
2246 | ** | |
2247 | ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xns/netinetin.h.html | |
2248 | */ | |
2249 | ||
2250 | typedef /*@unsignedintegraltype@*/ in_port_t; /* An unsigned integral type of exactly 16 bits. */ | |
2251 | typedef /*@unsignedintegraltype@*/ in_addr_t; /* An unsigned integral type of exactly 32 bits. */ | |
2252 | ||
2253 | typedef /*@unsignedintegraltype@*/ sa_family_t; | |
2254 | ||
2255 | struct in_addr { | |
2256 | in_addr_t s_addr; | |
2257 | } ; | |
2258 | ||
2259 | struct sockaddr_in { | |
2260 | sa_family_t sin_family; | |
2261 | in_port_t sin_port; | |
2262 | struct in_addr sin_addr; | |
2263 | unsigned char sin_zero[8]; | |
2264 | } ; | |
2265 | ||
2266 | ||
2267 | /* The <netinet/in.h> header defines the following macros for use as values of the level argument of | |
2268 | getsockopt() and setsockopt(): | |
2269 | */ | |
2270 | ||
2271 | /*@constant int IPPROTO_IP@*/ | |
2272 | /*@constant int IPPROTO_ICMP@*/ | |
2273 | /*@constant int IPPROTO_TCP@*/ | |
2274 | /*@constant int IPPROTO_UDP@*/ | |
2275 | ||
2276 | /* The <netinet/in.h> header defines the following macros for use as destination addresses for connect(), sendmsg() and sendto(): | |
2277 | */ | |
2278 | ||
2279 | /*@constant in_addr_t INADDR_ANY@*/ | |
2280 | /*@constant in_addr_t INADDR_BROADCAST@*/ | |
2281 | ||
8fe44445 | 2282 | /* |
2283 | ** arpa/inet.h | |
2284 | */ | |
2285 | ||
2286 | in_addr_t htonl (in_addr_t hostlong) /*@*/ ; | |
2287 | in_port_t htons (in_port_t hostshort) /*@*/ ; | |
2288 | in_addr_t ntohl (in_addr_t netlong) /*@*/ ; | |
2289 | in_port_t ntohs (in_port_t netshort) /*@*/ ; | |
2290 | ||
345671f3 | 2291 | /* |
2292 | ** dirent.h | |
2293 | ** | |
2294 | ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/dirent.h.html | |
2295 | */ | |
2296 | ||
8fe44445 | 2297 | /*@-redef@*/ /*@-matchfields@*/ /* Has d_ino field, not in posix (?) */ |
2298 | ||
345671f3 | 2299 | struct dirent |
2300 | { | |
2301 | ino_t d_ino; | |
2302 | char d_name[]; | |
8fe44445 | 2303 | } ; |
2304 | ||
2305 | /*@=redef@*/ /*@=matchfields@*/ | |
345671f3 | 2306 | |
2307 | typedef /*@abstract@*/ DIR; | |
2308 | ||
8fe44445 | 2309 | /*:i32 need to check annotations on these */ |
2310 | ||
345671f3 | 2311 | int closedir (DIR *) /*:errorcode -1*/ ; |
86d93ed3 | 2312 | /*@null@*/ /*@dependent@*/ DIR *opendir(const char *) /*@modifies errno, fileSystem@*/ ; |
d5047b91 | 2313 | |
2314 | /* in posix.h: struct dirent *readdir(DIR *); */ | |
2315 | ||
2316 | int readdir_r (DIR *, struct dirent *, /*@out@*/ struct dirent **result) | |
2317 | /*@modifies *result@*/ | |
2318 | /*:errorcode !0:*/ ; | |
2319 | ||
345671f3 | 2320 | void rewinddir(DIR *); |
2321 | void seekdir(DIR *, long int); | |
2322 | long int telldir(DIR *); | |
2323 | ||
2324 | /*drl added these functions | |
2325 | stpcpy and stpncpy are found on linux but | |
2326 | don't seem to be present on other unixes | |
2327 | ||
2328 | thanks to Jeff Johnson for pointing out that | |
2329 | these functions were in the unix library | |
2330 | */ | |
2331 | ||
2332 | /* this function is like strcpy but it reutrns a pointer to the null terminated character in dest instead of the beginning of dest */ | |
2333 | ||
2334 | extern char * stpcpy(/*@out@*/ /*@returned@*/ char * dest, const char * src) | |
2335 | /*@modifies *dest @*/ | |
2336 | /*@requires maxSet(dest) >= maxRead(src) @*/ | |
2337 | /*@ensures MaxRead(dest) == MaxRead (src) /\ MaxRead(result) == 0 /\ MaxSet(result) == ( maxSet(dest) - MaxRead(src) ); @*/; | |
2338 | ||
2339 | ||
2340 | extern char * stpncpy(/*@out@*/ /*@returned@*/ char * dest, | |
2341 | const char * src, size_t n) | |
2342 | /*@modifies *dest @*/ | |
2343 | /*@requires MaxSet(dest) >= ( n - 1 ); @*/ /*@ensures MaxRead (src) >= MaxRead(dest) /\ MaxRead (dest) <= n; @*/ | |
2344 | ; | |
2345 | ||
ed309918 | 2346 | /* drl added 09-25-001 |
2347 | Alexander Ma pointed out these were missing | |
2348 | */ | |
2349 | ||
ccf415d0 | 2350 | int usleep (useconds_t useconds) /*@modifies systemState, errno@*/ |
2351 | /*error -1 sucess 0 */ | |
2352 | /* warn opengroup unix specification recommends using setitimer(), timer_create(), timer_delete(), timer_getoverrun(), timer_gettime() or | |
2353 | timer_settime() instead of this interface. | |
2354 | */ | |
2355 | ; | |
2356 | ||
e5f31c00 | 2357 | |
2358 | /* drl added 10-27-001 */ | |
86d93ed3 | 2359 | /*not sure what the exact size of this is |
e5f31c00 | 2360 | also can IPv6 use this function? |
2361 | */ | |
86d93ed3 | 2362 | /*I'm going to assume that the address had the format: |
2363 | "###.###.###.###" which is 16 bytes*/ | |
e5f31c00 | 2364 | |
86d93ed3 | 2365 | /*@kept@*/ char *inet_ntoa(struct in_addr in) |
e5f31c00 | 2366 | /*@ensures maxSet(result) <= 15 /\ maxRead(result) <= 15 @*/ |
2367 | ; | |
2368 | ||
2369 | ||
ed309918 | 2370 | extern double hypot(double x, double y) /*@modifies errno@*/ /*error errno only*/; |
2371 | ||
2372 | ||
2373 | extern double j0(double x) /*@modifies errno @*/ /*error 0 or NaN */; | |
2374 | extern double j1(double x) /*@modifies errno @*/ /*error 0 or NaN */; | |
2375 | extern double jn(int n, double x) /*@modifies errno @*/ /*error 0 or NaN */; | |
2376 | ||
2377 | extern double y0(double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */ ; | |
2378 | extern double y1 (double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */; | |
2379 | extern double yn (int n, double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */; | |
2380 | ||
2381 | extern double acosh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno*/; | |
2382 | extern double asinh(double x) /*@modifies errno @*/ /*error NaN and may errno */; | |
2383 | ||
2384 | extern double atanh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno */ ; | |
2385 | ||
2386 | extern double lgamma(double x) /*@modifies errno @*/ /*error NaN or HUGE_VAL may set errno */; | |
2387 | ||
2388 | extern int signgam ; | |
2389 | ||
2390 | extern double erf(double x) /*@modifies errno @*/ /*error NaN or 0 may set errno */; | |
2391 | ||
2392 | extern double erfc (double x) /*@modifies errno @*/ /*error NaN or 0 | |
2393 | may set errno */; | |
2394 | ||
2395 | ||
2396 | ||
2397 | ||
2398 | ||
2399 |