]>
Commit | Line | Data |
---|---|---|
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 |