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