src/Headers/inputStream.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   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   /*@only@*/ 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
  41 extern /*@only@*/ inputStream
  42   inputStream_create (/*@only@*/ cstring p_name, cstring p_suffix, bool p_echo) /*@*/ ;
  43
  44 extern inputStream inputStream_fromString (cstring p_name, cstring p_str) /*@*/ ;
  45 extern /*@dependent@*/ /*@null@*/ char *inputStream_nextLine(inputStream p_s)
  46    /*@modifies p_s@*/ ;
  47
  48 extern int inputStream_nextChar (inputStream p_s) /*@modifies p_s@*/ ;
  49     /* Returns int for EOF */
  50
  51 extern int inputStream_peekChar (inputStream p_s) /*@modifies p_s@*/ ;
  52     /* Returns int for EOF */
  53
  54 extern int inputStream_peekNChar (inputStream p_s, int p_n) /*@modifies p_s@*/ ;
  55     /* Returns int for EOF */
  56
  57 extern bool inputStream_open (inputStream p_s) /*@modifies p_s, fileSystem@*/ ;
  58 extern bool inputStream_getPath (cstring p_path, inputStream p_s)
  59    /*@modifies p_s@*/ ;
  60
  61 extern /*@observer@*/ cstring inputStream_fileName (inputStream p_s) /*@*/ ;
  62 extern bool inputStream_isOpen (/*@sef@*/ inputStream p_s) /*@*/ ;
  63 extern int inputStream_thisLineNumber(inputStream p_s) /*@*/ ;
  64 extern /*:open:*/ /*@exposed@*/ FILE *inputStream_getFile (inputStream p_s) /*@*/ ;
  65
  66 # else
  67 # error "Multiple include"
  68 # endif
  69
  70
  71
  72
  73