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