lib/stdio.h

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