]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
c0de361f | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. |
885824d3 | 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[]) | |
885824d3 | 10 | /*@globals killed undef g_currentloc, |
885824d3 | 11 | killed undef g_currentSpec, |
12 | killed undef g_currentSpecName, | |
13 | killed undef g_currentloc, | |
14 | killed undef yyin, | |
80489f0a | 15 | undef g_warningstream; |
885824d3 | 16 | @*/ |
140c27a8 | 17 | /*@modifies g_currentloc, g_currentSpec, g_currentSpecName, |
885824d3 | 18 | yyin, internalState, fileSystem; |
19 | @*/ | |
885824d3 | 20 | ; |
21 | ||
27c9e640 | 22 | extern /*@noreturn@*/ void llexit (int p_status); |
885824d3 | 23 | extern void showHerald (void); |
24 | ||
abb1cb43 | 25 | /*@-redecl@*/ /*@-incondefs@*/ |
a956d444 | 26 | /*@-declundef@*/ |
885824d3 | 27 | extern int yyparse (void); |
abb1cb43 | 28 | extern void yyrestart (/*@dependent@*/ FILE *); |
885824d3 | 29 | |
885824d3 | 30 | extern int ylparse (void); |
31 | extern int lslparse (void); | |
885824d3 | 32 | |
15b3d2b2 | 33 | extern /*:open:*/ /*@dependent@*/ FILE *yyin; |
885824d3 | 34 | /*@=incondefs@*/ /*@=redecl@*/ |
a956d444 | 35 | /*@=declundef@*/ |
885824d3 | 36 | |
37 | # endif | |
38 | ||
39 |