lib/posix.h

   1 /*
   2 ** posix.h
   3 **
   4 ** This file should be processed with one of the standard libraries
   5 ** (standard.h or strict.h) to produce posix.lcd or posixstrict.lcd.
   6 */
   7
   8 /*@-nextlinemacros@*/
   9 /*@+allimponly@*/
  10 /*@+globsimpmodifiesnothing@*/
  11
  12 /*
  13  * LCLint ISO C + POSIX Library
  14  *
  15  * $Id$
  16  */
  17
  18 /*
  19  * In 1988, IEEE Std 1003.1-1988, commonly known as "POSIX" or the
  20  * "IEEE Portable Operating System Interface for Computing Environments"
  21  * was published as an American National Standard. In 1990, IEEE Std
  22  * 1003.1-1990 was published as an International Standard. The two
  23  * standards differ slightly, and where they do, the 1990 International
  24  * standard was used for this lclint library. The differences are:
  25  *
  26  *  1988: cuserid()
  27  *  1990: -removed- (but still in this lclint library)
  28  *
  29  *  1988:     int read (int, void*, unsigned int)
  30  *  1990: ssize_t read (int, void*, size_t)
  31  *
  32  *  1988:     int write (int, const void*, unsigned int)
  33  *  1990: ssize_t write (int, const void*, size_t)
  34  *
  35  * The other differences are in the semantics of functions.
  36  */
  37
  38 /*
  39  * The reference for the ISO C part of this library was
  40  * Plauger, Brodie's "Standard C - A Reference", Prentice Hall.
  41  * The reference for the POSIX part of this library was
  42  * Donald Lewine's "POSIX Programmer's Guide", O'Reilly.
  43  * Transcription by Jens Schweikhardt <schweikhardt@rus.uni-stuttgart.de>
  44  */
  45
  46 /*
  47  * Note that Amendment 1 to ISO C was published in 1995 after POSIX was out.
  48  * Amendment 1 basically adds support for wide characters and iso 646
  49  * source character sets. In particular, there are three new headers:
  50  * <iso646.h>, <wchar.h>, and <wctype.h>
  51  */
  52
  53 /*
  54  * Each header has annotations in this order:
  55  *
  56  *    1) type definitions (if any)
  57  *    2) constant definitions (if any)
  58  *    3) structure definitions (if any)
  59  *    4) function prototypes and externals (if any)
  60  *
  61  *    5) type definitions augmented by POSIX (if any)
  62  *    6) constant definitions augmented by POSIX (if any)
  63  *    7) structure definitions augmented by POSIX (if any)
  64  *    8) function prototypes and externals augmented by POSIX (if any)
  65  *
  66  * Builtins are mentioned in the header where they appear according to ISO.
  67  */
  68
  69 /*
  70 ** sys/types.h
  71 */
  72
  73 typedef /*@integraltype@*/ dev_t;
  74 typedef /*@integraltype@*/ gid_t;
  75 typedef /*@unsignedintegraltype@*/ ino_t; /*: is this definitely unsigned? */
  76 typedef /*@integraltype@*/ mode_t;
  77 typedef /*@integraltype@*/ nlink_t;
  78 typedef /*@integraltype@*/ off_t;
  79 typedef /*@integraltype@*/ pid_t;
  80 typedef /*@integraltype@*/ uid_t;
  81
  82 /*
  83 ** dirent.h
  84 */
  85
  86 typedef /*@abstract@*/ /*@mutable@*/ void *DIR;
  87
  88 struct dirent {
  89   char  d_name[];
  90 };
  91
  92 extern int closedir (DIR *dirp)
  93    /*@modifies errno@*/;
  94
  95    /*drl 1/4/2001 added the dependent annotation as suggested by
  96      Ralf Wildenhues */
  97
  98    extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname)
  99    /*@modifies errno, fileSystem@*/;
 100
 101 extern /*@null@*/ struct dirent *readdir (DIR *dirp)
 102    /*@modifies errno@*/;
 103
 104 extern void rewinddir (DIR *dirp)
 105    /*@*/;
 106
 107 /*
 108 ** errno.h
 109 */
 110
 111 /*@constant int E2BIG@*/
 112 /*@constant int EACCES@*/
 113 /*@constant int EAGAIN@*/
 114 /*@constant int EBADF@*/
 115 /*@constant int EBUSY@*/
 116 /*@constant int ECHILD@*/
 117 /*@constant int EDEADLK@*/
 118 /*@constant int EEXIST@*/
 119 /*@constant int EFAULT@*/
 120 /*@constant int EFBIG@*/
 121 /*@constant int EINTR@*/
 122 /*@constant int EINVAL@*/
 123 /*@constant int EIO@*/
 124 /*@constant int EISDIR@*/
 125 /*@constant int EMFILE@*/
 126 /*@constant int EMLINK@*/
 127 /*@constant int ENAMETOOLONG@*/
 128 /*@constant int ENFILE@*/
 129 /*@constant int ENODEV@*/
 130 /*@constant int ENOENT@*/
 131 /*@constant int ENOEXEC@*/
 132 /*@constant int ENOLCK@*/
 133 /*@constant int ENOMEM@*/
 134 /*@constant int ENOSPC@*/
 135 /*@constant int ENOSYS@*/
 136 /*@constant int ENOTDIR@*/
 137 /*@constant int ENOTEMPTY@*/
 138 /*@constant int ENOTTY@*/
 139 /*@constant int ENXIO@*/
 140 /*@constant int EPERM@*/
 141 /*@constant int EPIPE@*/
 142 /*@constant int EROFS@*/
 143 /*@constant int ESPIPE@*/
 144 /*@constant int ESRCH@*/
 145 /*@constant int EXDEV@*/
 146
 147 /*
 148 ** fcntl.h
 149 */
 150
 151 /*@constant int FD_CLOEXEC@*/
 152 /*@constant int F_DUPFD@*/
 153 /*@constant int F_GETFD@*/
 154 /*@constant int F_GETFL@*/
 155 /*@constant int F_GETLK@*/
 156 /*@constant int F_RDLCK@*/
 157 /*@constant int F_SETFD@*/
 158 /*@constant int F_SETFL@*/
 159 /*@constant int F_SETLK@*/
 160 /*@constant int F_SETLKW@*/
 161 /*@constant int F_UNLCK@*/
 162 /*@constant int F_WRLCK@*/
 163 /*@constant int O_ACCMODE@*/
 164 /*@constant int O_APPEND@*/
 165 /*@constant int O_CREAT@*/
 166 /*@constant int O_EXCL@*/
 167 /*@constant int O_NOCTTY@*/
 168 /*@constant int O_NONBLOCK@*/
 169 /*@constant int O_RDONLY@*/
 170 /*@constant int O_RDWR@*/
 171 /*@constant int O_TRUNC@*/
 172 /*@constant int O_WRONLY@*/
 173 /*@constant int SEEK_CUR@*/
 174 /*@constant int SEEK_END@*/
 175 /*@constant int SEEK_SET@*/
 176 /*@constant int S_IRGRP@*/
 177 /*@constant int S_IROTH@*/
 178 /*@constant int S_IUSR@*/
 179 /*@constant int S_IWXG@*/
 180 /*@constant int S_IWXO@*/
 181 /*@constant int S_IWXU@*/
 182 /*@constant int S_ISGID@*/
 183 /*@constant int S_ISUID@*/
 184 /*@constant int S_IWGRP@*/
 185 /*@constant int S_IWOTH@*/
 186 /*@constant int S_IWUSR@*/
 187 /*@constant int S_IXGRP@*/
 188 /*@constant int S_IXOTH@*/
 189 /*@constant int S_IXUSR@*/
 190
 191 struct flock {
 192   short l_type;
 193   short l_whence;
 194   off_t l_start;
 195   off_t l_len;
 196   pid_t l_pid;
 197 };
 198
 199 extern int creat (const char *path, mode_t mode)
 200    /*@modifies errno@*/;
 201
 202 extern int fcntl (int fd, int cmd, ...)
 203    /*@modifies errno@*/;
 204
 205 extern int open (const char *path, int oflag, ...)
 206   /*:checkerror -1 - returns -1 on error */
 207   /*@modifies errno@*/;
 208
 209 /*
 210 ** grp.h
 211 */
 212
 213 struct group {
 214   char *gr_name;
 215   gid_t gr_gid;
 216   char **gr_mem;
 217 };
 218
 219         extern /*@null@*/ struct group *
 220 getgrgid (gid_t gid)
 221         /*@modifies errno@*/;
 222
 223         extern /*@null@*/ struct group *
 224 getgrnam (const char *nm)
 225         /*@modifies errno@*/;
 226
 227 /*
 228 ** limits.h
 229 */
 230
 231 /* These are always defined: */
 232
 233 /*@constant int CHAR_BIT@*/
 234 /*@constant char CHAR_MIN@*/
 235 /*@constant char CHAR_MAX@*/
 236 /*@constant int INT_MIN@*/
 237 /*@constant int INT_MAX@*/
 238 /*@constant long LONG_MIN@*/
 239 /*@constant long LONG_MAX@*/
 240 /*@constant int MB_LEN_MAX@*/
 241 /*@constant signed char SCHAR_MIN@*/
 242 /*@constant signed char SCHAR_MAX@*/
 243 /*@constant short SHRT_MIN@*/
 244 /*@constant short SHRT_MAX@*/
 245 /*@constant unsigned char UCHAR_MAX@*/
 246 /*@constant unsigned int UINT_MAX@*/
 247 /*@constant unsigned long ULONG_MAX@*/
 248 /*@constant unsigned short USHRT_MAX@*/
 249
 250 /* When _POSIX_SOURCE is defined */
 251
 252 /*@constant long ARG_MAX@*/
 253 /*@constant long CHILD_MAX@*/
 254 /*@constant long LINK_MAX@*/
 255 /*@constant long MAX_CANON@*/
 256 /*@constant size_t MAX_INPUT@*/ /* evans 2001-10-15 changed type to size_t from long */
 257 /*@constant size_t NAME_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */
 258 /*@constant long NGROUPS_MAX@*/
 259 /*@constant long OPEN_MAX@*/
 260 /*@constant size_t PATH_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */
 261 /*@constant size_t PIPE_BUF@*/ /* evans 2001-10-15 changed type to size_t from long */
 262 /*@constant long SSIZE_MAX@*/
 263 /*@constant long STREAM_MAX@*/
 264 /*@constant long TZNAME_MAX@*/
 265 /*@constant long _POSIX_ARG_MAX@*/
 266 /*@constant long _POSIX_CHILD_MAX@*/
 267 /*@constant long _POSIX_LINK_MAX@*/
 268 /*@constant long _POSIX_MAX_CANON@*/
 269 /*@constant long _POSIX_MAX_INPUT@*/
 270 /*@constant long _POSIX_NAME_MAX@*/
 271 /*@constant long _POSIX_NGROUPS_MAX@*/
 272 /*@constant long _POSIX_OPEN_MAX@*/
 273 /*@constant long _POSIX_PATH_MAX@*/
 274 /*@constant long _POSIX_PIPE_BUF@*/
 275 /*@constant long _POSIX_SSIZE@*/
 276 /*@constant long _POSIX_STREAM@*/
 277 /*@constant long _POSIX_TZNAME_MAX@*/
 278
 279 /*
 280 ** pwd.h
 281 */
 282
 283 struct passwd {
 284   char *pw_name;
 285   uid_t pw_uid;
 286   gid_t pw_gid;
 287   char *pw_dir;
 288   char *pw_shell;
 289 } ;
 290
 291         extern /*@observer@*/ /*@null@*/ struct passwd *
 292         getpwnam (const char *)
 293         /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 294
 295         extern /*@observer@*/ /*@null@*/ struct passwd *
 296 getpwuid (uid_t uid)
 297         /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 298
 299 /*
 300 ** setjmp.h
 301 */
 302
 303 typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf;
 304
 305         extern /*@mayexit@*/ void
 306 siglongjmp (sigjmp_buf env, int val)
 307         /*@*/;
 308
 309         extern int
 310 sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask)
 311         /*@modifies env@*/;
 312
 313 /*
 314 ** signal.h
 315 */
 316
 317 typedef /*@abstract@*/ sigset_t;
 318
 319 /*@constant int SA_NOCLDSTOP@*/
 320 /*@constant int SIG_BLOCK@*/
 321 /*@constant int SIG_SETMASK@*/
 322 /*@constant int SIG_UNBLOCK@*/
 323 /*@constant int SIGALRM@*/
 324 /*@constant int SIGCHLD@*/
 325 /*@constant int SIGCONT@*/
 326 /*@constant int SIGHUP@*/
 327 /*@constant int SIGKILL@*/
 328 /*@constant int SIGPIPE@*/
 329 /*@constant int SIGQUIT@*/
 330 /*@constant int SIGSTOP@*/
 331 /*@constant int SIGTSTP@*/
 332 /*@constant int SIGTTIN@*/
 333 /*@constant int SIGTTOU@*/
 334 /*@constant int SIGUSR1@*/
 335 /*@constant int SIGUSR2@*/
 336
 337 struct sigaction {
 338   void (*sa_handler)();
 339   sigset_t sa_mask;
 340   int sa_flags;
 341 } ;
 342
 343         extern /*@mayexit@*/ int
 344 kill (pid_t pid, int sig)
 345         /*@modifies errno@*/;
 346
 347         extern int
 348 sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact)
 349         /*@modifies *oact, errno, systemState@*/;
 350
 351         extern int
 352 sigaddset (sigset_t *set, int signo)
 353         /*@modifies *set, errno@*/;
 354
 355         extern int
 356 sigdelset (sigset_t *set, int signo)
 357         /*@modifies *set, errno@*/;
 358
 359         extern int
 360 sigemptyset (/*@out@*/ sigset_t *set)
 361         /*@modifies *set, errno@*/;
 362
 363         extern int
 364 sigfillset (/*@out@*/ sigset_t *set)
 365         /*@modifies *set, errno@*/;
 366
 367         extern int
 368 sigismember (const sigset_t *set, int signo)
 369         /*@modifies errno@*/;
 370
 371         extern int
 372 sigpending (/*@out@*/ sigset_t *set)
 373         /*@modifies *set, errno@*/;
 374
 375         extern int
 376 sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset)
 377         /*@modifies *oset, errno, systemState@*/;
 378
 379         extern int
 380 sigsuspend (const sigset_t *sigmask)
 381         /*@modifies errno, systemState@*/;
 382
 383 /*
 384 ** stdio.h
 385 */
 386
 387 /*@constant int L_ctermid@*/
 388 /*@constant int L_cuserid@*/
 389 /*@constant int STREAM_MAX@*/
 390
 391 extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
 392    /*@modifies errno, fileSystem@*/;
 393
 394 extern int fileno (FILE *fp) /*@modifies errno@*/;
 395
 396 /*
 397 ** sys/stat.h
 398 */
 399
 400 /*@constant int S_IRGRP@*/
 401 /*@constant int S_IROTH@*/
 402 /*@constant int S_IUSR@*/
 403 /*@constant int S_IWXG@*/
 404 /*@constant int S_IWXO@*/
 405 /*@constant int S_IWXU@*/
 406 /*@constant int S_ISGID@*/
 407 /*@constant int S_ISUID@*/
 408 /*@constant int S_IWGRP@*/
 409 /*@constant int S_IWOTH@*/
 410 /*@constant int S_IWUSR@*/
 411 /*@constant int S_IXGRP@*/
 412 /*@constant int S_IXOTH@*/
 413 /*@constant int S_IXUSR@*/
 414
 415 struct stat {
 416   mode_t st_mode;
 417   ino_t st_ino;
 418   dev_t st_dev;
 419   nlink_t st_nlink;
 420   uid_t st_uid;
 421   gid_t st_gid;
 422   off_t st_size;
 423   time_t st_atime; /* evans 2001-08-23 - these were previously st_st_atime - POSIX spec says st_atime */
 424   time_t st_mtime; /* evans 2001-08-23 - these were previously st_st_mtime - POSIX spec says st_mtime */
 425   time_t st_ctime; /* evans 2001-08-23 - these were previously st_st_ctime - POSIX spec says st_ctime */
 426 } ;
 427
 428 /*
 429 ** POSIX does not require that the S_I* be functions. They're
 430 ** macros virtually everywhere.
 431 */
 432
 433 # ifdef STRICT
 434 /*@notfunction@*/
 435 # define SBOOLINT lltX_bool /*@alt int@*/
 436 # else
 437 /*@notfunction@*/
 438 # define SBOOLINT lltX_bool
 439 # endif
 440
 441 extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ;
 442
 443 extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ;
 444
 445 extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ;
 446
 447 extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ;
 448
 449 extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ;
 450
 451 int chmod (const char *path, mode_t mode)
 452      /*@modifies fileSystem, errno@*/ ;
 453
 454 int fstat (int fd, /*@out@*/ struct stat *buf)
 455      /*@modifies errno, *buf@*/ ;
 456
 457 int mkdir (const char *path, mode_t mode)
 458      /*@modifies fileSystem, errno@*/;
 459
 460 int mkfifo (const char *path, mode_t mode)
 461      /*@modifies fileSystem, errno@*/;
 462
 463 int stat (const char *path, /*@out@*/ struct stat *buf)
 464      /*:errorcode -1*/
 465      /*@modifies errno, *buf@*/;
 466
 467 int umask (mode_t cmask)
 468      /*@modifies systemState@*/;
 469
 470 /*
 471 ** sys/times.h
 472 */
 473
 474 struct tms {
 475   clock_t       tms_utime;
 476   clock_t       tms_stime;
 477   clock_t       tms_cutime;
 478   clock_t       tms_cstime;
 479 };
 480
 481         extern clock_t
 482 times (/*@out@*/ struct tms *tp)
 483         /*@modifies *tp@*/;
 484
 485 /*
 486 ** sys/utsname.h
 487 */
 488
 489 struct utsname {
 490   char  sysname[];
 491   char  nodename[];
 492   char  release[];
 493   char  version[];
 494   char  machine[];
 495 };
 496
 497         extern int
 498 uname (/*@out@*/ struct utsname *name)
 499      /*@modifies *name, errno@*/ ;
 500
 501 /*
 502 ** sys/wait.h
 503 */
 504
 505 extern int WEXITSTATUS (int status) /*@*/ ;
 506 extern int WIFEXITED (int status) /*@*/ ;
 507 extern int WIFSIGNALED (int status) /*@*/ ;
 508 extern int WIFSTOPPED (int status) /*@*/ ;
 509 extern int WSTOPSIG (int status) /*@*/ ;
 510 extern int WTERMSIG (int status) /*@*/ ;
 511
 512 /*@constant int WUNTRACED@*/
 513
 514 pid_t wait (/*@out@*/ /*@null@*/ int *st)
 515    /*@modifies *st, errno, systemState@*/;
 516
 517 pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
 518    /*@modifies *st, errno, systemState@*/;
 519
 520 /*
 521 ** termios.h
 522 */
 523
 524 typedef unsigned char /*@alt unsigned short@*/ cc_t;
 525 typedef unsigned long /*@alt long@*/ speed_t;
 526 typedef unsigned long /*@alt long@*/ tcflag_t;
 527
 528 /*@constant int B0@*/
 529 /*@constant int B50@*/
 530 /*@constant int B75@*/
 531 /*@constant int B110@*/
 532 /*@constant int B134@*/
 533 /*@constant int B150@*/
 534 /*@constant int B200@*/
 535 /*@constant int B300@*/
 536 /*@constant int B600@*/
 537 /*@constant int B1200@*/
 538 /*@constant int B1800@*/
 539 /*@constant int B2400@*/
 540 /*@constant int B4800@*/
 541 /*@constant int B9600@*/
 542 /*@constant int B19200@*/
 543 /*@constant int B38400@*/
 544 /*@constant int BRKINT@*/
 545 /*@constant int CLOCAL@*/
 546 /*@constant int CREAD@*/
 547 /*@constant int CS5@*/
 548 /*@constant int CS6@*/
 549 /*@constant int CS7@*/
 550 /*@constant int CS8@*/
 551 /*@constant int CSIZE@*/
 552 /*@constant int CSTOPB@*/
 553 /*@constant int ECHO@*/
 554 /*@constant int ECHOE@*/
 555 /*@constant int ECHOK@*/
 556 /*@constant int ECHONL@*/
 557 /*@constant int HUPCL@*/
 558 /*@constant int ICANON@*/
 559 /*@constant int ICRNL@*/
 560 /*@constant int IEXTEN@*/
 561 /*@constant int IGNBRK@*/
 562 /*@constant int IGNCR@*/
 563 /*@constant int IGNPAR@*/
 564 /*@constant int IGNLCR@*/
 565 /*@constant int INPCK@*/
 566 /*@constant int ISIG@*/
 567 /*@constant int ISTRIP@*/
 568 /*@constant int IXOFF@*/
 569 /*@constant int IXON@*/
 570 /*@constant int NCCS@*/
 571 /*@constant int NOFLSH@*/
 572 /*@constant int OPOST@*/
 573 /*@constant int PARENB@*/
 574 /*@constant int PARMRK@*/
 575 /*@constant int PARODD@*/
 576 /*@constant int TCIFLUSH@*/
 577 /*@constant int TCIOFF@*/
 578 /*@constant int TCIOFLUSH@*/
 579 /*@constant int TCION@*/
 580 /*@constant int TCOFLUSH@*/
 581 /*@constant int TCSADRAIN@*/
 582 /*@constant int TCSAFLUSH@*/
 583 /*@constant int TCSANOW@*/
 584 /*@constant int TOSTOP@*/
 585 /*@constant int VEOF@*/
 586 /*@constant int VEOL@*/
 587 /*@constant int VERASE@*/
 588 /*@constant int VINTR@*/
 589 /*@constant int VKILL@*/
 590 /*@constant int VMIN@*/
 591 /*@constant int VQUIT@*/
 592 /*@constant int VSTART@*/
 593 /*@constant int VSTOP@*/
 594 /*@constant int VSUSP@*/
 595 /*@constant int VTIME@*/
 596
 597 struct termios {
 598   tcflag_t      c_iflag;
 599   tcflag_t      c_oflag;
 600   tcflag_t      c_cflag;
 601   tcflag_t      c_lflag;
 602   cc_t          c_cc;
 603 } ;
 604
 605         extern speed_t
 606 cfgetispeed (const struct termios *p)
 607         /*@*/;
 608
 609         extern speed_t
 610 cfgetospeed (const struct termios *p)
 611         /*@*/;
 612
 613         extern int
 614 cfsetispeed (struct termios *p)
 615         /*@modifies *p@*/;
 616
 617         extern int
 618 cfsetospeed (struct termios *p)
 619         /*@modifies *p@*/;
 620
 621         extern int
 622 tcdrain (int fd)
 623         /*@modifies errno@*/;
 624
 625         extern int
 626 tcflow (int fd, int action)
 627         /*@modifies errno@*/;
 628
 629         extern int
 630 tcflush (int fd, int qs)
 631         /*@modifies errno@*/;
 632
 633         extern int
 634 tcgetattr (int fd, /*@out@*/ struct termios *p)
 635         /*@modifies errno, *p@*/;
 636
 637         extern int
 638 tcsendbreak (int fd, int d)
 639         /*@modifies errno@*/;
 640
 641         extern int
 642 tcsetattr (int fd, int opt, const struct termios *p)
 643         /*@modifies errno@*/;
 644
 645 /*
 646 ** time.h
 647 */
 648
 649 /* Environ must be known before it can be used in `globals' clauses. */
 650
 651 /*@unchecked@*/ extern char **environ;
 652
 653 /*@constant int CLK_TCK@*/
 654
 655         extern void
 656 tzset (void)
 657         /*@globals environ@*/ /*@modifies systemState@*/;
 658
 659 /*
 660 ** unistd.h
 661 */
 662
 663 /*@constant int F_OK@*/
 664 /*@constant int R_OK@*/
 665 /*@constant int SEEK_CUR@*/
 666 /*@constant int SEEK_END@*/
 667 /*@constant int SEEK_SET@*/
 668 /*@constant int STDERR_FILENO@*/
 669 /*@constant int STDIN_FILENO@*/
 670 /*@constant int STDOUT_FILENO@*/
 671 /*@constant int W_OK@*/
 672 /*@constant int X_OK@*/
 673 /*@constant int _PC_CHOWN_RESTRUCTED@*/
 674 /*@constant int _PC_MAX_CANON@*/
 675 /*@constant int _PC_MAX_INPUT@*/
 676 /*@constant int _PC_NAME_MAX@*/
 677 /*@constant int _PC_NO_TRUNC@*/
 678 /*@constant int _PC_PATH_MAX@*/
 679 /*@constant int _PC_PIPE_BUF@*/
 680 /*@constant int _PC_VDISABLE@*/
 681 /*@constant int _POSIX_CHOWN_RESTRICTED@*/
 682 /*@constant int _POSIX_JOB_CONTROL@*/
 683 /*@constant int _POSIX_NO_TRUNC@*/
 684 /*@constant int _POSIX_SAVED_IDS@*/
 685 /*@constant int _POSIX_VDISABLE@*/
 686 /*@constant int _POSIX_VERSION@*/
 687 /*@constant int _SC_ARG_MAX@*/
 688 /*@constant int _SC_CHILD_MAX@*/
 689 /*@constant int _SC_CLK_TCK@*/
 690 /*@constant int _SC_JOB_CONTROL@*/
 691 /*@constant int _SC_NGROUPS_MAX@*/
 692 /*@constant int _SC_OPEN_MAX@*/
 693 /*@constant int _SC_SAVED_IDS@*/
 694 /*@constant int _SC_STREAM_MAX@*/
 695 /*@constant int _SC_TZNAME_MAX@*/
 696 /*@constant int _SC_VERSION@*/
 697
 698 extern /*@exits@*/ void _exit (int status) /*@*/;
 699
 700 extern int access (const char *path, int mode) /*@modifies errno@*/;
 701
 702 extern unsigned int alarm (unsigned int) /*@modifies systemState@*/;
 703
 704 extern int chdir (const char *path) /*@modifies errno@*/;
 705
 706 extern int chown (const char *path, uid_t owner, gid_t group)
 707      /*@modifies fileSystem, errno@*/;
 708
 709         extern int
 710 close (int fd)
 711         /*@modifies fileSystem, errno, systemState@*/;
 712         /* state: record locks are unlocked */
 713
 714         extern char *
 715 ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
 716         /*@modifies *s, systemState@*/;
 717
 718         /* cuserid is in the 1988 version of POSIX but removed in 1990 */
 719         extern char *
 720 cuserid (/*@null@*/ /*@out@*/ char *s)
 721         /*@modifies *s@*/;
 722
 723         extern int
 724 dup2 (int fd, int fd2)
 725         /*@modifies errno, fileSystem@*/;
 726
 727         extern int
 728 dup (int fd)
 729         /*@modifies errno, fileSystem@*/;
 730
 731         extern /*@mayexit@*/ int
 732 execl (const char *path, const char *arg, ...)
 733         /*@modifies errno@*/;
 734
 735         extern /*@mayexit@*/ int
 736 execle (const char *file, const char *arg, ...)
 737         /*@modifies errno@*/;
 738
 739         extern /*@mayexit@*/ int
 740 execlp (const char *file, const char *arg, ...)
 741         /*@modifies errno@*/;
 742
 743         extern /*@mayexit@*/ int
 744 execv (const char *path, char *const argv[])
 745         /*@modifies errno@*/;
 746
 747         extern /*@mayexit@*/ int
 748 execve (const char *path, char *const argv[], char *const *envp)
 749         /*@modifies errno@*/;
 750
 751         extern /*@mayexit@*/ int
 752 execvp (const char *file, char *const argv[])
 753         /*@modifies errno@*/;
 754
 755         extern pid_t
 756 fork (void)
 757         /*@modifies fileSystem, errno@*/;
 758
 759         extern long
 760 fpathconf (int fd, int name)
 761         /*@modifies errno@*/;
 762
 763 extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size)
 764      /*@requires maxSet(buf) >= (size - 1)@*/
 765      /*@ensures  maxRead(buf) <= (size - 1)@*/
 766
 767      /*@modifies errno, *buf@*/ ;
 768
 769         extern gid_t
 770 getegid (void)
 771         /*@*/;
 772
 773         extern uid_t
 774 geteuid (void)
 775         /*@*/;
 776
 777         extern gid_t
 778 getgid (void)
 779         /*@*/;
 780
 781         extern int
 782 getgroups (int gs, /*@out@*/ gid_t gl[])
 783         /*@modifies errno, gl[]@*/;
 784
 785         extern /*@observer@*/ char *
 786 getlogin (void)
 787         /*@*/;
 788
 789         extern pid_t
 790 getpgrp (void)
 791         /*@*/;
 792
 793         extern pid_t
 794 getpid (void)
 795         /*@*/;
 796
 797         extern pid_t
 798 getppid (void)
 799         /*@*/;
 800
 801         extern uid_t
 802 getuid (void)
 803         /*@*/;
 804
 805         extern int
 806 isatty (int fd)
 807         /*@*/;
 808
 809         extern int
 810 link (const char *o, const char *n)
 811         /*@modifies errno, fileSystem@*/;
 812
 813         extern off_t
 814 lseek (int fd, off_t offset, int whence)
 815         /*@modifies errno@*/;
 816
 817         extern long
 818 pathconf (const char *path, int name)
 819         /*@modifies errno@*/;
 820
 821         extern int
 822 pause (void)
 823         /*@modifies errno@*/;
 824
 825         extern int
 826 pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */
 827         /*@modifies errno@*/;
 828
 829 extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte)
 830    /*@modifies errno, *buf@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/
 831    /*@ensures maxRead(buf) >= nbyte @*/ ;
 832
 833 extern int rmdir (const char *path)
 834    /*@modifies fileSystem, errno@*/;
 835
 836 extern int setgid (gid_t gid)
 837    /*@modifies errno, systemState@*/;
 838
 839 extern int setpgid (pid_t pid, pid_t pgid)
 840    /*@modifies errno, systemState@*/;
 841
 842 extern pid_t setsid (void) /*@modifies systemState@*/;
 843
 844 extern int setuid (uid_t uid)
 845    /*@modifies errno, systemState@*/;
 846
 847 unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ;
 848
 849 extern long sysconf (int name)
 850    /*@modifies errno@*/;
 851
 852 extern pid_t tcgetpgrp (int fd)
 853    /*@modifies errno@*/;
 854
 855 extern int tcsetpgrp (int fd, pid_t pgrpid)
 856    /*@modifies errno, systemState@*/;
 857
 858 /* Q: observer ok? */
 859 extern /*@null@*/ /*@observer@*/ char *ttyname (int fd)
 860    /*@modifies errno@*/;
 861
 862 extern int unlink (const char *path)
 863    /*@modifies fileSystem, errno@*/;
 864
 865 extern ssize_t write (int fd, const void *buf, size_t nbyte)
 866    /*@modifies errno@*/;
 867
 868 /*
 869 ** utime.h
 870 */
 871
 872 struct utimbuf {
 873   time_t        actime;
 874   time_t        modtime;
 875 } ;
 876
 877         extern int
 878 utime (const char *path, /*@null@*/ const struct utimbuf *times)
 879         /*@modifies fileSystem, errno@*/;
 880
 881 /*
 882 ** regex.h
 883 */
 884
 885 typedef /*@abstract@*/ /*@mutable@*/ void *regex_t;
 886 typedef /*@integraltype@*/ regoff_t;
 887
 888 typedef struct
 889 {
 890   regoff_t rm_so;
 891   regoff_t rm_eo;
 892 } regmatch_t;
 893
 894 int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags)
 895    /*:statusreturn@*/
 896    /*@modifies preg@*/ ;
 897
 898 int regexec (const regex_t *preg, /*@nullterminated@*/ const char *string, size_t nmatch, /*@out@*/ regmatch_t pmatch[], int eflags)
 899    /*@requires maxSet(pmatch) >= nmatch@*/
 900    /*@modifies pmatch@*/ ;
 901
 902 size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size)
 903    /*@requires maxSet(errbuf) >= errbuf_size@*/
 904    /*@modifies errbuf@*/ ;
 905
 906 void regfree (/*@only@*/ regex_t *preg) ;
 907
 908 /* regcomp flags */
 909 /*@constant int REG_BASIC@*/
 910 /*@constant int REG_EXTENDED@*/
 911 /*@constant int REG_ICASE@*/
 912 /*@constant int REG_NOSUB@*/
 913 /*@constant int REG_NEWLINE@*/
 914 /*@constant int REG_NOSPEC@*/
 915 /*@constant int REG_PEND@*/
 916 /*@constant int REG_DUMP@*/
 917
 918 /* regerror flags */
 919 /*@constant int REG_NOMATCH@*/
 920 /*@constant int REG_BADPAT@*/
 921 /*@constant int REG_ECOLLATE@*/
 922 /*@constant int REG_ECTYPE@*/
 923 /*@constant int REG_EESCAPE@*/
 924 /*@constant int REG_ESUBREG@*/
 925 /*@constant int REG_EBRACK@*/
 926 /*@constant int REG_EPAREN@*/
 927 /*@constant int REG_EBRACE@*/
 928 /*@constant int REG_BADBR@*/
 929 /*@constant int REG_ERANGE@*/
 930 /*@constant int REG_ESPACE@*/
 931 /*@constant int REG_BADRPT@*/
 932 /*@constant int REG_EMPTY@*/
 933 /*@constant int REG_ASSERT@*/
 934 /*@constant int REG_INVARG@*/
 935 /*@constant int REG_ATOI@*/ /* non standard */
 936 /*@constant int REG_ITOA@*/ /* non standard */
 937
 938 /* regexec flags */
 939 /*@constant int REG_NOTBOL@*/
 940 /*@constant int REG_NOTEOL@*/
 941 /*@constant int REG_STARTEND@*/
 942 /*@constant int REG_TRACE@*/
 943 /*@constant int REG_LARGE@*/
 944 /*@constant int REG_BACKR@*/
 945
 946