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