src/Headers/llmain.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 # ifndef LLMAIN_H
   7 # define LLMAIN_H
   8
   9 extern int main (int p_argc, char *p_argv[])
  10   /*@globals killed undef g_currentloc,
  11              killed undef g_currentSpec,
  12              killed undef g_currentSpecName,
  13              killed undef g_currentloc,
  14              killed undef yyin,
  15                     undef g_warningstream;
  16    @*/
  17   /*@modifies g_currentloc, g_currentSpec, g_currentSpecName,
  18               yyin, internalState, fileSystem;
  19   @*/
  20   ;
  21
  22 extern /*@noreturn@*/ void llexit (int p_status);
  23 extern void showHerald (void);
  24
  25 /*@-redecl@*/ /*@-incondefs@*/
  26 /*@-declundef@*/
  27 extern int yyparse (void);
  28 extern void yyrestart (/*@dependent@*/ FILE *);
  29
  30 extern int ylparse (void);
  31 extern int lslparse (void);
  32
  33 extern /*:open:*/ /*@dependent@*/ FILE *yyin;
  34 /*@=incondefs@*/ /*@=redecl@*/
  35 /*@=declundef@*/
  36
  37 # endif
  38
  39