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