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
 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@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
 125
 126  extern int getw (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; /*drl added 09-18-001 */ /*legacy */
 127
 128
 129  extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ;
 130
 131  extern void perror (/*@null@*/ char *s)
 132    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
 133
 134  extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype)
 135     /*@modifies fileSystem, errno@*/ ;
 136
 137  # ifdef STRICT
 138  /*@printflike@*/
 139  extern int printf (char *format, ...)
 140     /*@globals stdout@*/
 141     /*@modifies fileSystem, *stdout@*/ ;
 142  # else
 143  /*@printflike@*/
 144  extern int /*@alt void@*/ printf (char *format, ...)
 145     /*@globals stdout@*/
 146     /*@modifies fileSystem, *stdout@*/ ;
 147  # endif
 148
 149  extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 150    /*@modifies fileSystem, *stream, errno;@*/
 151       /*drl added errno 09-18-001 */ ;
 152
 153       extern int putchar (int /*@alt char@*/ c)
 154       /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 155       /*drl added errno 09-18-001 */ ;
 156
 157       extern int putc_unlocked (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 158    /*@modifies fileSystem, *stream, errno;@*/
 159   /*Drl added 09-19-001 */ ;
 160
 161       extern int putchar_unlocked (int /*@alt char@*/ c)
 162       /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 163     /*Drl added 09-19-001 */ ;
 164
 165     extern int puts (const char *s)
 166    /*@globals stdout@*/ /*@modifies fileSystem, *stdout, errno@*/
 167     /*drl added errno 09-19-001 */ ;
 168
 169
 170    extern int putw(int w, FILE *stream)
 171   /*@modifies fileSystem, *stream, errno@*/
 172       /*Drl added 09-19-001 */ /*legacy*/ ;
 173
 174     extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
 175
 176     extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/
 177   ;
 178
 179  extern void rewind (FILE *stream) /*@modifies *stream, fileSystem, errno@*/
 180   /*drl added errno AND fileSystem 09-19-001 */ ;
 181
 182  /*@scanflike@*/
 183  extern int scanf(char *format, ...)
 184    /*@globals stdin@*/
 185   /*@modifies fileSystem, *stdin, errno@*/
 186   /*drl added errno 09-19-001 */ ;
 187
 188   extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf)
 189     /*@modifies fileSystem, *stream, *buf@*/
 190      // /*@requires maxSet(buf) >= (BUFSIZ - 1) @*/
 191      ;
 192
 193     extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
 194             int mode, size_t size)
 195       /*@modifies fileSystem, *stream, *buf@*/  /*@requires maxSet(buf) >= (size - 1) @*/ ;
 196
 197  # ifdef STRICT
 198  /*@printflike@*/
 199  extern int snprintf (/*@out@*/ char *s,  size_t n, char *format, ...)
 200     /*@modifies *s@*/
 201
 202       /*@requires maxSet(s) >= (n - 1) @*/
 203       ;
 204
 205  # else
 206
 207     /*@printflike@*/
 208  extern int /*@alt void@*/ snprintf (/*@out@*/ char *s, size_t n, char *format, ...)
 209     /*@modifies *s@*/
 210      /*@requires maxSet(s) >= (n - 1) @*/
 211       ;
 212  # endif
 213
 214
 215  # ifdef STRICT
 216  /*@printflike@*/
 217  extern int sprintf (/*@out@*/ char *s, char *format, ...)
 218     /*@modifies *s@*/ ;
 219  # else
 220
 221     /*@printflike@*/
 222  extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
 223     /*@modifies *s@*/ ;
 224
 225  # endif
 226
 227     /*@scanflike@*/
 228     int sscanf (/*@out@*/ char *s, char *format, ...)
 229     /* modifies extra arguments */ /*@modifies errno@*/
 230   /*drl added errno 09-19-001 */ ;
 231
 232
 233  extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx)
 234     /*@modifies internalState, errno@*/
 235       /*@ensures maxSet(result) >= 0 /\ maxRead(result) >= 0 @*/
 236       /*warn that "Between the time a pathname is created and the file is opened, it is possible
 237       for some other process to create a file with the same name. Applications may find tmpfile()
 238       more useful. " */
 239
 240       /*drl added errno 09-19-001 */
 241
 242       ;
 243
 244
 245  extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem, errno@*/
 246  /*drl added errno 09-19-001 */
 247       ;
 248
 249  extern /*@observer@*/ char *
 250  tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
 251    /*@modifies *s, internalState @*/
 252      //      /*@requires maxSet(s) >= (L_tmpnam - 1) @*/
 253       /*warn Between the time a pathname is created and the file is opened, it is possible for some other
 254         process to create a file with the same name. Applications may find tmpfile() more useful. */
 255       ;
 256
 257  extern int ungetc (int /*@alt char@*/ c, FILE *stream)
 258   /*@modifies fileSystem, *stream @*/
 259
 260       /*drl REMOVED errno 09-19-001*/
 261       ;
 262
 263       int vfprintf (FILE *stream, char *format, va_list arg)
 264     /*@modifies fileSystem, *stream, arg, errno@*/ ;
 265
 266  int  vprintf (const char *format, va_list arg)
 267     /*@globals stdout@*/
 268     /*@modifies fileSystem, *stdout@*/ ;
 269
 270  int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
 271      /*@modifies str@*/
 272      /*@requires maxSet(str) >= (size - 1) @*/ ;
 273
 274 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
 275      /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
 276      /*@modifies str@*/  ;
 277
 278 extern char  *optarg;
 279 extern int    opterr;
 280 extern int    optind;  /*(LEGACY)*/
 281 extern int    optopt;
 282