+/*
+** 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 lltX_bool _IOFBF@*/
+/*@constant lltX_bool _IOLBF@*/
+/*@constant lltX_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*/ ;
+
+/*check returns*/
+/* cuserid is in the 1988 version of POSIX but removed in 1990 */
-/*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@*/
+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 fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
+/* in standard.h: int fclose (FILE *stream) @modifies *stream, errno, fileSystem;@ */
- extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
+/*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
/*@modifies errno, fileSystem@*/;
- 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@*/ ;
+/* feof, ferror fflush, fgetc, fgetpos, fgets - in standard.h */
- extern int fseeko (FILE *stream, off_t offset, int whence)
- /*@modifies fileSystem, *stream, errno@*/ ;
-
- extern int fsetpos (FILE *stream, fpos_t *pos)
- /*@modifies fileSystem, *stream, errno@*/ ;
-
- extern long int ftell(FILE *stream) /*@modifies errno@*/ ;
+int fileno (/*@notnull@*/ FILE *)
+ /*:errorcode -1:*/
+ /*@modifies errno@*/ ;
- extern off_t ftello(FILE *stream) /*@modifies errno@*/ ;
+void flockfile (/*@notnull@*/ FILE *f)
+ /*@modifies f, fileSystem@*/ ;
- extern void ftrylockfile (FILE *file) /*@modifies *file, fileSystem@*/ ;
-
- extern void funlockfile (FILE *file) /*@modifies *file, fileSystem;@*/ ;
+/* fopen, fprintf, fputc, fread, frepoen, fscanf, etc. in standard.h */
- 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 */
+int fseeko (FILE *stream, off_t offset, int whence)
+ /*:errorcode -1:*/
+ /*@modifies stream, errno@*/ ;
- extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*drl added errno */
+off_t ftello(FILE *stream)
+ /*:errorcode -1:*/ /*@modifies errno*/ ;
- extern int getc_unlocked (/*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ; /*Drl added 09-18-001 */
+int ftrylockfile(FILE *stream)
+ /*:errorcode !0:*/
+ /*@modifies stream, fileSystem, errno*/ ;
- extern int getchar_unlocked (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*Drl added 09-18-001 */
+void funlockfile (FILE *stream)
+ /*@modifies stream, fileSystem*/ ;
- /*@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) @*/
- ;
+int getc_unlocked(FILE *stream)
+ /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/
+ /*@modifies *stream, fileSystem, errno@*/ ;
-/*@-bufferoverflowhigh@*/
-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@*/ ;
-
-extern int getw (FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */
-
-extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ;
-
-extern void perror (/*@null@*/ char *s)
- /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
-
-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
-
- extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream, errno;@*/
- /*drl added errno 09-18-001 */ ;
-
- extern int putchar (int /*@alt char@*/ c)
- /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
- /*drl added errno 09-18-001 */ ;
-
- extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream, errno;@*/
- /*Drl added 09-19-001 */ ;
-
- extern int putchar_unlocked (int /*@alt char@*/ c)
- /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
- /*Drl added 09-19-001 */ ;
-
- 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@*/ /*@out@*/ char *buf)
- /*@modifies fileSystem, *stream, *buf@*/
- // *@requires maxSet(buf) >= (BUFSIZ - 1) @*/
- ;
-
- extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ 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@*/
-
- /*@requires maxSet(s) >= (n - 1) @*/
- ;
-
- # else
+ /*@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) @*/
+ ;
+
+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 */
+ ;
- extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/
- /*drl added errno 09-19-001 */
- ;
+/*@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) @*/ ;
-
-int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
- /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
- /*@modifies str@*/ ;
+ // *@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."*/
+ ;
-extern char *optarg;
-extern int opterr;
-extern int optind; /*(LEGACY)*/
-extern int optopt;
andersk / splint.git / blobdiff