More refactoring of library support.
[splint-patched.git] / imports / stdio.lcl
blobe7a95141c6b36223fa63c4292dab881225b2abbf
1 /*
2 ** stdio.lcl
3 **
4 ** based on /usr/include/stdio.h on red-cross
5 */
7 imports <stdlib> ;
9 /*
10 ** we need to allow casts to and from these types...
11 ** they should be exposed, but unknown type.
14 immutable type FILE;
16 typedef void *va_list;
17 typedef void *fpos_t;
19 FILE *stdin;
20 FILE *stdout;
21 FILE *stderr;
23 constant int EOF ;
25 | int : char | getc (FILE *stream )
27    ensures true;
30 | int : char | getchar (void)
32    ensures true;
35 | int : void | putc (| int : char | c, FILE *stream)
37    ensures true;
40 int putchar (|int : char| c)
42    ensures true;
45 | int : bool | feof (FILE *stream)
47    ensures true;
50 | int : bool | ferror (FILE *stream )
52    ensures true;
55 int fileno (FILE *stream)
57    ensures true;
60 int _filbuf (FILE *p)
62    ensures true;
65 int _flsbuf (unsigned char x, FILE *p)
67    ensures true;
70 void clearerr (FILE *stream)
72    ensures true;
75 | int : void | fclose (FILE *stream )
77    ensures true;
80 FILE * fdopen (int filedes, char *ttype)
82    ensures true;
85 | int : void | fflush (FILE *stream )
87    ensures true;
90 | int : char | fgetc (FILE *stream )
92    ensures true;
95 int fgetpos (FILE *stream, fpos_t *pos )
97    ensures true;
100 char *fgets (char *s, int n, FILE *stream )
102    ensures true;
106 FILE *fopen (char *filename, char *ttype )
108    ensures true;
111 printflike
112 | int : void | fprintf (FILE *stream, char *format, ...)
114    ensures true;
117 printflike
118 | int : void | sprintf (FILE *stream, char *format, ...)
120    ensures true;
123 | int : void | fputc (| int : char | c, FILE *stream )
125    ensures true;
128 | int : void | fputs( char *s, FILE *stream )
130    ensures true;
133 size_t fread (void *ptr, size_t size,
134               size_t nitems, FILE *stream )
136    ensures true;
139 FILE *freopen (char *filename, char *ttype,
140                FILE *stream)
142    ensures true;
145 scanflike
146 int fscanf (FILE *stream, char *format, ... )
148    ensures true;
151 | int : void | fseek (FILE *stream, long offset, int ptrname)
153    ensures true;
156 int fsetpos (FILE *stream, fpos_t *pos)
158    ensures true;
161 long ftell (FILE *stream)
163    ensures true;
166 size_t fwrite (void *ptr, size_t size,
167                size_t nitems, FILE *stream)
169    ensures true;
172 char *gets (char *s)
174    ensures true;
177 void perror (char *s)
179    ensures true;
182 FILE  *popen (char *command, char *ttype)
184    ensures true;
187 | int : void | ungetc(char c, FILE *stream)
189    ensures true;
192 printflike
193 | int : void | printf (char *format, ...)
195    ensures true;
198 | int : void | puts (char *s)
200    ensures true;
203 | int : bool | remove (char *filename)
205    ensures true;
208 | int : bool | rename (char *from, char *to)
210    ensures true;
213 void rewind (FILE *stream)
215    ensures true;
218 scanflike
219 | int : void | scanf (char *format, ...)
221    ensures true;
224 void setbuf (FILE *stream, char *buf)
226    ensures true;
229 int setvbuf (FILE *stream, char *buf,
230              int ttype, size_t size )
232    ensures true;
235 scanflike
236 | int : void | sscanf (char *s, char *format, ...)
238    ensures true;
241 FILE *tmpfile( void )
243    ensures true;
246 char *tmpnam (char *s)
248    ensures true;