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