lib/stdio.h

   1
   2 /*stuff from the unix specification*/
   3
   4 /*things from stdio.h */
   5 extern void clearerr (FILE *stream) /*@modifies *stream@*/ ;
   6
   7 extern char * ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
   8      /*@modifies *s @*/
   9      //     *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0 */
  10
  11        /*DRL 9-11-001 I've modified the definition in ansi.h to remove modifies SystemState and I've added a requires and ensures*/ ;
  12
  13       /*check returns*/
  14
  15             /* cuserid is in the 1988 version of POSIX but removed in 1990 */
  16          extern char *
  17  cuserid (/*@null@*/ /*@out@*/ char *s)
  18          /*@modifies *s@*/
  19      // *@requires maxSet(s) >= ( L_ctermid - 1) @*/ *@ensures maxRead(s) <= ( L_ctermid - 1) /\ maxRead(s) >= 0  /\ maxRead(result) <= ( L_ctermid - 1) /\ maxRead(result) >= 0 @*/
  20       ;
  21
  22       extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
  23
  24  extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
  25     /*@modifies errno, fileSystem@*/;
  26
  27  extern int feof (FILE *stream) /*@modifies errno@*/ ;
  28  extern int ferror (FILE *stream) /*@modifies errno@*/ ;
  29  extern int fflush (/*@null@*/ FILE *stream)
  30     /*@modifies *stream, errno, fileSystem;@*/ ;
  31
  32  extern int fgetc (FILE *stream)
  33   /*@modifies fileSystem, *stream, errno@*/ ;
  34
  35   extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
  36       /*@modifies *pos, errno@*/ /*@requires maxSet(pos) >= 0@*/
  37       /*@ensures maxRead(pos) >= 0 @*/;
  38
  39       extern /*@null@*/ char *
  40    fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
  41      /*@modifies fileSystem, *s, *stream, errno@*/
  42      /*@requires MaxSet(s) >= (n -1); @*/
  43       /*@ensures MaxRead(s) <= (n -1) /\ MaxRead(s) >= 0; @*/ ;
  44
  45  extern int fileno (FILE *fp) /*@modifies errno@*/;
  46
  47  extern void flockfile (FILE *file) /*@modifies *file, fileSystem@*/ ;
  48
  49      extern FILE * fopen (char *filename, char *mode)  /*@modifies errno, fileSystem;@*/ ;
  50
  51  # ifdef STRICT
  52  /*@printflike@*/
  53  extern int fprintf (FILE *stream, char *format, ...)
  54     /*@modifies fileSystem, *stream, errno@*/ ;
  55  # else
  56  /*@printflike@*/
  57  extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
  58     /*@modifies fileSystem, *stream, errno@*/ ;
  59  # endif
  60
  61     extern int fputc (int /*@alt char@*/ c, FILE *stream)
  62   /*@modifies fileSystem, *stream, errno@*/ ;
  63
  64  extern int fputs (char *s, FILE *stream)
  65   /*@modifies fileSystem, *stream, errno@*/ ;
  66  extern size_t
  67    fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
  68    /*@modifies fileSystem, *ptr, *stream, errno@*/
  69    /*requires maxSet(ptr) >= (size - 1) @*/ /*@ensures maxRead(ptr) == (size - 1) @*/
  70       ;
  71    extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
  72   /*@modifies *stream, fileSystem, errno@*/ ;
  73
  74   /*@scanflike@*/
  75  extern int fscanf (FILE *stream, char *format, ...)
  76     /*@modifies fileSystem, *stream, errno@*/ ;
  77  extern int fseek (FILE *stream, long int offset, int whence)
  78    /*@modifies fileSystem, *stream, errno@*/ ;
  79
  80   extern int fseeko (FILE *stream, off_t offset, int whence)
  81    /*@modifies fileSystem, *stream, errno@*/ ;
  82
  83  extern int fsetpos (FILE *stream, fpos_t *pos)
  84   /*@modifies fileSystem, *stream, errno@*/ ;
  85
  86   extern long int ftell(FILE *stream) /*@modifies errno@*/ ;
  87
  88   extern off_t ftello(FILE *stream) /*@modifies errno@*/ ;
  89
  90   extern void ftrylockfile (FILE *file) /*@modifies *file, fileSystem@*/ ;
  91
  92  extern void funlockfile (FILE *file) /*@modifies *file, fileSystem;@*/ ;
  93
  94  extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
  95   /*@modifies fileSystem, *stream, errno@*/
  96       /*@requires maxRead(ptr) >= size @*/;
  97
  98  extern int getc (/*@sef@*/ FILE *stream)
  99       /*@modifies fileSystem, *stream, errno@*/ ; /*drl added errno */
 100
 101  extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*drl added errno */
 102
 103  extern int  getc_unlocked (/*@sef@*/ FILE *stream)
 104       /*@modifies fileSystem, *stream, errno@*/ ; /*Drl added 09-18-001 */
 105
 106  extern int getchar_unlocked (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*Drl added 09-18-001 */
 107
 108  /*@unchecked@*/ extern char *optarg;
 109  /*@unchecked@*/ extern int optind;
 110  /*@unchecked@*/ extern int optopt;
 111  /*@unchecked@*/ extern int opterr;
 112  /*@unchecked@*/ extern int optreset;
 113
 114 extern int getopt (int argc, char * const *argv, const char *optstring)
 115      /*@globals optarg, optind, optopt, opterr, optreset@*/
 116      /*@modifies optarg, optind, optopt@*/
 117      /*@requires maxRead(argv) >= (argc - 1) @*/
 118      ;
 119
 120 /*@-bufferoverflowhigh@*/
 121 extern /*@null@*/ char *gets (/*@out@*/ char *s)
 122      /*@warn bufferoverflowhigh
 123        "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead"@*/
 124      /*@globals stdin@*/
 125      /*@modifies fileSystem, *s, *stdin, errno@*/ ;
 126
 127 extern int getw (FILE *stream)
 128      /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */
 129
 130 extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ;
 131
 132 extern void perror (/*@null@*/ char *s)
 133    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
 134
 135 extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype)
 136     /*@modifies fileSystem, errno@*/ ;
 137
 138  # ifdef STRICT
 139  /*@printflike@*/
 140  extern int printf (char *format, ...)
 141     /*@globals stdout@*/
 142     /*@modifies fileSystem, *stdout@*/ ;
 143  # else
 144  /*@printflike@*/
 145  extern int /*@alt void@*/ printf (char *format, ...)
 146     /*@globals stdout@*/
 147     /*@modifies fileSystem, *stdout@*/ ;
 148  # endif
 149
 150  extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 151    /*@modifies fileSystem, *stream, errno;@*/
 152       /*drl added errno 09-18-001 */ ;
 153
 154       extern int putchar (int /*@alt char@*/ c)
 155       /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 156       /*drl added errno 09-18-001 */ ;
 157
 158       extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 159    /*@modifies fileSystem, *stream, errno;@*/
 160   /*Drl added 09-19-001 */ ;
 161
 162       extern int putchar_unlocked (int /*@alt char@*/ c)
 163       /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 164     /*Drl added 09-19-001 */ ;
 165
 166     extern int puts (const char *s)
 167    /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 168     /*drl added errno 09-19-001 */ ;
 169
 170
 171    extern int putw(int w, FILE *stream)
 172   /*@modifies fileSystem, *stream, errno@*/
 173       /*Drl added 09-19-001 */ /*legacy*/ ;
 174
 175     extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
 176
 177     extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/
 178   ;
 179
 180  extern void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/
 181   /*drl added errno AND fileSystem 09-19-001 */ ;
 182
 183  /*@scanflike@*/
 184  extern int scanf(char *format, ...)
 185    /*@globals stdin@*/
 186   /*@modifies fileSystem, *stdin, errno@*/
 187   /*drl added errno 09-19-001 */ ;
 188
 189   extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
 190     /*@modifies fileSystem, *stream, *buf@*/
 191      // *@requires maxSet(buf) >= (BUFSIZ - 1) @*/
 192      ;
 193
 194      extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
 195             int mode, size_t size)
 196       /*@modifies fileSystem, *stream, *buf@*/  /*@requires maxSet(buf) >= (size - 1) @*/ ;
 197
 198  # ifdef STRICT
 199  /*@printflike@*/
 200  extern int snprintf (/*@out@*/ char *s,  size_t n, char *format, ...)
 201     /*@modifies *s@*/
 202
 203       /*@requires maxSet(s) >= (n - 1) @*/
 204       ;
 205
 206  # else
 207
 208     /*@printflike@*/
 209  extern int /*@alt void@*/ snprintf (/*@out@*/ char *s, size_t n, char *format, ...)
 210     /*@modifies *s@*/
 211      /*@requires maxSet(s) >= (n - 1) @*/
 212       ;
 213  # endif
 214
 215
 216  # ifdef STRICT
 217  /*@printflike@*/
 218  extern int sprintf (/*@out@*/ char *s, char *format, ...)
 219     /*@modifies *s@*/ ;
 220  # else
 221
 222     /*@printflike@*/
 223  extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
 224     /*@modifies *s@*/ ;
 225
 226  # endif
 227
 228     /*@scanflike@*/
 229     int sscanf (/*@out@*/ char *s, char *format, ...)
 230     /* modifies extra arguments */ /*@modifies errno@*/
 231   /*drl added errno 09-19-001 */ ;
 232
 233
 234  extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx)
 235     /*@modifies internalState, errno@*/
 236       /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/
 237       /*warn that "Between the time a pathname is created and the file is opened, it is possible
 238       for some other process to create a file with the same name. Applications may find tmpfile()
 239       more useful. " */
 240
 241       /*drl added errno 09-19-001 */
 242
 243       ;
 244
 245
 246  extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/
 247  /*drl added errno 09-19-001 */
 248       ;
 249
 250  extern /*@observer@*/ char *
 251  tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
 252    /*@modifies *s, internalState @*/
 253      //      *@requires maxSet(s) >= (L_tmpnam - 1) @*
 254       /*warn Between the time a pathname is created and the file is opened, it is possible for some other
 255         process to create a file with the same name. Applications may find tmpfile() more useful. */
 256       ;
 257
 258  extern int ungetc (int /*@alt char@*/ c, FILE *stream)
 259   /*@modifies fileSystem, *stream @*/
 260
 261       /*drl REMOVED errno 09-19-001*/
 262       ;
 263
 264       int vfprintf (FILE *stream, char *format, va_list arg)
 265     /*@modifies fileSystem, *stream, arg, errno@*/ ;
 266
 267  int  vprintf (const char *format, va_list arg)
 268     /*@globals stdout@*/
 269     /*@modifies fileSystem, *stdout@*/ ;
 270
 271  int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
 272      /*@modifies str@*/
 273      /*@requires maxSet(str) >= (size - 1) @*/ ;
 274
 275 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
 276      /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
 277      /*@modifies str@*/  ;
 278
 279 extern char  *optarg;
 280 extern int    opterr;
 281 extern int    optind;  /*(LEGACY)*/
 282 extern int    optopt;
 283