X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/345671f308ce68ce5c55ad3751f13185157189db..5b99bfd6792ab9229bb5b1d9048833d21b22ecef:/lib/stdio.h diff --git a/lib/stdio.h b/lib/stdio.h index 4e1336b..df49b76 100644 --- a/lib/stdio.h +++ b/lib/stdio.h @@ -1,284 +1,148 @@ - -/*stuff from the unix specification*/ - -/*things from stdio.h */ -extern void clearerr (FILE *stream) /*@modifies *stream@*/ ; - -extern char * ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s) - /*@modifies *s @*/ - // /*@requires maxSet(s) >= ( L_ctermid - 1) @*/ /*ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */ - - /*DRL 9-11-001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ; - - /*check returns*/ - - /* cuserid is in the 1988 version of POSIX but removed in 1990 */ - extern char * - cuserid (/*@null@*/ /*@out@*/ char *s) - /*@modifies *s@*/ - // /*@requires maxSet(s) >= ( L_ctermid - 1) @*/ /*@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ - ; - - extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; +/* +** stdio.h - Unix Specification +*/ + +/* +** evans 2001-12-30: added from http://www.opengroup.org/onlinepubs/007908799/xsh/stdio.h.html +*/ + +/*@constant unsignedintegraltype BUFSIZ@*/ +/*@constant unsignedintegraltype FILENAME_MAX@*/ +/*@constant unsignedintegraltype FOPEN_MAX@*/ +/*@constant _Bool _IOFBF@*/ +/*@constant _Bool _IOLBF@*/ +/*@constant _Bool _IONBF@*/ +/*@constant unsignedintegraltype L_ctermid@*/ +/*@constant unsignedintegraltype L_cuserid@*/ +/*@constant unsignedintegraltype L_tmpnam@*/ +/*@constant unsignedintegraltype SEEK_CUR@*/ +/*@constant unsignedintegraltype SEEK_END@*/ +/*@constant unsignedintegraltype SEEK_SET@*/ +/*@constant unsignedintegraltype TMP_MAX@*/ + +/*@constant observer char *P_tmpdir@*/ + +void clearerr (FILE *stream) /*@modifies *stream@*/ ; + +/*@dependent@*/ char *ctermid (/*@returned@*/ /*@null@*/ char *) /*@*/ ; + /* Result may be static pointer if parameter is NULL, otherwise is fresh. */ + + // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */ + /*DRL 9-11-2001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ; - extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) - /*@modifies errno, fileSystem@*/; +/*check returns*/ +/* cuserid is in the 1988 version of POSIX but removed in 1990 */ - extern int feof (FILE *stream) /*@modifies errno@*/ ; - extern int ferror (FILE *stream) /*@modifies errno@*/ ; - extern int fflush (/*@null@*/ FILE *stream) - /*@modifies *stream, errno, fileSystem;@*/ ; - - extern int fgetc (FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; - - extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) - /*@modifies *pos, errno@*/ /*@requires maxSet(pos) >= 0@*/ - /*@ensures maxRead(pos) >= 0 @*/; - - extern /*@null@*/ char * - fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) - /*@modifies fileSystem, *s, *stream, errno@*/ - /*@requires MaxSet(s) >= (n -1); @*/ - /*@ensures MaxRead(s) <= (n -1) /\ MaxRead(s) >= 0; @*/ ; - - extern int fileno (FILE *fp) /*@modifies errno@*/; - - extern void flockfile (FILE *file) /*@modifies *file, fileSystem@*/ ; - - extern FILE * fopen (char *filename, char *mode) /*@modifies errno, fileSystem;@*/ ; - - # ifdef STRICT - /*@printflike@*/ - extern int fprintf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream, errno@*/ ; - # else - /*@printflike@*/ - extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream, errno@*/ ; - # endif - - extern int fputc (int /*@alt char@*/ c, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; - - extern int fputs (char *s, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; - extern size_t - fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *ptr, *stream, errno@*/ - /*requires maxSet(ptr) >= (size - 1) @*/ /*@ensures maxRead(ptr) == (size - 1) @*/ - ; - extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) - /*@modifies *stream, fileSystem, errno@*/ ; - - /*@scanflike@*/ - extern int fscanf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream, errno@*/ ; - extern int fseek (FILE *stream, long int offset, int whence) - /*@modifies fileSystem, *stream, errno@*/ ; +char *cuserid (/*@null@*/ /*@out@*/ /*@returned@*/ char *s) + /*@warn legacy "cuserid is obsolete"@*/ + /*@modifies *s@*/ + // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/ + ; - extern int fseeko (FILE *stream, off_t offset, int whence) - /*@modifies fileSystem, *stream, errno@*/ ; +/* in standard.h: int fclose (FILE *stream) @modifies *stream, errno, fileSystem;@ */ - extern int fsetpos (FILE *stream, fpos_t *pos) - /*@modifies fileSystem, *stream, errno@*/ ; - - extern long int ftell(FILE *stream) /*@modifies errno@*/ ; - - extern off_t ftello(FILE *stream) /*@modifies errno@*/ ; - - extern void ftrylockfile (FILE *file) /*@modifies *file, fileSystem@*/ ; - - extern void funlockfile (FILE *file) /*@modifies *file, fileSystem;@*/ ; - - extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ - /*@requires maxRead(ptr) >= size @*/; - - extern int getc (/*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; /*drl added errno */ - - extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*drl added errno */ - - extern int getc_unlocked (/*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; /*Drl added 09-18-001 */ - - extern int getchar_unlocked (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*Drl added 09-18-001 */ - - /*@unchecked@*/ extern char *optarg; - /*@unchecked@*/ extern int optind; - /*@unchecked@*/ extern int optopt; - /*@unchecked@*/ extern int opterr; - /*@unchecked@*/ extern int optreset; - - extern int getopt (int argc, char * const *argv, const char *optstring) - /*@globals optarg, optind, optopt, opterr, optreset@*/ - /*@modifies optarg, optind, optopt@*/ - /*@requires maxRead(argv) >= (argc - 1) @*/ - - ; - - extern /*@null@*/ char *gets (/*@out@*/ char *s) - /*@warn bufferoverflowhigh - "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/ - /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ; +/*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) + /*@modifies errno, fileSystem@*/; - extern int getw (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */ +/* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */ +int fileno (/*@notnull@*/ FILE *) + /*:errorcode -1:*/ + /*@modifies errno@*/ ; - extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; +void flockfile (/*@notnull@*/ FILE *f) + /*@modifies f, fileSystem@*/ ; - extern void perror (/*@null@*/ char *s) - /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; +/* fopen, fprintf, fputc, fread, frepoen, fscanf, etc. in standard.h */ - extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype) - /*@modifies fileSystem, errno@*/ ; - # ifdef STRICT - /*@printflike@*/ - extern int printf (char *format, ...) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; - # else - /*@printflike@*/ - extern int /*@alt void@*/ printf (char *format, ...) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; - # endif +int fseeko (FILE *stream, off_t offset, int whence) + /*:errorcode -1:*/ + /*@modifies stream, errno@*/ ; - extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream, errno;@*/ - /*drl added errno 09-18-001 */ ; +off_t ftello(FILE *stream) + /*:errorcode -1:*/ /*@modifies errno*/ ; - extern int putchar (int /*@alt char@*/ c) - /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ - /*drl added errno 09-18-001 */ ; +int ftrylockfile(FILE *stream) + /*:errorcode !0:*/ + /*@modifies stream, fileSystem, errno*/ ; - extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream, errno;@*/ - /*Drl added 09-19-001 */ ; +void funlockfile (FILE *stream) + /*@modifies stream, fileSystem*/ ; - extern int putchar_unlocked (int /*@alt char@*/ c) - /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ - /*Drl added 09-19-001 */ ; +int getc_unlocked(FILE *stream) + /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/ + /*@modifies *stream, fileSystem, errno@*/ ; - extern int puts (const char *s) - /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/ - /*drl added errno 09-19-001 */ ; - - - extern int putw(int w, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ - /*Drl added 09-19-001 */ /*legacy*/ ; - - extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ; - - extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ - ; - - extern void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ - /*drl added errno AND fileSystem 09-19-001 */ ; - - /*@scanflike@*/ - extern int scanf(char *format, ...) +int getchar_unlocked (void) + /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/ /*@globals stdin@*/ - /*@modifies fileSystem, *stdin, errno@*/ - /*drl added errno 09-19-001 */ ; - - extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) - /*@modifies fileSystem, *stream, *buf@*/ - // /*@requires maxSet(buf) >= (BUFSIZ - 1) @*/ - ; - - extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, - int mode, size_t size) - /*@modifies fileSystem, *stream, *buf@*/ /*@requires maxSet(buf) >= (size - 1) @*/ ; - - # ifdef STRICT - /*@printflike@*/ - extern int snprintf (/*@out@*/ char *s, size_t n, char *format, ...) - /*@modifies *s@*/ + /*@modifies *stdin, fileSystem@*/ ; + +/*@unchecked@*/ char *optarg; +/*@unchecked@*/ int optind; +/*@unchecked@*/ int optopt; +/*@unchecked@*/ int opterr; +/*@unchecked@*/ int optreset; + +int getopt (int argc, char * const *argv, const char *optstring) + /*@warn legacy@*/ + /*@globals optarg, optind, optopt, opterr, optreset@*/ + /*@modifies optarg, optind, optopt@*/ + /*@requires maxRead(argv) >= (argc - 1) @*/ + ; - /*@requires maxSet(s) >= (n - 1) @*/ - ; - - # else +int getw (FILE *stream) + /*@warn legacy@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stream, errno@*/ ; - /*@printflike@*/ - extern int /*@alt void@*/ snprintf (/*@out@*/ char *s, size_t n, char *format, ...) - /*@modifies *s@*/ - /*@requires maxSet(s) >= (n - 1) @*/ - ; - # endif +int pclose(FILE *stream) + /*:errorcode -1:*/ + /*@modifies fileSystem, *stream, errno@*/ ; - - # ifdef STRICT - /*@printflike@*/ - extern int sprintf (/*@out@*/ char *s, char *format, ...) - /*@modifies *s@*/ ; - # else +/*@dependent@*/ /*@null@*/ FILE *popen (const char *command, const char *mode) + /*:errorcode NULL:*/ + /*@modifies fileSystem, errno@*/ ; - /*@printflike@*/ - extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) - /*@modifies *s@*/ ; +int putc_unlocked (int, FILE *stream) + /*@warn multithreaded "putc_unlocked is a thread unsafe version of putc"@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stream, errno@*/ ; - # endif +int putchar_unlocked(int) + /*@warn multithreaded "putchar_unlocked is a thread unsafe version of putchar"@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stdout, errno@*/ ; - /*@scanflike@*/ - int sscanf (/*@out@*/ char *s, char *format, ...) - /* modifies extra arguments */ /*@modifies errno@*/ - /*drl added errno 09-19-001 */ ; +int putw(int, FILE *stream) + /*@warn legacy@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stdout, errno@*/ ; +int remove (char *filename) /*@modifies fileSystem, errno@*/ ; +int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; +void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/ ; + +/* evans 2002-07-09: snprintf moved to standard.h (its in ISO C99 now) */ - extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) +/*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) /*@modifies internalState, errno@*/ - /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/ - /*warn that "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. Applications may find tmpfile() - more useful. " */ - - /*drl added errno 09-19-001 */ + /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/ + /*@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."*/ + /*drl added errno 09-19-001 */ + ; - ; +/*@null@*/ FILE *tmpfile (void) + /*@modifies fileSystem, errno@*/ + /*drl added errno 09-19-001 */ + ; - extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/ - /*drl added errno 09-19-001 */ - ; - - extern /*@observer@*/ char * - tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) +/*@observer@*/ char *tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) /*@modifies *s, internalState @*/ - // /*@requires maxSet(s) >= (L_tmpnam - 1) @*/ - /*warn 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. Applications may find tmpfile() more useful. */ - ; - - extern int ungetc (int /*@alt char@*/ c, FILE *stream) - /*@modifies fileSystem, *stream @*/ - - /*drl REMOVED errno 09-19-001*/ - ; - - int vfprintf (FILE *stream, char *format, va_list arg) - /*@modifies fileSystem, *stream, arg, errno@*/ ; - - int vprintf (const char *format, va_list arg) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; - - int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) - - /*@modifies str@*/ /*@requires maxSet(str) >= (size - 1) @*/ + // *@requires maxSet(s) >= (L_tmpnam - 1) @* + /*@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."*/ ; - - int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) - /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/ - /*@modifies str@*/ ; - - - extern char *optarg; - extern int opterr; - extern int optind; /*(LEGACY)*/ - extern int optopt; +