src/Headers/source.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** source.h
   7 */
   8
   9 # ifndef TSOURCE_H
  10 # define TSOURCE_H
  11
  12 /*@constant int STUBMAXRECORDSIZE; @*/
  13 # define STUBMAXRECORDSIZE 800
  14
  15 typedef struct {
  16     char        *name;
  17     /*@dependent@*/ /*@null@*/ FILE *file;
  18     char         buffer[STUBMAXRECORDSIZE+1];
  19     unsigned int lineNo;
  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 */
  24
  25 extern void tsource_free (/*@null@*/ /*@only@*/ tsource *p_s);
  26 extern bool tsource_close (tsource *p_s)
  27    /*@modifies *p_s, fileSystem@*/ ;
  28 extern tsource *
  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)
  32    /*@modifies *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)
  35    /*@modifies *p_s@*/ ;
  36
  37 # ifndef NOLCL
  38 extern /*@observer@*/ char *tsource_fileName (tsource *p_s) /*@*/ ;
  39 # define tsource_fileName(pS) ((pS)->name)
  40
  41 extern bool tsource_isOpen (/*@sef@*/ tsource *p_s) /*@*/ ;
  42 # define tsource_isOpen(pS)  ((pS)->file != 0 || (pS)->fromString)
  43
  44 extern unsigned int tsource_thisLineNumber(tsource *p_s) /*@*/ ;
  45 # define tsource_thisLineNumber(pS)     ((pS)->lineNo)
  46
  47 extern char *specFullName (char *p_specfile, /*@out@*/ char **p_inpath)
  48    /*@modifies *p_inpath@*/ ;
  49
  50 # endif
  51
  52 # else
  53 # error "Multiple include"
  54 # endif
  55
  56
  57
  58
  59