]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** posix.h | |
3 | ** | |
4 | ** This file should be processed with one of the standard libraries | |
5 | ** (standard.h or strict.h) to produce posix.lcd or posixstrict.lcd. | |
6 | */ | |
7 | ||
8 | /*@-nextlinemacros@*/ | |
9 | /*@+allimponly@*/ | |
10 | /*@+globsimpmodifiesnothing@*/ | |
11 | ||
12 | /* | |
13 | * LCLint ISO C + POSIX Library | |
14 | * | |
15 | * $Id$ | |
16 | */ | |
17 | ||
18 | /* | |
19 | * In 1988, IEEE Std 1003.1-1988, commonly known as "POSIX" or the | |
20 | * "IEEE Portable Operating System Interface for Computing Environments" | |
21 | * was published as an American National Standard. In 1990, IEEE Std | |
22 | * 1003.1-1990 was published as an International Standard. The two | |
23 | * standards differ slightly, and where they do, the 1990 International | |
24 | * standard was used for this lclint library. The differences are: | |
25 | * | |
26 | * 1988: cuserid() | |
27 | * 1990: -removed- (but still in this lclint library) | |
28 | * | |
29 | * 1988: int read (int, void*, unsigned int) | |
30 | * 1990: ssize_t read (int, void*, size_t) | |
31 | * | |
32 | * 1988: int write (int, const void*, unsigned int) | |
33 | * 1990: ssize_t write (int, const void*, size_t) | |
34 | * | |
35 | * The other differences are in the semantics of functions. | |
36 | */ | |
37 | ||
38 | /* | |
39 | * The reference for the ISO C part of this library was | |
40 | * Plauger, Brodie's "Standard C - A Reference", Prentice Hall. | |
41 | * The reference for the POSIX part of this library was | |
42 | * Donald Lewine's "POSIX Programmer's Guide", O'Reilly. | |
43 | * Transcription by Jens Schweikhardt <schweikhardt@rus.uni-stuttgart.de> | |
44 | */ | |
45 | ||
46 | /* | |
47 | * Note that Amendment 1 to ISO C was published in 1995 after POSIX was out. | |
48 | * Amendment 1 basically adds support for wide characters and iso 646 | |
49 | * source character sets. In particular, there are three new headers: | |
50 | * <iso646.h>, <wchar.h>, and <wctype.h> | |
51 | */ | |
52 | ||
53 | /* | |
54 | * Each header has annotations in this order: | |
55 | * | |
56 | * 1) type definitions (if any) | |
57 | * 2) constant definitions (if any) | |
58 | * 3) structure definitions (if any) | |
59 | * 4) function prototypes and externals (if any) | |
60 | * | |
61 | * 5) type definitions augmented by POSIX (if any) | |
62 | * 6) constant definitions augmented by POSIX (if any) | |
63 | * 7) structure definitions augmented by POSIX (if any) | |
64 | * 8) function prototypes and externals augmented by POSIX (if any) | |
65 | * | |
66 | * Builtins are mentioned in the header where they appear according to ISO. | |
67 | */ | |
68 | ||
69 | /* | |
70 | ** sys/types.h | |
71 | */ | |
72 | ||
73 | typedef /*@integraltype@*/ dev_t; | |
74 | typedef /*@integraltype@*/ gid_t; | |
75 | typedef /*@integraltype@*/ ino_t; | |
76 | typedef /*@integraltype@*/ mode_t; | |
77 | typedef /*@integraltype@*/ nlink_t; | |
78 | typedef /*@integraltype@*/ off_t; | |
79 | typedef /*@integraltype@*/ pid_t; | |
80 | typedef /*@integraltype@*/ uid_t; | |
81 | ||
82 | /* | |
83 | ** dirent.h | |
84 | */ | |
85 | ||
86 | typedef /*@abstract@*/ /*@mutable@*/ void *DIR; | |
87 | ||
88 | struct dirent { | |
89 | char d_name[]; | |
90 | }; | |
91 | ||
92 | extern int | |
93 | closedir (DIR *dirp) | |
94 | /*@modifies errno@*/; | |
95 | ||
96 | extern /*@null@*/ DIR * | |
97 | opendir (const char *dirname) | |
98 | /*@modifies errno@*/; | |
99 | ||
100 | extern /*@null@*/ struct dirent * | |
101 | readdir (DIR *dirp) | |
102 | /*@modifies errno@*/; | |
103 | ||
104 | extern void | |
105 | rewinddir (DIR *dirp) | |
106 | /*@*/; | |
107 | ||
108 | /* | |
109 | ** errno.h | |
110 | */ | |
111 | ||
112 | /*@constant int E2BIG@*/ | |
113 | /*@constant int EACCES@*/ | |
114 | /*@constant int EAGAIN@*/ | |
115 | /*@constant int EBADF@*/ | |
116 | /*@constant int EBUSY@*/ | |
117 | /*@constant int ECHILD@*/ | |
118 | /*@constant int EDEADLK@*/ | |
119 | /*@constant int EEXIST@*/ | |
120 | /*@constant int EFAULT@*/ | |
121 | /*@constant int EFBIG@*/ | |
122 | /*@constant int EINTR@*/ | |
123 | /*@constant int EINVAL@*/ | |
124 | /*@constant int EIO@*/ | |
125 | /*@constant int EISDIR@*/ | |
126 | /*@constant int EMFILE@*/ | |
127 | /*@constant int EMLINK@*/ | |
128 | /*@constant int ENAMETOOLONG@*/ | |
129 | /*@constant int ENFILE@*/ | |
130 | /*@constant int ENODEV@*/ | |
131 | /*@constant int ENOENT@*/ | |
132 | /*@constant int ENOEXEC@*/ | |
133 | /*@constant int ENOLCK@*/ | |
134 | /*@constant int ENOMEM@*/ | |
135 | /*@constant int ENOSPC@*/ | |
136 | /*@constant int ENOSYS@*/ | |
137 | /*@constant int ENOTDIR@*/ | |
138 | /*@constant int ENOTEMPTY@*/ | |
139 | /*@constant int ENOTTY@*/ | |
140 | /*@constant int ENXIO@*/ | |
141 | /*@constant int EPERM@*/ | |
142 | /*@constant int EPIPE@*/ | |
143 | /*@constant int EROFS@*/ | |
144 | /*@constant int ESPIPE@*/ | |
145 | /*@constant int ESRCH@*/ | |
146 | /*@constant int EXDEV@*/ | |
147 | ||
148 | /* | |
149 | ** fcntl.h | |
150 | */ | |
151 | ||
152 | /*@constant int FD_CLOEXEC@*/ | |
153 | /*@constant int F_DUPFD@*/ | |
154 | /*@constant int F_GETFD@*/ | |
155 | /*@constant int F_GETFL@*/ | |
156 | /*@constant int F_GETLK@*/ | |
157 | /*@constant int F_RDLCK@*/ | |
158 | /*@constant int F_SETFD@*/ | |
159 | /*@constant int F_SETFL@*/ | |
160 | /*@constant int F_SETLK@*/ | |
161 | /*@constant int F_SETLKW@*/ | |
162 | /*@constant int F_UNLCK@*/ | |
163 | /*@constant int F_WRLCK@*/ | |
164 | /*@constant int O_ACCMODE@*/ | |
165 | /*@constant int O_APPEND@*/ | |
166 | /*@constant int O_CREAT@*/ | |
167 | /*@constant int O_EXCL@*/ | |
168 | /*@constant int O_NOCTTY@*/ | |
169 | /*@constant int O_NONBLOCK@*/ | |
170 | /*@constant int O_RDONLY@*/ | |
171 | /*@constant int O_RDWR@*/ | |
172 | /*@constant int O_TRUNC@*/ | |
173 | /*@constant int O_WRONLY@*/ | |
174 | /*@constant int SEEK_CUR@*/ | |
175 | /*@constant int SEEK_END@*/ | |
176 | /*@constant int SEEK_SET@*/ | |
177 | /*@constant int S_IRGRP@*/ | |
178 | /*@constant int S_IROTH@*/ | |
179 | /*@constant int S_IUSR@*/ | |
180 | /*@constant int S_IWXG@*/ | |
181 | /*@constant int S_IWXO@*/ | |
182 | /*@constant int S_IWXU@*/ | |
183 | /*@constant int S_ISGID@*/ | |
184 | /*@constant int S_ISUID@*/ | |
185 | /*@constant int S_IWGRP@*/ | |
186 | /*@constant int S_IWOTH@*/ | |
187 | /*@constant int S_IWUSR@*/ | |
188 | /*@constant int S_IXGRP@*/ | |
189 | /*@constant int S_IXOTH@*/ | |
190 | /*@constant int S_IXUSR@*/ | |
191 | ||
192 | struct flock { | |
193 | short l_type; | |
194 | short l_whence; | |
195 | off_t l_start; | |
196 | off_t l_len; | |
197 | pid_t l_pid; | |
198 | }; | |
199 | ||
200 | extern int | |
201 | creat (const char *path, mode_t mode) | |
202 | /*@modifies errno@*/; | |
203 | ||
204 | extern int | |
205 | fcntl (int fd, int cmd, ...) | |
206 | /*@modifies errno@*/; | |
207 | ||
208 | extern int | |
209 | open (const char *path, int oflag, ...) | |
210 | /*@modifies errno@*/; | |
211 | ||
212 | /* | |
213 | ** grp.h | |
214 | */ | |
215 | ||
216 | struct group { | |
217 | char *gr_name; | |
218 | gid_t gr_gid; | |
219 | char **gr_mem; | |
220 | }; | |
221 | ||
222 | extern /*@null@*/ struct group * | |
223 | getgrgid (gid_t gid) | |
224 | /*@modifies errno@*/; | |
225 | ||
226 | extern /*@null@*/ struct group * | |
227 | getgrnam (const char *nm) | |
228 | /*@modifies errno@*/; | |
229 | ||
230 | /* | |
231 | ** limits.h | |
232 | */ | |
233 | ||
234 | /*@constant long ARG_MAX@*/ | |
235 | /*@constant long CHILD_MAX@*/ | |
236 | /*@constant long LINK_MAX@*/ | |
237 | /*@constant long MAX_CANON@*/ | |
238 | /*@constant long MAX_INPUT@*/ | |
239 | /*@constant long NAME_MAX@*/ | |
240 | /*@constant long NGROUPS_MAX@*/ | |
241 | /*@constant long OPEN_MAX@*/ | |
242 | /*@constant long PIPE_BUF@*/ | |
243 | /*@constant long SSIZE_MAX@*/ | |
244 | /*@constant long STREAM_MAX@*/ | |
245 | /*@constant long TZNAME_MAX@*/ | |
246 | /*@constant long _POSIX_ARG_MAX@*/ | |
247 | /*@constant long _POSIX_CHILD_MAX@*/ | |
248 | /*@constant long _POSIX_LINK_MAX@*/ | |
249 | /*@constant long _POSIX_MAX_CANON@*/ | |
250 | /*@constant long _POSIX_MAX_INPUT@*/ | |
251 | /*@constant long _POSIX_NAME_MAX@*/ | |
252 | /*@constant long _POSIX_NGROUPS_MAX@*/ | |
253 | /*@constant long _POSIX_OPEN_MAX@*/ | |
254 | /*@constant long _POSIX_PATH_MAX@*/ | |
255 | /*@constant long _POSIX_PIPE_BUF@*/ | |
256 | /*@constant long _POSIX_SSIZE@*/ | |
257 | /*@constant long _POSIX_STREAM@*/ | |
258 | /*@constant long _POSIX_TZNAME_MAX@*/ | |
259 | ||
260 | /* | |
261 | ** pwd.h | |
262 | */ | |
263 | ||
264 | struct passwd { | |
265 | char *pw_name; | |
266 | uid_t pw_uid; | |
267 | gid_t pw_gid; | |
268 | char *pw_dir; | |
269 | char *pw_shell; | |
270 | } ; | |
271 | ||
272 | extern /*@observer@*/ /*@null@*/ struct passwd * | |
273 | getpwnam (const char *) | |
274 | /*@modifies errno@*/; | |
275 | ||
276 | extern /*@observer@*/ /*@null@*/ struct passwd * | |
277 | getpwuid (uid_t uid) | |
278 | /*@modifies errno@*/; | |
279 | ||
280 | /* | |
281 | ** setjmp.h | |
282 | */ | |
283 | ||
284 | typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf; | |
285 | ||
286 | extern /*@mayexit@*/ void | |
287 | siglongjmp (sigjmp_buf env, int val) | |
288 | /*@*/; | |
289 | ||
290 | extern int | |
291 | sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) | |
292 | /*@modifies env@*/; | |
293 | ||
294 | /* | |
295 | ** signal.h | |
296 | */ | |
297 | ||
298 | typedef /*@abstract@*/ sigset_t; | |
299 | ||
300 | /*@constant int SA_NOCLDSTOP@*/ | |
301 | /*@constant int SIG_BLOCK@*/ | |
302 | /*@constant int SIG_SETMASK@*/ | |
303 | /*@constant int SIG_UNBLOCK@*/ | |
304 | /*@constant int SIGALRM@*/ | |
305 | /*@constant int SIGCHLD@*/ | |
306 | /*@constant int SIGCONT@*/ | |
307 | /*@constant int SIGHUP@*/ | |
308 | /*@constant int SIGKILL@*/ | |
309 | /*@constant int SIGPIPE@*/ | |
310 | /*@constant int SIGQUIT@*/ | |
311 | /*@constant int SIGSTOP@*/ | |
312 | /*@constant int SIGTSTP@*/ | |
313 | /*@constant int SIGTTIN@*/ | |
314 | /*@constant int SIGTTOU@*/ | |
315 | /*@constant int SIGUSR1@*/ | |
316 | /*@constant int SIGUSR2@*/ | |
317 | ||
318 | struct sigaction { | |
319 | void (*sa_handler)(); | |
320 | sigset_t sa_mask; | |
321 | int sa_flags; | |
322 | } ; | |
323 | ||
324 | extern /*@mayexit@*/ int | |
325 | kill (pid_t pid, int sig) | |
326 | /*@modifies errno@*/; | |
327 | ||
328 | extern int | |
329 | sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact) | |
330 | /*@modifies *oact, errno, internalState@*/; | |
331 | ||
332 | extern int | |
333 | sigaddset (sigset_t *set, int signo) | |
334 | /*@modifies *set, errno@*/; | |
335 | ||
336 | extern int | |
337 | sigdelset (sigset_t *set, int signo) | |
338 | /*@modifies *set, errno@*/; | |
339 | ||
340 | extern int | |
341 | sigemptyset (/*@out@*/ sigset_t *set) | |
342 | /*@modifies *set, errno@*/; | |
343 | ||
344 | extern int | |
345 | sigfillset (/*@out@*/ sigset_t *set) | |
346 | /*@modifies *set, errno@*/; | |
347 | ||
348 | extern int | |
349 | sigismember (const sigset_t *set, int signo) | |
350 | /*@modifies errno@*/; | |
351 | ||
352 | extern int | |
353 | sigpending (/*@out@*/ sigset_t *set) | |
354 | /*@modifies *set, errno@*/; | |
355 | ||
356 | extern int | |
357 | sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset) | |
358 | /*@modifies *oset, errno, internalState@*/; | |
359 | ||
360 | extern int | |
361 | sigsuspend (const sigset_t *sigmask) | |
362 | /*@modifies errno, internalState@*/; | |
363 | ||
364 | /* | |
365 | ** stdio.h | |
366 | */ | |
367 | ||
368 | /*@constant int L_ctermid@*/ | |
369 | /*@constant int L_cuserid@*/ | |
370 | /*@constant int STREAM_MAX@*/ | |
371 | ||
372 | extern /*@null@*/ /*@dependent@*/ FILE * | |
373 | fdopen (int fd, const char *type) | |
374 | /*@modifies errno, fileSystem@*/; | |
375 | ||
376 | extern int | |
377 | fileno (FILE *fp) | |
378 | /*@modifies errno@*/; | |
379 | ||
380 | /* | |
381 | ** sys/stat.h | |
382 | */ | |
383 | ||
384 | /*@constant int S_IRGRP@*/ | |
385 | /*@constant int S_IROTH@*/ | |
386 | /*@constant int S_IUSR@*/ | |
387 | /*@constant int S_IWXG@*/ | |
388 | /*@constant int S_IWXO@*/ | |
389 | /*@constant int S_IWXU@*/ | |
390 | /*@constant int S_ISGID@*/ | |
391 | /*@constant int S_ISUID@*/ | |
392 | /*@constant int S_IWGRP@*/ | |
393 | /*@constant int S_IWOTH@*/ | |
394 | /*@constant int S_IWUSR@*/ | |
395 | /*@constant int S_IXGRP@*/ | |
396 | /*@constant int S_IXOTH@*/ | |
397 | /*@constant int S_IXUSR@*/ | |
398 | ||
399 | struct stat { | |
400 | mode_t st_mode; | |
401 | ino_t st_ino; | |
402 | dev_t st_dev; | |
403 | nlink_t st_nlink; | |
404 | uid_t st_uid; | |
405 | gid_t st_gid; | |
406 | off_t st_size; | |
407 | time_t st_st_atime; | |
408 | time_t st_st_mtime; | |
409 | time_t st_st_ctime; | |
410 | } ; | |
411 | ||
412 | /* | |
413 | ** POSIX does not require that the S_I* be functions. They're | |
414 | ** macros virtually everywhere. | |
415 | */ | |
416 | ||
417 | # ifdef STRICT | |
418 | /*@notfunction@*/ | |
419 | # define SBOOLINT lltX_bool /*@alt int@*/ | |
420 | # else | |
421 | /*@notfunction@*/ | |
422 | # define SBOOLINT lltX_bool | |
423 | # endif | |
424 | ||
425 | extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ; | |
426 | ||
427 | extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ; | |
428 | ||
429 | extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ; | |
430 | ||
431 | extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ; | |
432 | ||
433 | extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ; | |
434 | ||
435 | extern int chmod (const char *path, mode_t mode) | |
436 | /*@modifies fileSystem, errno@*/ ; | |
437 | ||
438 | extern int fstat (int fd, /*@out@*/ struct stat *buf) | |
439 | /*@modifies errno, *buf@*/ ; | |
440 | ||
441 | extern int | |
442 | mkdir (const char *path, mode_t mode) | |
443 | /*@modifies fileSystem, errno@*/; | |
444 | ||
445 | extern int | |
446 | mkfifo (const char *path, mode_t mode) | |
447 | /*@modifies fileSystem, errno@*/; | |
448 | ||
449 | extern int | |
450 | stat (const char *path, /*@out@*/ struct stat *buf) | |
451 | /*@modifies errno, *buf@*/; | |
452 | ||
453 | extern int | |
454 | umask (mode_t cmask) | |
455 | /*@modifies internalState@*/; | |
456 | ||
457 | /* | |
458 | ** sys/times.h | |
459 | */ | |
460 | ||
461 | struct tms { | |
462 | clock_t tms_utime; | |
463 | clock_t tms_stime; | |
464 | clock_t tms_cutime; | |
465 | clock_t tms_cstime; | |
466 | }; | |
467 | ||
468 | extern clock_t | |
469 | times (/*@out@*/ struct tms *tp) | |
470 | /*@modifies *tp@*/; | |
471 | ||
472 | /* | |
473 | ** sys/utsname.h | |
474 | */ | |
475 | ||
476 | struct utsname { | |
477 | char sysname[]; | |
478 | char nodename[]; | |
479 | char release[]; | |
480 | char version[]; | |
481 | char machine[]; | |
482 | }; | |
483 | ||
484 | extern int | |
485 | uname (/*@out@*/ struct utsname *name) | |
486 | /*@modifies *name, errno@*/ ; | |
487 | ||
488 | /* | |
489 | ** sys/wait.h | |
490 | */ | |
491 | ||
492 | extern int WEXITSTATUS (int status) /*@*/ ; | |
493 | extern int WIFEXITED (int status) /*@*/ ; | |
494 | extern int WIFSIGNALED (int status) /*@*/ ; | |
495 | extern int WIFSTOPPED (int status) /*@*/ ; | |
496 | extern int WSTOPSIG (int status) /*@*/ ; | |
497 | extern int WTERMSIG (int status) /*@*/ ; | |
498 | ||
499 | /*@constant int WUNTRACED@*/ | |
500 | ||
501 | extern pid_t | |
502 | wait (/*@out@*/ /*@null@*/ int *st) | |
503 | /*@modifies *st, errno@*/; | |
504 | ||
505 | extern pid_t | |
506 | waitpid (pid_t pid, /*@out@*/ int *st, int opt) | |
507 | /*@modifies *st, errno@*/; | |
508 | ||
509 | /* | |
510 | ** termios.h | |
511 | */ | |
512 | ||
513 | typedef unsigned char /*@alt unsigned short@*/ cc_t; | |
514 | typedef unsigned long /*@alt long@*/ speed_t; | |
515 | typedef unsigned long /*@alt long@*/ tcflag_t; | |
516 | ||
517 | /*@constant int B0@*/ | |
518 | /*@constant int B50@*/ | |
519 | /*@constant int B75@*/ | |
520 | /*@constant int B110@*/ | |
521 | /*@constant int B134@*/ | |
522 | /*@constant int B150@*/ | |
523 | /*@constant int B200@*/ | |
524 | /*@constant int B300@*/ | |
525 | /*@constant int B600@*/ | |
526 | /*@constant int B1200@*/ | |
527 | /*@constant int B1800@*/ | |
528 | /*@constant int B2400@*/ | |
529 | /*@constant int B4800@*/ | |
530 | /*@constant int B9600@*/ | |
531 | /*@constant int B19200@*/ | |
532 | /*@constant int B38400@*/ | |
533 | /*@constant int BRKINT@*/ | |
534 | /*@constant int CLOCAL@*/ | |
535 | /*@constant int CREAD@*/ | |
536 | /*@constant int CS5@*/ | |
537 | /*@constant int CS6@*/ | |
538 | /*@constant int CS7@*/ | |
539 | /*@constant int CS8@*/ | |
540 | /*@constant int CSIZE@*/ | |
541 | /*@constant int CSTOPB@*/ | |
542 | /*@constant int ECHO@*/ | |
543 | /*@constant int ECHOE@*/ | |
544 | /*@constant int ECHOK@*/ | |
545 | /*@constant int ECHONL@*/ | |
546 | /*@constant int HUPCL@*/ | |
547 | /*@constant int ICANON@*/ | |
548 | /*@constant int ICRNL@*/ | |
549 | /*@constant int IEXTEN@*/ | |
550 | /*@constant int IGNBRK@*/ | |
551 | /*@constant int IGNCR@*/ | |
552 | /*@constant int IGNPAR@*/ | |
553 | /*@constant int IGNLCR@*/ | |
554 | /*@constant int INPCK@*/ | |
555 | /*@constant int ISIG@*/ | |
556 | /*@constant int ISTRIP@*/ | |
557 | /*@constant int IXOFF@*/ | |
558 | /*@constant int IXON@*/ | |
559 | /*@constant int NCCS@*/ | |
560 | /*@constant int NOFLSH@*/ | |
561 | /*@constant int OPOST@*/ | |
562 | /*@constant int PARENB@*/ | |
563 | /*@constant int PARMRK@*/ | |
564 | /*@constant int PARODD@*/ | |
565 | /*@constant int TCIFLUSH@*/ | |
566 | /*@constant int TCIOFF@*/ | |
567 | /*@constant int TCIOFLUSH@*/ | |
568 | /*@constant int TCION@*/ | |
569 | /*@constant int TCOFLUSH@*/ | |
570 | /*@constant int TCSADRAIN@*/ | |
571 | /*@constant int TCSAFLUSH@*/ | |
572 | /*@constant int TCSANOW@*/ | |
573 | /*@constant int TOSTOP@*/ | |
574 | /*@constant int VEOF@*/ | |
575 | /*@constant int VEOL@*/ | |
576 | /*@constant int VERASE@*/ | |
577 | /*@constant int VINTR@*/ | |
578 | /*@constant int VKILL@*/ | |
579 | /*@constant int VMIN@*/ | |
580 | /*@constant int VQUIT@*/ | |
581 | /*@constant int VSTART@*/ | |
582 | /*@constant int VSTOP@*/ | |
583 | /*@constant int VSUSP@*/ | |
584 | /*@constant int VTIME@*/ | |
585 | ||
586 | struct termios { | |
587 | tcflag_t c_iflag; | |
588 | tcflag_t c_oflag; | |
589 | tcflag_t c_cflag; | |
590 | tcflag_t c_lflag; | |
591 | cc_t c_cc; | |
592 | } ; | |
593 | ||
594 | extern speed_t | |
595 | cfgetispeed (const struct termios *p) | |
596 | /*@*/; | |
597 | ||
598 | extern speed_t | |
599 | cfgetospeed (const struct termios *p) | |
600 | /*@*/; | |
601 | ||
602 | extern int | |
603 | cfsetispeed (struct termios *p) | |
604 | /*@modifies *p@*/; | |
605 | ||
606 | extern int | |
607 | cfsetospeed (struct termios *p) | |
608 | /*@modifies *p@*/; | |
609 | ||
610 | extern int | |
611 | tcdrain (int fd) | |
612 | /*@modifies errno@*/; | |
613 | ||
614 | extern int | |
615 | tcflow (int fd, int action) | |
616 | /*@modifies errno@*/; | |
617 | ||
618 | extern int | |
619 | tcflush (int fd, int qs) | |
620 | /*@modifies errno@*/; | |
621 | ||
622 | extern int | |
623 | tcgetattr (int fd, /*@out@*/ struct termios *p) | |
624 | /*@modifies errno, *p@*/; | |
625 | ||
626 | extern int | |
627 | tcsendbreak (int fd, int d) | |
628 | /*@modifies errno@*/; | |
629 | ||
630 | extern int | |
631 | tcsetattr (int fd, int opt, const struct termios *p) | |
632 | /*@modifies errno@*/; | |
633 | ||
634 | /* | |
635 | ** time.h | |
636 | */ | |
637 | ||
638 | /* Environ must be known before it can be used in `globals' clauses. */ | |
639 | ||
640 | /*@unchecked@*/ extern char **environ; | |
641 | ||
642 | /*@constant int CLK_TCK@*/ | |
643 | ||
644 | extern void | |
645 | tzset (void) | |
646 | /*@globals environ@*/ /*@modifies internalState@*/; | |
647 | ||
648 | /* | |
649 | ** unistd.h | |
650 | */ | |
651 | ||
652 | /*@constant int F_OK@*/ | |
653 | /*@constant int R_OK@*/ | |
654 | /*@constant int SEEK_CUR@*/ | |
655 | /*@constant int SEEK_END@*/ | |
656 | /*@constant int SEEK_SET@*/ | |
657 | /*@constant int STDERR_FILENO@*/ | |
658 | /*@constant int STDIN_FILENO@*/ | |
659 | /*@constant int STDOUT_FILENO@*/ | |
660 | /*@constant int W_OK@*/ | |
661 | /*@constant int X_OK@*/ | |
662 | /*@constant int _PC_CHOWN_RESTRUCTED@*/ | |
663 | /*@constant int _PC_MAX_CANON@*/ | |
664 | /*@constant int _PC_MAX_INPUT@*/ | |
665 | /*@constant int _PC_NAME_MAX@*/ | |
666 | /*@constant int _PC_NO_TRUNC@*/ | |
667 | /*@constant int _PC_PATH_MAX@*/ | |
668 | /*@constant int _PC_PIPE_BUF@*/ | |
669 | /*@constant int _PC_VDISABLE@*/ | |
670 | /*@constant int _POSIX_CHOWN_RESTRICTED@*/ | |
671 | /*@constant int _POSIX_JOB_CONTROL@*/ | |
672 | /*@constant int _POSIX_NO_TRUNC@*/ | |
673 | /*@constant int _POSIX_SAVED_IDS@*/ | |
674 | /*@constant int _POSIX_VDISABLE@*/ | |
675 | /*@constant int _POSIX_VERSION@*/ | |
676 | /*@constant int _SC_ARG_MAX@*/ | |
677 | /*@constant int _SC_CHILD_MAX@*/ | |
678 | /*@constant int _SC_CLK_TCK@*/ | |
679 | /*@constant int _SC_JOB_CONTROL@*/ | |
680 | /*@constant int _SC_NGROUPS_MAX@*/ | |
681 | /*@constant int _SC_OPEN_MAX@*/ | |
682 | /*@constant int _SC_SAVED_IDS@*/ | |
683 | /*@constant int _SC_STREAM_MAX@*/ | |
684 | /*@constant int _SC_TZNAME_MAX@*/ | |
685 | /*@constant int _SC_VERSION@*/ | |
686 | ||
687 | extern /*@exits@*/ void | |
688 | _exit (int status) | |
689 | /*@*/; | |
690 | ||
691 | extern int | |
692 | access (const char *path, int mode) | |
693 | /*@modifies errno@*/; | |
694 | ||
695 | extern unsigned int | |
696 | alarm (unsigned int) | |
697 | /*@modifies internalState@*/; | |
698 | ||
699 | extern int | |
700 | chdir (const char *path) | |
701 | /*@modifies errno@*/; | |
702 | ||
703 | extern int | |
704 | chown (const char *path, uid_t owner, gid_t group) | |
705 | /*@modifies fileSystem, errno@*/; | |
706 | ||
707 | extern int | |
708 | close (int fd) | |
709 | /*@modifies fileSystem, errno, internalState@*/; | |
710 | /* state: record locks are unlocked */ | |
711 | ||
712 | extern char * | |
713 | ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s) | |
714 | /*@modifies *s, internalState@*/; | |
715 | ||
716 | /* cuserid is in the 1988 version of POSIX but removed in 1990 */ | |
717 | extern char * | |
718 | cuserid (/*@null@*/ /*@out@*/ char *s) | |
719 | /*@modifies *s@*/; | |
720 | ||
721 | extern int | |
722 | dup2 (int fd, int fd2) | |
723 | /*@modifies errno, fileSystem@*/; | |
724 | ||
725 | extern int | |
726 | dup (int fd) | |
727 | /*@modifies errno, fileSystem@*/; | |
728 | ||
729 | extern /*@mayexit@*/ int | |
730 | execl (const char *path, const char *arg, ...) | |
731 | /*@modifies errno@*/; | |
732 | ||
733 | extern /*@mayexit@*/ int | |
734 | execle (const char *file, const char *arg, ...) | |
735 | /*@modifies errno@*/; | |
736 | ||
737 | extern /*@mayexit@*/ int | |
738 | execlp (const char *file, const char *arg, ...) | |
739 | /*@modifies errno@*/; | |
740 | ||
741 | extern /*@mayexit@*/ int | |
742 | execv (const char *path, char *const argv[]) | |
743 | /*@modifies errno@*/; | |
744 | ||
745 | extern /*@mayexit@*/ int | |
746 | execve (const char *path, char *const argv[], char *const *envp) | |
747 | /*@modifies errno@*/; | |
748 | ||
749 | extern /*@mayexit@*/ int | |
750 | execvp (const char *file, char *const argv[]) | |
751 | /*@modifies errno@*/; | |
752 | ||
753 | extern pid_t | |
754 | fork (void) | |
755 | /*@modifies fileSystem, errno@*/; | |
756 | ||
757 | extern long | |
758 | fpathconf (int fd, int name) | |
759 | /*@modifies errno@*/; | |
760 | ||
761 | extern char * | |
762 | getcwd (/*@returned@*/ /*@out@*/ char *buf, size_t size) | |
763 | /*@modifies errno, *buf@*/; | |
764 | ||
765 | extern gid_t | |
766 | getegid (void) | |
767 | /*@*/; | |
768 | ||
769 | extern uid_t | |
770 | geteuid (void) | |
771 | /*@*/; | |
772 | ||
773 | extern gid_t | |
774 | getgid (void) | |
775 | /*@*/; | |
776 | ||
777 | extern int | |
778 | getgroups (int gs, /*@out@*/ gid_t gl[]) | |
779 | /*@modifies errno, gl[]@*/; | |
780 | ||
781 | extern /*@observer@*/ char * | |
782 | getlogin (void) | |
783 | /*@*/; | |
784 | ||
785 | extern pid_t | |
786 | getpgrp (void) | |
787 | /*@*/; | |
788 | ||
789 | extern pid_t | |
790 | getpid (void) | |
791 | /*@*/; | |
792 | ||
793 | extern pid_t | |
794 | getppid (void) | |
795 | /*@*/; | |
796 | ||
797 | extern uid_t | |
798 | getuid (void) | |
799 | /*@*/; | |
800 | ||
801 | extern int | |
802 | isatty (int fd) | |
803 | /*@*/; | |
804 | ||
805 | extern int | |
806 | link (const char *o, const char *n) | |
807 | /*@modifies errno, fileSystem@*/; | |
808 | ||
809 | extern off_t | |
810 | lseek (int fd, off_t offset, int whence) | |
811 | /*@modifies errno@*/; | |
812 | ||
813 | extern long | |
814 | pathconf (const char *path, int name) | |
815 | /*@modifies errno@*/; | |
816 | ||
817 | extern int | |
818 | pause (void) | |
819 | /*@modifies errno@*/; | |
820 | ||
821 | extern int | |
822 | pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */ | |
823 | /*@modifies errno@*/; | |
824 | ||
825 | extern ssize_t | |
826 | read (int fd, /*@out@*/ void *buf, size_t nbyte) | |
827 | /*@modifies errno, *buf@*/; | |
828 | ||
829 | extern int | |
830 | rmdir (const char *path) | |
831 | /*@modifies fileSystem, errno@*/; | |
832 | ||
833 | extern int | |
834 | setgid (gid_t gid) | |
835 | /*@modifies errno, internalState@*/; | |
836 | ||
837 | extern int | |
838 | setpgid (pid_t pid, pid_t pgid) | |
839 | /*@modifies errno, internalState@*/; | |
840 | ||
841 | extern pid_t | |
842 | setsid (void) | |
843 | /*@*/; | |
844 | ||
845 | extern int | |
846 | setuid (uid_t uid) | |
847 | /*@modifies errno, internalState@*/; | |
848 | ||
849 | extern unsigned int | |
850 | sleep (unsigned int sec) | |
851 | /*@*/; | |
852 | ||
853 | extern long | |
854 | sysconf (int name) | |
855 | /*@modifies errno@*/; | |
856 | ||
857 | extern pid_t | |
858 | tcgetpgrp (int fd) | |
859 | /*@modifies errno@*/; | |
860 | ||
861 | extern int | |
862 | tcsetpgrp (int fd, pid_t pgrpid) | |
863 | /*@modifies errno, internalState@*/; | |
864 | ||
865 | /* Q: observer ok? */ | |
866 | extern /*@null@*/ /*@observer@*/ char * | |
867 | ttyname (int fd) | |
868 | /*@modifies errno@*/; | |
869 | ||
870 | extern int | |
871 | unlink (const char *path) | |
872 | /*@modifies fileSystem, errno@*/; | |
873 | ||
874 | extern ssize_t | |
875 | write (int fd, const void *buf, size_t nbyte) | |
876 | /*@modifies errno@*/; | |
877 | ||
878 | /* | |
879 | ** utime.h | |
880 | */ | |
881 | ||
882 | struct utimbuf { | |
883 | time_t actime; | |
884 | time_t modtime; | |
885 | } ; | |
886 | ||
887 | extern int | |
888 | utime (const char *path, /*@null@*/ const struct utimbuf *times) | |
889 | /*@modifies fileSystem, errno@*/; | |
890 |