3 ltoken ltok; /* a leaf is also an ltoken */
6 /*@only@*/ ltokenList ltokenList;
7 /*@only@*/ abstDeclaratorNode abstDecl;
8 /*@only@*/ declaratorNode declare;
9 /*@only@*/ declaratorNodeList declarelist;
10 /*@only@*/ typeExpr typeexpr;
11 /*@only@*/ arrayQualNode array;
12 /*@only@*/ quantifierNode quantifier;
13 /*@only@*/ quantifierNodeList quantifiers;
14 /*@only@*/ varNode var;
15 /*@only@*/ varNodeList vars;
16 /*@only@*/ storeRefNode storeref;
17 /*@only@*/ storeRefNodeList storereflist;
18 /*@only@*/ termNode term;
19 /*@only@*/ termNodeList termlist;
20 /*@only@*/ programNode program;
21 /*@only@*/ stmtNode stmt;
22 /*@only@*/ claimNode claim;
23 /*@only@*/ typeNode type;
24 /*@only@*/ iterNode iter;
25 /*@only@*/ fcnNode fcn;
26 /*@only@*/ fcnNodeList fcns;
27 /*@only@*/ letDeclNode letdecl;
28 /*@only@*/ letDeclNodeList letdecls;
29 /*@only@*/ lclPredicateNode lclpredicate;
30 /*@only@*/ modifyNode modify;
31 /*@only@*/ paramNode param;
32 /*@only@*/ paramNodeList paramlist;
33 /*@only@*/ declaratorInvNodeList declaratorinvs;
34 /*@only@*/ declaratorInvNode declaratorinv;
35 /*@only@*/ abstBodyNode abstbody;
36 /*@only@*/ abstractNode abstract;
37 /*@only@*/ exposedNode exposed;
38 /* taggedUnionNode taggedunion; */
39 /*@only@*/ globalList globals;
40 /*@only@*/ constDeclarationNode constdeclaration;
41 /*@only@*/ varDeclarationNode vardeclaration;
42 /*@only@*/ varDeclarationNodeList vardeclarationlist;
43 /*@only@*/ initDeclNodeList initdecls;
44 /*@only@*/ initDeclNode initdecl;
45 /*@only@*/ stDeclNodeList structdecls;
46 /*@only@*/ stDeclNode structdecl;
47 /*@only@*/ strOrUnionNode structorunion;
48 /*@only@*/ enumSpecNode enumspec;
49 /*@only@*/ lclTypeSpecNode lcltypespec;
50 /*@only@*/ typeNameNode typname;
51 /*@only@*/ opFormNode opform;
52 /*@only@*/ sigNode signature;
53 /*@only@*/ nameNode name;
54 /*@only@*/ typeNameNodeList namelist;
55 /*@only@*/ replaceNode replace;
56 /*@only@*/ replaceNodeList replacelist;
57 /*@only@*/ renamingNode renaming;
58 /*@only@*/ traitRefNode traitref;
59 /*@only@*/ traitRefNodeList traitreflist;
60 /*@only@*/ importNode import;
61 /*@only@*/ importNodeList importlist;
62 /*@only@*/ interfaceNode iface;
63 /*@only@*/ interfaceNodeList interfacelist;
64 /*@only@*/ CTypesNode ctypes;
68 #define POSTFIX_OP 260
71 #define LLT_VERTICALBAR 263
72 #define ITERATION_OP 264
74 #define LLT_LBRACKET 266
76 #define LLT_IF_THEN_ELSE 268
79 #define equationSym 271
80 #define commentSym 272
81 #define LLT_WHITESPACE 273
83 #define LLT_TYPEDEF_NAME 275
84 #define quantifierSym 276
96 #define LLT_EQUALS 288
97 #define LLT_LBRACE 289
98 #define LLT_RBRACE 290
99 #define LLT_RBRACKET 291
101 #define LLT_QUOTE 293
103 #define LLT_CCHAR 295
104 #define LLT_CFLOAT 296
105 #define LLT_CINTEGER 297
106 #define LLT_LCSTRING 298
108 #define LLT_ANYTHING 300
111 #define LLT_CLAIMS 303
112 #define LLT_CHECKS 304
113 #define LLT_CONSTANT 305
115 #define LLT_ENSURES 307
117 #define LLT_FRESH 309
119 #define LLT_IMMUTABLE 311
120 #define LLT_IMPORTS 312
121 #define LLT_CONSTRAINT 313
122 #define LLT_ISSUB 314
124 #define LLT_MODIFIES 316
125 #define LLT_MUTABLE 317
126 #define LLT_NOTHING 318
127 #define LLT_INTERNAL 319
128 #define LLT_FILESYS 320
133 #define LLT_PARTIAL 325
134 #define LLT_OWNED 326
135 #define LLT_DEPENDENT 327
139 #define LLT_SHARED 331
140 #define LLT_UNIQUE 332
141 #define LLT_UNUSED 333
142 #define LLT_EXITS 334
143 #define LLT_MAYEXIT 335
144 #define LLT_NEVEREXIT 336
145 #define LLT_TRUEEXIT 337
146 #define LLT_FALSEEXIT 338
147 #define LLT_UNDEF 339
148 #define LLT_KILLED 340
149 #define LLT_CHECKMOD 341
150 #define LLT_CHECKED 342
151 #define LLT_UNCHECKED 343
152 #define LLT_CHECKEDSTRICT 344
153 #define LLT_TRUENULL 345
154 #define LLT_FALSENULL 346
155 #define LLT_LNULL 347
156 #define LLT_LNOTNULL 348
157 #define LLT_RETURNED 349
158 #define LLT_OBSERVER 350
159 #define LLT_EXPOSED 351
160 #define LLT_REFCOUNTED 352
162 #define LLT_RELNULL 354
163 #define LLT_RELDEF 355
164 #define LLT_KILLREF 356
165 #define LLT_NULLTERMINATED 357
166 #define LLT_TEMPREF 358
167 #define LLT_NEWREF 359
168 #define LLT_PRIVATE 360
169 #define LLT_REQUIRES 361
170 #define LLT_RESULT 362
171 #define LLT_SIZEOF 363
173 #define LLT_TAGGEDUNION 365
176 #define LLT_TYPEDEF 368
177 #define LLT_UNCHANGED 369
180 #define LLT_CONST 372
181 #define LLT_DOUBLE 373
183 #define LLT_FLOAT 375
186 #define LLT_YIELD 378
188 #define LLT_SHORT 380
189 #define LLT_SIGNED 381
190 #define LLT_UNKNOWN 382
191 #define LLT_STRUCT 383
192 #define LLT_TELIPSIS 384
193 #define LLT_UNION 385
194 #define LLT_UNSIGNED 386
196 #define LLT_VOLATILE 388
197 #define LLT_PRINTFLIKE 389
198 #define LLT_SCANFLIKE 390
199 #define LLT_MESSAGELIKE 391
202 extern YYSTYPE yllval;