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