2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
10 # define INPUTSTREAM_H
12 /*@constant int STUBMAXRECORDSIZE; @*/
13 # define STUBMAXRECORDSIZE 800
15 struct s_inputStream {
17 /*@open@*/ /*@dependent@*/ /*@null@*/ FILE *file;
18 char buffer[STUBMAXRECORDSIZE+1];
21 /*@dependent@*/ /*@null@*/ char *curLine;
22 bool echo, fromString;
23 /*@owned@*/ cstring stringSource;
24 /*@dependent@*/ cstring stringSourceTail;
27 /* in forwardTypes.h: abst_typedef null struct _inputStream *inputStream; */
29 extern /*@falsenull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
30 extern /*@truenull@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
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)
37 extern void inputStream_free (/*@null@*/ /*@only@*/ inputStream p_s);
38 extern bool inputStream_close (inputStream p_s)
39 /*@modifies p_s, fileSystem@*/ ;
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)
46 extern int inputStream_nextChar (inputStream p_s) /*@modifies p_s@*/ ;
47 /* Returns int for EOF */
49 extern int inputStream_peekChar (inputStream p_s) /*@modifies p_s@*/ ;
50 /* Returns int for EOF */
52 extern int inputStream_peekNChar (inputStream p_s, int p_n) /*@modifies p_s@*/ ;
53 /* Returns int for EOF */
55 extern bool inputStream_open (inputStream p_s) /*@modifies p_s, fileSystem@*/ ;
56 extern bool inputStream_getPath (cstring p_path, inputStream p_s)
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) /*@*/ ;
65 # error "Multiple include"