]>
Commit | Line | Data |
---|---|---|
f9264521 | 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 */ | |
345671f3 | 35 | |
f9264521 | 36 | char *cuserid (/*@null@*/ /*@out@*/ /*@returned@*/ char *s) |
37 | /*@warn legacy "cuserid is obsolete"@*/ | |
38 | /*@modifies *s@*/ | |
4aadc959 | 39 | // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ |
f9264521 | 40 | ; |
345671f3 | 41 | |
f9264521 | 42 | /* in standard.h: int fclose (FILE *stream) @modifies *stream, errno, fileSystem;@ */ |
345671f3 | 43 | |
f9264521 | 44 | /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) |
345671f3 | 45 | /*@modifies errno, fileSystem@*/; |
46 | ||
f9264521 | 47 | /* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */ |
345671f3 | 48 | |
f9264521 | 49 | int fileno (/*@notnull@*/ FILE *) |
50 | /*:errorcode -1:*/ | |
51 | /*@modifies errno@*/ ; | |
345671f3 | 52 | |
f9264521 | 53 | void flockfile (/*@notnull@*/ FILE *f) |
54 | /*@modifies f, fileSystem@*/ ; | |
345671f3 | 55 | |
f9264521 | 56 | /* fopen, fprintf, fputc, fread, frepoen, fscanf, etc. in standard.h */ |
345671f3 | 57 | |
345671f3 | 58 | |
f9264521 | 59 | int fseeko (FILE *stream, off_t offset, int whence) |
60 | /*:errorcode -1:*/ | |
61 | /*@modifies stream, errno@*/ ; | |
345671f3 | 62 | |
f9264521 | 63 | off_t ftello(FILE *stream) |
64 | /*:errorcode -1:*/ /*@modifies errno*/ ; | |
345671f3 | 65 | |
f9264521 | 66 | int ftrylockfile(FILE *stream) |
67 | /*:errorcode !0:*/ | |
68 | /*@modifies stream, fileSystem, errno*/ ; | |
345671f3 | 69 | |
f9264521 | 70 | void funlockfile (FILE *stream) |
71 | /*@modifies stream, fileSystem*/ ; | |
345671f3 | 72 | |
f9264521 | 73 | int getc_unlocked(FILE *stream) |
74 | /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/ | |
75 | /*@modifies *stream, fileSystem, errno@*/ ; | |
155af98d | 76 | |
f9264521 | 77 | int getchar_unlocked (void) |
78 | /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/ | |
345671f3 | 79 | /*@globals stdin@*/ |
f9264521 | 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@*/ ; | |
345671f3 | 99 | |
f9264521 | 100 | int pclose(FILE *stream) |
101 | /*:errorcode -1:*/ | |
102 | /*@modifies fileSystem, *stream, errno@*/ ; | |
345671f3 | 103 | |
f9264521 | 104 | /*@dependent@*/ /*@null@*/ FILE *popen (const char *command, const char *mode) |
105 | /*:errorcode NULL:*/ | |
106 | /*@modifies fileSystem, errno@*/ ; | |
345671f3 | 107 | |
f9264521 | 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@*/ ; | |
345671f3 | 112 | |
f9264521 | 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@*/ ; | |
345671f3 | 117 | |
f9264521 | 118 | int putw(int, FILE *stream) |
119 | /*@warn legacy@*/ | |
120 | /*:errorcode EOF:*/ | |
121 | /*@modifies fileSystem, *stdout, errno@*/ ; | |
345671f3 | 122 | |
f9264521 | 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) */ | |
345671f3 | 128 | |
f9264521 | 129 | /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) |
345671f3 | 130 | /*@modifies internalState, errno@*/ |
f9264521 | 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 | ; | |
345671f3 | 135 | |
136 | ||
f9264521 | 137 | /*@null@*/ FILE *tmpfile (void) |
138 | /*@modifies fileSystem, errno@*/ | |
139 | /*drl added errno 09-19-001 */ | |
140 | ; | |
345671f3 | 141 | |
f9264521 | 142 | /*@observer@*/ char *tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) |
345671f3 | 143 | /*@modifies *s, internalState @*/ |
f9264521 | 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 | ; | |
bb7c2085 | 147 | |
345671f3 | 148 |