]>
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 @*/ | |
9 | // /*@requires maxSet(s) >= ( L_ctermid - 1) @*/ /*ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */ | |
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@*/ | |
19 | // /*@requires maxSet(s) >= ( L_ctermid - 1) @*/ /*@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ | |
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 | ||
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 | ||
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@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ; | |
125 | ||
126 | extern int getw (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */ | |
127 | ||
128 | ||
129 | extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; | |
130 | ||
131 | extern void perror (/*@null@*/ char *s) | |
132 | /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; | |
133 | ||
134 | extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype) | |
135 | /*@modifies fileSystem, errno@*/ ; | |
136 | ||
137 | # ifdef STRICT | |
138 | /*@printflike@*/ | |
139 | extern int printf (char *format, ...) | |
140 | /*@globals stdout@*/ | |
141 | /*@modifies fileSystem, *stdout@*/ ; | |
142 | # else | |
143 | /*@printflike@*/ | |
144 | extern int /*@alt void@*/ printf (char *format, ...) | |
145 | /*@globals stdout@*/ | |
146 | /*@modifies fileSystem, *stdout@*/ ; | |
147 | # endif | |
148 | ||
149 | extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) | |
150 | /*@modifies fileSystem, *stream, errno;@*/ | |
151 | /*drl added errno 09-18-001 */ ; | |
152 | ||
153 | extern int putchar (int /*@alt char@*/ c) | |
154 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
155 | /*drl added errno 09-18-001 */ ; | |
156 | ||
157 | extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) | |
158 | /*@modifies fileSystem, *stream, errno;@*/ | |
159 | /*Drl added 09-19-001 */ ; | |
160 | ||
161 | extern int putchar_unlocked (int /*@alt char@*/ c) | |
162 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
163 | /*Drl added 09-19-001 */ ; | |
164 | ||
165 | extern int puts (const char *s) | |
166 | /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ | |
167 | /*drl added errno 09-19-001 */ ; | |
168 | ||
169 | ||
170 | extern int putw(int w, FILE *stream) | |
171 | /*@modifies fileSystem, *stream, errno@*/ | |
172 | /*Drl added 09-19-001 */ /*legacy*/ ; | |
173 | ||
174 | extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ; | |
175 | ||
176 | extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ | |
177 | ; | |
178 | ||
179 | extern void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ | |
180 | /*drl added errno AND fileSystem 09-19-001 */ ; | |
181 | ||
182 | /*@scanflike@*/ | |
183 | extern int scanf(char *format, ...) | |
184 | /*@globals stdin@*/ | |
185 | /*@modifies fileSystem, *stdin, errno@*/ | |
186 | /*drl added errno 09-19-001 */ ; | |
187 | ||
188 | extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) | |
189 | /*@modifies fileSystem, *stream, *buf@*/ | |
190 | // /*@requires maxSet(buf) >= (BUFSIZ - 1) @*/ | |
191 | ; | |
192 | ||
193 | extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, | |
194 | int mode, size_t size) | |
195 | /*@modifies fileSystem, *stream, *buf@*/ /*@requires maxSet(buf) >= (size - 1) @*/ ; | |
196 | ||
197 | # ifdef STRICT | |
198 | /*@printflike@*/ | |
199 | extern int snprintf (/*@out@*/ char *s, size_t n, char *format, ...) | |
200 | /*@modifies *s@*/ | |
201 | ||
202 | /*@requires maxSet(s) >= (n - 1) @*/ | |
203 | ; | |
204 | ||
205 | # else | |
206 | ||
207 | /*@printflike@*/ | |
208 | extern int /*@alt void@*/ snprintf (/*@out@*/ char *s, size_t n, char *format, ...) | |
209 | /*@modifies *s@*/ | |
210 | /*@requires maxSet(s) >= (n - 1) @*/ | |
211 | ; | |
212 | # endif | |
213 | ||
214 | ||
215 | # ifdef STRICT | |
216 | /*@printflike@*/ | |
217 | extern int sprintf (/*@out@*/ char *s, char *format, ...) | |
218 | /*@modifies *s@*/ ; | |
219 | # else | |
220 | ||
221 | /*@printflike@*/ | |
222 | extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) | |
223 | /*@modifies *s@*/ ; | |
224 | ||
225 | # endif | |
226 | ||
227 | /*@scanflike@*/ | |
228 | int sscanf (/*@out@*/ char *s, char *format, ...) | |
229 | /* modifies extra arguments */ /*@modifies errno@*/ | |
230 | /*drl added errno 09-19-001 */ ; | |
231 | ||
232 | ||
233 | extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) | |
234 | /*@modifies internalState, errno@*/ | |
235 | /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/ | |
236 | /*warn that "Between the time a pathname is created and the file is opened, it is possible | |
237 | for some other process to create a file with the same name. Applications may find tmpfile() | |
238 | more useful. " */ | |
239 | ||
240 | /*drl added errno 09-19-001 */ | |
241 | ||
242 | ; | |
243 | ||
244 | ||
245 | extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/ | |
246 | /*drl added errno 09-19-001 */ | |
247 | ; | |
248 | ||
249 | extern /*@observer@*/ char * | |
250 | tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) | |
251 | /*@modifies *s, internalState @*/ | |
252 | // /*@requires maxSet(s) >= (L_tmpnam - 1) @*/ | |
253 | /*warn Between the time a pathname is created and the file is opened, it is possible for some other | |
254 | process to create a file with the same name. Applications may find tmpfile() more useful. */ | |
255 | ; | |
256 | ||
257 | extern int ungetc (int /*@alt char@*/ c, FILE *stream) | |
258 | /*@modifies fileSystem, *stream @*/ | |
259 | ||
260 | /*drl REMOVED errno 09-19-001*/ | |
261 | ; | |
262 | ||
263 | int vfprintf (FILE *stream, char *format, va_list arg) | |
264 | /*@modifies fileSystem, *stream, arg, errno@*/ ; | |
265 | ||
266 | int vprintf (const char *format, va_list arg) | |
267 | /*@globals stdout@*/ | |
268 | /*@modifies fileSystem, *stdout@*/ ; | |
269 | ||
bb7c2085 | 270 | int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) |
271 | /*@modifies str@*/ | |
272 | /*@requires maxSet(str) >= (size - 1) @*/ ; | |
345671f3 | 273 | |
bb7c2085 | 274 | int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) |
275 | /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/ | |
276 | /*@modifies str@*/ ; | |
277 | ||
278 | extern char *optarg; | |
279 | extern int opterr; | |
280 | extern int optind; /*(LEGACY)*/ | |
281 | extern int optopt; | |
345671f3 | 282 |