2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
3 ** See ../LICENSE for license information.
12 /*@constant int STUBMAXRECORDSIZE; @*/
13 # define STUBMAXRECORDSIZE 800
17 /*@dependent@*/ /*@null@*/ FILE *file;
18 char buffer[STUBMAXRECORDSIZE+1];
20 bool echo, fromString;
21 /*@owned@*/ /*@null@*/ char *stringSource;
22 /*@null@*/ /*@dependent@*/ char *stringSourceTail;
23 } tsource; /* renamed from "source" to avoid cc parse bug on lex.yy.c */
25 extern void tsource_free (/*@null@*/ /*@only@*/ tsource *p_s);
26 extern bool tsource_close (tsource *p_s)
27 /*@modifies *p_s, fileSystem@*/ ;
29 tsource_create (/*@temp@*/ char *p_name, char *p_suffix, bool p_echo) /*@*/ ;
30 extern tsource *tsource_fromString (char *p_name, char *p_str) /*@*/ ;
31 extern /*@dependent@*/ /*@null@*/ char *tsource_nextLine(tsource *p_s)
33 extern bool tsource_open (tsource *p_s) /*@modifies p_s, fileSystem@*/ ;
34 extern bool tsource_getPath (char *p_path, tsource *p_s)
38 extern /*@observer@*/ char *tsource_fileName (tsource *p_s) /*@*/ ;
39 # define tsource_fileName(pS) ((pS)->name)
41 extern bool tsource_isOpen (/*@sef@*/ tsource *p_s) /*@*/ ;
42 # define tsource_isOpen(pS) ((pS)->file != 0 || (pS)->fromString)
44 extern unsigned int tsource_thisLineNumber(tsource *p_s) /*@*/ ;
45 # define tsource_thisLineNumber(pS) ((pS)->lineNo)
47 extern char *specFullName (char *p_specfile, /*@out@*/ char **p_inpath)
48 /*@modifies *p_inpath@*/ ;
53 # error "Multiple include"