Updated copyrights

[splint.git] / src / Headers / llmain.h

/*
** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
**
*/
# ifndef LLMAIN_H
# define LLMAIN_H

extern int main (int p_argc, char *p_argv[])
  /*@globals killed undef g_currentloc,
	     killed undef g_currentSpec,
	     killed undef g_currentSpecName,
	     killed undef g_currentloc,
	     killed undef yyin,
                    undef g_warningstream;
   @*/
  /*@modifies g_currentloc, g_currentSpec, g_currentSpecName,
	      yyin, internalState, fileSystem; 
  @*/ 
  ;

extern /*@noreturn@*/ void llexit (int p_status);      
extern void showHerald (void);

/*@-redecl@*/ /*@-incondefs@*/
/*@-declundef@*/
extern int yyparse (void);
extern void yyrestart (/*@dependent@*/ FILE *);

extern int ylparse (void);
extern int lslparse (void);

extern /*:open:*/ /*@dependent@*/ FILE *yyin;
/*@=incondefs@*/ /*@=redecl@*/
/*@=declundef@*/

# endif