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 extern /*@null@*/ DIR *opendir (const char *dirname)
98 extern /*@null@*/ struct dirent *readdir (DIR *dirp)
101 extern void rewinddir (DIR *dirp)
108 /*@constant int E2BIG@*/
109 /*@constant int EACCES@*/
110 /*@constant int EAGAIN@*/
111 /*@constant int EBADF@*/
112 /*@constant int EBUSY@*/
113 /*@constant int ECHILD@*/
114 /*@constant int EDEADLK@*/
115 /*@constant int EEXIST@*/
116 /*@constant int EFAULT@*/
117 /*@constant int EFBIG@*/
118 /*@constant int EINTR@*/
119 /*@constant int EINVAL@*/
120 /*@constant int EIO@*/
121 /*@constant int EISDIR@*/
122 /*@constant int EMFILE@*/
123 /*@constant int EMLINK@*/
124 /*@constant int ENAMETOOLONG@*/
125 /*@constant int ENFILE@*/
126 /*@constant int ENODEV@*/
127 /*@constant int ENOENT@*/
128 /*@constant int ENOEXEC@*/
129 /*@constant int ENOLCK@*/
130 /*@constant int ENOMEM@*/
131 /*@constant int ENOSPC@*/
132 /*@constant int ENOSYS@*/
133 /*@constant int ENOTDIR@*/
134 /*@constant int ENOTEMPTY@*/
135 /*@constant int ENOTTY@*/
136 /*@constant int ENXIO@*/
137 /*@constant int EPERM@*/
138 /*@constant int EPIPE@*/
139 /*@constant int EROFS@*/
140 /*@constant int ESPIPE@*/
141 /*@constant int ESRCH@*/
142 /*@constant int EXDEV@*/
148 /*@constant int FD_CLOEXEC@*/
149 /*@constant int F_DUPFD@*/
150 /*@constant int F_GETFD@*/
151 /*@constant int F_GETFL@*/
152 /*@constant int F_GETLK@*/
153 /*@constant int F_RDLCK@*/
154 /*@constant int F_SETFD@*/
155 /*@constant int F_SETFL@*/
156 /*@constant int F_SETLK@*/
157 /*@constant int F_SETLKW@*/
158 /*@constant int F_UNLCK@*/
159 /*@constant int F_WRLCK@*/
160 /*@constant int O_ACCMODE@*/
161 /*@constant int O_APPEND@*/
162 /*@constant int O_CREAT@*/
163 /*@constant int O_EXCL@*/
164 /*@constant int O_NOCTTY@*/
165 /*@constant int O_NONBLOCK@*/
166 /*@constant int O_RDONLY@*/
167 /*@constant int O_RDWR@*/
168 /*@constant int O_TRUNC@*/
169 /*@constant int O_WRONLY@*/
170 /*@constant int SEEK_CUR@*/
171 /*@constant int SEEK_END@*/
172 /*@constant int SEEK_SET@*/
173 /*@constant int S_IRGRP@*/
174 /*@constant int S_IROTH@*/
175 /*@constant int S_IUSR@*/
176 /*@constant int S_IWXG@*/
177 /*@constant int S_IWXO@*/
178 /*@constant int S_IWXU@*/
179 /*@constant int S_ISGID@*/
180 /*@constant int S_ISUID@*/
181 /*@constant int S_IWGRP@*/
182 /*@constant int S_IWOTH@*/
183 /*@constant int S_IWUSR@*/
184 /*@constant int S_IXGRP@*/
185 /*@constant int S_IXOTH@*/
186 /*@constant int S_IXUSR@*/
196 extern int creat (const char *path, mode_t mode)
197 /*@modifies errno@*/;
199 extern int fcntl (int fd, int cmd, ...)
200 /*@modifies errno@*/;
202 extern int open (const char *path, int oflag, ...)
203 /*:checkerror -1 - returns -1 on error */
204 /*@modifies errno@*/;
216 extern /*@null@*/ struct group *
218 /*@modifies errno@*/;
220 extern /*@null@*/ struct group *
221 getgrnam (const char *nm)
222 /*@modifies errno@*/;
228 /* These are always defined: */
230 /*@constant int CHAR_BIT@*/
231 /*@constant char CHAR_MIN@*/
232 /*@constant char CHAR_MAX@*/
233 /*@constant int INT_MIN@*/
234 /*@constant int INT_MAX@*/
235 /*@constant long LONG_MIN@*/
236 /*@constant long LONG_MAX@*/
237 /*@constant int MB_LEN_MAX@*/
238 /*@constant signed char SCHAR_MIN@*/
239 /*@constant signed char SCHAR_MAX@*/
240 /*@constant short SHRT_MIN@*/
241 /*@constant short SHRT_MAX@*/
242 /*@constant unsigned char UCHAR_MAX@*/
243 /*@constant unsigned int UINT_MAX@*/
244 /*@constant unsigned long ULONG_MAX@*/
245 /*@constant unsigned short USHRT_MAX@*/
247 /* When _POSIX_SOURCE is defined */
249 /*@constant long ARG_MAX@*/
250 /*@constant long CHILD_MAX@*/
251 /*@constant long LINK_MAX@*/
252 /*@constant long MAX_CANON@*/
253 /*@constant size_t MAX_INPUT@*/ /* evans 2001-10-15 changed type to size_t from long */
254 /*@constant size_t NAME_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */
255 /*@constant long NGROUPS_MAX@*/
256 /*@constant long OPEN_MAX@*/
257 /*@constant size_t PATH_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */
258 /*@constant size_t PIPE_BUF@*/ /* evans 2001-10-15 changed type to size_t from long */
259 /*@constant long SSIZE_MAX@*/
260 /*@constant long STREAM_MAX@*/
261 /*@constant long TZNAME_MAX@*/
262 /*@constant long _POSIX_ARG_MAX@*/
263 /*@constant long _POSIX_CHILD_MAX@*/
264 /*@constant long _POSIX_LINK_MAX@*/
265 /*@constant long _POSIX_MAX_CANON@*/
266 /*@constant long _POSIX_MAX_INPUT@*/
267 /*@constant long _POSIX_NAME_MAX@*/
268 /*@constant long _POSIX_NGROUPS_MAX@*/
269 /*@constant long _POSIX_OPEN_MAX@*/
270 /*@constant long _POSIX_PATH_MAX@*/
271 /*@constant long _POSIX_PIPE_BUF@*/
272 /*@constant long _POSIX_SSIZE@*/
273 /*@constant long _POSIX_STREAM@*/
274 /*@constant long _POSIX_TZNAME_MAX@*/
288 extern /*@observer@*/ /*@null@*/ struct passwd *
289 getpwnam (const char *)
290 /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
292 extern /*@observer@*/ /*@null@*/ struct passwd *
294 /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
300 typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf;
302 extern /*@mayexit@*/ void
303 siglongjmp (sigjmp_buf env, int val)
307 sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask)
314 typedef /*@abstract@*/ sigset_t;
316 /*@constant int SA_NOCLDSTOP@*/
317 /*@constant int SIG_BLOCK@*/
318 /*@constant int SIG_SETMASK@*/
319 /*@constant int SIG_UNBLOCK@*/
320 /*@constant int SIGALRM@*/
321 /*@constant int SIGCHLD@*/
322 /*@constant int SIGCONT@*/
323 /*@constant int SIGHUP@*/
324 /*@constant int SIGKILL@*/
325 /*@constant int SIGPIPE@*/
326 /*@constant int SIGQUIT@*/
327 /*@constant int SIGSTOP@*/
328 /*@constant int SIGTSTP@*/
329 /*@constant int SIGTTIN@*/
330 /*@constant int SIGTTOU@*/
331 /*@constant int SIGUSR1@*/
332 /*@constant int SIGUSR2@*/
335 void (*sa_handler)();
340 extern /*@mayexit@*/ int
341 kill (pid_t pid, int sig)
342 /*@modifies errno@*/;
345 sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact)
346 /*@modifies *oact, errno, systemState@*/;
349 sigaddset (sigset_t *set, int signo)
350 /*@modifies *set, errno@*/;
353 sigdelset (sigset_t *set, int signo)
354 /*@modifies *set, errno@*/;
357 sigemptyset (/*@out@*/ sigset_t *set)
358 /*@modifies *set, errno@*/;
361 sigfillset (/*@out@*/ sigset_t *set)
362 /*@modifies *set, errno@*/;
365 sigismember (const sigset_t *set, int signo)
366 /*@modifies errno@*/;
369 sigpending (/*@out@*/ sigset_t *set)
370 /*@modifies *set, errno@*/;
373 sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset)
374 /*@modifies *oset, errno, systemState@*/;
377 sigsuspend (const sigset_t *sigmask)
378 /*@modifies errno, systemState@*/;
384 /*@constant int L_ctermid@*/
385 /*@constant int L_cuserid@*/
386 /*@constant int STREAM_MAX@*/
388 extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
389 /*@modifies errno, fileSystem@*/;
391 extern int fileno (FILE *fp) /*@modifies errno@*/;
397 /*@constant int S_IRGRP@*/
398 /*@constant int S_IROTH@*/
399 /*@constant int S_IUSR@*/
400 /*@constant int S_IWXG@*/
401 /*@constant int S_IWXO@*/
402 /*@constant int S_IWXU@*/
403 /*@constant int S_ISGID@*/
404 /*@constant int S_ISUID@*/
405 /*@constant int S_IWGRP@*/
406 /*@constant int S_IWOTH@*/
407 /*@constant int S_IWUSR@*/
408 /*@constant int S_IXGRP@*/
409 /*@constant int S_IXOTH@*/
410 /*@constant int S_IXUSR@*/
420 time_t st_atime; /* evans 2001-08-23 - these were previously st_st_atime - POSIX spec says st_atime */
421 time_t st_mtime; /* evans 2001-08-23 - these were previously st_st_mtime - POSIX spec says st_mtime */
422 time_t st_ctime; /* evans 2001-08-23 - these were previously st_st_ctime - POSIX spec says st_ctime */
426 ** POSIX does not require that the S_I* be functions. They're
427 ** macros virtually everywhere.
432 # define SBOOLINT lltX_bool /*@alt int@*/
435 # define SBOOLINT lltX_bool
438 extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ;
440 extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ;
442 extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ;
444 extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ;
446 extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ;
448 int chmod (const char *path, mode_t mode)
449 /*@modifies fileSystem, errno@*/ ;
451 int fstat (int fd, /*@out@*/ struct stat *buf)
452 /*@modifies errno, *buf@*/ ;
454 int mkdir (const char *path, mode_t mode)
455 /*@modifies fileSystem, errno@*/;
457 int mkfifo (const char *path, mode_t mode)
458 /*@modifies fileSystem, errno@*/;
460 int stat (const char *path, /*@out@*/ struct stat *buf)
462 /*@modifies errno, *buf@*/;
464 int umask (mode_t cmask)
465 /*@modifies systemState@*/;
479 times (/*@out@*/ struct tms *tp)
495 uname (/*@out@*/ struct utsname *name)
496 /*@modifies *name, errno@*/ ;
502 extern int WEXITSTATUS (int status) /*@*/ ;
503 extern int WIFEXITED (int status) /*@*/ ;
504 extern int WIFSIGNALED (int status) /*@*/ ;
505 extern int WIFSTOPPED (int status) /*@*/ ;
506 extern int WSTOPSIG (int status) /*@*/ ;
507 extern int WTERMSIG (int status) /*@*/ ;
509 /*@constant int WUNTRACED@*/
511 pid_t wait (/*@out@*/ /*@null@*/ int *st)
512 /*@modifies *st, errno, systemState@*/;
514 pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
515 /*@modifies *st, errno, systemState@*/;
521 typedef unsigned char /*@alt unsigned short@*/ cc_t;
522 typedef unsigned long /*@alt long@*/ speed_t;
523 typedef unsigned long /*@alt long@*/ tcflag_t;
525 /*@constant int B0@*/
526 /*@constant int B50@*/
527 /*@constant int B75@*/
528 /*@constant int B110@*/
529 /*@constant int B134@*/
530 /*@constant int B150@*/
531 /*@constant int B200@*/
532 /*@constant int B300@*/
533 /*@constant int B600@*/
534 /*@constant int B1200@*/
535 /*@constant int B1800@*/
536 /*@constant int B2400@*/
537 /*@constant int B4800@*/
538 /*@constant int B9600@*/
539 /*@constant int B19200@*/
540 /*@constant int B38400@*/
541 /*@constant int BRKINT@*/
542 /*@constant int CLOCAL@*/
543 /*@constant int CREAD@*/
544 /*@constant int CS5@*/
545 /*@constant int CS6@*/
546 /*@constant int CS7@*/
547 /*@constant int CS8@*/
548 /*@constant int CSIZE@*/
549 /*@constant int CSTOPB@*/
550 /*@constant int ECHO@*/
551 /*@constant int ECHOE@*/
552 /*@constant int ECHOK@*/
553 /*@constant int ECHONL@*/
554 /*@constant int HUPCL@*/
555 /*@constant int ICANON@*/
556 /*@constant int ICRNL@*/
557 /*@constant int IEXTEN@*/
558 /*@constant int IGNBRK@*/
559 /*@constant int IGNCR@*/
560 /*@constant int IGNPAR@*/
561 /*@constant int IGNLCR@*/
562 /*@constant int INPCK@*/
563 /*@constant int ISIG@*/
564 /*@constant int ISTRIP@*/
565 /*@constant int IXOFF@*/
566 /*@constant int IXON@*/
567 /*@constant int NCCS@*/
568 /*@constant int NOFLSH@*/
569 /*@constant int OPOST@*/
570 /*@constant int PARENB@*/
571 /*@constant int PARMRK@*/
572 /*@constant int PARODD@*/
573 /*@constant int TCIFLUSH@*/
574 /*@constant int TCIOFF@*/
575 /*@constant int TCIOFLUSH@*/
576 /*@constant int TCION@*/
577 /*@constant int TCOFLUSH@*/
578 /*@constant int TCSADRAIN@*/
579 /*@constant int TCSAFLUSH@*/
580 /*@constant int TCSANOW@*/
581 /*@constant int TOSTOP@*/
582 /*@constant int VEOF@*/
583 /*@constant int VEOL@*/
584 /*@constant int VERASE@*/
585 /*@constant int VINTR@*/
586 /*@constant int VKILL@*/
587 /*@constant int VMIN@*/
588 /*@constant int VQUIT@*/
589 /*@constant int VSTART@*/
590 /*@constant int VSTOP@*/
591 /*@constant int VSUSP@*/
592 /*@constant int VTIME@*/
603 cfgetispeed (const struct termios *p)
607 cfgetospeed (const struct termios *p)
611 cfsetispeed (struct termios *p)
615 cfsetospeed (struct termios *p)
620 /*@modifies errno@*/;
623 tcflow (int fd, int action)
624 /*@modifies errno@*/;
627 tcflush (int fd, int qs)
628 /*@modifies errno@*/;
631 tcgetattr (int fd, /*@out@*/ struct termios *p)
632 /*@modifies errno, *p@*/;
635 tcsendbreak (int fd, int d)
636 /*@modifies errno@*/;
639 tcsetattr (int fd, int opt, const struct termios *p)
640 /*@modifies errno@*/;
646 /* Environ must be known before it can be used in `globals' clauses. */
648 /*@unchecked@*/ extern char **environ;
650 /*@constant int CLK_TCK@*/
654 /*@globals environ@*/ /*@modifies systemState@*/;
660 /*@constant int F_OK@*/
661 /*@constant int R_OK@*/
662 /*@constant int SEEK_CUR@*/
663 /*@constant int SEEK_END@*/
664 /*@constant int SEEK_SET@*/
665 /*@constant int STDERR_FILENO@*/
666 /*@constant int STDIN_FILENO@*/
667 /*@constant int STDOUT_FILENO@*/
668 /*@constant int W_OK@*/
669 /*@constant int X_OK@*/
670 /*@constant int _PC_CHOWN_RESTRUCTED@*/
671 /*@constant int _PC_MAX_CANON@*/
672 /*@constant int _PC_MAX_INPUT@*/
673 /*@constant int _PC_NAME_MAX@*/
674 /*@constant int _PC_NO_TRUNC@*/
675 /*@constant int _PC_PATH_MAX@*/
676 /*@constant int _PC_PIPE_BUF@*/
677 /*@constant int _PC_VDISABLE@*/
678 /*@constant int _POSIX_CHOWN_RESTRICTED@*/
679 /*@constant int _POSIX_JOB_CONTROL@*/
680 /*@constant int _POSIX_NO_TRUNC@*/
681 /*@constant int _POSIX_SAVED_IDS@*/
682 /*@constant int _POSIX_VDISABLE@*/
683 /*@constant int _POSIX_VERSION@*/
684 /*@constant int _SC_ARG_MAX@*/
685 /*@constant int _SC_CHILD_MAX@*/
686 /*@constant int _SC_CLK_TCK@*/
687 /*@constant int _SC_JOB_CONTROL@*/
688 /*@constant int _SC_NGROUPS_MAX@*/
689 /*@constant int _SC_OPEN_MAX@*/
690 /*@constant int _SC_SAVED_IDS@*/
691 /*@constant int _SC_STREAM_MAX@*/
692 /*@constant int _SC_TZNAME_MAX@*/
693 /*@constant int _SC_VERSION@*/
695 extern /*@exits@*/ void _exit (int status) /*@*/;
697 extern int access (const char *path, int mode) /*@modifies errno@*/;
699 extern unsigned int alarm (unsigned int) /*@modifies systemState@*/;
701 extern int chdir (const char *path) /*@modifies errno@*/;
703 extern int chown (const char *path, uid_t owner, gid_t group)
704 /*@modifies fileSystem, errno@*/;
708 /*@modifies fileSystem, errno, systemState@*/;
709 /* state: record locks are unlocked */
712 ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
713 /*@modifies *s, systemState@*/;
715 /* cuserid is in the 1988 version of POSIX but removed in 1990 */
717 cuserid (/*@null@*/ /*@out@*/ char *s)
721 dup2 (int fd, int fd2)
722 /*@modifies errno, fileSystem@*/;
726 /*@modifies errno, fileSystem@*/;
728 extern /*@mayexit@*/ int
729 execl (const char *path, const char *arg, ...)
730 /*@modifies errno@*/;
732 extern /*@mayexit@*/ int
733 execle (const char *file, const char *arg, ...)
734 /*@modifies errno@*/;
736 extern /*@mayexit@*/ int
737 execlp (const char *file, const char *arg, ...)
738 /*@modifies errno@*/;
740 extern /*@mayexit@*/ int
741 execv (const char *path, char *const argv[])
742 /*@modifies errno@*/;
744 extern /*@mayexit@*/ int
745 execve (const char *path, char *const argv[], char *const *envp)
746 /*@modifies errno@*/;
748 extern /*@mayexit@*/ int
749 execvp (const char *file, char *const argv[])
750 /*@modifies errno@*/;
754 /*@modifies fileSystem, errno@*/;
757 fpathconf (int fd, int name)
758 /*@modifies errno@*/;
760 extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size)
761 /*@requires maxSet(buf) >= (size - 1)@*/
762 /*@ensures maxRead(buf) <= (size - 1)@*/
764 /*@modifies errno, *buf@*/ ;
779 getgroups (int gs, /*@out@*/ gid_t gl[])
780 /*@modifies errno, gl[]@*/;
782 extern /*@observer@*/ char *
807 link (const char *o, const char *n)
808 /*@modifies errno, fileSystem@*/;
811 lseek (int fd, off_t offset, int whence)
812 /*@modifies errno@*/;
815 pathconf (const char *path, int name)
816 /*@modifies errno@*/;
820 /*@modifies errno@*/;
823 pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */
824 /*@modifies errno@*/;
826 extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte)
827 /*@modifies errno, *buf@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/
828 /*@ensures maxRead(buf) >= nbyte @*/ ;
830 extern int rmdir (const char *path)
831 /*@modifies fileSystem, errno@*/;
833 extern int setgid (gid_t gid)
834 /*@modifies errno, systemState@*/;
836 extern int setpgid (pid_t pid, pid_t pgid)
837 /*@modifies errno, systemState@*/;
839 extern pid_t setsid (void) /*@modifies systemState@*/;
841 extern int setuid (uid_t uid)
842 /*@modifies errno, systemState@*/;
844 unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ;
846 extern long sysconf (int name)
847 /*@modifies errno@*/;
849 extern pid_t tcgetpgrp (int fd)
850 /*@modifies errno@*/;
852 extern int tcsetpgrp (int fd, pid_t pgrpid)
853 /*@modifies errno, systemState@*/;
855 /* Q: observer ok? */
856 extern /*@null@*/ /*@observer@*/ char *ttyname (int fd)
857 /*@modifies errno@*/;
859 extern int unlink (const char *path)
860 /*@modifies fileSystem, errno@*/;
862 extern ssize_t write (int fd, const void *buf, size_t nbyte)
863 /*@modifies errno@*/;
875 utime (const char *path, /*@null@*/ const struct utimbuf *times)
876 /*@modifies fileSystem, errno@*/;
882 typedef /*@abstract@*/ /*@mutable@*/ void *regex_t;
883 typedef /*@integraltype@*/ regoff_t;
891 int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags)
893 /*@modifies preg@*/ ;
895 int regexec (const regex_t *preg, /*@nullterminated@*/ const char *string, size_t nmatch, /*@out@*/ regmatch_t pmatch[], int eflags)
896 /*@requires maxSet(pmatch) >= nmatch@*/
897 /*@modifies pmatch@*/ ;
899 size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size)
900 /*@requires maxSet(errbuf) >= errbuf_size@*/
901 /*@modifies errbuf@*/ ;
903 void regfree (/*@only@*/ regex_t *preg) ;
906 /*@constant int REG_BASIC@*/
907 /*@constant int REG_EXTENDED@*/
908 /*@constant int REG_ICASE@*/
909 /*@constant int REG_NOSUB@*/
910 /*@constant int REG_NEWLINE@*/
911 /*@constant int REG_NOSPEC@*/
912 /*@constant int REG_PEND@*/
913 /*@constant int REG_DUMP@*/
916 /*@constant int REG_NOMATCH@*/
917 /*@constant int REG_BADPAT@*/
918 /*@constant int REG_ECOLLATE@*/
919 /*@constant int REG_ECTYPE@*/
920 /*@constant int REG_EESCAPE@*/
921 /*@constant int REG_ESUBREG@*/
922 /*@constant int REG_EBRACK@*/
923 /*@constant int REG_EPAREN@*/
924 /*@constant int REG_EBRACE@*/
925 /*@constant int REG_BADBR@*/
926 /*@constant int REG_ERANGE@*/
927 /*@constant int REG_ESPACE@*/
928 /*@constant int REG_BADRPT@*/
929 /*@constant int REG_EMPTY@*/
930 /*@constant int REG_ASSERT@*/
931 /*@constant int REG_INVARG@*/
932 /*@constant int REG_ATOI@*/ /* non standard */
933 /*@constant int REG_ITOA@*/ /* non standard */
936 /*@constant int REG_NOTBOL@*/
937 /*@constant int REG_NOTEOL@*/
938 /*@constant int REG_STARTEND@*/
939 /*@constant int REG_TRACE@*/
940 /*@constant int REG_LARGE@*/
941 /*@constant int REG_BACKR@*/