src/Headers/inputStream.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** inputStream.h
   7 */
   8
   9 # ifndef INPUTSTREAM_H
  10 # define INPUTSTREAM_H
  11
  12 /*@constant int STUBMAXRECORDSIZE; @*/
  13 # define STUBMAXRECORDSIZE 800
  14
  15 struct s_inputStream {
  16   cstring name;
  17   /*:open:*/ /*@dependent@*/ /*@null@*/ FILE *file;
  18   char buffer[STUBMAXRECORDSIZE+1];
  19   int lineNo;
  20   size_t charNo;
  21   /*@dependent@*/ /*@null@*/ char *curLine;
  22   bool echo, fromString;
  23   /*@owned@*/ cstring  stringSource;
  24   /*@dependent@*/ cstring stringSourceTail;
  25 } ;
  26
  27 /* in forwardTypes.h: abst_typedef null struct _inputStream *inputStream; */
  28
  29 extern /*@falsewhennull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
  30 extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
  31
  32 /*@constant null inputStream inputStream_undefined; @*/
  33 # define inputStream_undefined      ((inputStream) NULL)
  34 # define inputStream_isDefined(f)   ((f) != inputStream_undefined)
  35 # define inputStream_isUndefined(f) ((f) == inputStream_undefined)
  36
  37 extern void inputStream_free (/*@null@*/ /*@only@*/ inputStream p_s);
  38 extern bool inputStream_close (inputStream p_s)
  39    /*@modifies p_s, fileSystem@*/ ;
  40 extern inputStream
  41   inputStream_create (/*@only@*/ cstring p_name, cstring p_suffix, bool p_echo) /*@*/ ;
  42 extern inputStream inputStream_fromString (cstring p_name, cstring p_str) /*@*/ ;
  43 extern /*@dependent@*/ /*@null@*/ char *inputStream_nextLine(inputStream p_s)
  44    /*@modifies p_s@*/ ;
  45
  46 extern int inputStream_nextChar (inputStream p_s) /*@modifies p_s@*/ ;
  47     /* Returns int for EOF */
  48
  49 extern int inputStream_peekChar (inputStream p_s) /*@modifies p_s@*/ ;
  50     /* Returns int for EOF */
  51
  52 extern int inputStream_peekNChar (inputStream p_s, int p_n) /*@modifies p_s@*/ ;
  53     /* Returns int for EOF */
  54
  55 extern bool inputStream_open (inputStream p_s) /*@modifies p_s, fileSystem@*/ ;
  56 extern bool inputStream_getPath (cstring p_path, inputStream p_s)
  57    /*@modifies p_s@*/ ;
  58
  59 extern /*@observer@*/ cstring inputStream_fileName (inputStream p_s) /*@*/ ;
  60 extern bool inputStream_isOpen (/*@sef@*/ inputStream p_s) /*@*/ ;
  61 extern int inputStream_thisLineNumber(inputStream p_s) /*@*/ ;
  62 extern /*:open:*/ /*@exposed@*/ FILE *inputStream_getFile (inputStream p_s) /*@*/ ;
  63
  64 # else
  65 # error "Multiple include"
  66 # endif
  67
  68
  69
  70
  71