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.
10 /*@+globsimpmodifiesnothing@*/
13 * LCLint ISO C + POSIX Library
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:
27 * 1990: -removed- (but still in this lclint library)
29 * 1988: int read (int, void*, unsigned int)
30 * 1990: ssize_t read (int, void*, size_t)
32 * 1988: int write (int, const void*, unsigned int)
33 * 1990: ssize_t write (int, const void*, size_t)
35 * The other differences are in the semantics of functions.
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>
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>
54 * Each header has annotations in this order:
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)
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)
66 * Builtins are mentioned in the header where they appear according to ISO.
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;
86 typedef /*@abstract@*/ /*@mutable@*/ void *DIR;
92 extern int closedir (DIR *dirp)
95 /*drl 1/4/2001 added the dependent annotation as suggested by
98 extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname)
99 /*@modifies errno, fileSystem@*/;
101 extern /*@dependent@*/ /*@null@*/ struct dirent *readdir (DIR *dirp)
102 /*@modifies errno@*/;
104 extern void rewinddir (DIR *dirp)
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@*/
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@*/
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@*/
185 /*@constant mode_t S_IRWXU@*/
186 /*@constant mode_t S_IRUSR@*/
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@*/
211 extern int creat (const char *path, mode_t mode)
212 /*@modifies errno@*/;
214 extern int fcntl (int fd, int cmd, ...)
215 /*@modifies errno@*/;
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@*/ ;
232 /* evans 2002-07-09: added observer annotation (reported by Enrico Scholz). */
234 /*@observer@*/ /*@null@*/ struct group * getgrgid (gid_t gid)
235 /*@modifies errno@*/;
237 /*@observer@*/ /*@null@*/ struct group *getgrnam (const char *nm)
238 /*@modifies errno@*/;
244 /* These are always defined: */
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@*/
263 /* When _POSIX_SOURCE is defined */
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@*/
304 /*@observer@*/ /*@null@*/ struct passwd *getpwnam (const char *)
305 /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
307 /*@observer@*/ /*@null@*/ struct passwd *getpwuid (uid_t uid)
308 /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
314 typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf;
316 /*@mayexit@*/ void siglongjmp (sigjmp_buf env, int val) /*@*/;
318 int sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) /*@modifies env@*/;
321 ** moved up from signal.h
324 typedef /*@abstract@*/ sigset_t;
336 typedef /*@abstract@*/ mcontext_t;
338 typedef struct s_ucontext_t {
339 /*@null@*/ struct s_ucontext_t *uc_link;
342 mcontext_t uc_mcontext;
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);
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@*/
386 union sigval si_value;
395 void (*sa_handler)();
398 void (*sa_sigaction)(int, siginfo_t *, void *); /* Added 2003-06-13: Noticed by Jerry James */
401 extern /*@mayexit@*/ int
402 kill (pid_t pid, int sig)
403 /*@modifies errno@*/;
406 sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact)
407 /*@modifies *oact, errno, systemState@*/;
410 sigaddset (sigset_t *set, int signo)
411 /*@modifies *set, errno@*/;
414 sigdelset (sigset_t *set, int signo)
415 /*@modifies *set, errno@*/;
418 sigemptyset (/*@out@*/ sigset_t *set)
419 /*@modifies *set, errno@*/;
422 sigfillset (/*@out@*/ sigset_t *set)
423 /*@modifies *set, errno@*/;
426 sigismember (const sigset_t *set, int signo)
427 /*@modifies errno@*/;
430 sigpending (/*@out@*/ sigset_t *set)
431 /*@modifies *set, errno@*/;
434 sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset)
435 /*@modifies *oset, errno, systemState@*/;
438 sigsuspend (const sigset_t *sigmask)
439 /*@modifies errno, systemState@*/;
445 /*@constant int L_ctermid@*/
446 /*@constant int L_cuserid@*/
447 /*@constant int STREAM_MAX@*/
449 extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
450 /*@modifies errno, fileSystem@*/;
452 extern int fileno (FILE *fp) /*@modifies errno@*/;
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 */
472 ** POSIX does not require that the S_I* be functions. They're
473 ** macros virtually everywhere.
478 # define SBOOLINT _Bool /*@alt int@*/
481 # define SBOOLINT _Bool
484 extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ;
486 extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ;
488 extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ;
490 extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ;
492 extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ;
494 int chmod (const char *path, mode_t mode)
495 /*@modifies fileSystem, errno@*/ ;
497 int fstat (int fd, /*@out@*/ struct stat *buf)
498 /*@modifies errno, *buf@*/ ;
500 int mkdir (const char *path, mode_t mode)
501 /*@modifies fileSystem, errno@*/;
503 int mkfifo (const char *path, mode_t mode)
504 /*@modifies fileSystem, errno@*/;
506 int stat (const char *path, /*@out@*/ struct stat *buf)
508 /*@modifies errno, *buf@*/;
510 int umask (mode_t cmask)
511 /*@modifies systemState@*/;
525 times (/*@out@*/ struct tms *tp)
541 uname (/*@out@*/ struct utsname *name)
542 /*@modifies *name, errno@*/ ;
548 extern int WEXITSTATUS (int status) /*@*/ ;
549 extern int WIFEXITED (int status) /*@*/ ;
550 extern int WIFSIGNALED (int status) /*@*/ ;
551 extern int WIFSTOPPED (int status) /*@*/ ;
552 extern int WSTOPSIG (int status) /*@*/ ;
553 extern int WTERMSIG (int status) /*@*/ ;
555 /*@constant int WUNTRACED@*/
557 /* These are in Unix spec, are they in POSIX? */
558 /*@constant int WCONTINUED@*/
559 /*@constant int WNOHANG@*/
561 pid_t wait (/*@out@*/ /*@null@*/ int *st)
562 /*@modifies *st, errno, systemState@*/;
564 pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
565 /*@modifies *st, errno, systemState@*/;
571 typedef unsigned char /*@alt unsigned short@*/ cc_t;
572 typedef unsigned long /*@alt long@*/ speed_t;
573 typedef unsigned long /*@alt long@*/ tcflag_t;
575 /*@constant int B0@*/
576 /*@constant int B50@*/
577 /*@constant int B75@*/
578 /*@constant int B110@*/
579 /*@constant int B134@*/
580 /*@constant int B150@*/
581 /*@constant int B200@*/
582 /*@constant int B300@*/
583 /*@constant int B600@*/
584 /*@constant int B1200@*/
585 /*@constant int B1800@*/
586 /*@constant int B2400@*/
587 /*@constant int B4800@*/
588 /*@constant int B9600@*/
589 /*@constant int B19200@*/
590 /*@constant int B38400@*/
591 /*@constant int BRKINT@*/
592 /*@constant int CLOCAL@*/
593 /*@constant int CREAD@*/
594 /*@constant int CS5@*/
595 /*@constant int CS6@*/
596 /*@constant int CS7@*/
597 /*@constant int CS8@*/
598 /*@constant int CSIZE@*/
599 /*@constant int CSTOPB@*/
600 /*@constant int ECHO@*/
601 /*@constant int ECHOE@*/
602 /*@constant int ECHOK@*/
603 /*@constant int ECHONL@*/
604 /*@constant int HUPCL@*/
605 /*@constant int ICANON@*/
606 /*@constant int ICRNL@*/
607 /*@constant int IEXTEN@*/
608 /*@constant int IGNBRK@*/
609 /*@constant int IGNCR@*/
610 /*@constant int IGNPAR@*/
611 /*@constant int IGNLCR@*/
612 /*@constant int INPCK@*/
613 /*@constant int ISIG@*/
614 /*@constant int ISTRIP@*/
615 /*@constant int IXOFF@*/
616 /*@constant int IXON@*/
617 /*@constant int NCCS@*/
618 /*@constant int NOFLSH@*/
619 /*@constant int OPOST@*/
620 /*@constant int PARENB@*/
621 /*@constant int PARMRK@*/
622 /*@constant int PARODD@*/
623 /*@constant int TCIFLUSH@*/
624 /*@constant int TCIOFF@*/
625 /*@constant int TCIOFLUSH@*/
626 /*@constant int TCION@*/
627 /*@constant int TCOFLUSH@*/
628 /*@constant int TCSADRAIN@*/
629 /*@constant int TCSAFLUSH@*/
630 /*@constant int TCSANOW@*/
631 /*@constant int TOSTOP@*/
632 /*@constant int VEOF@*/
633 /*@constant int VEOL@*/
634 /*@constant int VERASE@*/
635 /*@constant int VINTR@*/
636 /*@constant int VKILL@*/
637 /*@constant int VMIN@*/
638 /*@constant int VQUIT@*/
639 /*@constant int VSTART@*/
640 /*@constant int VSTOP@*/
641 /*@constant int VSUSP@*/
642 /*@constant int VTIME@*/
653 cfgetispeed (const struct termios *p)
657 cfgetospeed (const struct termios *p)
661 cfsetispeed (struct termios *p)
665 cfsetospeed (struct termios *p)
670 /*@modifies errno@*/;
673 tcflow (int fd, int action)
674 /*@modifies errno@*/;
677 tcflush (int fd, int qs)
678 /*@modifies errno@*/;
681 tcgetattr (int fd, /*@out@*/ struct termios *p)
682 /*@modifies errno, *p@*/;
685 tcsendbreak (int fd, int d)
686 /*@modifies errno@*/;
689 tcsetattr (int fd, int opt, const struct termios *p)
690 /*@modifies errno@*/;
696 /* Environ must be known before it can be used in `globals' clauses. */
698 /*@unchecked@*/ extern char **environ;
700 /*@constant int CLK_TCK@*/
704 /*@globals environ@*/ /*@modifies systemState@*/;
710 /*@constant int F_OK@*/
711 /*@constant int R_OK@*/
712 /*@constant int SEEK_CUR@*/
713 /*@constant int SEEK_END@*/
714 /*@constant int SEEK_SET@*/
715 /*@constant int STDERR_FILENO@*/
716 /*@constant int STDIN_FILENO@*/
717 /*@constant int STDOUT_FILENO@*/
718 /*@constant int W_OK@*/
719 /*@constant int X_OK@*/
720 /*@constant int _PC_CHOWN_RESTRUCTED@*/
721 /*@constant int _PC_MAX_CANON@*/
722 /*@constant int _PC_MAX_INPUT@*/
723 /*@constant int _PC_NAME_MAX@*/
724 /*@constant int _PC_NO_TRUNC@*/
725 /*@constant int _PC_PATH_MAX@*/
726 /*@constant int _PC_PIPE_BUF@*/
727 /*@constant int _PC_VDISABLE@*/
728 /*@constant int _POSIX_CHOWN_RESTRICTED@*/
729 /*@constant int _POSIX_JOB_CONTROL@*/
730 /*@constant int _POSIX_NO_TRUNC@*/
731 /*@constant int _POSIX_SAVED_IDS@*/
732 /*@constant int _POSIX_VDISABLE@*/
733 /*@constant int _POSIX_VERSION@*/
734 /*@constant int _SC_ARG_MAX@*/
735 /*@constant int _SC_CHILD_MAX@*/
736 /*@constant int _SC_CLK_TCK@*/
737 /*@constant int _SC_JOB_CONTROL@*/
738 /*@constant int _SC_NGROUPS_MAX@*/
739 /*@constant int _SC_OPEN_MAX@*/
740 /*@constant int _SC_SAVED_IDS@*/
741 /*@constant int _SC_STREAM_MAX@*/
742 /*@constant int _SC_TZNAME_MAX@*/
743 /*@constant int _SC_VERSION@*/
745 extern /*@exits@*/ void _exit (int status) /*@*/;
747 extern int access (const char *path, int mode) /*@modifies errno@*/;
749 extern unsigned int alarm (unsigned int) /*@modifies systemState@*/;
751 extern int chdir (const char *path) /*@modifies errno@*/;
753 extern int chown (const char *path, uid_t owner, gid_t group)
754 /*@modifies fileSystem, errno@*/;
758 /*@modifies fileSystem, errno, systemState@*/;
759 /* state: record locks are unlocked */
762 ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
763 /*@modifies *s, systemState@*/;
765 /* cuserid is in the 1988 version of POSIX but removed in 1990 */
767 cuserid (/*@null@*/ /*@out@*/ char *s)
771 dup2 (int fd, int fd2)
772 /*@modifies errno, fileSystem@*/;
776 /*@modifies errno, fileSystem@*/;
778 extern /*@mayexit@*/ int
779 execl (const char *path, const char *arg, ...)
780 /*@modifies errno@*/;
782 extern /*@mayexit@*/ int
783 execle (const char *file, const char *arg, ...)
784 /*@modifies errno@*/;
786 extern /*@mayexit@*/ int
787 execlp (const char *file, const char *arg, ...)
788 /*@modifies errno@*/;
790 extern /*@mayexit@*/ int
791 execv (const char *path, char *const argv[])
792 /*@modifies errno@*/;
794 extern /*@mayexit@*/ int
795 execve (const char *path, char *const argv[], char *const *envp)
796 /*@modifies errno@*/;
798 extern /*@mayexit@*/ int
799 execvp (const char *file, char *const argv[])
800 /*@modifies errno@*/;
804 /*@modifies fileSystem, errno@*/;
807 fpathconf (int fd, int name)
808 /*@modifies errno@*/;
810 extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size)
811 /*@requires maxSet(buf) >= (size - 1)@*/
812 /*@ensures maxRead(buf) <= (size - 1)@*/
814 /*@modifies errno, *buf@*/ ;
829 getgroups (int gs, /*@out@*/ gid_t gl[])
830 /*@modifies errno, gl[]@*/;
832 extern /*@observer@*/ char *
857 link (const char *o, const char *n)
858 /*@modifies errno, fileSystem@*/;
861 lseek (int fd, off_t offset, int whence)
862 /*@modifies errno@*/;
865 pathconf (const char *path, int name)
866 /*@modifies errno@*/;
870 /*@modifies errno@*/;
873 pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */
874 /*@modifies errno@*/;
876 extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte)
877 /*@modifies errno, *buf@*/
878 /*@requires maxSet(buf) >= (nbyte - 1) @*/
879 /*@ensures maxRead(buf) >= nbyte @*/ ;
881 extern int rmdir (const char *path)
882 /*@modifies fileSystem, errno@*/;
884 extern int setgid (gid_t gid)
885 /*@modifies errno, systemState@*/;
887 extern int setpgid (pid_t pid, pid_t pgid)
888 /*@modifies errno, systemState@*/;
890 extern pid_t setsid (void) /*@modifies systemState@*/;
892 extern int setuid (uid_t uid)
893 /*@modifies errno, systemState@*/;
895 unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ;
897 extern long sysconf (int name)
898 /*@modifies errno@*/;
900 extern pid_t tcgetpgrp (int fd)
901 /*@modifies errno@*/;
903 extern int tcsetpgrp (int fd, pid_t pgrpid)
904 /*@modifies errno, systemState@*/;
906 /* Q: observer ok? */
907 extern /*@null@*/ /*@observer@*/ char *ttyname (int fd)
908 /*@modifies errno@*/;
910 extern int unlink (const char *path)
911 /*@modifies fileSystem, errno@*/;
913 extern ssize_t write (int fd, const void *buf, size_t nbyte)
914 /*@requires maxRead(buf) >= nbyte@*/
915 /*@modifies errno@*/;
927 utime (const char *path, /*@null@*/ const struct utimbuf *times)
928 /*@modifies fileSystem, errno@*/;
934 typedef /*@abstract@*/ /*@mutable@*/ void *regex_t;
935 typedef /*@integraltype@*/ regoff_t;
943 int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags)
945 /*@modifies preg@*/ ;
947 int regexec (const regex_t *preg, /*@nullterminated@*/ const char *string, size_t nmatch, /*@out@*/ regmatch_t pmatch[], int eflags)
948 /*@requires maxSet(pmatch) >= nmatch@*/
949 /*@modifies pmatch@*/ ;
951 size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size)
952 /*@requires maxSet(errbuf) >= errbuf_size@*/
953 /*@modifies errbuf@*/ ;
955 void regfree (/*@only@*/ regex_t *preg) ;
958 /*@constant int REG_BASIC@*/
959 /*@constant int REG_EXTENDED@*/
960 /*@constant int REG_ICASE@*/
961 /*@constant int REG_NOSUB@*/
962 /*@constant int REG_NEWLINE@*/
963 /*@constant int REG_NOSPEC@*/
964 /*@constant int REG_PEND@*/
965 /*@constant int REG_DUMP@*/
968 /*@constant int REG_NOMATCH@*/
969 /*@constant int REG_BADPAT@*/
970 /*@constant int REG_ECOLLATE@*/
971 /*@constant int REG_ECTYPE@*/
972 /*@constant int REG_EESCAPE@*/
973 /*@constant int REG_ESUBREG@*/
974 /*@constant int REG_EBRACK@*/
975 /*@constant int REG_EPAREN@*/
976 /*@constant int REG_EBRACE@*/
977 /*@constant int REG_BADBR@*/
978 /*@constant int REG_ERANGE@*/
979 /*@constant int REG_ESPACE@*/
980 /*@constant int REG_BADRPT@*/
981 /*@constant int REG_EMPTY@*/
982 /*@constant int REG_ASSERT@*/
983 /*@constant int REG_INVARG@*/
984 /*@constant int REG_ATOI@*/ /* non standard */
985 /*@constant int REG_ITOA@*/ /* non standard */
988 /*@constant int REG_NOTBOL@*/
989 /*@constant int REG_NOTEOL@*/
990 /*@constant int REG_STARTEND@*/
991 /*@constant int REG_TRACE@*/
992 /*@constant int REG_LARGE@*/
993 /*@constant int REG_BACKR@*/