lib/unix.h

   1 /*
   2 ** unix.h
   3 */
   4
   5 /*@-nextlinemacros@*/
   6
   7 /*
   8 ** sys/types.h
   9 **
  10 ** evans - 2001-08-27: from http://www.opengroup.org/onlinepubs/007908799/xsh/systypes.h.html
  11 */
  12
  13 typedef /*@integraltype@*/ blkcnt_t;
  14 typedef /*@integraltype@*/ blksize_t;
  15
  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;
  27
  28 /*@=redef@*/
  29
  30 typedef /*@integraltype@*/ clockid_t;
  31 typedef /*@unsignedintegraltype@*/ fsblkcnt_t;
  32 typedef /*@unsignedintegraltype@*/ fsfilcnt_t;
  33 typedef /*@integraltype@*/ id_t;
  34
  35 typedef /*@integraltype@*/ key_t;
  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;
  49
  50 /*
  51 ** Extra stuff in some unixen, not in posix.
  52 */
  53
  54 extern /*@unchecked@*/ int signgam;
  55
  56 /*@-redef@*/ /* Defined by ansi: */
  57 typedef /*@integraltype@*/ clockid_t;
  58 /*@=redef@*/
  59
  60 extern void bcopy (char *b1, /*@out@*/ char *b2, int length)
  61    /*@modifies *b2@*/ ;  /* Yes, the second parameter is the out param! */
  62
  63 extern int /*@alt _Bool@*/ bcmp (char *b1, char *b2, int length) /*@*/ ;
  64    /* Return value is NOT like strcmp! */
  65
  66 extern void bzero (/*@out@*/ char *b1, int length) /*@modifies *b1@*/ ;
  67 extern int ffs (int i) /*@*/ ;
  68 extern int symlink (char *name1, char *name2) /*@modifies fileSystem@*/ ;
  69
  70 extern int
  71   setvbuf_unlocked (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
  72                     int mode, size_t size)
  73   /*@modifies internalState@*/ ;
  74
  75 extern void
  76   setbuffer (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, int size)
  77   /*@modifies internalState@*/ ;
  78
  79 extern void setlinebuf (FILE *stream) /*@modifies internalState@*/ ;
  80
  81 extern int strerror_r (int errnum, /*@out@*/ char *strerrbuf, int buflen)
  82   /*@modifies strerrbuf@*/ ;
  83
  84 extern size_t
  85   fread_unlocked (/*@out@*/ void *ptr, size_t size, size_t nitems,
  86                   FILE *stream)
  87   /*@modifies *stream, *ptr;@*/ ;
  88
  89 extern size_t
  90   fwrite_unlocked (void *pointer, size_t size, size_t num_items, FILE *stream)
  91   /*@modifies *stream;@*/ ;
  92
  93 extern void /*@alt void * @*/
  94   memccpy (/*@returned@*/ /*@out@*/ void *s1,
  95            /*@unique@*/ void *s2, int c, size_t n)
  96   /*@modifies *s1@*/ ;
  97
  98 extern int strcasecmp (char *s1, char *s2) /*@*/ ;
  99 extern int strncasecmp (char *s1, char *s2, int n) /*@*/ ;
 100 extern /*@null@*/ /*@only@*/ char *strdup (char *s) /*@*/ ;
 101
 102 extern /*@null@*/ /*@dependent@*/ char *
 103   index (/*@returned@*/ char *s, char c) /*@*/ ;
 104
 105 extern /*@null@*/ /*@dependent@*/ char *
 106   rindex (/*@returned@*/ char *s, char c) /*@*/ ;
 107
 108 # if 0
 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) /*@*/ ;
 113 # endif
 114
 115
 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@*/
 175
 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@*/
 181
 182 /*@-incondefs@*/ /* some constant are also declared in posix.h*/
 183
 184 /*@constant long NAME_MAX@*/
 185
 186 /*@constant long NGROUPS_MAX@*/
 187
 188 /*@constant long MAX_CANON@*/
 189 /*@constant int MAX_CHAR@*/
 190 /*@constant long OPEN_MAX@*/
 191 /*@constant int PASS_MAX@*/
 192
 193 /*@constant int PID_MAX@*/
 194 /*@constant int SYSPID_MAX@*/
 195 /*@constant long PIPE_BUF@*/
 196 /*@=incondefs@*/
 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 @*/
 212
 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@*/
 226
 227 /*@constant double MAXFLOAT@*/
 228 /*@constant double HUGE@*/
 229
 230 /*@constant int DOMAIN@*/
 231 /*@constant int SING@*/
 232 /*@constant int OVERFLOW@*/
 233 /*@constant int UNDERFLOW@*/
 234 /*@constant int TLOSS@*/
 235 /*@constant int PLOSS@*/
 236
 237 extern /*@unchecked@*/ int daylight;
 238 extern /*@unchecked@*/ long timezone;
 239 extern /*@unchecked@*/ char *tzname[];
 240
 241 /*@-incondefs@*/
 242 extern void tzset(void) /*@modifies daylight, timezone, tzname@*/ ;
 243 /*@=incondefs@*/
 244
 245 /*@-redef@*/ /* Defined by ansi: */
 246 typedef /*@integraltype@*/ key_t;
 247 /*@-incondefs@*/ typedef long timer_t; /*@=incondefs@*/
 248 /*@=redef@*/
 249
 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;
 259 typedef int level_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;
 265 typedef short cnt_t;
 266 typedef int chan_t;
 267 typedef int paddr_t;
 268 typedef void *mid_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;
 275 typedef uint_t uint;
 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;
 289
 290 int ioctl (int d, int /*@alt long@*/ request, /*@out@*/ void *arg)
 291    /*@modifies *arg, errno@*/ ;  /* depends on request! */
 292
 293 pid_t vfork (void) /*@modifies fileSystem@*/ ;
 294
 295 /*
 296 ** sys/uio.h
 297 */
 298
 299 struct iovec {
 300   /*@dependent@*/ void *iov_base;
 301   size_t iov_len; /*: maxSet(iov_base) = iov_len */
 302 };
 303
 304 /* from limits.h */
 305 /*@constant int UIO_MAXIOV@*/   /* BSD */
 306 /*@constant int IOV_MAX@*/      /* supposedly SVR4 */
 307
 308 ssize_t readv (int fd, const struct iovec *iov, int iovcnt)
 309      /*@modifies iov->iov_base, fileSystem, errno@*/;
 310
 311 ssize_t writev (int fd, const struct iovec *iov, int iovcnt)
 312      /*@modifies errno@*/;
 313
 314 /*________________________________________________________________________
 315  * poll.h
 316  */
 317
 318  struct poll {
 319         int fd;
 320         short events;
 321         short revents;
 322 };
 323
 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@*/
 334
 335 extern int poll (struct poll pollfd[], unsigned long nfds, int timeout)
 336   /*@modifies pollfd[].revents, errno@*/ ;
 337
 338 /*
 339 ** free does not take null
 340 */
 341
 342 /*@-incondefs@*/
 343 extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ ;
 344 /*@=incondefs@*/
 345
 346 /*________________________________________________________________________
 347  * sys/socket.h
 348  */
 349
 350
 351
 352
 353 /*@constant int SOCK_RDM@*/
 354
 355
 356
 357
 358
 359
 360
 361 /*@constant int SO_USELOOPBACK@*/
 362
 363
 364 /*@constant int SO_REUSEPORT@*/
 365
 366
 367
 368
 369
 370
 371
 372
 373
 374
 375 /*@constant int AF_LOCAL@*/
 376
 377
 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@*/
 405
 406
 407
 408
 409
 410
 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@*/
 449
 450 /*moved this to before socket.h to get splint to parse the header*/
 451 typedef /*@unsignedintegraltype@*/ sa_family_t;
 452
 453 /*
 454 ** sys/socket.h
 455 ** (updated 26 May 2002)
 456 */
 457
 458 typedef /*@unsignedintegraltype@*/ __socklen_t; /* not in USB, but needed by linux */
 459 typedef /*@unsignedintegraltype@*/ socklen_t;
 460
 461 struct sockaddr {
 462   sa_family_t   sa_family;              /* address family */
 463   char          sa_data[];              /* variable length */
 464 };
 465
 466 struct sockaddr_storage {
 467   sa_family_t ss_family;
 468 } ;
 469
 470 struct msghdr {
 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 */
 478 } ;
 479
 480 struct cmsghdr {
 481   socklen_t cmsg_len;           /* data byte count, including hdr */
 482   int cmsg_level;               /* originating protocol */
 483   int cmsg_type;                /* protocol-specific type */
 484 } ;
 485
 486 /*@constant int SCM_RIGHTS@*/
 487
 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 *) /*@*/ ;
 491
 492 struct linger {
 493   int l_onoff;
 494   int l_linger;
 495 };
 496
 497 /*@constant int SOCK_DGRAM@*/
 498 /*@constant int SOCK_RAW@*/
 499 /*@constant int SOCK_SEQPACKET@*/
 500 /*@constant int SOCK_STREAM@*/
 501
 502 /*@constant int SOL_SOCKET@*/
 503
 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@*/
 520
 521 /*@constant int SOMAXCONN@*/
 522
 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@*/
 530
 531 /*@constant int AF_INET@*/
 532 /*@constant int AF_INET6@*/
 533 /*@constant int AF_UNIX@*/
 534 /*@constant int AF_UNSPEC@*/
 535
 536 /*@constant int SHUT_RD@*/
 537 /*@constant int SHUT_RDWR@*/
 538 /*@constant int SHUT_WR@*/
 539
 540 # if 0
 541 /*
 542 ** These were in the old unix.h spec, but are not in SUS6
 543 */
 544
 545 struct sockproto {
 546   u_short       sp_family;              /* address family */
 547   u_short       sp_protocol;            /* protocol */
 548 };
 549
 550 # endif
 551
 552 int accept (int s, struct sockaddr *addr, int *addrlen)
 553   /*@modifies *addrlen, errno@*/;
 554
 555 int bind (int s, const struct sockaddr *name, int namelen)
 556   /*@modifies errno, fileSystem@*/;
 557
 558 int connect (int s, const struct sockaddr *name, int namelen)
 559   /*@modifies errno, internalState@*/;
 560
 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@*/;
 564
 565 #ifdef STRICT
 566
 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@*/;
 570
 571 #else
 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@*/;
 575
 576 #endif
 577
 578 int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen)
 579         /*@modifies *optval, *optlen, errno@*/;
 580
 581         extern int
 582 listen (int s, int backlog)
 583         /*@modifies errno, internalState@*/;
 584
 585         extern ssize_t
 586 recv (int s, /*@out@*/ void *buf, size_t len, int flags)
 587         /*@modifies *buf, errno@*/;
 588
 589         extern ssize_t
 590 recvfrom (int s, void *buf, size_t len, int flags, /*@null@*/ struct sockaddr *from, int *fromlen)
 591         /*@modifies *buf, *from, *fromlen, errno@*/;
 592
 593         extern ssize_t
 594 recvmsg (int s, struct msghdr *msg, int flags)
 595         /*@modifies msg->msg_iov->iov_base[], errno@*/;
 596
 597         extern ssize_t
 598 send (int s, const void *msg, size_t len, int flags)
 599         /*@modifies errno@*/;
 600
 601         extern ssize_t
 602 sendto (int s, const void *msg, size_t len, int flags, const struct sockaddr *to, int tolen)
 603         /*@modifies errno@*/;
 604
 605         extern ssize_t
 606 sendmsg (int s, const struct msghdr *msg, int flags)
 607         /*@modifies errno@*/;
 608
 609         extern int
 610 setsockopt (int s, int level, int optname, const void *optval, int optlen)
 611         /*@modifies internalState, errno@*/;
 612
 613         extern int
 614 shutdown (int s, int how)
 615         /*@modifies errno@*/;
 616
 617         extern int
 618 socket (int domain, int type, int protocol)
 619         /*@modifies errno@*/;
 620
 621         extern int
 622 socketpair (int d, int type, int protocol, /*@out@*/ int *sv)
 623         /*@modifies errno@*/;
 624
 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@*/
 644
 645 extern void psignal (int sig, const char *msg)
 646    /*@modifies fileSystem@*/;
 647
 648         extern int
 649 setenv (const char *name, const char *value, int overwrite)
 650         /*@globals environ@*/
 651         /*@modifies *environ, errno@*/;
 652
 653         extern void
 654 unsetenv (const char *name)
 655         /*@globals environ@*/
 656         /*@modifies *environ@*/;
 657
 658 /*________________________________________________________________________
 659  * sys/wait.h
 660  */
 661
 662         extern int
 663 WCOREDUMP (int x)
 664         /*@*/;
 665
 666         extern int
 667 W_EXITCODE (int ret, int sig)
 668         /*@*/;
 669
 670         extern int
 671 W_STOPCODE (int sig)
 672         /*@*/;
 673
 674 /*@constant int WAIT_ANY@*/
 675 /*@constant int WAIT_MYPGRP@*/
 676 /*@constant int WSTOPPED@*/
 677
 678         extern pid_t
 679 wait3 (int *statloc, int options, /*@null@*/ /*@out@*/ struct rusage *rusage)
 680         /*@modifies *statloc, *rusage, errno@*/;
 681
 682         extern pid_t
 683 wait4 (pid_t p, int *statloc, int opt, /*@null@*/ /*@out@*/ struct rusage *r)
 684         /*@modifies *statloc, *r, errno@*/;
 685
 686 struct timeval {
 687   long  tv_sec;
 688   long  tv_usec;
 689 } ;
 690
 691 struct timespec {
 692   long  ts_sec;
 693   long  ts_nsec;
 694 } ;
 695
 696 struct timezone {
 697   int   tz_minuteswest;
 698   int   tz_dsttime;
 699 } ;
 700
 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@*/
 708
 709 /*@constant int ITIMER_PROF@*/
 710 /*@constant int ITIMER_REAL@*/
 711 /*@constant int ITIMER_VIRTUAL@*/
 712
 713  struct itimerval {
 714         struct  timeval it_interval;
 715         struct  timeval it_value;
 716 };
 717
 718  struct clockinfo {
 719         int     hz;
 720         int     tick;
 721         int     stathz;
 722         int     profhz;
 723 };
 724
 725         extern int
 726 adjtime (const struct timeval *delta, /*@null@*/ /*@out@*/ struct timeval *olddelta)
 727         /*@modifies internalState, *olddelta, errno@*/;
 728
 729         extern int
 730 getitimer (int which, /*@out@*/ struct itimerval *value)
 731         /*@modifies errno, *value*/;
 732
 733         extern int
 734 gettimeofday (/*@null@*/ /*@out@*/ struct timeval *tp, /*@null@*/ /*@out@*/ struct timezone *tzp)
 735         /*@modifies *tp, *tzp, errno@*/;
 736
 737         extern int
 738 setitimer (int which, struct itimerval *val, /*@null@*/ /*@out@*/ struct itimerval *oval)
 739         /*@modifies *oval, errno, internalState*/;
 740
 741         extern int
 742 settimeofday (const struct timeval *t, const struct timezone *z)
 743         /*@modifies internalState, errno@*/;
 744
 745         extern int
 746 utimes (const char *file, /*@null@*/ const struct timeval *times)
 747         /*@modifies fileSystem, errno*/;
 748
 749 /*________________________________________________________________________
 750  * sys/mman.h
 751  */
 752
 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@*/
 774
 775         extern caddr_t
 776 mmap (/*@null@*/ /*@returned@*/ caddr_t addr, size_t len, int prot, int flags, int fd, off_t offset)
 777         /*@modifies addr@*/;
 778
 779         extern int
 780 madvise (caddr_t addr, int len, int behav)
 781         /*@*/;
 782
 783         extern int
 784 mprotect (caddr_t addr, int len, int prot)
 785         /*@*/;
 786
 787         extern int
 788         int munmap (/*@only@*/ caddr_t addr, size_t len)
 789      /*@modifies fileSystem, *addr, errno @*/;
 790
 791         extern int
 792 msync (caddr_t addr, int len, int flags)
 793         /*@*/;
 794
 795         extern int
 796 mlock (caddr_t addr, size_t len)
 797         /*@*/;
 798
 799         extern int
 800 munlock (caddr_t addr, size_t len)
 801         /*@*/;
 802
 803
 804 /*________________________________________________________________________
 805  * sys/ioctl.h
 806  */
 807
 808  struct winsize {
 809         unsigned short  ws_row;
 810         unsigned short  ws_col;
 811         unsigned short  ws_xpixel;
 812         unsigned short  ws_ypixel;
 813 };
 814
 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@*/
 880
 881 /*@constant int MAXHOSTNAMELEN@*/
 882
 883 extern void FD_CLR (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@modifies *p@*/ ;
 884 extern void FD_COPY (/*@sef@*/ fd_set *f, /*@out@*/ fd_set *t) /*@modifies *t@*/ ;
 885 extern int /*@alt _Bool@*/ FD_ISSET (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@*/ ;
 886 extern void FD_SET (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@modifies *p@*/ ;
 887 extern void FD_ZERO (/*@sef@*/ fd_set /*@out@*/ *p) /*@modifies *p@*/;
 888
 889 extern int fchdir (int fd) /*@modifies internalState, errno@*/;
 890 extern int fchown (int fd, uid_t owner, gid_t group) /*@modifies errno, fileSystem@*/;
 891 extern int fsync (int fd) /*@modifies errno, fileSystem@*/;
 892
 893 extern int ftruncate (int fd, off_t length) /*@modifies errno, fileSystem@*/;
 894
 895 int gethostname (/*@out@*/ char *address, size_t address_len)
 896    /*:errorstatus@*/
 897    /*@modifies address@*/ ;
 898
 899 int initgroups (const char *name, int basegid)
 900    /*@modifies internalState@*/;
 901
 902 int lchown (const char *path, uid_t owner, gid_t group)
 903      /*@modifies errno, fileSystem@*/;
 904
 905 int select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w,
 906             fd_set /*@null@*/ *e, /*@null@*/ struct timeval *t)
 907   /*@modifies *r, *w, *e, *t, errno@*/;
 908   /* evans - 2002-05-26: added null for t, bug reported by Enrico Scholz */
 909
 910 int setegid (gid_t egid)
 911   /*@modifies errno, internalState@*/;
 912
 913 int seteuid (uid_t euid)
 914    /*@modifies errno, internalState@*/;
 915
 916 int setgroups (int ngroups, const gid_t *gidset)
 917    /*@modifies errno, internalState@*/;
 918
 919 int setregid (gid_t rgid, gid_t egid)
 920    /*@modifies errno, internalState@*/;
 921
 922 int setreuid (gid_t ruid, gid_t euid)
 923    /*@modifies errno, internalState@*/;
 924
 925 void sync (void)
 926    /*@modifies fileSystem@*/;
 927
 928 int symlink (const char *path, const char *path2)
 929    /*@modifies fileSystem@*/;
 930
 931 int truncate (const char *name, off_t length)
 932    /*@modifies errno, fileSystem@*/;
 933
 934 /*@constant int EBADRPC@*/
 935 /*@constant int ERPCMISMATCH@*/
 936 /*@constant int EPROGUNAVAIL@*/
 937 /*@constant int EPROGMISMATCH@*/
 938 /*@constant int EPROCUNAVAIL@*/
 939 /*@constant int EFTYPE@*/
 940 /*@constant int EAUTH@*/
 941 /*@constant int ENEEDAUTH@*/
 942 /*@constant int ELAST@*/
 943
 944 /*
 945 ** tar.h
 946 */
 947
 948 /*@unchecked@*/ extern char *TMAGIC;
 949 /*@constant int TMAGLEN@*/
 950 /*@unchecked@*/ extern char *TVERSION;
 951 /*@constant int TVERSLEN@*/
 952
 953 /*@constant int REGTYPE@*/
 954 /*@constant int AREGTYPE@*/
 955 /*@constant int LNKTYPE@*/
 956 /*@constant int SYMTYPE@*/
 957 /*@constant int CHRTYPE@*/
 958 /*@constant int BLKTYPE@*/
 959 /*@constant int DIRTYPE@*/
 960 /*@constant int FIFOTYPE@*/
 961 /*@constant int CONTTYPE@*/
 962
 963 /*@constant int TSUID@*/
 964 /*@constant int TSGID@*/
 965 /*@constant int TSVTX@*/
 966
 967 /*@constant int TUREAD@*/
 968 /*@constant int TUWRITE@*/
 969 /*@constant int TUEXEC@*/
 970 /*@constant int TGREAD@*/
 971 /*@constant int TGWRITE@*/
 972 /*@constant int TGEXEC@*/
 973 /*@constant int TOREAD@*/
 974 /*@constant int TOWRITE@*/
 975 /*@constant int TOEXEC@*/
 976
 977 struct ipc_perm {
 978   uid_t uid;    /* user id */
 979   gid_t gid;    /* group id */
 980   uid_t cuid;   /* creator user id */
 981   gid_t cgid;   /* creator group id */
 982   mode_t        mode;   /* r/w permission */
 983   ulong seq;    /* slot usage sequence number */
 984   key_t key;    /* user specified msg/sem/shm key */
 985 } ;
 986
 987 /*@constant int IPC_R@*/
 988 /*@constant int IPC_W@*/
 989 /*@constant int IPC_M@*/
 990 /*@constant int IPC_CREAT@*/
 991 /*@constant int IPC_EXCL@*/
 992 /*@constant int IPC_NOWAIT@*/
 993 /*@constant key_t IPC_PRIVATE@*/
 994 /*@constant int IPC_RMID@*/
 995 /*@constant int IPC_SET@*/
 996 /*@constant int IPC_STAT@*/
 997
 998 /*
 999 ** sys/msg.h
1000 */
1001
1002  struct msqid_ds {
1003         struct  ipc_perm msg_perm;      /* msg queue permission bits */
1004         struct  msg *msg_first; /* first message in the queue */
1005         struct  msg *msg_last;  /* last message in the queue */
1006         u_long  msg_cbytes;     /* number of bytes in use on the queue */
1007         u_long  msg_qnum;       /* number of msgs in the queue */
1008         u_long  msg_qbytes;     /* max # of bytes on the queue */
1009         pid_t   msg_lspid;      /* pid of last msgsnd() */
1010         pid_t   msg_lrpid;      /* pid of last msgrcv() */
1011         time_t  msg_stime;      /* time of last msgsnd() */
1012         time_t  msg_rtime;      /* time of last msgrcv() */
1013         time_t  msg_ctime;      /* time of last msgctl() */
1014 };
1015
1016  struct mymesg {
1017         long    mtype;          /* message type (+ve integer) */
1018         char    mtext[];        /* message body */
1019 };
1020
1021 /*@constant int MSG_NOERROR@*/
1022 /*@constant int MSGMAX@*/
1023 /*@constant int MSGMNB@*/
1024 /*@constant int MSGMNI@*/
1025 /*@constant int MSGTQL@*/
1026
1027         extern int
1028 msgctl (int id , int cmd, /*@out@*/ struct msqid_ds *buf)
1029         /*@modifies errno, *buf@*/;
1030
1031         extern int
1032 msgget (key_t key, int flag)
1033         /*@modifies errno@*/;
1034
1035         extern int
1036 msgrcv (int id, /*@out@*/ void *ptr, size_t nbytes, long type, int flags)
1037         /*@modifies errno, *ptr@*/;
1038
1039         extern int
1040 msgsnd (int id, const void *ptr, size_t nbytes, int flag)
1041         /*@modifies errno@*/;
1042
1043 /*
1044 ** sys/sem.h
1045 */
1046
1047  struct semid_ds {
1048         struct ipc_perm sem_perm;
1049         struct sem     *sem_base;
1050         ushort          sem_nsems;
1051         time_t          sem_otime;
1052         time_t          sem_ctime;
1053 };
1054
1055  struct sem {
1056         ushort semval;
1057         pid_t  sempid;
1058         ushort semncnt;
1059         ushort semzcnt;
1060 };
1061
1062  union semun {
1063         int val;
1064         struct semid_ds *buf;
1065         ushort *array;
1066 };
1067
1068  struct sembuf {
1069         ushort sem_num;
1070         short sem_op;
1071         short sem_flg;
1072 };
1073
1074 /*@constant int SEM_A@*/
1075 /*@constant int SEMAEM@*/
1076 /*@constant int SEMMNI@*/
1077 /*@constant int SEMMNS@*/
1078 /*@constant int SEMMNU@*/
1079 /*@constant int SEMMSL@*/
1080 /*@constant int SEMOPN@*/
1081 /*@constant int SEM_R@*/
1082 /*@constant int SEMUME@*/
1083 /*@constant int SEM_UNDO@*/
1084 /*@constant int SEMVMX@*/
1085 /*@constant int GETVAL@*/
1086 /*@constant int SETVAL@*/
1087 /*@constant int GETPID@*/
1088 /*@constant int GETNCNT@*/
1089 /*@constant int GETZCNT@*/
1090 /*@constant int GETALL@*/
1091 /*@constant int SETALL@*/
1092
1093 /*@constant int ERMID@*/
1094
1095         extern int
1096 semctl (int id, int semnum, int cmd, union semun arg)
1097         /*@modifies errno@*/;
1098
1099         extern int
1100 semget (key_t key, int nsems, int flag)
1101         /*@modifies errno@*/;
1102
1103         extern int
1104 semop (int id, struct sembuf *semoparray, size_t nops)
1105         /*@modifies errno@*/;
1106
1107 /*
1108 ** sys/shm.h
1109 */
1110
1111  struct shmid_ds {
1112         struct ipc_perm shm_perm;
1113         int shm_segsz;
1114         ushort shm_lkcnt;
1115         pid_t shm_lpid;
1116         pid_t shm_cpid;
1117         ulong shm_nattch;
1118         ulong shm_cnattch;
1119         time_t shm_atime;
1120         time_t shm_dtime;
1121         time_t shm_ctime;
1122 };
1123
1124 /*@constant int SHMLBA@*/
1125 /*@constant int SHM_LOCK@*/
1126 /*@constant int SHMMAX@*/
1127 /*@constant int SHMMIN@*/
1128 /*@constant int SHMMNI@*/
1129 /*@constant int SHM_R@*/
1130 /*@constant int SHM_RDONLY@*/
1131 /*@constant int SHM_RND@*/
1132 /*@constant int SHMSEG@*/
1133 /*@constant int SHM_W@*/
1134 /*@constant int SHM_UNLOCK@*/
1135
1136 void * shmat (int id, /*@null@*/ void *addr, int flag)
1137      /*@modifies errno@*/ ;
1138
1139 extern int shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf)
1140      /*@modifies errno, *buf@*/ ;
1141
1142 extern int shmdt (void *addr)
1143      /*@modifies errno@*/ ;
1144
1145 extern int shmget (key_t key, int size, int flag)
1146      /*@modifies errno@*/ ;
1147
1148
1149 /*
1150 ** stdio.h - in separte file stdio.h
1151 */
1152
1153 /*
1154 ** syslog.h
1155 */
1156
1157 /*@constant int LOG_EMERG@*/
1158 /*@constant int LOG_ALERT@*/
1159 /*@constant int LOG_CRIT@*/
1160 /*@constant int LOG_ERR@*/
1161 /*@constant int LOG_WARNING@*/
1162 /*@constant int LOG_NOTICE@*/
1163 /*@constant int LOG_INFO@*/
1164 /*@constant int LOG_DEBUG@*/
1165
1166 /*@constant int LOG_KERN@*/
1167 /*@constant int LOG_USER@*/
1168 /*@constant int LOG_MAIL@*/
1169 /*@constant int LOG_DAEMON@*/
1170 /*@constant int LOG_AUTH@*/
1171 /*@constant int LOG_SYSLOG@*/
1172 /*@constant int LOG_LPR@*/
1173 /*@constant int LOG_NEWS@*/
1174 /*@constant int LOG_UUCP@*/
1175 /*@constant int LOG_CRON@*/
1176 /*@constant int LOG_AUTHPRIV@*/
1177 /*@constant int LOG_FTP@*/
1178 /*@constant int LOG_LOCAL0@*/
1179 /*@constant int LOG_LOCAL1@*/
1180 /*@constant int LOG_LOCAL2@*/
1181 /*@constant int LOG_LOCAL3@*/
1182 /*@constant int LOG_LOCAL4@*/
1183 /*@constant int LOG_LOCAL5@*/
1184 /*@constant int LOG_LOCAL6@*/
1185 /*@constant int LOG_LOCAL7@*/
1186
1187 /*@constant int LOG_PID@*/
1188 /*@constant int LOG_CONS@*/
1189 /*@constant int LOG_ODELAY@*/
1190 /*@constant int LOG_NDELAY@*/
1191 /*@constant int LOG_NOWAIT@*/
1192 /*@constant int LOG_PERROR@*/
1193
1194 int LOG_MASK (int pri)
1195      /*@*/;
1196
1197 int LOG_UPTO (int pri)
1198      /*@*/;
1199
1200 void closelog (void)
1201      /*@modifies fileSystem@*/;
1202
1203 void openlog (const char *ident, int logopt, int facility)
1204      /*@modifies fileSystem@*/;
1205
1206 int setlogmask (int maskpri)
1207      /*@modifies internalState@*/;
1208
1209 void /*@printflike@*/ syslog (int priority, const char *message, ...)
1210      /*@modifies fileSystem@*/;
1211
1212 void vsyslog (int priority, const char *message, va_list args)
1213      /*@modifies fileSystem@*/;
1214
1215 /*________________________________________________________________________
1216  * pwd.h
1217  */
1218
1219         extern extern void
1220 endpwent (void)
1221         /*@modifies internalState@*/;
1222
1223         extern /*@null@*/ struct passwd *
1224 getpwent (void)
1225         /*@modifies internalState@*/;
1226
1227         extern int
1228 setpassent (int stayopen)
1229         /*@modifies internalState@*/;
1230
1231         extern int
1232 setpwent (void)
1233         /*@modifies internalState@*/;
1234
1235 /*
1236 ** grp.h
1237 */
1238
1239 void endgrent (void) /*@modifies internalState@*/;
1240
1241 /*@null@*/ /*@observer@*/ struct group *getgrent (void)
1242    /*@modifies internalState@*/;
1243
1244 int setgrent (void) /*@modifies internalState@*/;
1245
1246 void setgrfile (const char *name) /*@modifies internalState@*/;
1247
1248 int setgroupent (int stayopen) /*@modifies internalState@*/;
1249
1250 /*
1251 ** sys/stat.h
1252 **
1253 ** evans 2001-08-26 - updated from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstat.h.html
1254 */
1255
1256 /*
1257 ** struct stat replaces POSIX version - more required fields in Unix
1258 */
1259
1260 /*@-redef@*/ /*@-matchfields@*/
1261 struct stat {
1262   dev_t     st_dev; /* ID of device containing file */
1263   ino_t     st_ino; /* file serial number */
1264   mode_t    st_mode; /* mode of file (see below) */
1265   nlink_t   st_nlink; /* number of links to the file */
1266   uid_t     st_uid; /* user ID of file */
1267   gid_t     st_gid; /* group ID of file */
1268   dev_t     st_rdev; /* device ID (if file is character or block special) */
1269   off_t     st_size; /* file size in bytes (if file is a regular file) */
1270   time_t    st_atime; /* time of last access */
1271   time_t    st_mtime; /* time of last data modification */
1272   time_t    st_ctime; /* time of last status change */
1273   blksize_t st_blksize; /* a filesystem-specific preferred I/O block size for
1274                            this object.  In some filesystem types, this may
1275                            vary from file to file */
1276   blkcnt_t  st_blocks; /*  number of blocks allocated for this object */
1277 } ;
1278 /*@=redef@*/ /*@=matchfields@*/
1279
1280 /*@constant mode_t S_IWUSR@*/
1281 /*@constant mode_t S_IXUSR@*/
1282 /*@constant mode_t S_IRWXG@*/
1283 /*@constant mode_t S_IRGRP@*/
1284 /*@constant mode_t S_IWGRP@*/
1285 /*@constant mode_t S_IXGRP@*/
1286 /*@constant mode_t S_IRWXO@*/
1287 /*@constant mode_t S_IROTH@*/
1288 /*@constant mode_t S_IWOTH@*/
1289 /*@constant mode_t S_IXOTH@*/
1290 /*@constant mode_t S_ISUID@*/
1291 /*@constant mode_t S_ISGID@*/
1292 /*@constant mode_t S_ISVTX@*/
1293
1294 # if 0
1295 /*These are the old definitions - they don't appear to be in the Single UNIX Specification */
1296
1297 /*@constant int S_ISTXT@*/
1298 /*@constant int S_IREAD@*/
1299 /*@constant int S_IWRITE@*/
1300 /*@constant int S_IEXEC@*/
1301 /*@constant int S_IFMT@*/
1302 /*@constant int S_IFIFO@*/
1303 /*@constant int S_IFCHR@*/
1304 /*@constant int S_IFDIR@*/
1305 /*@constant int S_IFBLK@*/
1306 /*@constant int S_IFREG@*/
1307 /*@constant int S_IFLNK@*/
1308 /*@constant int S_IFSOCK@*/
1309 /*@constant int S_ISVTX@*/
1310 /*@constant int S_ISVTX@*/
1311 /*@constant int SF_SETTABLE@*/
1312 /*@constant int SF_ARCHIVED@*/
1313 /*@constant int ACCESSPERMS@*/
1314 /*@constant int ALLPERMS@*/
1315 /*@constant int DEFFILEMODE@*/
1316 /*@constant int S_BLKSIZE@*/
1317 /*@constant int SF_IMMUTABLE@*/
1318 /*@constant int SF_APPEND@*/
1319 /*@constant int UF_NODUMP@*/
1320 /*@constant int UF_IMMUTABLE@*/
1321 /*@constant int UF_APPEND@*/
1322 # endif
1323
1324 int /*@alt _Bool@*/ S_ISBLK (/*@sef@*/ mode_t m) /*@*/;
1325 int /*@alt _Bool@*/ S_ISCHR (/*@sef@*/ mode_t m) /*@*/;
1326 int /*@alt _Bool@*/ S_ISDIR (/*@sef@*/ mode_t m) /*@*/;
1327 int /*@alt _Bool@*/ S_ISFIFO (/*@sef@*/ mode_t m) /*@*/;
1328 int /*@alt _Bool@*/ S_ISREG (/*@sef@*/ mode_t m) /*@*/;
1329 int /*@alt _Bool@*/ S_ISLNK (/*@sef@*/ mode_t m) /*@*/;
1330
1331 int /*@alt _Bool@*/ S_TYPEISMQ (/*@sef@*/ struct stat *buf) /*@*/ ;
1332 int /*@alt _Bool@*/ S_TYPEISSEM (/*@sef@*/ struct stat *buf) /*@*/ ;
1333 int /*@alt _Bool@*/ S_TYPEISSHM  (/*@sef@*/ struct stat *buf) /*@*/ ;
1334
1335 /* in POSIX: chmod, fstat, mkdir, mkfifo, stat, umask */
1336
1337 int lstat(const char *, /*@out@*/ struct stat *)
1338      /*:errorcode -1:*/
1339      /*@modifies errno@*/ ;
1340
1341 int mknod (const char *, mode_t, dev_t)
1342   /*@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."@*/
1343   /*:errorcode -1:*/
1344   /*@modifies errno@*/ ;
1345
1346 int chflags (const char *path, u_long flags)
1347   /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
1348   /*@modifies fileSystem, errno@*/;
1349
1350 int fchflags (int fd, u_long flags)
1351   /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
1352   /*@modifies fileSystem, errno@*/;
1353
1354 /* evans 2002-03-17: this was missing, reported by Ralf Wildenhues */
1355 int fchmod(int fildes, mode_t mode)
1356    /*@modifies fileSystem, errno@*/ ;
1357
1358 /*
1359 ** sys/statvfs.h
1360 ** from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstatvfs.h.html
1361 */
1362
1363 struct statvfs {
1364    unsigned long f_bsize;
1365    unsigned long f_frsize;
1366    fsblkcnt_t    f_blocks;
1367    fsblkcnt_t    f_bfree;
1368    fsblkcnt_t    f_bavail;
1369    fsfilcnt_t    f_files;
1370    fsfilcnt_t    f_ffree;
1371    fsfilcnt_t    f_favail;
1372    unsigned long f_fsid;
1373    unsigned long f_flag;
1374    unsigned long f_namemax;
1375 } ;
1376
1377 /*@constant unsigned long ST_RDONLY; @*/
1378 /*@constant unsigned long ST_NOSUID; @*/
1379
1380 int fstatvfs (int fildes, /*@out@*/ struct statvfs *buf)
1381    /*@modifies buf@*/ ;
1382
1383 int statvfs (const char *path, /*@out@*/ struct statvfs *buf)
1384     /*@modifies buf@*/ ;
1385
1386
1387 /*________________________________________________________________________
1388  * stropts.h
1389  */
1390
1391 /*@constant int FMNAMESZ@*/
1392 /*@constant int MSG_BAND@*/
1393 /*@constant int MSG_HIPRI@*/
1394 /*@constant int RS_HIPRI@*/
1395 /*@constant int S_INPUT@*/
1396 /*@constant int S_RDNORM@*/
1397 /*@constant int S_RDBAND@*/
1398 /*@constant int S_BANDURG@*/
1399 /*@constant int S_HIPRI@*/
1400 /*@constant int S_OUTPUT@*/
1401 /*@constant int S_WRNORM@*/
1402 /*@constant int S_WRBAND@*/
1403 /*@constant int S_MSG@*/
1404 /*@constant int S_ERROR@*/
1405 /*@constant int S_HANGUP@*/
1406
1407  struct strbuf {
1408         int maxlen;
1409         int len;
1410         char *buf;
1411 }
1412
1413  struct str_mlist {
1414         char l_name[];
1415 }
1416
1417  struct str_list {
1418         int sl_nmods;
1419         struct str_mlist *sl_modlist;
1420 }
1421
1422         extern int
1423 getmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *f)
1424         /*@modifies *c, *d, errno@*/;
1425
1426         extern int
1427 getpmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *b, int *f)
1428         /*@modifies *b, *c, *d, errno@*/;
1429
1430         extern int
1431 putmsg (int fd, const struct strbuf *c, const struct strbuf *d, int *f)
1432         /*@modifies internalState, errno@*/;
1433
1434 extern int putpmsg (int fd, const struct strbuf *c, const struct strbuf *d, int b, int *f)
1435    /*@modifies internalState, errno@*/;
1436
1437 /*
1438 ** sys/resource.h
1439 **
1440 ** Update 2002-07-09 from
1441 ** http://www.opengroup.org/onlinepubs/007904975/basedefs/sys/resource.h.html
1442 */
1443
1444 /*@constant int PRIO_PROCESS@*/
1445 /*@constant int PRIO_PGRP@*/
1446 /*@constant int PRIO_USER@*/
1447
1448 typedef /*@unsignedintegraltype@*/ rlim_t;
1449
1450 /*@constant rlim_t RLIM_INFINITY@*/
1451 /*@constant rlim_t RLIM_SAVED_MAX@*/
1452 /*@constant rlim_t RLIM_SAVED_CUR@*/
1453
1454 /*@constant int RUSAGE_SELF@*/
1455 /*@constant int RUSAGE_CHILDREN@*/
1456
1457 struct rlimit {
1458   rlim_t rlim_cur;
1459   rlim_t rlim_max;
1460 };
1461
1462 struct rusage {
1463   struct timeval ru_utime;        /* user time used */
1464   struct timeval ru_stime;        /* system time used */
1465   /* other members optional */
1466 };
1467
1468 /*@constant int RLIMIT_CORE@*/
1469 /*@constant int RLIMIT_CPU@*/
1470 /*@constant int RLIMIT_DATA@*/
1471 /*@constant int RLIMIT_FSIZE@*/
1472 /*@constant int RLIMIT_NOFILE@*/
1473 /*@constant int RLIMIT_STACK@*/
1474 /*@constant int RLIMIT_AS@*/
1475
1476 int getpriority (int which, id_t who)
1477    /*@modifies errno@*/;
1478
1479 int getrlimit (int res, /*@out@*/ struct rlimit *rlp)
1480    /*@modifies *rlp, errno@*/;
1481
1482 int getrusage (int who, /*@out@*/ struct rusage *rusage)
1483    /*@modifies *rusage, errno@*/;
1484
1485 int setpriority (int which, id_t who, int prio)
1486    /*@modifies errno, internalState@*/;
1487
1488 int setrlimit (int resource, const struct rlimit *rlp)
1489    /*@modifies errno, internalState@*/;
1490
1491 /*
1492 ** in <netdb.h>
1493 */
1494
1495 struct servent
1496 {
1497   /*@observer@*/ char *s_name;                  /* Official service name.  */
1498   /*@observer@*/ char **s_aliases;              /* Alias list.  */
1499   int s_port;                                   /* Port number.  */
1500   /*@observer@*/ char *s_proto;                 /* Protocol to use.  */
1501 } ;
1502
1503 /*@observer@*/ /*@dependent@*/ /*@null@*/ struct servent *getservbyname (const char *name, /*@null@*/ const char *proto)
1504      /*@warn multithreaded "Unsafe in multithreaded applications, use getsrvbyname_r instead"@*/ ;
1505
1506 struct servent *getservbyname_r (const char *name, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
1507      /*@requires maxSet (buffer) >= buflen@*/ ;
1508
1509
1510 /*@observer@*/ /*@dependent@*/ struct servent *getservbyport (int port, /*@null@*/ const char *proto)
1511      /*@warn multithreaded "Unsafe in multithreaded applications, use getservbyport_r instead"@*/ ;
1512
1513 struct servent *getservbyport_r (int port, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
1514      /*@requires maxSet (buffer) >= buflen@*/ ;
1515
1516 /*@null@*/ struct servent *getservent (void);
1517
1518 /*@null@*/ struct servent *getservent_r (struct servent *result, char *buffer, int buflen);
1519
1520 int setservent (int stayopen);
1521 int endservent (void);
1522
1523 extern int h_errno;
1524
1525 /*@null@*/ /*@observer@*/ struct hostent *gethostbyname (/*@nullterminated@*/ /*@notnull@*/ const char *name)
1526      /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyname_r instead"@*/
1527      /*@modifies h_errno@*/ ;
1528
1529 struct hostent *gethostbyname_r (/*@nullterminated@*/ const char *name, /*@notnull@*/ /*@returned@*/ struct hostent *hent, /*@out@*/ /*@exposed@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
1530      /*@requires maxSet(buffer) >= bufsize@*/ ;
1531
1532 /*@null@*/ /*@observer@*/ struct hostent *gethostbyaddr (/*@notnull@*/ const void *addr, size_t addrlen, int type)
1533      /*@requires maxRead(addr) == addrlen@*/ /*:i534 ??? is this right? */
1534      /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyaddr_r instead"@*/
1535      /*@modifies h_errno@*/ ;
1536
1537 struct hostent *gethostbyaddr_r (/*@notnull@*/ const void *addr, size_t addrlen, int type,
1538                                  /*@returned@*/ /*@out@*/ struct hostent *hent,
1539                                  /*@exposed@*/ /*@out@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
1540      /*@requires maxRead(addr) == addrlen /\ maxSet(buffer) >= bufsize@*/
1541      /*:i534 ??? is this right? */ ;
1542
1543 /*@observer@*/ /*@null@*/ struct hostent *gethostent (void)
1544     /*@warn multithreaded "Unsafe in multithreaded applications, use gethostent_r instead"@*/ ;
1545
1546 struct hostent *gethostent_r (/*@out@*/ /*@returned@*/ struct hostent *hent, /*@exposed@*/ /*@out@*/ char *buffer, int bufsize)
1547      /*@requires maxSet(buffer) >= bufsize@*/ ;
1548
1549 /*:i534 need to annotate these: */
1550
1551 struct hostent *fgethostent(FILE *f);
1552 struct hostent *fgethostent_r(FILE*f, struct hostent *hent, char buffer, int bufsize);
1553 void sethostent(int stayopen);
1554 void endhostent(void);
1555 void herror(const char *string);
1556 char *hstrerror(int err);
1557
1558 struct hostent {
1559   /*@observer@*/ /*@nullterminated@*/ char *h_name;   /* official name of host */
1560   /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_aliases;   /* alias list */
1561   int  h_addrtype;   /* host address type*/
1562   int  h_length;   /* length ofaddress*/
1563   /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_addr_list; /* list of addressesfrom name server */
1564   /*@observer@*/ /*@nullterminated@*/ char *h_addr; /* first address in list (backward compatibility) */
1565 } ;
1566
1567 /*
1568 ** unistd.h
1569 ** from http://www.opengroup.org/onlinepubs/007908799/xsh/unistd.h.html
1570 */
1571
1572 /*@constant int _POSIX_VERSION@*/
1573 /*@constant int _POSIX2_VERSION@*/
1574 /*@constant int _POSIX2_C_VERSION@*/
1575 /*@constant int _XOPEN_VERSION@*/
1576 /*@constant int _XOPEN_XCU_VERSION@*/
1577
1578 /* for access: */
1579
1580 /*@constant int R_OK@*/
1581 /*@constant int W_OK@*/
1582 /*@constant int X_OK@*/
1583 /*@constant int F_OK@*/
1584
1585 /* for confstr: */
1586 /*@constant int _CS_PATH@*/
1587 /*@constant int _CS_XBS5_ILP32_OFF32_CFLAGS@*/
1588 /*@constant int _CS_XBS5_ILP32_OFF32_LDFLAGS@*/
1589 /*@constant int _CS_XBS5_ILP32_OFF32_LIBS@*/
1590 /*@constant int _CS_XBS5_ILP32_OFF32_LINTFLAGS@*/
1591 /*@constant int _CS_XBS5_ILP32_OFFBIG_CFLAGS@*/
1592 /*@constant int _CS_XBS5_ILP32_OFFBIG_LDFLAGS@*/
1593 /*@constant int _CS_XBS5_ILP32_OFFBIG_LIBS@*/
1594 /*@constant int _CS_XBS5_ILP32_OFFBIG_LINTFLAGS@*/
1595 /*@constant int _CS_XBS5_LP64_OFF64_CFLAGS@*/
1596 /*@constant int _CS_XBS5_LP64_OFF64_LDFLAGS@*/
1597 /*@constant int _CS_XBS5_LP64_OFF64_LIBS@*/
1598 /*@constant int _CS_XBS5_LP64_OFF64_LINTFLAGS@*/
1599 /*@constant int _CS_XBS5_LPBIG_OFFBIG_CFLAGS@*/
1600 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LDFLAGS@*/
1601 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LIBS@*/
1602 /*@constant int _CS_XBS5_LPBIG_OFFBIG_LINTFLAGS@*/
1603
1604 /* name parameters to sysconf: */
1605
1606 /*@constant int _SC_2_C_BIND@*/
1607 /*@constant int _SC_2_C_DEV@*/
1608 /*@constant int _SC_2_C_VERSION@*/
1609 /*@constant int _SC_2_FORT_DEV@*/
1610 /*@constant int _SC_2_FORT_RUN@*/
1611 /*@constant int _SC_2_LOCALEDEF@*/
1612 /*@constant int _SC_2_SW_DEV@*/
1613 /*@constant int _SC_2_UPE@*/
1614 /*@constant int _SC_2_VERSION@*/
1615 /*@constant int _SC_ARG_MAX@*/
1616 /*@constant int _SC_AIO_LISTIO_MAX@*/
1617 /*@constant int _SC_AIO_MAX@*/
1618 /*@constant int _SC_AIO_PRIO_DELTA_MAX@*/
1619 /*@constant int _SC_ASYNCHRONOUS_IO@*/
1620 /*@constant int _SC_ATEXIT_MAX@*/
1621 /*@constant int _SC_BC_BASE_MAX@*/
1622 /*@constant int _SC_BC_DIM_MAX@*/
1623 /*@constant int _SC_BC_SCALE_MAX@*/
1624 /*@constant int _SC_BC_STRING_MAX@*/
1625 /*@constant int _SC_CHILD_MAX@*/
1626 /*@constant int _SC_CLK_TCK@*/
1627 /*@constant int _SC_COLL_WEIGHTS_MAX@*/
1628 /*@constant int _SC_DELAYTIMER_MAX@*/
1629 /*@constant int _SC_EXPR_NEST_MAX@*/
1630 /*@constant int _SC_FSYNC@*/
1631 /*@constant int _SC_GETGR_R_SIZE_MAX@*/
1632 /*@constant int _SC_GETPW_R_SIZE_MAX@*/
1633 /*@constant int _SC_IOV_MAX@*/
1634 /*@constant int _SC_JOB_CONTROL@*/
1635 /*@constant int _SC_LINE_MAX@*/
1636 /*@constant int _SC_LOGIN_NAME_MAX@*/
1637 /*@constant int _SC_MAPPED_FILES@*/
1638 /*@constant int _SC_MEMLOCK@*/
1639 /*@constant int _SC_MEMLOCK_RANGE@*/
1640 /*@constant int _SC_MEMORY_PROTECTION@*/
1641 /*@constant int _SC_MESSAGE_PASSING@*/
1642 /*@constant int _SC_MQ_OPEN_MAX@*/
1643 /*@constant int _SC_MQ_PRIO_MAX@*/
1644 /*@constant int _SC_NGROUPS_MAX@*/
1645 /*@constant int _SC_OPEN_MAX@*/
1646 /*@constant int _SC_PAGESIZE@*/
1647 /*@constant int _SC_PAGE_SIZE@*/
1648 /*@constant int _SC_PASS_MAX@*/
1649 /*@constant int _SC_PRIORITIZED_IO@*/
1650 /*@constant int _SC_PRIORITY_SCHEDULING@*/
1651 /*@constant int _SC_RE_DUP_MAX@*/
1652 /*@constant int _SC_REALTIME_SIGNALS@*/
1653 /*@constant int _SC_RTSIG_MAX@*/
1654 /*@constant int _SC_SAVED_IDS@*/
1655 /*@constant int _SC_SEMAPHORES@*/
1656 /*@constant int _SC_SEM_NSEMS_MAX@*/
1657 /*@constant int _SC_SEM_VALUE_MAX@*/
1658 /*@constant int _SC_SHARED_MEMORY_OBJECTS@*/
1659 /*@constant int _SC_SIGQUEUE_MAX@*/
1660 /*@constant int _SC_STREAM_MAX@*/
1661 /*@constant int _SC_SYNCHRONIZED_IO@*/
1662 /*@constant int _SC_THREADS@*/
1663 /*@constant int _SC_THREAD_ATTR_STACKADDR@*/
1664 /*@constant int _SC_THREAD_ATTR_STACKSIZE@*/
1665 /*@constant int _SC_THREAD_DESTRUCTOR_ITERATIONS@*/
1666 /*@constant int _SC_THREAD_KEYS_MAX@*/
1667 /*@constant int _SC_THREAD_PRIORITY_SCHEDULING@*/
1668 /*@constant int _SC_THREAD_PRIO_INHERIT@*/
1669 /*@constant int _SC_THREAD_PRIO_PROTECT@*/
1670 /*@constant int _SC_THREAD_PROCESS_SHARED@*/
1671 /*@constant int _SC_THREAD_SAFE_FUNCTIONS@*/
1672 /*@constant int _SC_THREAD_STACK_MIN@*/
1673 /*@constant int _SC_THREAD_THREADS_MAX@*/
1674 /*@constant int _SC_TIMERS@*/
1675 /*@constant int _SC_TIMER_MAX@*/
1676 /*@constant int _SC_TTY_NAME_MAX@*/
1677 /*@constant int _SC_TZNAME_MAX@*/
1678 /*@constant int _SC_VERSION@*/
1679 /*@constant int _SC_XOPEN_VERSION@*/
1680 /*@constant int _SC_XOPEN_CRYPT@*/
1681 /*@constant int _SC_XOPEN_ENH_I18N@*/
1682 /*@constant int _SC_XOPEN_SHM@*/
1683 /*@constant int _SC_XOPEN_UNIX@*/
1684 /*@constant int _SC_XOPEN_XCU_VERSION@*/
1685 /*@constant int _SC_XOPEN_LEGACY@*/
1686 /*@constant int _SC_XOPEN_REALTIME@*/
1687 /*@constant int _SC_XOPEN_REALTIME_THREADS@*/
1688 /*@constant int _SC_XBS5_ILP32_OFF32@*/
1689 /*@constant int _SC_XBS5_ILP32_OFFBIG@*/
1690 /*@constant int _SC_XBS5_LP64_OFF64@*/
1691 /*@constant int _SC_XBS5_LPBIG_OFFBIG@*/
1692
1693
1694 int access(const char *, int) /*@modifies errno@*/ /*:errorcode -1:*/ ;
1695 unsigned int alarm (unsigned int) /*@modifies internalState@*/ ;
1696
1697 int brk(void *)
1698      /*@modifies errno@*/
1699      /*:errorcode -1:*/
1700      /*@warn legacy "brk is obsolete"@*/ ;
1701
1702 int chdir (const char *)
1703      /*@modifies internalState, errno@*/
1704      /*:errorcode -1:*/ ;
1705
1706 int chown (const char *, uid_t, gid_t)
1707      /*@modifies internalState, errno@*/
1708      /*:errorcode -1:*/ ;
1709
1710 int close (int)
1711      /*@modifies internalState, errno@*/
1712      /*:errorcode -1:*/ ;
1713
1714 size_t confstr(int, /*@null@*/ char *, size_t)
1715      /*@globals internalState@*/
1716      /*@modifies errno@*/
1717      /*:errorcode 0:*/ ;
1718
1719 /*@dependent@*/ /*@null@*/ char *crypt(const char *, const char *)
1720      /*@modifies errno, internalState@*/ ;
1721
1722 /*@dependent@*/ /*@null@*/ char *ctermid(/*@returned@*/ /*@null@*/ /*@out@*/ char *s)
1723      /*@modifies s@*/ ;
1724
1725 /*@null@*/ /*@dependent@*/ char *cuserid (/*@null@*/ /*@returned@*/ char *s)
1726      /*@warn legacy "cuserid is obsolete"@*/
1727      /*@modifies s@*/ ;
1728
1729 int dup(int)
1730      /*@modifies errno, internalState@*/
1731      /*:errorcode -1:*/ ;
1732
1733 int dup2(int, int)
1734      /*@modifies errno, internalState@*/
1735      /*:errorcode -1:*/ ;
1736
1737 void encrypt(char p_block[], int)
1738      /*@requires maxSet(p_block) == 63@*/
1739      /*@modifies p_block, errno@*/ ;
1740
1741 extern char **environ;
1742
1743 int execl (const char *, const char *, ...)
1744      /*@modifies errno, internalState@*/
1745      /*:errorcode -1:*/ ;
1746
1747 int execle(const char *, const char *, ...)
1748      /*@modifies errno, internalState@*/
1749      /*:errorcode -1:*/ ;
1750
1751 int execlp(const char *, const char *, ...)
1752      /*@modifies errno, internalState@*/
1753      /*:errorcode -1:*/ ;
1754
1755 int execv(const char *, char *const [])
1756      /*@modifies errno, internalState@*/
1757      /*:errorcode -1:*/ ;
1758
1759 int execve(const char *, char *const [], char *const [])
1760      /*@modifies errno, internalState@*/
1761      /*:errorcode -1:*/ ;
1762
1763 int execvp(const char *, char *const [])
1764      /*@modifies errno, internalState@*/
1765      /*:errorcode -1:*/ ;
1766
1767 /*@exits@*/ void _exit (int);
1768
1769 int fchown (int, uid_t, gid_t)
1770      /*@modifies errno, fileSystem@*/
1771      /*:errorcode -1:*/ ;
1772
1773 int fchdir (int)
1774      /*@modifies errno, fileSystem@*/
1775      /*:errorcode -1:*/ ;
1776
1777 int fdatasync (int)
1778      /*@modifies errno, fileSystem@*/
1779      /*:errorcode -1:*/ ;
1780
1781 pid_t fork (void)
1782      /*@modifies errno, internalState@*/
1783      /*:errorcode -1:*/ ;
1784
1785 long int fpathconf(int, int)
1786      /*@modifies errno, internalState@*/
1787      /*:errorcode -1:*/ ;
1788
1789 int fsync(int)
1790      /*@modifies errno, fileSystem@*/
1791      /*:errorcode -1:*/ ;
1792
1793 int ftruncate(int, off_t)
1794      /*@modifies errno, fileSystem@*/
1795      /*:errorcode -1:*/ ;
1796
1797 /*@null@*/ char *getcwd (/*@returned@*/ char *buf, size_t size)
1798      /*@requires maxSet(buf) >= size;@*/
1799      /*@modifies errno@*/ ;
1800
1801 int getdtablesize (void)
1802      /*@warn legacy "getdtablesize is obsolete"@*/ ;
1803
1804 gid_t getegid (void) /*@globals internalState*/ ;
1805 uid_t geteuid (void) /*@globals internalState*/ ;
1806 gid_t getgid (void) /*@globals internalState*/ ;
1807
1808 int getgroups (int gidsetsize, gid_t grouplist[])
1809      /*@requires maxSet(grouplist) >= gidsetsize@*/
1810      /*@modifies errno@*/
1811      /*:errorcode -1:*/ ;
1812
1813 long gethostid (void) /*@globals internalState@*/ ;
1814
1815 /*@null@*/ /*@dependent@*/ char *getlogin (void)
1816      /*@modifies errno@*/ ;
1817
1818 int getlogin_r (char *name, size_t namesize)
1819      /*@requires maxSet(name) >= namesize@*/
1820      /*:errorcode !0:*/ ;
1821
1822 extern char *optarg;
1823 extern int optind;
1824 extern int opterr;
1825 extern int optopt;
1826
1827 int getopt(int, char * const [], const char *)
1828      /*@modifies optind, opterr, optopt, errno@*/
1829      /*:errorcode -1:*/ ;
1830
1831 int getpagesize(void)
1832      /*@warn legacy "getpagesize is obsolete"@*/ ;
1833
1834 /*@dependent@*/ /*@null@*/ char *getpass(/*@nullterminated@*/ const char *)
1835      /*@warn legacy "getpass is obsolete"@*/ ;
1836
1837 pid_t getpgid(pid_t)
1838      /*@modifies errno@*/
1839      /*@globals internalState@*/
1840      /*:errorcode (pid_t)-1:*/ ;
1841
1842 pid_t getpgrp(void) /*@globals internalState*/ ;
1843
1844 pid_t getpid(void) /*@globals internalState*/ ;
1845 pid_t getppid(void) /*@globals internalState*/ ;
1846
1847 pid_t getsid(pid_t)
1848      /*@modifies errno@*/
1849      /*@globals internalState@*/
1850      /*:errorcode (pid_t)-1:*/ ;
1851
1852 uid_t getuid(void) /*@globals internalState@*/ ;
1853
1854 /*@null@*/ char *getwd (/*@returned@*/ char *path_name)
1855      /*@modifies path_name@*/ ;
1856
1857 int isatty(int)
1858      /*@globals internalState@*/
1859      /*@modifies errno@*/
1860      /*:errorcode 0:*/ ;
1861
1862 int lchown(const char *, uid_t, gid_t)
1863      /*@modifies errno, fileSystem@*/
1864      /*:errorcode -1:*/ ;
1865
1866 int link(const char *, const char *)
1867      /*@modifies errno, fileSystem@*/
1868      /*:errorcode -1:*/ ;
1869
1870 int lockf(int, int, off_t)
1871      /*@modifies errno, fileSystem@*/
1872      /*:errorcode -1:*/ ;
1873
1874 off_t lseek(int, off_t, int)
1875      /*@modifies errno, fileSystem@*/
1876      /*:errorcode (off_t)-1:*/ ;
1877
1878 int nice(int)
1879      /*@modifies errno, fileSystem@*/
1880      /*:errorcode -1:*/ ;
1881
1882 long int pathconf(const char *, int)
1883      /*@modifies errno, internalState@*/
1884      /*:errorcode -1:*/ ;
1885
1886 int pause(void)
1887      /*@modifies errno, internalState@*/
1888      /*:errorcode -1:*/ ;
1889
1890 int pipe(int p[])
1891      /*@requires maxRead(p) == 1@*/
1892      /*@modifies errno, fileSystem@*/
1893      /*:errorcode -1:*/ ;
1894
1895 ssize_t pread(int, /*@out@*/ void *buf, size_t nbyte, off_t offset)
1896      /*@modifies errno, fileSystem@*/
1897      /*@requires maxSet(buf) >= (nbyte - 1) @*/
1898      /*@ensures maxRead(buf) >= nbyte @*/
1899      /*:errorcode -1:*/ ;
1900
1901 int pthread_atfork(void (*)(void), void (*)(void), void(*)(void))
1902      /*@modifies errno, fileSystem@*/
1903      /*:errorcode !0:*/ ;
1904
1905 ssize_t pwrite(int, const void *buf, size_t nbyte, off_t)
1906      /*@requires maxRead(buf) >= nbyte@*/
1907      /*@modifies errno, fileSystem@*/
1908      /*:errorcode -1:*/ ;
1909
1910 /*     ssize_t      read(int, void *, size_t); in posix.h */
1911
1912 int readlink(const char *, char *buf, size_t bufsize)
1913      /*@requires maxSet(buf) >= (bufsize - 1)@*/
1914      /*@modifies errno, fileSystem, *buf@*/
1915      /*:errorcode -1:*/ ;
1916
1917 /* int          rmdir(const char *); in posix.h */
1918
1919 void *sbrk(intptr_t)
1920      /*@modifies errno@*/
1921      /*:errorcode (void *)-1:*/
1922      /*@warn legacy "sbrk is obsolete"@*/ ;
1923
1924      /*     int          setgid(gid_t);
1925             int          setpgid(pid_t, pid_t);
1926      */
1927
1928 pid_t setpgrp(void) /*@modifies internalState@*/ ;
1929
1930 int setregid(gid_t, gid_t)
1931      /*@modifies errno, internalState@*/
1932      /*:errorcode -1:*/ ;
1933
1934 int setreuid(uid_t, uid_t)
1935      /*@modifies errno, internalState@*/
1936      /*:errorcode -1:*/ ;
1937
1938 pid_t setsid(void)
1939      /*@modifies errno, internalState@*/
1940      /*:errorcode (pid_t) -1:*/ ;
1941
1942 int setuid(uid_t)
1943      /*@modifies errno, internalState@*/
1944      /*:errorcode -1:*/ ;
1945
1946 unsigned int sleep(unsigned int)
1947      /*@modifies systemState@*/ ;
1948
1949 void swab(/*@unique@*/ const void *src, /*@unique@*/ void *dest, ssize_t nbytes)
1950      /*@requires maxSet(dest) >= (nbytes - 1)@*/ ;
1951
1952 int symlink(const char *, const char *)
1953      /*@modifies errno, fileSystem@*/
1954      /*:errorcode -1:*/ ;
1955
1956 void sync(void) /*@modifies systemState@*/ ;
1957
1958 long int sysconf(int)
1959      /*@modifies errno, systemState@*/
1960      /*:errorcode -1:*/ ;
1961
1962 pid_t tcgetpgrp(int)
1963      /*@globals systemState@*/
1964      /*@modifies errno@*/
1965      /*:errorcode -1:*/ ;
1966
1967 int tcsetpgrp(int, pid_t)
1968      /*@modifies errno, systemState@*/
1969      /*:errorcode -1:*/ ;
1970
1971 int truncate(const char *, off_t)
1972      /*@modifies errno, fileSystem@*/
1973      /*:errorcode -1:*/ ;
1974
1975 /*@dependent@*/ /*@null@*/ char *ttyname(int)
1976      /*@globals systemState@*/
1977      /*@modifies errno@*/
1978      /*:errorcode -1:*/ ;
1979
1980 int ttyname_r(int, char *name, size_t namesize)
1981      /*@requires maxSet(name) >= (namesize - 1)@*/ ;
1982      /*:errorcode !0:*/ ;
1983
1984 useconds_t ualarm(useconds_t, useconds_t)
1985      /*@modifies systemState@*/ ;
1986
1987 int unlink(const char *)
1988      /*@modifies fileSystem, errno@*/
1989      /*:errorcode -1:*/ ;
1990
1991 int usleep(useconds_t)
1992      /*@modifies fileSystem, errno@*/
1993      /*:errorcode -1:*/ ;
1994
1995 pid_t vfork(void)
1996      /*@modifies fileSystem, errno@*/
1997      /*:errorcode -1:*/ ;
1998
1999      /* in posix.h ssize_t write(int, const void *, size_t); */
2000
2001
2002 int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path)
2003      /*@modifies internalState, errno@*/
2004      /*:errorcode -1:*/
2005      /*@warn superuser "Only super-user processes may call chroot."@*/ ;
2006
2007 int fchroot (int fildes)
2008    /*:statusreturn@*/
2009    /*@warn superuser "Only super-user processes may call fchroot."@*/ ;
2010
2011
2012 /*
2013 ** ctype.h
2014 **
2015 ** evans 2001-08-26 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/ctype.h.html
2016 */
2017
2018 # ifdef STRICT
2019 _Bool isascii(int) /*@*/ ;
2020 _Bool toascii(int) /*@*/ ;
2021 char _toupper(/*@sef@*/ int) /*@*/ ;
2022 char  _tolower(/*@sef@*/ int) /*@*/ ;
2023 # else
2024 _Bool /*@alt int@*/ isascii(int /*@alt unsigned char@*/) /*@*/ ;
2025 _Bool /*@alt int@*/ toascii(int /*@alt unsigned char@*/);
2026 char  /*@alt int@*/ _toupper(/*@sef@*/ int /*@alt unsigned char@*/);
2027 char /*@alt int@*/ _tolower(/*@sef@*/ int /*@alt unsigned char@*/);
2028 # endif
2029
2030 /* other ctype.h functions in ansi.h */
2031
2032 /*
2033 ** stdlib.h
2034 **
2035 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/drand48.html
2036 */
2037
2038 double drand48 (void) /*@modifies internalState@*/ ;
2039 double erand48 (unsigned short int /*@-fixedformalarray@*/ xsubi[3] /*@=fixedformalarray@*/ )
2040    /*@modifies internalState@*/ ;
2041
2042 void srand48 (long int seedval) /*@modifies internalState@*/ ;
2043
2044 /*
2045 ** netinet/in.h
2046 **
2047 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xns/netinetin.h.html
2048 */
2049
2050 typedef /*@unsignedintegraltype@*/ in_port_t; /* An unsigned integral type of exactly 16 bits. */
2051 typedef /*@unsignedintegraltype@*/ in_addr_t; /* An unsigned integral type of exactly 32 bits. */
2052
2053 /* sa_family_t moved earlier */
2054
2055 struct in_addr {
2056   in_addr_t      s_addr;
2057 } ;
2058
2059 struct sockaddr_in {
2060   sa_family_t    sin_family;
2061   in_port_t      sin_port;
2062   struct in_addr sin_addr;
2063   unsigned char  sin_zero[8];
2064 } ;
2065
2066
2067 /* The <netinet/in.h> header defines the following macros for use as values of the level argument of
2068    getsockopt() and setsockopt():
2069  */
2070
2071 /*@constant int IPPROTO_IP@*/
2072 /*@constant int IPPROTO_ICMP@*/
2073 /*@constant int IPPROTO_TCP@*/
2074 /*@constant int IPPROTO_UDP@*/
2075
2076 /* The <netinet/in.h> header defines the following macros for use as destination addresses for connect(), sendmsg() and sendto():
2077  */
2078
2079 /*@constant in_addr_t INADDR_ANY@*/
2080 /*@constant in_addr_t INADDR_BROADCAST@*/
2081
2082 /*
2083 ** arpa/inet.h
2084 */
2085
2086 in_addr_t htonl (in_addr_t hostlong) /*@*/ ;
2087 in_port_t htons (in_port_t hostshort) /*@*/ ;
2088 in_addr_t ntohl (in_addr_t netlong) /*@*/ ;
2089 in_port_t ntohs (in_port_t netshort) /*@*/ ;
2090
2091 /*
2092 ** dirent.h
2093 **
2094 ** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/dirent.h.html
2095 */
2096
2097 /*@-redef@*/ /*@-matchfields@*/ /* Has d_ino field, not in posix (?) */
2098
2099 struct dirent
2100 {
2101   ino_t  d_ino;
2102   char   d_name[];
2103 } ;
2104
2105 /*@=redef@*/ /*@=matchfields@*/
2106
2107 typedef /*@abstract@*/ DIR;
2108
2109 /*:i32 need to check annotations on these */
2110
2111 int closedir (DIR *) /*:errorcode -1*/ ;
2112 /*@null@*/ /*@dependent@*/ DIR *opendir(const char *)  /*@modifies errno, fileSystem@*/ ;
2113
2114 /* in posix.h: struct dirent *readdir(DIR *); */
2115
2116 int readdir_r (DIR *, struct dirent *, /*@out@*/ struct dirent **result)
2117      /*@modifies *result@*/
2118      /*:errorcode !0:*/ ;
2119
2120 void rewinddir(DIR *);
2121 void seekdir(DIR *, long int);
2122 long int telldir(DIR *);
2123
2124 /*drl added these functions
2125   stpcpy and stpncpy are found on linux but
2126   don't seem to be present on other unixes
2127
2128   thanks to Jeff Johnson for pointing out that
2129   these functions were in the unix library
2130 */
2131
2132 /* this function is like strcpy but it reutrns a pointer to the null terminated character in dest instead of the beginning of dest */
2133
2134 extern char * stpcpy(/*@out@*/ /*@returned@*/ char * dest, const char * src)
2135              /*@modifies *dest @*/
2136      /*@requires maxSet(dest) >= maxRead(src) @*/
2137      /*@ensures MaxRead(dest) == MaxRead (src) /\ MaxRead(result) == 0 /\ MaxSet(result) == ( maxSet(dest) - MaxRead(src) ); @*/;
2138
2139
2140 extern char * stpncpy(/*@out@*/ /*@returned@*/ char * dest,
2141                       const char * src, size_t n)
2142            /*@modifies *dest @*/
2143    /*@requires MaxSet(dest) >= ( n - 1 ); @*/ /*@ensures MaxRead (src) >= MaxRead(dest) /\ MaxRead (dest) <= n; @*/
2144   ;
2145
2146   /* drl added 09-25-001
2147      Alexander Ma pointed out these were missing
2148   */
2149
2150 int usleep (useconds_t useconds) /*@modifies systemState, errno@*/
2151      /*error -1 sucess 0 */
2152      /* warn opengroup unix specification recommends using setitimer(), timer_create(), timer_delete(), timer_getoverrun(), timer_gettime() or
2153      timer_settime() instead of this interface.
2154      */
2155      ;
2156
2157
2158      /* drl added 10-27-001 */
2159          /*not sure what the exact size of this is
2160        also can IPv6 use this function?
2161       */
2162      /*I'm going to assume that the address had the format:
2163        "###.###.###.###" which is 16 bytes*/
2164
2165        /*@kept@*/ char *inet_ntoa(struct in_addr in)
2166      /*@ensures maxSet(result) <= 15 /\ maxRead(result) <= 15 @*/
2167      ;
2168
2169
2170      extern  double hypot(double x, double y) /*@modifies errno@*/ /*error errno only*/;
2171
2172
2173      extern double j0(double x) /*@modifies errno @*/ /*error 0 or NaN */;
2174  extern      double j1(double x) /*@modifies errno @*/ /*error 0 or NaN */;
2175  extern      double jn(int n, double x) /*@modifies errno @*/ /*error 0 or NaN */;
2176
2177      extern double y0(double x) /*@modifies errno @*/  /*error NaN -HUGE_VAL 0.0 */     ;
2178      extern      double y1 (double x) /*@modifies errno @*/  /*error NaN -HUGE_VAL 0.0 */;
2179      extern      double yn (int n, double x)  /*@modifies errno @*/  /*error NaN -HUGE_VAL 0.0 */;
2180
2181      extern       double acosh(double x)  /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno*/;
2182      extern       double asinh(double x) /*@modifies errno @*/  /*error NaN and may errno */;
2183
2184   extern        double atanh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno */ ;
2185
2186      extern         double lgamma(double x)  /*@modifies errno @*/  /*error NaN or HUGE_VAL may set errno */;
2187
2188      extern int signgam ;
2189
2190       extern      double erf(double x)  /*@modifies errno @*/  /*error NaN or 0 may set errno */;
2191
2192    extern      double erfc (double x) /*@modifies errno @*/  /*error NaN or 0
2193                                         may set errno */;
2194
2195
2196
2197
2198
2199