]> andersk Git - splint.git/blame - lib/posix.h
Added missing signal.h information to posix.h
[splint.git] / lib / posix.h
CommitLineData
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
73typedef /*@integraltype@*/ dev_t;
74typedef /*@integraltype@*/ gid_t;
8fe44445 75typedef /*@unsignedintegraltype@*/ ino_t; /*: is this definitely unsigned? */
885824d3 76typedef /*@integraltype@*/ mode_t;
77typedef /*@integraltype@*/ nlink_t;
78typedef /*@integraltype@*/ off_t;
79typedef /*@integraltype@*/ pid_t;
80typedef /*@integraltype@*/ uid_t;
81
82/*
83** dirent.h
84*/
85
86typedef /*@abstract@*/ /*@mutable@*/ void *DIR;
87
88struct dirent {
89 char d_name[];
90};
91
8fe44445 92extern 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 98extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname)
86d93ed3 99 /*@modifies errno, fileSystem@*/;
885824d3 100
d5047b91 101extern /*@dependent@*/ /*@null@*/ struct dirent *readdir (DIR *dirp)
8fe44445 102 /*@modifies errno@*/;
885824d3 103
8fe44445 104extern 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
203struct 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 211extern int creat (const char *path, mode_t mode)
212 /*@modifies errno@*/;
885824d3 213
1d239d69 214extern int fcntl (int fd, int cmd, ...)
215 /*@modifies errno@*/;
885824d3 216
1d239d69 217extern 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
226struct 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
296struct 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
314typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf;
315
f9264521 316/*@mayexit@*/ void siglongjmp (sigjmp_buf env, int val) /*@*/;
885824d3 317
f9264521 318int sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) /*@modifies env@*/;
885824d3 319
320/*
5e3d3b85 321** moved up from signal.h
885824d3 322*/
323
324typedef /*@abstract@*/ sigset_t;
325
5e3d3b85 326typedef struct {
327 void *ss_sp;
328 size_t ss_size;
329 int ss_flags;
330} stack_t;
331
332/*
333** ucontext.h
334*/
335
336typedef /*@abstract@*/ mcontext_t;
337
338typedef 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
345int getcontext(ucontext_t *);
346int setcontext(const ucontext_t *);
347void makecontext(ucontext_t *, void (*)(void), int, ...);
348int 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 372struct sigstack {
373 int ss_onstack;
374 void *ss_sp;
375} ;
376
377typedef 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
389typedef union {
390 int sival_int;
391 void *sival_ptr;
392} sigval;
393
885824d3 394struct 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
402kill (pid_t pid, int sig)
403 /*@modifies errno@*/;
404
405 extern int
406sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact)
ccf0a4a8 407 /*@modifies *oact, errno, systemState@*/;
885824d3 408
409 extern int
410sigaddset (sigset_t *set, int signo)
411 /*@modifies *set, errno@*/;
412
413 extern int
414sigdelset (sigset_t *set, int signo)
415 /*@modifies *set, errno@*/;
416
417 extern int
418sigemptyset (/*@out@*/ sigset_t *set)
419 /*@modifies *set, errno@*/;
420
421 extern int
422sigfillset (/*@out@*/ sigset_t *set)
423 /*@modifies *set, errno@*/;
424
425 extern int
426sigismember (const sigset_t *set, int signo)
427 /*@modifies errno@*/;
428
429 extern int
430sigpending (/*@out@*/ sigset_t *set)
431 /*@modifies *set, errno@*/;
432
433 extern int
434sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset)
ccf0a4a8 435 /*@modifies *oset, errno, systemState@*/;
885824d3 436
437 extern int
438sigsuspend (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 449extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
450 /*@modifies errno, fileSystem@*/;
885824d3 451
15b3d2b2 452extern int fileno (FILE *fp) /*@modifies errno@*/;
885824d3 453
454/*
455** sys/stat.h
456*/
457
885824d3 458struct 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} ;
470
471/*
472** POSIX does not require that the S_I* be functions. They're
473** macros virtually everywhere.
474*/
475
476# ifdef STRICT
477/*@notfunction@*/
0bd4c301 478# define SBOOLINT _Bool /*@alt int@*/
885824d3 479# else
480/*@notfunction@*/
0bd4c301 481# define SBOOLINT _Bool
885824d3 482# endif
483
484extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ;
485
486extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ;
487
488extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ;
489
490extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ;
491
492extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ;
493
1d239d69 494int chmod (const char *path, mode_t mode)
495 /*@modifies fileSystem, errno@*/ ;
496
497int fstat (int fd, /*@out@*/ struct stat *buf)
885824d3 498 /*@modifies errno, *buf@*/ ;
499
1d239d69 500int mkdir (const char *path, mode_t mode)
501 /*@modifies fileSystem, errno@*/;
502
503int mkfifo (const char *path, mode_t mode)
504 /*@modifies fileSystem, errno@*/;
885824d3 505
1d239d69 506int stat (const char *path, /*@out@*/ struct stat *buf)
507 /*:errorcode -1*/
508 /*@modifies errno, *buf@*/;
885824d3 509
1d239d69 510int umask (mode_t cmask)
511 /*@modifies systemState@*/;
885824d3 512
513/*
514** sys/times.h
515*/
516
517struct tms {
518 clock_t tms_utime;
519 clock_t tms_stime;
520 clock_t tms_cutime;
521 clock_t tms_cstime;
522};
523
524 extern clock_t
525times (/*@out@*/ struct tms *tp)
526 /*@modifies *tp@*/;
527
528/*
529** sys/utsname.h
530*/
531
532struct utsname {
533 char sysname[];
534 char nodename[];
535 char release[];
536 char version[];
537 char machine[];
538};
539
540 extern int
541uname (/*@out@*/ struct utsname *name)
542 /*@modifies *name, errno@*/ ;
543
544/*
545** sys/wait.h
546*/
547
548extern int WEXITSTATUS (int status) /*@*/ ;
549extern int WIFEXITED (int status) /*@*/ ;
550extern int WIFSIGNALED (int status) /*@*/ ;
551extern int WIFSTOPPED (int status) /*@*/ ;
552extern int WSTOPSIG (int status) /*@*/ ;
553extern int WTERMSIG (int status) /*@*/ ;
554
555/*@constant int WUNTRACED@*/
556
d5047b91 557/* These are in Unix spec, are they in POSIX? */
558/*@constant int WCONTINUED@*/
559/*@constant int WNOHANG@*/
560
ccf0a4a8 561pid_t wait (/*@out@*/ /*@null@*/ int *st)
562 /*@modifies *st, errno, systemState@*/;
885824d3 563
ccf0a4a8 564pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
565 /*@modifies *st, errno, systemState@*/;
885824d3 566
567/*
568** termios.h
569*/
570
571typedef unsigned char /*@alt unsigned short@*/ cc_t;
572typedef unsigned long /*@alt long@*/ speed_t;
573typedef unsigned long /*@alt long@*/ tcflag_t;
574
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@*/
643
644struct termios {
645 tcflag_t c_iflag;
646 tcflag_t c_oflag;
647 tcflag_t c_cflag;
648 tcflag_t c_lflag;
649 cc_t c_cc;
650} ;
651
652 extern speed_t
653cfgetispeed (const struct termios *p)
654 /*@*/;
655
656 extern speed_t
657cfgetospeed (const struct termios *p)
658 /*@*/;
659
660 extern int
661cfsetispeed (struct termios *p)
662 /*@modifies *p@*/;
663
664 extern int
665cfsetospeed (struct termios *p)
666 /*@modifies *p@*/;
667
668 extern int
669tcdrain (int fd)
670 /*@modifies errno@*/;
671
672 extern int
673tcflow (int fd, int action)
674 /*@modifies errno@*/;
675
676 extern int
677tcflush (int fd, int qs)
678 /*@modifies errno@*/;
679
680 extern int
681tcgetattr (int fd, /*@out@*/ struct termios *p)
682 /*@modifies errno, *p@*/;
683
684 extern int
685tcsendbreak (int fd, int d)
686 /*@modifies errno@*/;
687
688 extern int
689tcsetattr (int fd, int opt, const struct termios *p)
690 /*@modifies errno@*/;
691
692/*
693** time.h
694*/
695
696/* Environ must be known before it can be used in `globals' clauses. */
697
698/*@unchecked@*/ extern char **environ;
699
700/*@constant int CLK_TCK@*/
701
702 extern void
703tzset (void)
ccf0a4a8 704 /*@globals environ@*/ /*@modifies systemState@*/;
885824d3 705
706/*
707** unistd.h
708*/
709
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@*/
744
53a89507 745extern /*@exits@*/ void _exit (int status) /*@*/;
885824d3 746
53a89507 747extern int access (const char *path, int mode) /*@modifies errno@*/;
885824d3 748
53a89507 749extern unsigned int alarm (unsigned int) /*@modifies systemState@*/;
885824d3 750
53a89507 751extern int chdir (const char *path) /*@modifies errno@*/;
885824d3 752
53a89507 753extern int chown (const char *path, uid_t owner, gid_t group)
754 /*@modifies fileSystem, errno@*/;
885824d3 755
756 extern int
757close (int fd)
ccf0a4a8 758 /*@modifies fileSystem, errno, systemState@*/;
885824d3 759 /* state: record locks are unlocked */
760
761 extern char *
762ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
ccf0a4a8 763 /*@modifies *s, systemState@*/;
885824d3 764
765 /* cuserid is in the 1988 version of POSIX but removed in 1990 */
766 extern char *
767cuserid (/*@null@*/ /*@out@*/ char *s)
768 /*@modifies *s@*/;
769
770 extern int
771dup2 (int fd, int fd2)
772 /*@modifies errno, fileSystem@*/;
773
774 extern int
775dup (int fd)
776 /*@modifies errno, fileSystem@*/;
777
778 extern /*@mayexit@*/ int
779execl (const char *path, const char *arg, ...)
780 /*@modifies errno@*/;
781
782 extern /*@mayexit@*/ int
783execle (const char *file, const char *arg, ...)
784 /*@modifies errno@*/;
785
786 extern /*@mayexit@*/ int
787execlp (const char *file, const char *arg, ...)
788 /*@modifies errno@*/;
789
790 extern /*@mayexit@*/ int
791execv (const char *path, char *const argv[])
792 /*@modifies errno@*/;
793
794 extern /*@mayexit@*/ int
795execve (const char *path, char *const argv[], char *const *envp)
796 /*@modifies errno@*/;
797
798 extern /*@mayexit@*/ int
799execvp (const char *file, char *const argv[])
800 /*@modifies errno@*/;
801
802 extern pid_t
803fork (void)
804 /*@modifies fileSystem, errno@*/;
805
806 extern long
807fpathconf (int fd, int name)
808 /*@modifies errno@*/;
809
53a89507 810extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size)
e5f31c00 811 /*@requires maxSet(buf) >= (size - 1)@*/
135ea728 812 /*@ensures maxRead(buf) <= (size - 1)@*/
e5f31c00 813
814 /*@modifies errno, *buf@*/ ;
885824d3 815
816 extern gid_t
817getegid (void)
818 /*@*/;
819
820 extern uid_t
821geteuid (void)
822 /*@*/;
823
824 extern gid_t
825getgid (void)
826 /*@*/;
827
828 extern int
829getgroups (int gs, /*@out@*/ gid_t gl[])
830 /*@modifies errno, gl[]@*/;
831
832 extern /*@observer@*/ char *
833getlogin (void)
834 /*@*/;
835
836 extern pid_t
837getpgrp (void)
838 /*@*/;
839
840 extern pid_t
841getpid (void)
842 /*@*/;
843
844 extern pid_t
845getppid (void)
846 /*@*/;
847
848 extern uid_t
849getuid (void)
850 /*@*/;
851
852 extern int
853isatty (int fd)
854 /*@*/;
855
856 extern int
857link (const char *o, const char *n)
858 /*@modifies errno, fileSystem@*/;
859
860 extern off_t
861lseek (int fd, off_t offset, int whence)
862 /*@modifies errno@*/;
863
864 extern long
865pathconf (const char *path, int name)
866 /*@modifies errno@*/;
867
868 extern int
869pause (void)
870 /*@modifies errno@*/;
871
872 extern int
873pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */
874 /*@modifies errno@*/;
875
15b3d2b2 876extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte)
b87215ab 877 /*@modifies errno, *buf@*/
878 /*@requires maxSet(buf) >= (nbyte - 1) @*/
15b3d2b2 879 /*@ensures maxRead(buf) >= nbyte @*/ ;
885824d3 880
15b3d2b2 881extern int rmdir (const char *path)
882 /*@modifies fileSystem, errno@*/;
885824d3 883
15b3d2b2 884extern int setgid (gid_t gid)
885 /*@modifies errno, systemState@*/;
885824d3 886
15b3d2b2 887extern int setpgid (pid_t pid, pid_t pgid)
888 /*@modifies errno, systemState@*/;
885824d3 889
15b3d2b2 890extern pid_t setsid (void) /*@modifies systemState@*/;
891
892extern int setuid (uid_t uid)
893 /*@modifies errno, systemState@*/;
885824d3 894
ccf0a4a8 895unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ;
885824d3 896
15b3d2b2 897extern long sysconf (int name)
898 /*@modifies errno@*/;
885824d3 899
15b3d2b2 900extern pid_t tcgetpgrp (int fd)
901 /*@modifies errno@*/;
885824d3 902
15b3d2b2 903extern int tcsetpgrp (int fd, pid_t pgrpid)
904 /*@modifies errno, systemState@*/;
885824d3 905
15b3d2b2 906/* Q: observer ok? */
907extern /*@null@*/ /*@observer@*/ char *ttyname (int fd)
908 /*@modifies errno@*/;
885824d3 909
15b3d2b2 910extern int unlink (const char *path)
911 /*@modifies fileSystem, errno@*/;
885824d3 912
15b3d2b2 913extern ssize_t write (int fd, const void *buf, size_t nbyte)
b87215ab 914 /*@requires maxRead(buf) >= nbyte@*/
915 /*@modifies errno@*/;
885824d3 916
917/*
918** utime.h
919*/
920
921struct utimbuf {
922 time_t actime;
923 time_t modtime;
924} ;
925
926 extern int
927utime (const char *path, /*@null@*/ const struct utimbuf *times)
928 /*@modifies fileSystem, errno@*/;
929
b072092f 930/*
931** regex.h
932*/
933
934typedef /*@abstract@*/ /*@mutable@*/ void *regex_t;
935typedef /*@integraltype@*/ regoff_t;
936
937typedef struct
938{
939 regoff_t rm_so;
940 regoff_t rm_eo;
941} regmatch_t;
942
943int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags)
944 /*:statusreturn@*/
945 /*@modifies preg@*/ ;
946
947int 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@*/ ;
950
951size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size)
952 /*@requires maxSet(errbuf) >= errbuf_size@*/
953 /*@modifies errbuf@*/ ;
954
955void regfree (/*@only@*/ regex_t *preg) ;
956
957/* regcomp flags */
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@*/
966
967/* regerror flags */
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 */
986
987/* regexec flags */
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@*/
994
ccf0a4a8 995
This page took 0.355377 seconds and 5 git commands to generate.