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