]>
Commit | Line | Data |
---|---|---|
1 | /* | |
2 | ** stdio.h - Unix Specification | |
3 | */ | |
4 | ||
5 | /* | |
6 | ** evans 2001-12-30: added from http://www.opengroup.org/onlinepubs/007908799/xsh/stdio.h.html | |
7 | */ | |
8 | ||
9 | /*@constant unsignedintegraltype BUFSIZ@*/ | |
10 | /*@constant unsignedintegraltype FILENAME_MAX@*/ | |
11 | /*@constant unsignedintegraltype FOPEN_MAX@*/ | |
12 | /*@constant lltX_bool _IOFBF@*/ | |
13 | /*@constant lltX_bool _IOLBF@*/ | |
14 | /*@constant lltX_bool _IONBF@*/ | |
15 | /*@constant unsignedintegraltype L_ctermid@*/ | |
16 | /*@constant unsignedintegraltype L_cuserid@*/ | |
17 | /*@constant unsignedintegraltype L_tmpnam@*/ | |
18 | /*@constant unsignedintegraltype SEEK_CUR@*/ | |
19 | /*@constant unsignedintegraltype SEEK_END@*/ | |
20 | /*@constant unsignedintegraltype SEEK_SET@*/ | |
21 | /*@constant unsignedintegraltype TMP_MAX@*/ | |
22 | ||
23 | /*@constant observer char *P_tmpdir@*/ | |
24 | ||
25 | void clearerr (FILE *stream) /*@modifies *stream@*/ ; | |
26 | ||
27 | /*@dependent@*/ char *ctermid (/*@returned@*/ /*@null@*/ char *) /*@*/ ; | |
28 | /* Result may be static pointer if parameter is NULL, otherwise is fresh. */ | |
29 | ||
30 | // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */ | |
31 | /*DRL 9-11-2001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ; | |
32 | ||
33 | /*check returns*/ | |
34 | /* cuserid is in the 1988 version of POSIX but removed in 1990 */ | |
35 | ||
36 | char *cuserid (/*@null@*/ /*@out@*/ /*@returned@*/ char *s) | |
37 | /*@warn legacy "cuserid is obsolete"@*/ | |
38 | /*@modifies *s@*/ | |
39 | // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ | |
40 | ; | |
41 | ||
42 | /* in standard.h: int fclose (FILE *stream) @modifies *stream, errno, fileSystem;@ */ | |
43 | ||
44 | /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) | |
45 | /*@modifies errno, fileSystem@*/; | |
46 | ||
47 | /* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */ | |
48 | ||
49 | int fileno (/*@notnull@*/ FILE *) | |
50 | /*:errorcode -1:*/ | |
51 | /*@modifies errno@*/ ; | |
52 | ||
53 | void flockfile (/*@notnull@*/ FILE *f) | |
54 | /*@modifies f, fileSystem@*/ ; | |
55 | ||
56 | /* fopen, fprintf, fputc, fread, frepoen, fscanf, etc. in standard.h */ | |
57 | ||
58 | ||
59 | int fseeko (FILE *stream, off_t offset, int whence) | |
60 | /*:errorcode -1:*/ | |
61 | /*@modifies stream, errno@*/ ; | |
62 | ||
63 | off_t ftello(FILE *stream) | |
64 | /*:errorcode -1:*/ /*@modifies errno*/ ; | |
65 | ||
66 | int ftrylockfile(FILE *stream) | |
67 | /*:errorcode !0:*/ | |
68 | /*@modifies stream, fileSystem, errno*/ ; | |
69 | ||
70 | void funlockfile (FILE *stream) | |
71 | /*@modifies stream, fileSystem*/ ; | |
72 | ||
73 | int getc_unlocked(FILE *stream) | |
74 | /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/ | |
75 | /*@modifies *stream, fileSystem, errno@*/ ; | |
76 | ||
77 | int getchar_unlocked (void) | |
78 | /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/ | |
79 | /*@globals stdin@*/ | |
80 | /*@modifies *stdin, fileSystem@*/ ; | |
81 | ||
82 | /*@unchecked@*/ char *optarg; | |
83 | /*@unchecked@*/ int optind; | |
84 | /*@unchecked@*/ int optopt; | |
85 | /*@unchecked@*/ int opterr; | |
86 | /*@unchecked@*/ int optreset; | |
87 | ||
88 | int getopt (int argc, char * const *argv, const char *optstring) | |
89 | /*@warn legacy@*/ | |
90 | /*@globals optarg, optind, optopt, opterr, optreset@*/ | |
91 | /*@modifies optarg, optind, optopt@*/ | |
92 | /*@requires maxRead(argv) >= (argc - 1) @*/ | |
93 | ; | |
94 | ||
95 | int getw (FILE *stream) | |
96 | /*@warn legacy@*/ | |
97 | /*:errorcode EOF:*/ | |
98 | /*@modifies fileSystem, *stream, errno@*/ ; | |
99 | ||
100 | int pclose(FILE *stream) | |
101 | /*:errorcode -1:*/ | |
102 | /*@modifies fileSystem, *stream, errno@*/ ; | |
103 | ||
104 | /*@dependent@*/ /*@null@*/ FILE *popen (const char *command, const char *mode) | |
105 | /*:errorcode NULL:*/ | |
106 | /*@modifies fileSystem, errno@*/ ; | |
107 | ||
108 | int putc_unlocked (int, FILE *stream) | |
109 | /*@warn multithreaded "putc_unlocked is a thread unsafe version of putc"@*/ | |
110 | /*:errorcode EOF:*/ | |
111 | /*@modifies fileSystem, *stream, errno@*/ ; | |
112 | ||
113 | int putchar_unlocked(int) | |
114 | /*@warn multithreaded "putchar_unlocked is a thread unsafe version of putchar"@*/ | |
115 | /*:errorcode EOF:*/ | |
116 | /*@modifies fileSystem, *stdout, errno@*/ ; | |
117 | ||
118 | int putw(int, FILE *stream) | |
119 | /*@warn legacy@*/ | |
120 | /*:errorcode EOF:*/ | |
121 | /*@modifies fileSystem, *stdout, errno@*/ ; | |
122 | ||
123 | int remove (char *filename) /*@modifies fileSystem, errno@*/ ; | |
124 | int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; | |
125 | void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ ; | |
126 | ||
127 | /* evans 2002-07-09: snprintf moved to standard.h (its in ISO C99 now) */ | |
128 | ||
129 | /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) | |
130 | /*@modifies internalState, errno@*/ | |
131 | /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/ | |
132 | /*@warn toctou "Between the time a pathname is created and the file is opened, it is possible for some other process to create a file with the same name. Use tmpfile instead."*/ | |
133 | /*drl added errno 09-19-001 */ | |
134 | ; | |
135 | ||
136 | ||
137 | /*@null@*/ FILE *tmpfile (void) | |
138 | /*@modifies fileSystem, errno@*/ | |
139 | /*drl added errno 09-19-001 */ | |
140 | ; | |
141 | ||
142 | /*@observer@*/ char *tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) | |
143 | /*@modifies *s, internalState @*/ | |
144 | // *@requires maxSet(s) >= (L_tmpnam - 1) @* | |
145 | /*@warn toctou "Between the time a pathname is created and the file is opened, another process may create a file with the same name. Use tmpfile instead."*/ | |
146 | ; | |
147 | ||
148 |