10 ** evans - 2001-08-27: from http://www.opengroup.org/onlinepubs/007908799/xsh/systypes.h.html
13 typedef /*@integraltype@*/ blkcnt_t;
14 typedef /*@integraltype@*/ blksize_t;
16 /*@-redef@*/ /* These are also defined by ansi.h: */
17 typedef /*@integraltype@*/ clock_t;
18 typedef /*@integraltype@*/ dev_t;
19 typedef /*@integraltype@*/ gid_t;
20 typedef /*@unsignedintegraltype@*/ ino_t;
21 typedef /*@integraltype@*/ mode_t;
22 typedef /*@integraltype@*/ nlink_t;
23 typedef /*@integraltype@*/ off_t;
24 typedef /*@integraltype@*/ pid_t;
25 typedef /*@integraltype@*/ time_t;
26 typedef /*@integraltype@*/ uid_t;
30 typedef /*@integraltype@*/ clockid_t;
31 typedef /*@unsignedintegraltype@*/ fsblkcnt_t;
32 typedef /*@unsignedintegraltype@*/ fsfilcnt_t;
33 typedef /*@integraltype@*/ id_t;
35 typedef /*@integraltype@*/ key_t;
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;
47 typedef /*@integraltype@*/ timer_t;
48 typedef /*@unsignedintegraltype@*/ useconds_t;
51 ** Extra stuff in some unixen, not in posix.
54 extern /*@unchecked@*/ int signgam;
56 /*@-redef@*/ /* Defined by ansi: */
57 typedef /*@integraltype@*/ clockid_t;
60 extern void bcopy (char *b1, /*@out@*/ char *b2, int length)
61 /*@modifies *b2@*/ ; /* Yes, the second parameter is the out param! */
63 extern int /*@alt lltX_bool@*/ bcmp (char *b1, char *b2, int length) /*@*/ ;
64 /* Return value is NOT like strcmp! */
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@*/ ;
71 setvbuf_unlocked (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
72 int mode, size_t size)
73 /*@modifies internalState@*/ ;
76 setbuffer (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, int size)
77 /*@modifies internalState@*/ ;
79 extern void setlinebuf (FILE *stream) /*@modifies internalState@*/ ;
81 extern int strerror_r (int errnum, /*@out@*/ char *strerrbuf, int buflen)
82 /*@modifies strerrbuf@*/ ;
85 fread_unlocked (/*@out@*/ void *ptr, size_t size, size_t nitems,
87 /*@modifies *stream, *ptr;@*/ ;
90 fwrite_unlocked (void *pointer, size_t size, size_t num_items, FILE *stream)
91 /*@modifies *stream;@*/ ;
93 extern void /*@alt void * @*/
94 memccpy (/*@returned@*/ /*@out@*/ void *s1,
95 /*@unique@*/ void *s2, int c, size_t n)
98 extern int strcasecmp (char *s1, char *s2) /*@*/ ;
99 extern int strncasecmp (char *s1, char *s2, int n) /*@*/ ;
100 extern /*@null@*/ /*@only@*/ char *strdup (char *s) /*@*/ ;
102 extern /*@null@*/ /*@dependent@*/ char *
103 index (/*@returned@*/ char *s, char c) /*@*/ ;
105 extern /*@null@*/ /*@dependent@*/ char *
106 rindex (/*@returned@*/ char *s, char c) /*@*/ ;
109 These are in ISO C99. Moved to standard.h:
110 extern double cbrt (double x) /*@modifies errno@*/ ;
111 extern double rint (double x) /*@*/ ;
112 extern double trunc (double x) /*@*/ ;
116 /*@constant int ENOTBLK@*/
117 /*@constant int ETXTBSY@*/
118 /*@constant int EWOULDBLOCK@*/
119 /*@constant int EINPROGRESS@*/
120 /*@constant int EALREADY@*/
121 /*@constant int ENOTSOCK@*/
122 /*@constant int EDESTADDRREQ@*/
123 /*@constant int EMSGSIZE@*/
124 /*@constant int EPROTOTYPE@*/
125 /*@constant int ENOPROTOOPT@*/
126 /*@constant int EPROTONOSUPPORT@*/
127 /*@constant int ESOCKTNOSUPPORT@*/
128 /*@constant int EOPNOTSUPP@*/
129 /*@constant int EPFNOSUPPORT@*/
130 /*@constant int EAFNOSUPPORT@*/
131 /*@constant int EADDRINUSE@*/
132 /*@constant int EADDRNOTAVAIL@*/
133 /*@constant int ENETDOWN@*/
134 /*@constant int ENETUNREACH@*/
135 /*@constant int ENETRESET@*/
136 /*@constant int ECONNABORTED@*/
137 /*@constant int ECONNRESET@*/
138 /*@constant int ENOBUFS@*/
139 /*@constant int EISCONN@*/
140 /*@constant int ENOTCONN@*/
141 /*@constant int ESHUTDOWN@*/
142 /*@constant int ETOOMANYREFS@*/
143 /*@constant int ETIMEDOUT@*/
144 /*@constant int ECONNREFUSED@*/
145 /*@constant int ENAMETOOLONG@*/
146 /*@constant int EHOSTDOWN@*/
147 /*@constant int EHOSTUNREACH@*/
148 /*@constant int ENOTEMPTY@*/
149 /*@constant int EPROCLIM@*/
150 /*@constant int EUSERS@*/
151 /*@constant int EDQUOT@*/
152 /*@constant int ESTALE@*/
153 /*@constant int EREMOTE@*/
154 /*@constant int ENOMSG@*/
155 /*@constant int EIDRM@*/
156 /*@constant int EALIGN@*/
157 /*@constant int EDEADLK@*/
158 /*@constant int ENOLCK@*/
159 /*@constant int ENOSYS@*/
160 /*@constant int EACTIVE@*/
161 /*@constant int ENOACTIVE@*/
162 /*@constant int ENORESOURCES@*/
163 /*@constant int ENOSYSTEM@*/
164 /*@constant int ENODUST@*/
165 /*@constant int EDUPNOCONN@*/
166 /*@constant int EDUPNODISCONN@*/
167 /*@constant int EDUPNOTCNTD@*/
168 /*@constant int EDUPNOTIDLE@*/
169 /*@constant int EDUPNOTWAIT@*/
170 /*@constant int EDUPNOTRUN@*/
171 /*@constant int EDUPBADOPCODE@*/
172 /*@constant int EDUPINTRANSIT@*/
173 /*@constant int EDUPTOOMANYCPUS@*/
174 /*@constant int ELOOP@*/
176 /*@constant int LOCK_MAX@*/
177 /*@constant int FCHR_MAX@*/
178 /*@constant int USI_MAX@*/
179 /*@constant int WORD_BIT@*/
180 /*@constant int LONG_BIT@*/
182 /*@-incondefs@*/ /* some constant are also declared in posix.h*/
184 /*@constant long NAME_MAX@*/
186 /*@constant long NGROUPS_MAX@*/
188 /*@constant long MAX_CANON@*/
189 /*@constant int MAX_CHAR@*/
190 /*@constant long OPEN_MAX@*/
191 /*@constant int PASS_MAX@*/
193 /*@constant int PID_MAX@*/
194 /*@constant int SYSPID_MAX@*/
195 /*@constant long PIPE_BUF@*/
197 /*@constant int PIPE_MAX@*/
198 /*@constant int PROC_MAX@*/
199 /*@constant int STD_BLK@*/
200 /*@constant int SYS_NMLN@*/
201 /*@constant int SYS_OPEN@*/
202 /*@constant int NZERO@*/
203 /*@constant int UID_MAX@*/
204 /*@constant long MB_LEN_MAX@*/
205 /*@constant int NL_ARGMAX@*/
206 /*@constant int NL_MSGMAX@*/
207 /*@constant int NL_NMAX@*/
208 /*@constant int NL_SETMAX@*/
209 /*@constant int NL_TEXTMAX@*/
210 /*@constant int NL_LBLMAX@*/
211 /*@constant int NL_LANGMAX @*/
213 /*@constant double M_E@*/
214 /*@constant double M_LOG2E@*/
215 /*@constant double M_LOG10E@*/
216 /*@constant double M_LN2@*/
217 /*@constant double M_LN10@*/
218 /*@constant double M_PI@*/
219 /*@constant double M_PI_2@*/
220 /*@constant double M_PI_4@*/
221 /*@constant double M_1_PI@*/
222 /*@constant double M_2_PI@*/
223 /*@constant double M_2_SQRTPI@*/
224 /*@constant double M_SQRT2@*/
225 /*@constant double M_SQRT1_2@*/
227 /*@constant double MAXFLOAT@*/
228 /*@constant double HUGE@*/
230 /*@constant int DOMAIN@*/
231 /*@constant int SING@*/
232 /*@constant int OVERFLOW@*/
233 /*@constant int UNDERFLOW@*/
234 /*@constant int TLOSS@*/
235 /*@constant int PLOSS@*/
237 extern /*@unchecked@*/ int daylight;
238 extern /*@unchecked@*/ long timezone;
239 extern /*@unchecked@*/ char *tzname[];
242 extern void tzset(void) /*@modifies daylight, timezone, tzname@*/ ;
245 /*@-redef@*/ /* Defined by ansi: */
246 typedef /*@integraltype@*/ key_t;
247 /*@-incondefs@*/ typedef long timer_t; /*@=incondefs@*/
250 typedef unsigned char uchar_t;
251 typedef unsigned short ushort_t;
252 typedef unsigned int uint_t;
253 typedef unsigned long ulong_t;
254 typedef volatile unsigned char vuchar_t;
255 typedef volatile unsigned short vushort_t;
256 typedef volatile unsigned int vuint_t;
257 typedef volatile unsigned long vulong_t;
258 typedef long label_t;
260 typedef /*@integraltype@*/ daddr_t;
261 typedef char *caddr_t;
262 typedef long *qaddr_t;
263 typedef char *addr_t;
264 typedef long physadr_t;
269 typedef char slab_t[12];
270 typedef ulong_t shmatt_t;
271 typedef ulong_t msgqnum_t;
272 typedef ulong_t msglen_t;
273 typedef uchar_t uchar;
274 typedef ushort_t ushort;
276 typedef ulong_t ulong;
277 typedef uchar_t u_char;
278 typedef ushort_t u_short;
279 typedef uint_t u_int;
280 typedef ulong_t u_long;
281 typedef vuchar_t vu_char;
282 typedef vushort_t vu_short;
283 typedef vuint_t vu_int;
284 typedef vulong_t vu_long;
285 typedef long swblk_t;
286 typedef u_long fixpt_t;
287 typedef long segsz_t;
288 typedef /*@abstract@*/ fd_set;
290 int ioctl (int d, int /*@alt long@*/ request, /*@out@*/ void *arg)
291 /*@modifies *arg, errno@*/ ; /* depends on request! */
293 pid_t vfork (void) /*@modifies fileSystem@*/ ;
300 /*@dependent@*/ void *iov_base;
301 size_t iov_len; /*: maxSet(iov_base) = iov_len */
305 /*@constant int UIO_MAXIOV@*/ /* BSD */
306 /*@constant int IOV_MAX@*/ /* supposedly SVR4 */
308 ssize_t readv (int fd, const struct iovec *iov, int iovcnt)
309 /*@modifies iov->iov_base, fileSystem, errno@*/;
311 ssize_t writev (int fd, const struct iovec *iov, int iovcnt)
312 /*@modifies errno@*/;
314 /*________________________________________________________________________
324 /*@constant short POLLIN@*/
325 /*@constant short POLLRDNORM@*/
326 /*@constant short POLLRDBAND@*/
327 /*@constant short POLLPRI@*/
328 /*@constant short POLLOUT@*/
329 /*@constant short POLLWRNORM@*/
330 /*@constant short POLLWRBAND@*/
331 /*@constant short POLLERR@*/
332 /*@constant short POLLHUP@*/
333 /*@constant short POLLNVAL@*/
335 extern int poll (struct poll pollfd[], unsigned long nfds, int timeout)
336 /*@modifies pollfd[].revents, errno@*/ ;
339 ** free does not take null
343 extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ ;
346 /*________________________________________________________________________
353 /*@constant int SOCK_RDM@*/
361 /*@constant int SO_USELOOPBACK@*/
364 /*@constant int SO_REUSEPORT@*/
375 /*@constant int AF_LOCAL@*/
378 /*@constant int AF_IMPLINK@*/
379 /*@constant int AF_PUP@*/
380 /*@constant int AF_CHAOS@*/
381 /*@constant int AF_NS@*/
382 /*@constant int AF_ISO@*/
383 /*@constant int AF_OSI@*/
384 /*@constant int AF_ECMA@*/
385 /*@constant int AF_DATAKIT@*/
386 /*@constant int AF_CCITT@*/
387 /*@constant int AF_SNA@*/
388 /*@constant int AF_DECnet@*/
389 /*@constant int AF_DLI@*/
390 /*@constant int AF_LAT@*/
391 /*@constant int AF_HYLINK@*/
392 /*@constant int AF_APPLETALK@*/
393 /*@constant int AF_ROUTE@*/
394 /*@constant int AF_LINK@*/
395 /*@constant int pseudo_AF_XTP@*/
396 /*@constant int AF_COIP@*/
397 /*@constant int AF_CNT@*/
398 /*@constant int pseudo_AF_RTIP@*/
399 /*@constant int AF_IPX@*/
400 /*@constant int AF_SIP@*/
401 /*@constant int pseudo_AF_PIP@*/
402 /*@constant int AF_ISDN@*/
403 /*@constant int AF_E164@*/
404 /*@constant int AF_MAX@*/
411 /*@constant int MSG_DONTWAIT@*/
412 /*@constant int MSG_EOF@*/
413 /*@constant int MSG_COMPAT@*/
414 /*@constant int PF_UNSPEC@*/
415 /*@constant int PF_LOCAL@*/
416 /*@constant int PF_UNIX@*/
417 /*@constant int PF_INET@*/
418 /*@constant int PF_IMPLINK@*/
419 /*@constant int PF_PUP@*/
420 /*@constant int PF_CHAOS@*/
421 /*@constant int PF_NS@*/
422 /*@constant int PF_ISO@*/
423 /*@constant int PF_OSI@*/
424 /*@constant int PF_ECMA@*/
425 /*@constant int PF_DATAKIT@*/
426 /*@constant int PF_CCITT@*/
427 /*@constant int PF_SNA@*/
428 /*@constant int PF_DECnet@*/
429 /*@constant int PF_DLI@*/
430 /*@constant int PF_LAT@*/
431 /*@constant int PF_HYLINK@*/
432 /*@constant int PF_APPLETALK@*/
433 /*@constant int PF_ROUTE@*/
434 /*@constant int PF_LINK@*/
435 /*@constant int PF_XTP@*/
436 /*@constant int PF_COIP@*/
437 /*@constant int PF_CNT@*/
438 /*@constant int PF_SIP@*/
439 /*@constant int PF_IPX@*/
440 /*@constant int PF_RTIP@*/
441 /*@constant int PF_PIP@*/
442 /*@constant int PF_ISDN@*/
443 /*@constant int PF_MAX@*/
444 /*@constant int NET_MAXID@*/
445 /*@constant int NET_RT_DUMP@*/
446 /*@constant int NET_RT_FLAGS@*/
447 /*@constant int NET_RT_IFLIST@*/
448 /*@constant int NET_RT_MAXID@*/
450 /*moved this to before socket.h to get splint to parse the header*/
451 typedef /*@unsignedintegraltype@*/ sa_family_t;
455 ** (updated 26 May 2002)
458 typedef /*@unsignedintegraltype@*/ __socklen_t; /* not in USB, but needed by linux */
459 typedef /*@unsignedintegraltype@*/ socklen_t;
462 sa_family_t sa_family; /* address family */
463 char sa_data[]; /* variable length */
466 struct sockaddr_storage {
467 sa_family_t ss_family;
471 /*@dependent@*/ void *msg_name;
472 socklen_t msg_namelen; /*: maxSet (msg_name) >= msg_namelen */
473 /*@dependent@*/ struct iovec *msg_iov; /* scatter/gather array */
474 int msg_iovlen; /* # elements in msg_iov */ /*: maxSet (msg_iov) >= msg_iovlen */
475 /*@dependent@*/ void *msg_control; /* ancillary data, see below */
476 socklen_t msg_controllen; /*: maxSet (msg_control) >= msg_controllen */
477 int msg_flags; /* flags on received message */
481 socklen_t cmsg_len; /* data byte count, including hdr */
482 int cmsg_level; /* originating protocol */
483 int cmsg_type; /* protocol-specific type */
486 /*@constant int SCM_RIGHTS@*/
488 /*@exposed@*/ unsigned char *CMSG_DATA (/*@sef@*/ struct cmsghdr *) /*@*/ ;
489 /*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_NXTHDR (struct msghdr *, struct cmsghdr *) /*@*/ ;
490 /*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_FIRSTHDR (struct msghdr *) /*@*/ ;
497 /*@constant int SOCK_DGRAM@*/
498 /*@constant int SOCK_RAW@*/
499 /*@constant int SOCK_SEQPACKET@*/
500 /*@constant int SOCK_STREAM@*/
502 /*@constant int SOL_SOCKET@*/
504 /*@constant int SO_ACCEPTCONN@*/
505 /*@constant int SO_BROADCAST@*/
506 /*@constant int SO_DEBUG@*/
507 /*@constant int SO_DONTROUTE@*/
508 /*@constant int SO_ERROR@*/
509 /*@constant int SO_KEEPALIVE@*/
510 /*@constant int SO_LINGER@*/
511 /*@constant int SO_OOBINLINE@*/
512 /*@constant int SO_RCVBUF@*/
513 /*@constant int SO_RCVLOWAT@*/
514 /*@constant int SO_RCVTIMEO@*/
515 /*@constant int SO_REUSEADDR@*/
516 /*@constant int SO_SNDBUF@*/
517 /*@constant int SO_SNDLOWAT@*/
518 /*@constant int SO_SNDTIMEO@*/
519 /*@constant int SO_TYPE@*/
521 /*@constant int SOMAXCONN@*/
523 /*@constant int MSG_CTRUNC@*/
524 /*@constant int MSG_DONTROUTE@*/
525 /*@constant int MSG_EOR@*/
526 /*@constant int MSG_OOB@*/
527 /*@constant int MSG_PEEK@*/
528 /*@constant int MSG_TRUNC@*/
529 /*@constant int MSG_WAITALL@*/
531 /*@constant int AF_INET@*/
532 /*@constant int AF_INET6@*/
533 /*@constant int AF_UNIX@*/
534 /*@constant int AF_UNSPEC@*/
536 /*@constant int SHUT_RD@*/
537 /*@constant int SHUT_RDWR@*/
538 /*@constant int SHUT_WR@*/
542 ** These were in the old unix.h spec, but are not in SUS6
546 u_short sp_family; /* address family */
547 u_short sp_protocol; /* protocol */
552 int accept (int s, struct sockaddr *addr, int *addrlen)
553 /*@modifies *addrlen, errno@*/;
555 int bind (int s, const struct sockaddr *name, int namelen)
556 /*@modifies errno, fileSystem@*/;
558 int connect (int s, const struct sockaddr *name, int namelen)
559 /*@modifies errno, internalState@*/;
561 int getpeername (int s, /*@out@*/ struct sockaddr */*restrict*/ name, socklen_t */*restrict*/ namelen)
562 /*drl splint doesn't handle restrict yet*/
563 /*@modifies *name, *namelen, errno@*/;
567 int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t *address_len)
568 /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/
569 /*@modifies *address, *address_len, errno@*/;
572 int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t /*@alt size_t@*/ *address_len)
573 /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/
574 /*@modifies *address, *address_len, errno@*/;
578 int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen)
579 /*@modifies *optval, *optlen, errno@*/;
582 listen (int s, int backlog)
583 /*@modifies errno, internalState@*/;
586 recv (int s, /*@out@*/ void *buf, size_t len, int flags)
587 /*@modifies *buf, errno@*/;
590 recvfrom (int s, void *buf, size_t len, int flags, /*@null@*/ struct sockaddr *from, int *fromlen)
591 /*@modifies *buf, *from, *fromlen, errno@*/;
594 recvmsg (int s, struct msghdr *msg, int flags)
595 /*@modifies msg->msg_iov->iov_base[], errno@*/;
598 send (int s, const void *msg, size_t len, int flags)
599 /*@modifies errno@*/;
602 sendto (int s, const void *msg, size_t len, int flags, const struct sockaddr *to, int tolen)
603 /*@modifies errno@*/;
606 sendmsg (int s, const struct msghdr *msg, int flags)
607 /*@modifies errno@*/;
610 setsockopt (int s, int level, int optname, const void *optval, int optlen)
611 /*@modifies internalState, errno@*/;
614 shutdown (int s, int how)
615 /*@modifies errno@*/;
618 socket (int domain, int type, int protocol)
619 /*@modifies errno@*/;
622 socketpair (int d, int type, int protocol, /*@out@*/ int *sv)
623 /*@modifies errno@*/;
625 /*@constant int BADSIG@*/
626 /*@constant int SA_ONSTACK@*/
627 /*@constant int SA_RESTART@*/
628 /*@constant int SA_DISABLE@*/
629 /*@constant int SIGBUS@*/
630 /*@constant int SIGEMT@*/
631 /*@constant int SIGINFO@*/
632 /*@constant int SIGIO@*/
633 /*@constant int SIGIOT@*/
634 /*@constant int SIGPOLL@*/
635 /*@constant int SIGPROF@*/
636 /*@constant int SIGPWR@*/
637 /*@constant int SIGSYS@*/
638 /*@constant int SIGTRAP@*/
639 /*@constant int SIGURG@*/
640 /*@constant int SIGVTALRM@*/
641 /*@constant int SIGWINCH@*/
642 /*@constant int SIGXCPU@*/
643 /*@constant int SIGXFSZ@*/
645 extern void psignal (int sig, const char *msg)
646 /*@modifies fileSystem@*/;
649 setenv (const char *name, const char *value, int overwrite)
650 /*@globals environ@*/
651 /*@modifies *environ, errno@*/;
654 unsetenv (const char *name)
655 /*@globals environ@*/
656 /*@modifies *environ@*/;
658 /*________________________________________________________________________
667 W_EXITCODE (int ret, int sig)
674 /*@constant int WAIT_ANY@*/
675 /*@constant int WAIT_MYPGRP@*/
676 /*@constant int WSTOPPED@*/
679 wait3 (int *statloc, int options, /*@null@*/ /*@out@*/ struct rusage *rusage)
680 /*@modifies *statloc, *rusage, errno@*/;
683 wait4 (pid_t p, int *statloc, int opt, /*@null@*/ /*@out@*/ struct rusage *r)
684 /*@modifies *statloc, *r, errno@*/;
701 /*@constant int DST_NONE@*/
702 /*@constant int DST_USA@*/
703 /*@constant int DST_AUST@*/
704 /*@constant int DST_WET@*/
705 /*@constant int DST_MET@*/
706 /*@constant int DST_EET@*/
707 /*@constant int DST_CAN@*/
709 /*@constant int ITIMER_PROF@*/
710 /*@constant int ITIMER_REAL@*/
711 /*@constant int ITIMER_VIRTUAL@*/
714 struct timeval it_interval;
715 struct timeval it_value;
726 adjtime (const struct timeval *delta, /*@null@*/ /*@out@*/ struct timeval *olddelta)
727 /*@modifies internalState, *olddelta, errno@*/;
730 getitimer (int which, /*@out@*/ struct itimerval *value)
731 /*@modifies errno, *value*/;
734 gettimeofday (/*@null@*/ /*@out@*/ struct timeval *tp, /*@null@*/ /*@out@*/ struct timezone *tzp)
735 /*@modifies *tp, *tzp, errno@*/;
738 setitimer (int which, struct itimerval *val, /*@null@*/ /*@out@*/ struct itimerval *oval)
739 /*@modifies *oval, errno, internalState*/;
742 settimeofday (const struct timeval *t, const struct timezone *z)
743 /*@modifies internalState, errno@*/;
746 utimes (const char *file, /*@null@*/ const struct timeval *times)
747 /*@modifies fileSystem, errno*/;
749 /*________________________________________________________________________
753 /*@constant int PROT_READ@*/
754 /*@constant int PROT_WRITE@*/
755 /*@constant int PROT_EXEC@*/
756 /*@constant int MAP_SHARED@*/
757 /*@constant int MAP_PRIVATE@*/
758 /*@constant int MAP_COPY@*/
759 /*@constant int MAP_FIXED@*/
760 /*@constant int MAP_RENAME@*/
761 /*@constant int MAP_NORESERVE@*/
762 /*@constant int MAP_INHERIT@*/
763 /*@constant int MAP_NOEXTEND@*/
764 /*@constant int MAP_HASSEMAPHORE@*/
765 /*@constant int MS_ASYNC@*/
766 /*@constant int MS_INVALIDATE@*/
767 /*@constant int MAP_FILE@*/
768 /*@constant int MAP_ANON@*/
769 /*@constant int MADV_NORMAL@*/
770 /*@constant int MADV_RANDOM@*/
771 /*@constant int MADV_SEQUENTIAL@*/
772 /*@constant int MADV_WILLNEED@*/
773 /*@constant int MADV_DONTNEED@*/
776 mmap (/*@null@*/ /*@returned@*/ caddr_t addr, size_t len, int prot, int flags, int fd, off_t offset)
780 madvise (caddr_t addr, int len, int behav)
784 mprotect (caddr_t addr, int len, int prot)
788 int munmap (/*@only@*/ caddr_t addr, size_t len)
789 /*@modifies fileSystem, *addr, errno @*/;
792 msync (caddr_t addr, int len, int flags)
796 mlock (caddr_t addr, size_t len)
800 munlock (caddr_t addr, size_t len)
804 /*________________________________________________________________________
809 unsigned short ws_row;
810 unsigned short ws_col;
811 unsigned short ws_xpixel;
812 unsigned short ws_ypixel;
815 /*@constant int TIOCMODG@*/
816 /*@constant int TIOCMODS@*/
817 /*@constant int TIOCM_LE@*/
818 /*@constant int TIOCM_DTR@*/
819 /*@constant int TIOCM_RTS@*/
820 /*@constant int TIOCM_ST@*/
821 /*@constant int TIOCM_SR@*/
822 /*@constant int TIOCM_CTS@*/
823 /*@constant int TIOCM_CAR@*/
824 /*@constant int TIOCM_CD@*/
825 /*@constant int TIOCM_RNG@*/
826 /*@constant int TIOCM_RI@*/
827 /*@constant int TIOCM_DSR@*/
828 /*@constant int TIOCEXCL@*/
829 /*@constant int TIOCNXCL@*/
830 /*@constant int TIOCFLUSH@*/
831 /*@constant int TIOCGETA@*/
832 /*@constant int TIOCSETA@*/
833 /*@constant int TIOCSETAW@*/
834 /*@constant int TIOCSETAF@*/
835 /*@constant int TIOCGETD@*/
836 /*@constant int TIOCSETD@*/
837 /*@constant int TIOCSBRK@*/
838 /*@constant int TIOCCBRK@*/
839 /*@constant int TIOCSDTR@*/
840 /*@constant int TIOCCDTR@*/
841 /*@constant int TIOCGPGRP@*/
842 /*@constant int TIOCSPGRP@*/
843 /*@constant int TIOCOUTQ@*/
844 /*@constant int TIOCSTI@*/
845 /*@constant int TIOCNOTTY@*/
846 /*@constant int TIOCPKT@*/
847 /*@constant int TIOCPKT_DATA@*/
848 /*@constant int TIOCPKT_FLUSHREAD@*/
849 /*@constant int TIOCPKT_FLUSHWRITE@*/
850 /*@constant int TIOCPKT_STOP@*/
851 /*@constant int TIOCPKT_START@*/
852 /*@constant int TIOCPKT_NOSTOP@*/
853 /*@constant int TIOCPKT_DOSTOP@*/
854 /*@constant int TIOCPKT_IOCTL@*/
855 /*@constant int TIOCSTOP@*/
856 /*@constant int TIOCSTART@*/
857 /*@constant int TIOCMSET@*/
858 /*@constant int TIOCMBIS@*/
859 /*@constant int TIOCMBIC@*/
860 /*@constant int TIOCMGET@*/
861 /*@constant int TIOCREMOTE@*/
862 /*@constant int TIOCGWINSZ@*/
863 /*@constant int TIOCSWINSZ@*/
864 /*@constant int TIOCUCNTL@*/
865 /*@constant int TIOCSTAT@*/
866 /*@constant int TIOCCONS@*/
867 /*@constant int TIOCSCTTY@*/
868 /*@constant int TIOCEXT@*/
869 /*@constant int TIOCSIG@*/
870 /*@constant int TIOCDRAIN@*/
871 /*@constant int TIOCMSDTRWAIT@*/
872 /*@constant int TIOCMGDTRWAIT@*/
873 /*@constant int TIOCTIMESTAMP@*/
874 /*@constant int TIOCSDRAINWAIT@*/
875 /*@constant int TIOCGDRAINWAIT@*/
876 /*@constant int TTYDISC@*/
877 /*@constant int TABLDISC@*/
878 /*@constant int SLIPDISC@*/
879 /*@constant int PPPDISC@*/
881 /*@constant int MAXHOSTNAMELEN@*/
884 FD_CLR (int n, fd_set *p)
888 FD_COPY (fd_set *f, /*@out@*/ fd_set *t)
891 extern int /*@alt lltX_bool@*/
892 FD_ISSET (int n, fd_set *p)
896 FD_SET (int n, fd_set *p)
900 FD_ZERO (fd_set /*@out@*/ *p)
905 /*@modifies internalState, errno@*/;
908 fchown (int fd, uid_t owner, gid_t group)
909 /*@modifies errno, fileSystem@*/;
913 /*@modifies errno, fileSystem@*/;
916 ftruncate (int fd, off_t length)
917 /*@modifies errno, fileSystem@*/;
919 int gethostname (/*@out@*/ char *address, size_t address_len)
921 /*@modifies address@*/ ;
923 int initgroups (const char *name, int basegid)
924 /*@modifies internalState@*/;
926 int lchown (const char *path, uid_t owner, gid_t group)
927 /*@modifies errno, fileSystem@*/;
929 int select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, fd_set /*@null@*/ *e, /*@null@*/ struct timeval *t)
930 /*@modifies *r, *w, *e, *t, errno@*/;
931 /* evans - 2002-05-26: added null for t, bug reported by Enrico Scholz */
933 int setegid (gid_t egid)
934 /*@modifies errno, internalState@*/;
936 int seteuid (uid_t euid)
937 /*@modifies errno, internalState@*/;
939 int setgroups (int ngroups, const gid_t *gidset)
940 /*@modifies errno, internalState@*/;
942 int setregid (gid_t rgid, gid_t egid)
943 /*@modifies errno, internalState@*/;
945 int setreuid (gid_t ruid, gid_t euid)
946 /*@modifies errno, internalState@*/;
949 /*@modifies fileSystem@*/;
951 int symlink (const char *path, const char *path2)
952 /*@modifies fileSystem@*/;
954 int truncate (const char *name, off_t length)
955 /*@modifies errno, fileSystem@*/;
957 /*@constant int EBADRPC@*/
958 /*@constant int ERPCMISMATCH@*/
959 /*@constant int EPROGUNAVAIL@*/
960 /*@constant int EPROGMISMATCH@*/
961 /*@constant int EPROCUNAVAIL@*/
962 /*@constant int EFTYPE@*/
963 /*@constant int EAUTH@*/
964 /*@constant int ENEEDAUTH@*/
965 /*@constant int ELAST@*/
971 /*@unchecked@*/ extern char *TMAGIC;
972 /*@constant int TMAGLEN@*/
973 /*@unchecked@*/ extern char *TVERSION;
974 /*@constant int TVERSLEN@*/
976 /*@constant int REGTYPE@*/
977 /*@constant int AREGTYPE@*/
978 /*@constant int LNKTYPE@*/
979 /*@constant int SYMTYPE@*/
980 /*@constant int CHRTYPE@*/
981 /*@constant int BLKTYPE@*/
982 /*@constant int DIRTYPE@*/
983 /*@constant int FIFOTYPE@*/
984 /*@constant int CONTTYPE@*/
986 /*@constant int TSUID@*/
987 /*@constant int TSGID@*/
988 /*@constant int TSVTX@*/
990 /*@constant int TUREAD@*/
991 /*@constant int TUWRITE@*/
992 /*@constant int TUEXEC@*/
993 /*@constant int TGREAD@*/
994 /*@constant int TGWRITE@*/
995 /*@constant int TGEXEC@*/
996 /*@constant int TOREAD@*/
997 /*@constant int TOWRITE@*/
998 /*@constant int TOEXEC@*/
1001 uid_t uid; /* user id */
1002 gid_t gid; /* group id */
1003 uid_t cuid; /* creator user id */
1004 gid_t cgid; /* creator group id */
1005 mode_t mode; /* r/w permission */
1006 ulong seq; /* slot usage sequence number */
1007 key_t key; /* user specified msg/sem/shm key */
1010 /*@constant int IPC_R@*/
1011 /*@constant int IPC_W@*/
1012 /*@constant int IPC_M@*/
1013 /*@constant int IPC_CREAT@*/
1014 /*@constant int IPC_EXCL@*/
1015 /*@constant int IPC_NOWAIT@*/
1016 /*@constant key_t IPC_PRIVATE@*/
1017 /*@constant int IPC_RMID@*/
1018 /*@constant int IPC_SET@*/
1019 /*@constant int IPC_STAT@*/
1026 struct ipc_perm msg_perm; /* msg queue permission bits */
1027 struct msg *msg_first; /* first message in the queue */
1028 struct msg *msg_last; /* last message in the queue */
1029 u_long msg_cbytes; /* number of bytes in use on the queue */
1030 u_long msg_qnum; /* number of msgs in the queue */
1031 u_long msg_qbytes; /* max # of bytes on the queue */
1032 pid_t msg_lspid; /* pid of last msgsnd() */
1033 pid_t msg_lrpid; /* pid of last msgrcv() */
1034 time_t msg_stime; /* time of last msgsnd() */
1035 time_t msg_rtime; /* time of last msgrcv() */
1036 time_t msg_ctime; /* time of last msgctl() */
1040 long mtype; /* message type (+ve integer) */
1041 char mtext[]; /* message body */
1044 /*@constant int MSG_NOERROR@*/
1045 /*@constant int MSGMAX@*/
1046 /*@constant int MSGMNB@*/
1047 /*@constant int MSGMNI@*/
1048 /*@constant int MSGTQL@*/
1051 msgctl (int id , int cmd, /*@out@*/ struct msqid_ds *buf)
1052 /*@modifies errno, *buf@*/;
1055 msgget (key_t key, int flag)
1056 /*@modifies errno@*/;
1059 msgrcv (int id, /*@out@*/ void *ptr, size_t nbytes, long type, int flags)
1060 /*@modifies errno, *ptr@*/;
1063 msgsnd (int id, const void *ptr, size_t nbytes, int flag)
1064 /*@modifies errno@*/;
1071 struct ipc_perm sem_perm;
1072 struct sem *sem_base;
1087 struct semid_ds *buf;
1097 /*@constant int SEM_A@*/
1098 /*@constant int SEMAEM@*/
1099 /*@constant int SEMMNI@*/
1100 /*@constant int SEMMNS@*/
1101 /*@constant int SEMMNU@*/
1102 /*@constant int SEMMSL@*/
1103 /*@constant int SEMOPN@*/
1104 /*@constant int SEM_R@*/
1105 /*@constant int SEMUME@*/
1106 /*@constant int SEM_UNDO@*/
1107 /*@constant int SEMVMX@*/
1108 /*@constant int GETVAL@*/
1109 /*@constant int SETVAL@*/
1110 /*@constant int GETPID@*/
1111 /*@constant int GETNCNT@*/
1112 /*@constant int GETZCNT@*/
1113 /*@constant int GETALL@*/
1114 /*@constant int SETALL@*/
1116 /*@constant int ERMID@*/
1119 semctl (int id, int semnum, int cmd, union semun arg)
1120 /*@modifies errno@*/;
1123 semget (key_t key, int nsems, int flag)
1124 /*@modifies errno@*/;
1127 semop (int id, struct sembuf *semoparray, size_t nops)
1128 /*@modifies errno@*/;
1135 struct ipc_perm shm_perm;
1147 /*@constant int SHMLBA@*/
1148 /*@constant int SHM_LOCK@*/
1149 /*@constant int SHMMAX@*/
1150 /*@constant int SHMMIN@*/
1151 /*@constant int SHMMNI@*/
1152 /*@constant int SHM_R@*/
1153 /*@constant int SHM_RDONLY@*/
1154 /*@constant int SHM_RND@*/
1155 /*@constant int SHMSEG@*/
1156 /*@constant int SHM_W@*/
1157 /*@constant int SHM_UNLOCK@*/
1159 void * shmat (int id, /*@null@*/ void *addr, int flag)
1160 /*@modifies errno@*/ ;
1162 extern int shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf)
1163 /*@modifies errno, *buf@*/ ;
1165 extern int shmdt (void *addr)
1166 /*@modifies errno@*/ ;
1168 extern int shmget (key_t key, int size, int flag)
1169 /*@modifies errno@*/ ;
1173 ** stdio.h - in separte file stdio.h
1180 /*@constant int LOG_EMERG@*/
1181 /*@constant int LOG_ALERT@*/
1182 /*@constant int LOG_CRIT@*/
1183 /*@constant int LOG_ERR@*/
1184 /*@constant int LOG_WARNING@*/
1185 /*@constant int LOG_NOTICE@*/
1186 /*@constant int LOG_INFO@*/
1187 /*@constant int LOG_DEBUG@*/
1189 /*@constant int LOG_KERN@*/
1190 /*@constant int LOG_USER@*/
1191 /*@constant int LOG_MAIL@*/
1192 /*@constant int LOG_DAEMON@*/
1193 /*@constant int LOG_AUTH@*/
1194 /*@constant int LOG_SYSLOG@*/
1195 /*@constant int LOG_LPR@*/
1196 /*@constant int LOG_NEWS@*/
1197 /*@constant int LOG_UUCP@*/
1198 /*@constant int LOG_CRON@*/
1199 /*@constant int LOG_AUTHPRIV@*/
1200 /*@constant int LOG_FTP@*/
1201 /*@constant int LOG_LOCAL0@*/
1202 /*@constant int LOG_LOCAL1@*/
1203 /*@constant int LOG_LOCAL2@*/
1204 /*@constant int LOG_LOCAL3@*/
1205 /*@constant int LOG_LOCAL4@*/
1206 /*@constant int LOG_LOCAL5@*/
1207 /*@constant int LOG_LOCAL6@*/
1208 /*@constant int LOG_LOCAL7@*/
1210 /*@constant int LOG_PID@*/
1211 /*@constant int LOG_CONS@*/
1212 /*@constant int LOG_ODELAY@*/
1213 /*@constant int LOG_NDELAY@*/
1214 /*@constant int LOG_NOWAIT@*/
1215 /*@constant int LOG_PERROR@*/
1217 int LOG_MASK (int pri)
1220 int LOG_UPTO (int pri)
1223 void closelog (void)
1224 /*@modifies fileSystem@*/;
1226 void openlog (const char *ident, int logopt, int facility)
1227 /*@modifies fileSystem@*/;
1229 int setlogmask (int maskpri)
1230 /*@modifies internalState@*/;
1232 void /*@printflike@*/ syslog (int priority, const char *message, ...)
1233 /*@modifies fileSystem@*/;
1235 void vsyslog (int priority, const char *message, va_list args)
1236 /*@modifies fileSystem@*/;
1238 /*________________________________________________________________________
1244 /*@modifies internalState@*/;
1246 extern /*@null@*/ struct passwd *
1248 /*@modifies internalState@*/;
1251 setpassent (int stayopen)
1252 /*@modifies internalState@*/;
1256 /*@modifies internalState@*/;
1262 void endgrent (void) /*@modifies internalState@*/;
1264 /*@null@*/ /*@observer@*/ struct group *getgrent (void)
1265 /*@modifies internalState@*/;
1267 int setgrent (void) /*@modifies internalState@*/;
1269 void setgrfile (const char *name) /*@modifies internalState@*/;
1271 int setgroupent (int stayopen) /*@modifies internalState@*/;
1276 ** evans 2001-08-26 - updated from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstat.h.html
1280 ** struct stat replaces POSIX version - more required fields in Unix
1283 /*@-redef@*/ /*@-matchfields@*/
1285 dev_t st_dev; /* ID of device containing file */
1286 ino_t st_ino; /* file serial number */
1287 mode_t st_mode; /* mode of file (see below) */
1288 nlink_t st_nlink; /* number of links to the file */
1289 uid_t st_uid; /* user ID of file */
1290 gid_t st_gid; /* group ID of file */
1291 dev_t st_rdev; /* device ID (if file is character or block special) */
1292 off_t st_size; /* file size in bytes (if file is a regular file) */
1293 time_t st_atime; /* time of last access */
1294 time_t st_mtime; /* time of last data modification */
1295 time_t st_ctime; /* time of last status change */
1296 blksize_t st_blksize; /* a filesystem-specific preferred I/O block size for
1297 this object. In some filesystem types, this may
1298 vary from file to file */
1299 blkcnt_t st_blocks; /* number of blocks allocated for this object */
1301 /*@=redef@*/ /*@=matchfields@*/
1303 /*@constant mode_t S_IWUSR@*/
1304 /*@constant mode_t S_IXUSR@*/
1305 /*@constant mode_t S_IRWXG@*/
1306 /*@constant mode_t S_IRGRP@*/
1307 /*@constant mode_t S_IWGRP@*/
1308 /*@constant mode_t S_IXGRP@*/
1309 /*@constant mode_t S_IRWXO@*/
1310 /*@constant mode_t S_IROTH@*/
1311 /*@constant mode_t S_IWOTH@*/
1312 /*@constant mode_t S_IXOTH@*/
1313 /*@constant mode_t S_ISUID@*/
1314 /*@constant mode_t S_ISGID@*/
1315 /*@constant mode_t S_ISVTX@*/
1318 /*These are the old definitions - they don't appear to be in the Single UNIX Specification */
1320 /*@constant int S_ISTXT@*/
1321 /*@constant int S_IREAD@*/
1322 /*@constant int S_IWRITE@*/
1323 /*@constant int S_IEXEC@*/
1324 /*@constant int S_IFMT@*/
1325 /*@constant int S_IFIFO@*/
1326 /*@constant int S_IFCHR@*/
1327 /*@constant int S_IFDIR@*/
1328 /*@constant int S_IFBLK@*/
1329 /*@constant int S_IFREG@*/
1330 /*@constant int S_IFLNK@*/
1331 /*@constant int S_IFSOCK@*/
1332 /*@constant int S_ISVTX@*/
1333 /*@constant int S_ISVTX@*/
1334 /*@constant int SF_SETTABLE@*/
1335 /*@constant int SF_ARCHIVED@*/
1336 /*@constant int ACCESSPERMS@*/
1337 /*@constant int ALLPERMS@*/
1338 /*@constant int DEFFILEMODE@*/
1339 /*@constant int S_BLKSIZE@*/
1340 /*@constant int SF_IMMUTABLE@*/
1341 /*@constant int SF_APPEND@*/
1342 /*@constant int UF_NODUMP@*/
1343 /*@constant int UF_IMMUTABLE@*/
1344 /*@constant int UF_APPEND@*/
1347 int /*@alt lltX_bool@*/ S_ISBLK (/*@sef@*/ mode_t m) /*@*/;
1348 int /*@alt lltX_bool@*/ S_ISCHR (/*@sef@*/ mode_t m) /*@*/;
1349 int /*@alt lltX_bool@*/ S_ISDIR (/*@sef@*/ mode_t m) /*@*/;
1350 int /*@alt lltX_bool@*/ S_ISFIFO (/*@sef@*/ mode_t m) /*@*/;
1351 int /*@alt lltX_bool@*/ S_ISREG (/*@sef@*/ mode_t m) /*@*/;
1352 int /*@alt lltX_bool@*/ S_ISLNK (/*@sef@*/ mode_t m) /*@*/;
1354 int /*@alt lltX_bool@*/ S_TYPEISMQ (/*@sef@*/ struct stat *buf) /*@*/ ;
1355 int /*@alt lltX_bool@*/ S_TYPEISSEM (/*@sef@*/ struct stat *buf) /*@*/ ;
1356 int /*@alt lltX_bool@*/ S_TYPEISSHM (/*@sef@*/ struct stat *buf) /*@*/ ;
1358 /* in POSIX: chmod, fstat, mkdir, mkfifo, stat, umask */
1360 int lstat(const char *, /*@out@*/ struct stat *)
1362 /*@modifies errno@*/ ;
1364 int mknod (const char *, mode_t, dev_t)
1365 /*@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."@*/
1367 /*@modifies errno@*/ ;
1369 int chflags (const char *path, u_long flags)
1370 /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
1371 /*@modifies fileSystem, errno@*/;
1373 int fchflags (int fd, u_long flags)
1374 /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
1375 /*@modifies fileSystem, errno@*/;
1377 /* evans 2002-03-17: this was missing, reported by Ralf Wildenhues */
1378 int fchmod(int fildes, mode_t mode)
1379 /*@modifies fileSystem, errno@*/ ;
1383 ** from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstatvfs.h.html
1387 unsigned long f_bsize;
1388 unsigned long f_frsize;
1389 fsblkcnt_t f_blocks;
1391 fsblkcnt_t f_bavail;
1394 fsfilcnt_t f_favail;
1395 unsigned long f_fsid;
1396 unsigned long f_flag;
1397 unsigned long f_namemax;
1400 /*@constant unsigned long ST_RDONLY; @*/
1401 /*@constant unsigned long ST_NOSUID; @*/
1403 int fstatvfs (int fildes, /*@out@*/ struct statvfs *buf)
1404 /*@modifies buf@*/ ;
1406 int statvfs (const char *path, /*@out@*/ struct statvfs *buf)
1407 /*@modifies buf@*/ ;
1410 /*________________________________________________________________________
1414 /*@constant int FMNAMESZ@*/
1415 /*@constant int MSG_BAND@*/
1416 /*@constant int MSG_HIPRI@*/
1417 /*@constant int RS_HIPRI@*/
1418 /*@constant int S_INPUT@*/
1419 /*@constant int S_RDNORM@*/
1420 /*@constant int S_RDBAND@*/
1421 /*@constant int S_BANDURG@*/
1422 /*@constant int S_HIPRI@*/
1423 /*@constant int S_OUTPUT@*/
1424 /*@constant int S_WRNORM@*/
1425 /*@constant int S_WRBAND@*/
1426 /*@constant int S_MSG@*/
1427 /*@constant int S_ERROR@*/
1428 /*@constant int S_HANGUP@*/
1442 struct str_mlist *sl_modlist;
1446 getmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *f)
1447 /*@modifies *c, *d, errno@*/;
1450 getpmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *b, int *f)
1451 /*@modifies *b, *c, *d, errno@*/;
1454 putmsg (int fd, const struct strbuf *c, const struct strbuf *d, int *f)
1455 /*@modifies internalState, errno@*/;
1457 extern int putpmsg (int fd, const struct strbuf *c, const struct strbuf *d, int b, int *f)
1458 /*@modifies internalState, errno@*/;
1463 ** Update 2002-07-09 from
1464 ** http://www.opengroup.org/onlinepubs/007904975/basedefs/sys/resource.h.html
1467 /*@constant int PRIO_PROCESS@*/
1468 /*@constant int PRIO_PGRP@*/
1469 /*@constant int PRIO_USER@*/
1471 typedef /*@unsignedintegraltype@*/ rlim_t;
1473 /*@constant rlim_t RLIM_INFINITY@*/
1474 /*@constant rlim_t RLIM_SAVED_MAX@*/
1475 /*@constant rlim_t RLIM_SAVED_CUR@*/
1477 /*@constant int RUSAGE_SELF@*/
1478 /*@constant int RUSAGE_CHILDREN@*/
1486 struct timeval ru_utime; /* user time used */
1487 struct timeval ru_stime; /* system time used */
1488 /* other members optional */
1491 /*@constant int RLIMIT_CORE@*/
1492 /*@constant int RLIMIT_CPU@*/
1493 /*@constant int RLIMIT_DATA@*/
1494 /*@constant int RLIMIT_FSIZE@*/
1495 /*@constant int RLIMIT_NOFILE@*/
1496 /*@constant int RLIMIT_STACK@*/
1497 /*@constant int RLIMIT_AS@*/
1499 int getpriority (int which, id_t who)
1500 /*@modifies errno@*/;
1502 int getrlimit (int res, /*@out@*/ struct rlimit *rlp)
1503 /*@modifies *rlp, errno@*/;
1505 int getrusage (int who, /*@out@*/ struct rusage *rusage)
1506 /*@modifies *rusage, errno@*/;
1508 int setpriority (int which, id_t who, int prio)
1509 /*@modifies errno, internalState@*/;
1511 int setrlimit (int resource, const struct rlimit *rlp)
1512 /*@modifies errno, internalState@*/;
1520 /*@observer@*/ char *s_name; /* Official service name. */
1521 /*@observer@*/ char **s_aliases; /* Alias list. */
1522 int s_port; /* Port number. */
1523 /*@observer@*/ char *s_proto; /* Protocol to use. */
1526 /*@observer@*/ /*@dependent@*/ /*@null@*/ struct servent *getservbyname (const char *name, /*@null@*/ const char *proto)
1527 /*@warn multithreaded "Unsafe in multithreaded applications, use getsrvbyname_r instead"@*/ ;
1529 struct servent *getservbyname_r (const char *name, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
1530 /*@requires maxSet (buffer) >= buflen@*/ ;
1533 /*@observer@*/ /*@dependent@*/ struct servent *getservbyport (int port, /*@null@*/ const char *proto)
1534 /*@warn multithreaded "Unsafe in multithreaded applications, use getservbyport_r instead"@*/ ;
1536 struct servent *getservbyport_r (int port, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
1537 /*@requires maxSet (buffer) >= buflen@*/ ;
1539 /*@null@*/ struct servent *getservent (void);
1541 /*@null@*/ struct servent *getservent_r (struct servent *result, char *buffer, int buflen);
1543 int setservent (int stayopen);
1544 int endservent (void);
1548 /*@null@*/ /*@observer@*/ struct hostent *gethostbyname (/*@nullterminated@*/ /*@notnull@*/ const char *name)
1549 /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyname_r instead"@*/
1550 /*@modifies h_errno@*/ ;
1552 struct hostent *gethostbyname_r (/*@nullterminated@*/ const char *name, /*@notnull@*/ /*@returned@*/ struct hostent *hent, /*@out@*/ /*@exposed@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
1553 /*@requires maxSet(buffer) >= bufsize@*/ ;
1555 /*@null@*/ /*@observer@*/ struct hostent *gethostbyaddr (/*@notnull@*/ const void *addr, size_t addrlen, int type)
1556 /*@requires maxRead(addr) == addrlen@*/ /*:i534 ??? is this right? */
1557 /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyaddr_r instead"@*/
1558 /*@modifies h_errno@*/ ;
1560 struct hostent *gethostbyaddr_r (/*@notnull@*/ const void *addr, size_t addrlen, int type,
1561 /*@returned@*/ /*@out@*/ struct hostent *hent,
1562 /*@exposed@*/ /*@out@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
1563 /*@requires maxRead(addr) == addrlen /\ maxSet(buffer) >= bufsize@*/
1564 /*:i534 ??? is this right? */ ;
1566 /*@observer@*/ /*@null@*/ struct hostent *gethostent (void)
1567 /*@warn multithreaded "Unsafe in multithreaded applications, use gethostent_r instead"@*/ ;
1569 struct hostent *gethostent_r (/*@out@*/ /*@returned@*/ struct hostent *hent, /*@exposed@*/ /*@out@*/ char *buffer, int bufsize)
1570 /*@requires maxSet(buffer) >= bufsize@*/ ;
1572 /*:i534 need to annotate these: */
1574 struct hostent *fgethostent(FILE *f);
1575 struct hostent *fgethostent_r(FILE*f, struct hostent *hent, char buffer, int bufsize);
1576 void sethostent(int stayopen);
1577 void endhostent(void);
1578 void herror(const char *string);
1579 char *hstrerror(int err);
1582 /*@observer@*/ /*@nullterminated@*/ char *h_name; /* official name of host */
1583 /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_aliases; /* alias list */
1584 int h_addrtype; /* host address type*/
1585 int h_length; /* length ofaddress*/
1586 /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_addr_list; /* list of addressesfrom name server */
1587 /*@observer@*/ /*@nullterminated@*/ char *h_addr; /* first address in list (backward compatibility) */
1592 ** from http://www.opengroup.org/onlinepubs/007908799/xsh/unistd.h.html
1595 /*@constant int _POSIX_VERSION@*/
1596 /*@constant int _POSIX2_VERSION@*/
1597 /*@constant int _POSIX2_C_VERSION@*/
1598 /*@constant int _XOPEN_VERSION@*/
1599 /*@constant int _XOPEN_XCU_VERSION@*/
1603 /*@constant int R_OK@*/
1604 /*@constant int W_OK@*/
1605 /*@constant int X_OK@*/
1606 /*@constant int F_OK@*/
1609 /*@constant int _CS_PATH@*/
1610 /*@constant int _CS_XBS5_ILP32_OFF32_CFLAGS@*/
1611 /*@constant int _CS_XBS5_ILP32_OFF32_LDFLAGS@*/
1612 /*@constant int _CS_XBS5_ILP32_OFF32_LIBS@*/
1613 /*@constant int _CS_XBS5_ILP32_OFF32_LINTFLAGS@*/
1614 /*@constant int _CS_XBS5_ILP32_OFFBIG_CFLAGS@*/
1615 /*@constant int _CS_XBS5_ILP32_OFFBIG_LDFLAGS@*/
1616 /*@constant int _CS_XBS5_ILP32_OFFBIG_LIBS@*/
1617 /*@constant int _CS_XBS5_ILP32_OFFBIG_LINTFLAGS@*/
1618 /*@constant int _CS_XBS5_LP64_OFF64_CFLAGS@*/
1619 /*@constant int _CS_XBS5_LP64_OFF64_LDFLAGS@*/
1620 /*@constant int _CS_XBS5_LP64_OFF64_LIBS@*/
1621 /*@constant int _CS_XBS5_LP64_OFF64_LINTFLAGS@*/
1622 /*@constant int _CS_XBS5_LPBIG_OFFBIG_CFLAGS@*/
1623 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LDFLAGS@*/
1624 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LIBS@*/
1625 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LINTFLAGS@*/
1627 /* name parameters to sysconf: */
1629 /*@constant int _SC_2_C_BIND@*/
1630 /*@constant int _SC_2_C_DEV@*/
1631 /*@constant int _SC_2_C_VERSION@*/
1632 /*@constant int _SC_2_FORT_DEV@*/
1633 /*@constant int _SC_2_FORT_RUN@*/
1634 /*@constant int _SC_2_LOCALEDEF@*/
1635 /*@constant int _SC_2_SW_DEV@*/
1636 /*@constant int _SC_2_UPE@*/
1637 /*@constant int _SC_2_VERSION@*/
1638 /*@constant int _SC_ARG_MAX@*/
1639 /*@constant int _SC_AIO_LISTIO_MAX@*/
1640 /*@constant int _SC_AIO_MAX@*/
1641 /*@constant int _SC_AIO_PRIO_DELTA_MAX@*/
1642 /*@constant int _SC_ASYNCHRONOUS_IO@*/
1643 /*@constant int _SC_ATEXIT_MAX@*/
1644 /*@constant int _SC_BC_BASE_MAX@*/
1645 /*@constant int _SC_BC_DIM_MAX@*/
1646 /*@constant int _SC_BC_SCALE_MAX@*/
1647 /*@constant int _SC_BC_STRING_MAX@*/
1648 /*@constant int _SC_CHILD_MAX@*/
1649 /*@constant int _SC_CLK_TCK@*/
1650 /*@constant int _SC_COLL_WEIGHTS_MAX@*/
1651 /*@constant int _SC_DELAYTIMER_MAX@*/
1652 /*@constant int _SC_EXPR_NEST_MAX@*/
1653 /*@constant int _SC_FSYNC@*/
1654 /*@constant int _SC_GETGR_R_SIZE_MAX@*/
1655 /*@constant int _SC_GETPW_R_SIZE_MAX@*/
1656 /*@constant int _SC_IOV_MAX@*/
1657 /*@constant int _SC_JOB_CONTROL@*/
1658 /*@constant int _SC_LINE_MAX@*/
1659 /*@constant int _SC_LOGIN_NAME_MAX@*/
1660 /*@constant int _SC_MAPPED_FILES@*/
1661 /*@constant int _SC_MEMLOCK@*/
1662 /*@constant int _SC_MEMLOCK_RANGE@*/
1663 /*@constant int _SC_MEMORY_PROTECTION@*/
1664 /*@constant int _SC_MESSAGE_PASSING@*/
1665 /*@constant int _SC_MQ_OPEN_MAX@*/
1666 /*@constant int _SC_MQ_PRIO_MAX@*/
1667 /*@constant int _SC_NGROUPS_MAX@*/
1668 /*@constant int _SC_OPEN_MAX@*/
1669 /*@constant int _SC_PAGESIZE@*/
1670 /*@constant int _SC_PAGE_SIZE@*/
1671 /*@constant int _SC_PASS_MAX@*/
1672 /*@constant int _SC_PRIORITIZED_IO@*/
1673 /*@constant int _SC_PRIORITY_SCHEDULING@*/
1674 /*@constant int _SC_RE_DUP_MAX@*/
1675 /*@constant int _SC_REALTIME_SIGNALS@*/
1676 /*@constant int _SC_RTSIG_MAX@*/
1677 /*@constant int _SC_SAVED_IDS@*/
1678 /*@constant int _SC_SEMAPHORES@*/
1679 /*@constant int _SC_SEM_NSEMS_MAX@*/
1680 /*@constant int _SC_SEM_VALUE_MAX@*/
1681 /*@constant int _SC_SHARED_MEMORY_OBJECTS@*/
1682 /*@constant int _SC_SIGQUEUE_MAX@*/
1683 /*@constant int _SC_STREAM_MAX@*/
1684 /*@constant int _SC_SYNCHRONIZED_IO@*/
1685 /*@constant int _SC_THREADS@*/
1686 /*@constant int _SC_THREAD_ATTR_STACKADDR@*/
1687 /*@constant int _SC_THREAD_ATTR_STACKSIZE@*/
1688 /*@constant int _SC_THREAD_DESTRUCTOR_ITERATIONS@*/
1689 /*@constant int _SC_THREAD_KEYS_MAX@*/
1690 /*@constant int _SC_THREAD_PRIORITY_SCHEDULING@*/
1691 /*@constant int _SC_THREAD_PRIO_INHERIT@*/
1692 /*@constant int _SC_THREAD_PRIO_PROTECT@*/
1693 /*@constant int _SC_THREAD_PROCESS_SHARED@*/
1694 /*@constant int _SC_THREAD_SAFE_FUNCTIONS@*/
1695 /*@constant int _SC_THREAD_STACK_MIN@*/
1696 /*@constant int _SC_THREAD_THREADS_MAX@*/
1697 /*@constant int _SC_TIMERS@*/
1698 /*@constant int _SC_TIMER_MAX@*/
1699 /*@constant int _SC_TTY_NAME_MAX@*/
1700 /*@constant int _SC_TZNAME_MAX@*/
1701 /*@constant int _SC_VERSION@*/
1702 /*@constant int _SC_XOPEN_VERSION@*/
1703 /*@constant int _SC_XOPEN_CRYPT@*/
1704 /*@constant int _SC_XOPEN_ENH_I18N@*/
1705 /*@constant int _SC_XOPEN_SHM@*/
1706 /*@constant int _SC_XOPEN_UNIX@*/
1707 /*@constant int _SC_XOPEN_XCU_VERSION@*/
1708 /*@constant int _SC_XOPEN_LEGACY@*/
1709 /*@constant int _SC_XOPEN_REALTIME@*/
1710 /*@constant int _SC_XOPEN_REALTIME_THREADS@*/
1711 /*@constant int _SC_XBS5_ILP32_OFF32@*/
1712 /*@constant int _SC_XBS5_ILP32_OFFBIG@*/
1713 /*@constant int _SC_XBS5_LP64_OFF64@*/
1714 /*@constant int _SC_XBS5_LPBIG_OFFBIG@*/
1717 int access(const char *, int) /*@modifies errno@*/ /*:errorcode -1:*/ ;
1718 unsigned int alarm (unsigned int) /*@modifies internalState@*/ ;
1721 /*@modifies errno@*/
1723 /*@warn legacy "brk is obsolete"@*/ ;
1725 int chdir (const char *)
1726 /*@modifies internalState, errno@*/
1727 /*:errorcode -1:*/ ;
1729 int chown (const char *, uid_t, gid_t)
1730 /*@modifies internalState, errno@*/
1731 /*:errorcode -1:*/ ;
1734 /*@modifies internalState, errno@*/
1735 /*:errorcode -1:*/ ;
1737 size_t confstr(int, /*@null@*/ char *, size_t)
1738 /*@globals internalState@*/
1739 /*@modifies errno@*/
1742 /*@dependent@*/ /*@null@*/ char *crypt(const char *, const char *)
1743 /*@modifies errno, internalState@*/ ;
1745 /*@dependent@*/ /*@null@*/ char *ctermid(/*@returned@*/ /*@null@*/ /*@out@*/ char *s)
1748 /*@null@*/ /*@dependent@*/ char *cuserid (/*@null@*/ /*@returned@*/ char *s)
1749 /*@warn legacy "cuserid is obsolete"@*/
1753 /*@modifies errno, internalState@*/
1754 /*:errorcode -1:*/ ;
1757 /*@modifies errno, internalState@*/
1758 /*:errorcode -1:*/ ;
1760 void encrypt(char p_block[], int)
1761 /*@requires maxSet(p_block) == 63@*/
1762 /*@modifies p_block, errno@*/ ;
1764 extern char **environ;
1766 int execl (const char *, const char *, ...)
1767 /*@modifies errno, internalState@*/
1768 /*:errorcode -1:*/ ;
1770 int execle(const char *, const char *, ...)
1771 /*@modifies errno, internalState@*/
1772 /*:errorcode -1:*/ ;
1774 int execlp(const char *, const char *, ...)
1775 /*@modifies errno, internalState@*/
1776 /*:errorcode -1:*/ ;
1778 int execv(const char *, char *const [])
1779 /*@modifies errno, internalState@*/
1780 /*:errorcode -1:*/ ;
1782 int execve(const char *, char *const [], char *const [])
1783 /*@modifies errno, internalState@*/
1784 /*:errorcode -1:*/ ;
1786 int execvp(const char *, char *const [])
1787 /*@modifies errno, internalState@*/
1788 /*:errorcode -1:*/ ;
1790 /*@exits@*/ void _exit (int);
1792 int fchown (int, uid_t, gid_t)
1793 /*@modifies errno, fileSystem@*/
1794 /*:errorcode -1:*/ ;
1797 /*@modifies errno, fileSystem@*/
1798 /*:errorcode -1:*/ ;
1801 /*@modifies errno, fileSystem@*/
1802 /*:errorcode -1:*/ ;
1805 /*@modifies errno, internalState@*/
1806 /*:errorcode -1:*/ ;
1808 long int fpathconf(int, int)
1809 /*@modifies errno, internalState@*/
1810 /*:errorcode -1:*/ ;
1813 /*@modifies errno, fileSystem@*/
1814 /*:errorcode -1:*/ ;
1816 int ftruncate(int, off_t)
1817 /*@modifies errno, fileSystem@*/
1818 /*:errorcode -1:*/ ;
1820 /*@null@*/ char *getcwd (/*@returned@*/ char *buf, size_t size)
1821 /*@requires maxSet(buf) >= size;@*/
1822 /*@modifies errno@*/ ;
1824 int getdtablesize (void)
1825 /*@warn legacy "getdtablesize is obsolete"@*/ ;
1827 gid_t getegid (void) /*@globals internalState*/ ;
1828 uid_t geteuid (void) /*@globals internalState*/ ;
1829 gid_t getgid (void) /*@globals internalState*/ ;
1831 int getgroups (int gidsetsize, gid_t grouplist[])
1832 /*@requires maxSet(grouplist) >= gidsetsize@*/
1833 /*@modifies errno@*/
1834 /*:errorcode -1:*/ ;
1836 long gethostid (void) /*@globals internalState@*/ ;
1838 /*@null@*/ /*@dependent@*/ char *getlogin (void)
1839 /*@modifies errno@*/ ;
1841 int getlogin_r (char *name, size_t namesize)
1842 /*@requires maxSet(name) >= namesize@*/
1843 /*:errorcode !0:*/ ;
1845 extern char *optarg;
1850 int getopt(int, char * const [], const char *)
1851 /*@modifies optind, opterr, optopt, errno@*/
1852 /*:errorcode -1:*/ ;
1854 int getpagesize(void)
1855 /*@warn legacy "getpagesize is obsolete"@*/ ;
1857 /*@dependent@*/ /*@null@*/ char *getpass(/*@nullterminated@*/ const char *)
1858 /*@warn legacy "getpass is obsolete"@*/ ;
1860 pid_t getpgid(pid_t)
1861 /*@modifies errno@*/
1862 /*@globals internalState@*/
1863 /*:errorcode (pid_t)-1:*/ ;
1865 pid_t getpgrp(void) /*@globals internalState*/ ;
1867 pid_t getpid(void) /*@globals internalState*/ ;
1868 pid_t getppid(void) /*@globals internalState*/ ;
1871 /*@modifies errno@*/
1872 /*@globals internalState@*/
1873 /*:errorcode (pid_t)-1:*/ ;
1875 uid_t getuid(void) /*@globals internalState@*/ ;
1877 /*@null@*/ char *getwd (/*@returned@*/ char *path_name)
1878 /*@modifies path_name@*/ ;
1881 /*@globals internalState@*/
1882 /*@modifies errno@*/
1885 int lchown(const char *, uid_t, gid_t)
1886 /*@modifies errno, fileSystem@*/
1887 /*:errorcode -1:*/ ;
1889 int link(const char *, const char *)
1890 /*@modifies errno, fileSystem@*/
1891 /*:errorcode -1:*/ ;
1893 int lockf(int, int, off_t)
1894 /*@modifies errno, fileSystem@*/
1895 /*:errorcode -1:*/ ;
1897 off_t lseek(int, off_t, int)
1898 /*@modifies errno, fileSystem@*/
1899 /*:errorcode (off_t)-1:*/ ;
1902 /*@modifies errno, fileSystem@*/
1903 /*:errorcode -1:*/ ;
1905 long int pathconf(const char *, int)
1906 /*@modifies errno, internalState@*/
1907 /*:errorcode -1:*/ ;
1910 /*@modifies errno, internalState@*/
1911 /*:errorcode -1:*/ ;
1914 /*@requires maxRead(p) == 1@*/
1915 /*@modifies errno, fileSystem@*/
1916 /*:errorcode -1:*/ ;
1918 ssize_t pread(int, /*@out@*/ void *buf, size_t nbyte, off_t offset)
1919 /*@modifies errno, fileSystem@*/
1920 /*@requires maxSet(buf) >= (nbyte - 1) @*/
1921 /*@ensures maxRead(buf) >= nbyte @*/
1922 /*:errorcode -1:*/ ;
1924 int pthread_atfork(void (*)(void), void (*)(void), void(*)(void))
1925 /*@modifies errno, fileSystem@*/
1926 /*:errorcode !0:*/ ;
1928 ssize_t pwrite(int, const void *buf, size_t nbyte, off_t)
1929 /*@requires maxRead(buf) >= nbyte@*/
1930 /*@modifies errno, fileSystem@*/
1931 /*:errorcode -1:*/ ;
1933 /* ssize_t read(int, void *, size_t); in posix.h */
1935 int readlink(const char *, char *buf, size_t bufsize)
1936 /*@requires maxSet(buf) >= (bufsize - 1)@*/
1937 /*@modifies errno, fileSystem, *buf@*/
1938 /*:errorcode -1:*/ ;
1940 /* int rmdir(const char *); in posix.h */
1942 void *sbrk(intptr_t)
1943 /*@modifies errno@*/
1944 /*:errorcode (void *)-1:*/
1945 /*@warn legacy "sbrk is obsolete"@*/ ;
1947 /* int setgid(gid_t);
1948 int setpgid(pid_t, pid_t);
1951 pid_t setpgrp(void) /*@modifies internalState@*/ ;
1953 int setregid(gid_t, gid_t)
1954 /*@modifies errno, internalState@*/
1955 /*:errorcode -1:*/ ;
1957 int setreuid(uid_t, uid_t)
1958 /*@modifies errno, internalState@*/
1959 /*:errorcode -1:*/ ;
1962 /*@modifies errno, internalState@*/
1963 /*:errorcode (pid_t) -1:*/ ;
1966 /*@modifies errno, internalState@*/
1967 /*:errorcode -1:*/ ;
1969 unsigned int sleep(unsigned int)
1970 /*@modifies systemState@*/ ;
1972 void swab(/*@unique@*/ const void *src, /*@unique@*/ void *dest, ssize_t nbytes)
1973 /*@requires maxSet(dest) >= (nbytes - 1)@*/ ;
1975 int symlink(const char *, const char *)
1976 /*@modifies errno, fileSystem@*/
1977 /*:errorcode -1:*/ ;
1979 void sync(void) /*@modifies systemState@*/ ;
1981 long int sysconf(int)
1982 /*@modifies errno, systemState@*/
1983 /*:errorcode -1:*/ ;
1985 pid_t tcgetpgrp(int)
1986 /*@globals systemState@*/
1987 /*@modifies errno@*/
1988 /*:errorcode -1:*/ ;
1990 int tcsetpgrp(int, pid_t)
1991 /*@modifies errno, systemState@*/
1992 /*:errorcode -1:*/ ;
1994 int truncate(const char *, off_t)
1995 /*@modifies errno, fileSystem@*/
1996 /*:errorcode -1:*/ ;
1998 /*@dependent@*/ /*@null@*/ char *ttyname(int)
1999 /*@globals systemState@*/
2000 /*@modifies errno@*/
2001 /*:errorcode -1:*/ ;
2003 int ttyname_r(int, char *name, size_t namesize)
2004 /*@requires maxSet(name) >= (namesize - 1)@*/ ;
2005 /*:errorcode !0:*/ ;
2007 useconds_t ualarm(useconds_t, useconds_t)
2008 /*@modifies systemState@*/ ;
2010 int unlink(const char *)
2011 /*@modifies fileSystem, errno@*/
2012 /*:errorcode -1:*/ ;
2014 int usleep(useconds_t)
2015 /*@modifies fileSystem, errno@*/
2016 /*:errorcode -1:*/ ;
2019 /*@modifies fileSystem, errno@*/
2020 /*:errorcode -1:*/ ;
2022 /* in posix.h ssize_t write(int, const void *, size_t); */
2025 int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path)
2026 /*@modifies internalState, errno@*/
2028 /*@warn superuser "Only super-user processes may call chroot."@*/ ;
2030 int fchroot (int fildes)
2032 /*@warn superuser "Only super-user processes may call fchroot."@*/ ;
2038 ** evans 2001-08-26 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/ctype.h.html
2042 lltX_bool isascii(int) /*@*/ ;
2043 lltX_bool toascii(int) /*@*/ ;
2044 char _toupper(/*@sef@*/ int) /*@*/ ;
2045 char _tolower(/*@sef@*/ int) /*@*/ ;
2047 lltX_bool /*@alt int@*/ isascii(int /*@alt unsigned char@*/) /*@*/ ;
2048 lltX_bool /*@alt int@*/ toascii(int /*@alt unsigned char@*/);
2049 char /*@alt int@*/ _toupper(/*@sef@*/ int /*@alt unsigned char@*/);
2050 char /*@alt int@*/ _tolower(/*@sef@*/ int /*@alt unsigned char@*/);
2053 /* other ctype.h functions in ansi.h */
2058 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/drand48.html
2061 double drand48 (void) /*@modifies internalState@*/ ;
2062 double erand48 (unsigned short int /*@-fixedformalarray@*/ xsubi[3] /*@=fixedformalarray@*/ )
2063 /*@modifies internalState@*/ ;
2065 void srand48 (long int seedval) /*@modifies internalState@*/ ;
2070 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xns/netinetin.h.html
2073 typedef /*@unsignedintegraltype@*/ in_port_t; /* An unsigned integral type of exactly 16 bits. */
2074 typedef /*@unsignedintegraltype@*/ in_addr_t; /* An unsigned integral type of exactly 32 bits. */
2076 /* sa_family_t moved earlier */
2082 struct sockaddr_in {
2083 sa_family_t sin_family;
2085 struct in_addr sin_addr;
2086 unsigned char sin_zero[8];
2090 /* The <netinet/in.h> header defines the following macros for use as values of the level argument of
2091 getsockopt() and setsockopt():
2094 /*@constant int IPPROTO_IP@*/
2095 /*@constant int IPPROTO_ICMP@*/
2096 /*@constant int IPPROTO_TCP@*/
2097 /*@constant int IPPROTO_UDP@*/
2099 /* The <netinet/in.h> header defines the following macros for use as destination addresses for connect(), sendmsg() and sendto():
2102 /*@constant in_addr_t INADDR_ANY@*/
2103 /*@constant in_addr_t INADDR_BROADCAST@*/
2109 in_addr_t htonl (in_addr_t hostlong) /*@*/ ;
2110 in_port_t htons (in_port_t hostshort) /*@*/ ;
2111 in_addr_t ntohl (in_addr_t netlong) /*@*/ ;
2112 in_port_t ntohs (in_port_t netshort) /*@*/ ;
2117 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/dirent.h.html
2120 /*@-redef@*/ /*@-matchfields@*/ /* Has d_ino field, not in posix (?) */
2128 /*@=redef@*/ /*@=matchfields@*/
2130 typedef /*@abstract@*/ DIR;
2132 /*:i32 need to check annotations on these */
2134 int closedir (DIR *) /*:errorcode -1*/ ;
2135 /*@null@*/ /*@dependent@*/ DIR *opendir(const char *) /*@modifies errno, fileSystem@*/ ;
2137 /* in posix.h: struct dirent *readdir(DIR *); */
2139 int readdir_r (DIR *, struct dirent *, /*@out@*/ struct dirent **result)
2140 /*@modifies *result@*/
2141 /*:errorcode !0:*/ ;
2143 void rewinddir(DIR *);
2144 void seekdir(DIR *, long int);
2145 long int telldir(DIR *);
2147 /*drl added these functions
2148 stpcpy and stpncpy are found on linux but
2149 don't seem to be present on other unixes
2151 thanks to Jeff Johnson for pointing out that
2152 these functions were in the unix library
2155 /* this function is like strcpy but it reutrns a pointer to the null terminated character in dest instead of the beginning of dest */
2157 extern char * stpcpy(/*@out@*/ /*@returned@*/ char * dest, const char * src)
2158 /*@modifies *dest @*/
2159 /*@requires maxSet(dest) >= maxRead(src) @*/
2160 /*@ensures MaxRead(dest) == MaxRead (src) /\ MaxRead(result) == 0 /\ MaxSet(result) == ( maxSet(dest) - MaxRead(src) ); @*/;
2163 extern char * stpncpy(/*@out@*/ /*@returned@*/ char * dest,
2164 const char * src, size_t n)
2165 /*@modifies *dest @*/
2166 /*@requires MaxSet(dest) >= ( n - 1 ); @*/ /*@ensures MaxRead (src) >= MaxRead(dest) /\ MaxRead (dest) <= n; @*/
2169 /* drl added 09-25-001
2170 Alexander Ma pointed out these were missing
2173 int usleep (useconds_t useconds) /*@modifies systemState, errno@*/
2174 /*error -1 sucess 0 */
2175 /* warn opengroup unix specification recommends using setitimer(), timer_create(), timer_delete(), timer_getoverrun(), timer_gettime() or
2176 timer_settime() instead of this interface.
2181 /* drl added 10-27-001 */
2182 /*not sure what the exact size of this is
2183 also can IPv6 use this function?
2185 /*I'm going to assume that the address had the format:
2186 "###.###.###.###" which is 16 bytes*/
2188 /*@kept@*/ char *inet_ntoa(struct in_addr in)
2189 /*@ensures maxSet(result) <= 15 /\ maxRead(result) <= 15 @*/
2193 extern double hypot(double x, double y) /*@modifies errno@*/ /*error errno only*/;
2196 extern double j0(double x) /*@modifies errno @*/ /*error 0 or NaN */;
2197 extern double j1(double x) /*@modifies errno @*/ /*error 0 or NaN */;
2198 extern double jn(int n, double x) /*@modifies errno @*/ /*error 0 or NaN */;
2200 extern double y0(double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */ ;
2201 extern double y1 (double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */;
2202 extern double yn (int n, double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */;
2204 extern double acosh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno*/;
2205 extern double asinh(double x) /*@modifies errno @*/ /*error NaN and may errno */;
2207 extern double atanh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno */ ;
2209 extern double lgamma(double x) /*@modifies errno @*/ /*error NaN or HUGE_VAL may set errno */;
2211 extern int signgam ;
2213 extern double erf(double x) /*@modifies errno @*/ /*error NaN or 0 may set errno */;
2215 extern double erfc (double x) /*@modifies errno @*/ /*error NaN or 0