]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 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 { | |
6fcd0b1e | 16 | /*@only@*/ cstring name; |
15b3d2b2 | 17 | /*:open:*/ /*@dependent@*/ /*@null@*/ FILE *file; |
28bf4b0b | 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 | ||
0e41eb0e | 29 | extern /*@falsewhennull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ; |
30 | extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ; | |
28bf4b0b | 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@*/ ; | |
6fcd0b1e | 40 | |
41 | extern /*@only@*/ inputStream | |
28bf4b0b | 42 | inputStream_create (/*@only@*/ cstring p_name, cstring p_suffix, bool p_echo) /*@*/ ; |
6fcd0b1e | 43 | |
28bf4b0b | 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) /*@*/ ; | |
15b3d2b2 | 64 | extern /*:open:*/ /*@exposed@*/ FILE *inputStream_getFile (inputStream p_s) /*@*/ ; |
28bf4b0b | 65 | |
66 | # else | |
67 | # error "Multiple include" | |
68 | # endif | |
69 | ||
70 | ||
71 | ||
72 | ||
73 |