2 ** Inserted at beginning of c files generated by bison
3 ** REMEMBER: Change bison.reset too.
42 /*@-unqualifiedtrans@*/
45 /* < end of bison.head > */
49 ltoken ltok; /* a leaf is also an ltoken */
52 /*@only@*/ ltokenList ltokenList;
53 /*@only@*/ abstDeclaratorNode abstDecl;
54 /*@only@*/ declaratorNode declare;
55 /*@only@*/ declaratorNodeList declarelist;
56 /*@only@*/ typeExpr typeexpr;
57 /*@only@*/ arrayQualNode array;
58 /*@only@*/ quantifierNode quantifier;
59 /*@only@*/ quantifierNodeList quantifiers;
60 /*@only@*/ varNode var;
61 /*@only@*/ varNodeList vars;
62 /*@only@*/ storeRefNode storeref;
63 /*@only@*/ storeRefNodeList storereflist;
64 /*@only@*/ termNode term;
65 /*@only@*/ termNodeList termlist;
66 /*@only@*/ programNode program;
67 /*@only@*/ stmtNode stmt;
68 /*@only@*/ claimNode claim;
69 /*@only@*/ typeNode type;
70 /*@only@*/ iterNode iter;
71 /*@only@*/ fcnNode fcn;
72 /*@only@*/ fcnNodeList fcns;
73 /*@only@*/ letDeclNode letdecl;
74 /*@only@*/ letDeclNodeList letdecls;
75 /*@only@*/ lclPredicateNode lclpredicate;
76 /*@only@*/ modifyNode modify;
77 /*@only@*/ paramNode param;
78 /*@only@*/ paramNodeList paramlist;
79 /*@only@*/ declaratorInvNodeList declaratorinvs;
80 /*@only@*/ declaratorInvNode declaratorinv;
81 /*@only@*/ abstBodyNode abstbody;
82 /*@only@*/ abstractNode abstract;
83 /*@only@*/ exposedNode exposed;
84 /* taggedUnionNode taggedunion; */
85 /*@only@*/ globalList globals;
86 /*@only@*/ constDeclarationNode constdeclaration;
87 /*@only@*/ varDeclarationNode vardeclaration;
88 /*@only@*/ varDeclarationNodeList vardeclarationlist;
89 /*@only@*/ initDeclNodeList initdecls;
90 /*@only@*/ initDeclNode initdecl;
91 /*@only@*/ stDeclNodeList structdecls;
92 /*@only@*/ stDeclNode structdecl;
93 /*@only@*/ strOrUnionNode structorunion;
94 /*@only@*/ enumSpecNode enumspec;
95 /*@only@*/ lclTypeSpecNode lcltypespec;
96 /*@only@*/ typeNameNode typname;
97 /*@only@*/ opFormNode opform;
98 /*@only@*/ sigNode signature;
99 /*@only@*/ nameNode name;
100 /*@only@*/ typeNameNodeList namelist;
101 /*@only@*/ replaceNode replace;
102 /*@only@*/ replaceNodeList replacelist;
103 /*@only@*/ renamingNode renaming;
104 /*@only@*/ traitRefNode traitref;
105 /*@only@*/ traitRefNodeList traitreflist;
106 /*@only@*/ importNode import;
107 /*@only@*/ importNodeList importlist;
108 /*@only@*/ interfaceNode iface;
109 /*@only@*/ interfaceNodeList interfacelist;
110 /*@only@*/ CTypesNode ctypes;
113 #define PREFIX_OP 259
114 #define POSTFIX_OP 260
115 #define LLT_MULOP 261
117 #define LLT_VERTICALBAR 263
118 #define ITERATION_OP 264
120 #define LLT_LBRACKET 266
121 #define selectSym 267
122 #define LLT_IF_THEN_ELSE 268
123 #define logicalOp 269
125 #define equationSym 271
126 #define commentSym 272
127 #define LLT_WHITESPACE 273
129 #define LLT_TYPEDEF_NAME 275
130 #define quantifierSym 276
136 #define markerSym 282
140 #define LLT_COLON 286
141 #define LLT_COMMA 287
142 #define LLT_EQUALS 288
143 #define LLT_LBRACE 289
144 #define LLT_RBRACE 290
145 #define LLT_RBRACKET 291
147 #define LLT_QUOTE 293
149 #define LLT_CCHAR 295
150 #define LLT_CFLOAT 296
151 #define LLT_CINTEGER 297
152 #define LLT_LCSTRING 298
154 #define LLT_ANYTHING 300
157 #define LLT_CLAIMS 303
158 #define LLT_CHECKS 304
159 #define LLT_CONSTANT 305
161 #define LLT_ENSURES 307
163 #define LLT_FRESH 309
165 #define LLT_IMMUTABLE 311
166 #define LLT_IMPORTS 312
167 #define LLT_CONSTRAINT 313
168 #define LLT_ISSUB 314
170 #define LLT_MODIFIES 316
171 #define LLT_MUTABLE 317
172 #define LLT_NOTHING 318
173 #define LLT_INTERNAL 319
174 #define LLT_FILESYS 320
179 #define LLT_PARTIAL 325
180 #define LLT_OWNED 326
181 #define LLT_DEPENDENT 327
185 #define LLT_SHARED 331
186 #define LLT_UNIQUE 332
187 #define LLT_UNUSED 333
188 #define LLT_EXITS 334
189 #define LLT_MAYEXIT 335
190 #define LLT_NEVEREXIT 336
191 #define LLT_TRUEEXIT 337
192 #define LLT_FALSEEXIT 338
193 #define LLT_UNDEF 339
194 #define LLT_KILLED 340
195 #define LLT_CHECKMOD 341
196 #define LLT_CHECKED 342
197 #define LLT_UNCHECKED 343
198 #define LLT_CHECKEDSTRICT 344
199 #define LLT_TRUENULL 345
200 #define LLT_FALSENULL 346
201 #define LLT_LNULL 347
202 #define LLT_LNOTNULL 348
203 #define LLT_RETURNED 349
204 #define LLT_OBSERVER 350
205 #define LLT_EXPOSED 351
206 #define LLT_REFCOUNTED 352
208 #define LLT_RELNULL 354
209 #define LLT_RELDEF 355
210 #define LLT_KILLREF 356
211 #define LLT_NULLTERMINATED 357
212 #define LLT_TEMPREF 358
213 #define LLT_NEWREF 359
214 #define LLT_PRIVATE 360
215 #define LLT_REQUIRES 361
216 #define LLT_RESULT 362
217 #define LLT_SIZEOF 363
219 #define LLT_TAGGEDUNION 365
222 #define LLT_TYPEDEF 368
223 #define LLT_UNCHANGED 369
226 #define LLT_CONST 372
227 #define LLT_DOUBLE 373
229 #define LLT_FLOAT 375
232 #define LLT_YIELD 378
234 #define LLT_SHORT 380
235 #define LLT_SIGNED 381
236 #define LLT_UNKNOWN 382
237 #define LLT_STRUCT 383
238 #define LLT_TELIPSIS 384
239 #define LLT_UNION 385
240 #define LLT_UNSIGNED 386
242 #define LLT_VOLATILE 388
243 #define LLT_PRINTFLIKE 389
244 #define LLT_SCANFLIKE 390
245 #define LLT_MESSAGELIKE 391
248 extern YYSTYPE yllval;