]>
Commit | Line | Data |
---|---|---|
345671f3 | 1 | |
2 | /*stuff from the unix specification*/ | |
3 | ||
4 | /*things from stdio.h */ | |
5 | extern void clearerr (FILE *stream) /*@modifies *stream@*/ ; | |
6 | ||
7 | extern char * ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s) | |
8 | /*@modifies *s @*/ | |
4aadc959 | 9 | // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */ |
345671f3 | 10 | |
11 | /*DRL 9-11-001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ; | |
12 | ||
13 | /*check returns*/ | |
14 | ||
15 | /* cuserid is in the 1988 version of POSIX but removed in 1990 */ | |
16 | extern char * | |
17 | cuserid (/*@null@*/ /*@out@*/ char *s) | |
18 | /*@modifies *s@*/ | |
4aadc959 | 19 | // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ |
345671f3 | 20 | ; |
21 | ||
22 | extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; | |
23 | ||
24 | extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) | |
25 | /*@modifies errno, fileSystem@*/; | |
26 | ||
27 | extern int feof (FILE *stream) /*@modifies errno@*/ ; | |
28 | extern int ferror (FILE *stream) /*@modifies errno@*/ ; | |
29 | extern int fflush (/*@null@*/ FILE *stream) | |
30 | /*@modifies *stream, errno, fileSystem;@*/ ; | |
31 | ||
32 | extern int fgetc (FILE *stream) | |
33 | /*@modifies fileSystem, *stream, errno@*/ ; | |
34 | ||
35 | extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) | |
36 | /*@modifies *pos, errno@*/ /*@requires maxSet(pos) >= 0@*/ | |
37 | /*@ensures maxRead(pos) >= 0 @*/; | |
38 | ||
39 | extern /*@null@*/ char * | |
40 | fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) | |
41 | /*@modifies fileSystem, *s, *stream, errno@*/ | |
42 | /*@requires MaxSet(s) >= (n -1); @*/ | |
43 | /*@ensures MaxRead(s) <= (n -1) /\ MaxRead(s) >= 0; @*/ ; | |
44 | ||
45 | extern int fileno (FILE *fp) /*@modifies errno@*/; | |
46 | ||
47 | extern void flockfile (FILE *file) /*@modifies *file, fileSystem@*/ ; | |
48 | ||
49 | extern FILE * fopen (char *filename, char *mode) /*@modifies errno, fileSystem;@*/ ; | |
50 | ||
51 | # ifdef STRICT | |
52 | /*@printflike@*/ | |
53 | extern int fprintf (FILE *stream, char *format, ...) | |
54 | /*@modifies fileSystem, *stream, errno@*/ ; | |
55 | # else | |
56 | /*@printflike@*/ | |
57 | extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) | |
58 | /*@modifies fileSystem, *stream, errno@*/ ; | |
59 | # endif | |
60 | ||
61 | extern int fputc (int /*@alt char@*/ c, FILE *stream) | |
62 | /*@modifies fileSystem, *stream, errno@*/ ; | |
63 | ||
64 | extern int fputs (char *s, FILE *stream) | |
65 | /*@modifies fileSystem, *stream, errno@*/ ; | |
66 | extern size_t | |
67 | fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream) | |
68 | /*@modifies fileSystem, *ptr, *stream, errno@*/ | |
69 | /*requires maxSet(ptr) >= (size - 1) @*/ /*@ensures maxRead(ptr) == (size - 1) @*/ | |
70 | ; | |
71 | extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) | |
72 | /*@modifies *stream, fileSystem, errno@*/ ; | |
73 | ||
74 | /*@scanflike@*/ | |
75 | extern int fscanf (FILE *stream, char *format, ...) | |
76 | /*@modifies fileSystem, *stream, errno@*/ ; | |
77 | extern int fseek (FILE *stream, long int offset, int whence) | |
78 | /*@modifies fileSystem, *stream, errno@*/ ; | |
79 | ||
80 | extern int fseeko (FILE *stream, off_t offset, int whence) | |
81 | /*@modifies fileSystem, *stream, errno@*/ ; | |
82 | ||
83 | extern int fsetpos (FILE *stream, fpos_t *pos) | |
84 | /*@modifies fileSystem, *stream, errno@*/ ; | |
85 | ||
86 | extern long int ftell(FILE *stream) /*@modifies errno@*/ ; | |
87 | ||
88 | extern off_t ftello(FILE *stream) /*@modifies errno@*/ ; | |
89 | ||
90 | extern void ftrylockfile (FILE *file) /*@modifies *file, fileSystem@*/ ; | |
91 | ||
92 | extern void funlockfile (FILE *file) /*@modifies *file, fileSystem;@*/ ; | |
93 | ||
94 | extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) | |
95 | /*@modifies fileSystem, *stream, errno@*/ | |
96 | /*@requires maxRead(ptr) >= size @*/; | |
97 | ||
98 | extern int getc (/*@sef@*/ FILE *stream) | |
99 | /*@modifies fileSystem, *stream, errno@*/ ; /*drl added errno */ | |
100 | ||
101 | extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*drl added errno */ | |
102 | ||
103 | extern int getc_unlocked (/*@sef@*/ FILE *stream) | |
104 | /*@modifies fileSystem, *stream, errno@*/ ; /*Drl added 09-18-001 */ | |
105 | ||
106 | extern int getchar_unlocked (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*Drl added 09-18-001 */ | |
107 | ||
108 | /*@unchecked@*/ extern char *optarg; | |
109 | /*@unchecked@*/ extern int optind; | |
110 | /*@unchecked@*/ extern int optopt; | |
111 | /*@unchecked@*/ extern int opterr; | |
112 | /*@unchecked@*/ extern int optreset; | |
113 | ||
155af98d | 114 | extern int getopt (int argc, char * const *argv, const char *optstring) |
115 | /*@globals optarg, optind, optopt, opterr, optreset@*/ | |
116 | /*@modifies optarg, optind, optopt@*/ | |
117 | /*@requires maxRead(argv) >= (argc - 1) @*/ | |
118 | ; | |
119 | ||
120 | /*@-bufferoverflowhigh@*/ | |
121 | extern /*@null@*/ char *gets (/*@out@*/ char *s) | |
122 | /*@warn bufferoverflowhigh | |
123 | "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/ | |
124 | /*@globals stdin@*/ | |
125 | /*@modifies fileSystem, *s, *stdin, errno@*/ ; | |
345671f3 | 126 | |
155af98d | 127 | extern int getw (FILE *stream) |
128 | /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */ | |
345671f3 | 129 | |
155af98d | 130 | extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; |
345671f3 | 131 | |
155af98d | 132 | extern void perror (/*@null@*/ char *s) |
345671f3 | 133 | /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; |
134 | ||
155af98d | 135 | extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype) |
345671f3 | 136 | /*@modifies fileSystem, errno@*/ ; |
137 | ||
138 | # ifdef STRICT | |
139 | /*@printflike@*/ | |
140 | extern int printf (char *format, ...) | |
141 | /*@globals stdout@*/ | |
142 | /*@modifies fileSystem, *stdout@*/ ; | |
143 | # else | |
144 | /*@printflike@*/ | |
145 | extern int /*@alt void@*/ printf (char *format, ...) | |
146 | /*@globals stdout@*/ | |
147 | /*@modifies fileSystem, *stdout@*/ ; | |
148 | # endif | |
149 | ||
150 | extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) | |
151 | /*@modifies fileSystem, *stream, errno;@*/ | |
152 | /*drl added errno 09-18-001 */ ; | |
153 | ||
154 | extern int putchar (int /*@alt char@*/ c) | |
155 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
156 | /*drl added errno 09-18-001 */ ; | |
157 | ||
158 | extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) | |
159 | /*@modifies fileSystem, *stream, errno;@*/ | |
160 | /*Drl added 09-19-001 */ ; | |
161 | ||
162 | extern int putchar_unlocked (int /*@alt char@*/ c) | |
163 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
164 | /*Drl added 09-19-001 */ ; | |
165 | ||
166 | extern int puts (const char *s) | |
167 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
168 | /*drl added errno 09-19-001 */ ; | |
169 | ||
170 | ||
171 | extern int putw(int w, FILE *stream) | |
172 | /*@modifies fileSystem, *stream, errno@*/ | |
173 | /*Drl added 09-19-001 */ /*legacy*/ ; | |
174 | ||
175 | extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ; | |
176 | ||
177 | extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ | |
178 | ; | |
179 | ||
180 | extern void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ | |
181 | /*drl added errno AND fileSystem 09-19-001 */ ; | |
182 | ||
183 | /*@scanflike@*/ | |
184 | extern int scanf(char *format, ...) | |
185 | /*@globals stdin@*/ | |
186 | /*@modifies fileSystem, *stdin, errno@*/ | |
187 | /*drl added errno 09-19-001 */ ; | |
188 | ||
86d93ed3 | 189 | extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) |
345671f3 | 190 | /*@modifies fileSystem, *stream, *buf@*/ |
4aadc959 | 191 | // *@requires maxSet(buf) >= (BUFSIZ - 1) @*/ |
345671f3 | 192 | ; |
193 | ||
86d93ed3 | 194 | extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, |
345671f3 | 195 | int mode, size_t size) |
196 | /*@modifies fileSystem, *stream, *buf@*/ /*@requires maxSet(buf) >= (size - 1) @*/ ; | |
197 | ||
198 | # ifdef STRICT | |
199 | /*@printflike@*/ | |
200 | extern int snprintf (/*@out@*/ char *s, size_t n, char *format, ...) | |
201 | /*@modifies *s@*/ | |
202 | ||
203 | /*@requires maxSet(s) >= (n - 1) @*/ | |
204 | ; | |
205 | ||
206 | # else | |
207 | ||
208 | /*@printflike@*/ | |
209 | extern int /*@alt void@*/ snprintf (/*@out@*/ char *s, size_t n, char *format, ...) | |
210 | /*@modifies *s@*/ | |
211 | /*@requires maxSet(s) >= (n - 1) @*/ | |
212 | ; | |
213 | # endif | |
214 | ||
215 | ||
216 | # ifdef STRICT | |
217 | /*@printflike@*/ | |
218 | extern int sprintf (/*@out@*/ char *s, char *format, ...) | |
219 | /*@modifies *s@*/ ; | |
220 | # else | |
221 | ||
222 | /*@printflike@*/ | |
223 | extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) | |
224 | /*@modifies *s@*/ ; | |
225 | ||
226 | # endif | |
227 | ||
228 | /*@scanflike@*/ | |
229 | int sscanf (/*@out@*/ char *s, char *format, ...) | |
230 | /* modifies extra arguments */ /*@modifies errno@*/ | |
231 | /*drl added errno 09-19-001 */ ; | |
232 | ||
233 | ||
234 | extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) | |
235 | /*@modifies internalState, errno@*/ | |
236 | /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/ | |
237 | /*warn that "Between the time a pathname is created and the file is opened, it is possible | |
238 | for some other process to create a file with the same name. Applications may find tmpfile() | |
239 | more useful. " */ | |
240 | ||
241 | /*drl added errno 09-19-001 */ | |
242 | ||
243 | ; | |
244 | ||
245 | ||
246 | extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/ | |
247 | /*drl added errno 09-19-001 */ | |
248 | ; | |
249 | ||
250 | extern /*@observer@*/ char * | |
251 | tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) | |
252 | /*@modifies *s, internalState @*/ | |
4aadc959 | 253 | // *@requires maxSet(s) >= (L_tmpnam - 1) @* |
345671f3 | 254 | /*warn Between the time a pathname is created and the file is opened, it is possible for some other |
255 | process to create a file with the same name. Applications may find tmpfile() more useful. */ | |
256 | ; | |
257 | ||
258 | extern int ungetc (int /*@alt char@*/ c, FILE *stream) | |
259 | /*@modifies fileSystem, *stream @*/ | |
260 | ||
261 | /*drl REMOVED errno 09-19-001*/ | |
262 | ; | |
263 | ||
264 | int vfprintf (FILE *stream, char *format, va_list arg) | |
265 | /*@modifies fileSystem, *stream, arg, errno@*/ ; | |
266 | ||
267 | int vprintf (const char *format, va_list arg) | |
268 | /*@globals stdout@*/ | |
269 | /*@modifies fileSystem, *stdout@*/ ; | |
270 | ||
bb7c2085 | 271 | int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) |
272 | /*@modifies str@*/ | |
273 | /*@requires maxSet(str) >= (size - 1) @*/ ; | |
345671f3 | 274 | |
bb7c2085 | 275 | int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) |
276 | /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/ | |
277 | /*@modifies str@*/ ; | |
278 | ||
279 | extern char *optarg; | |
280 | extern int opterr; | |
281 | extern int optind; /*(LEGACY)*/ | |
282 | extern int optopt; | |
345671f3 | 283 |