]>
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 { | |
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 /*@falsenull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ; | |
30 | extern /*@truenull@*/ 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 |