home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / splint3s.zip / splint-3.0.1.6 / lib / posix.h < prev    next >
C/C++ Source or Header  |  2002-02-13  |  22KB  |  947 lines
  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: posix.h,v 1.13 2002/01/07 03:37:25 drl7x Exp $
  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.  
  947.