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 258
114 #define POSTFIX_OP 259
115 #define LLT_MULOP 260
117 #define LLT_VERTICALBAR 262
118 #define ITERATION_OP 263
120 #define LLT_LBRACKET 265
121 #define selectSym 266
122 #define LLT_IF_THEN_ELSE 267
123 #define logicalOp 268
125 #define equationSym 270
126 #define commentSym 271
127 #define LLT_WHITESPACE 272
129 #define LLT_TYPEDEF_NAME 274
130 #define quantifierSym 275
136 #define markerSym 281
140 #define LLT_COLON 285
141 #define LLT_COMMA 286
142 #define LLT_EQUALS 287
143 #define LLT_LBRACE 288
144 #define LLT_RBRACE 289
145 #define LLT_RBRACKET 290
147 #define LLT_QUOTE 292
149 #define LLT_CCHAR 294
150 #define LLT_CFLOAT 295
151 #define LLT_CINTEGER 296
152 #define LLT_LCSTRING 297
154 #define LLT_ANYTHING 299
157 #define LLT_CLAIMS 302
158 #define LLT_CHECKS 303
159 #define LLT_CONSTANT 304
161 #define LLT_ENSURES 306
163 #define LLT_FRESH 308
165 #define LLT_IMMUTABLE 310
166 #define LLT_IMPORTS 311
167 #define LLT_CONSTRAINT 312
168 #define LLT_ISSUB 313
170 #define LLT_MODIFIES 315
171 #define LLT_MUTABLE 316
172 #define LLT_NOTHING 317
173 #define LLT_INTERNAL 318
174 #define LLT_FILESYS 319
179 #define LLT_PARTIAL 324
180 #define LLT_OWNED 325
181 #define LLT_DEPENDENT 326
185 #define LLT_SHARED 330
186 #define LLT_UNIQUE 331
187 #define LLT_UNUSED 332
188 #define LLT_EXITS 333
189 #define LLT_MAYEXIT 334
190 #define LLT_NEVEREXIT 335
191 #define LLT_TRUEEXIT 336
192 #define LLT_FALSEEXIT 337
193 #define LLT_UNDEF 338
194 #define LLT_KILLED 339
195 #define LLT_CHECKMOD 340
196 #define LLT_CHECKED 341
197 #define LLT_UNCHECKED 342
198 #define LLT_CHECKEDSTRICT 343
199 #define LLT_TRUENULL 344
200 #define LLT_FALSENULL 345
201 #define LLT_LNULL 346
202 #define LLT_LNOTNULL 347
203 #define LLT_RETURNED 348
204 #define LLT_OBSERVER 349
205 #define LLT_EXPOSED 350
206 #define LLT_REFCOUNTED 351
208 #define LLT_RELNULL 353
209 #define LLT_RELDEF 354
210 #define LLT_KILLREF 355
211 #define LLT_NULLTERMINATED 356
212 #define LLT_TEMPREF 357
213 #define LLT_NEWREF 358
214 #define LLT_PRIVATE 359
215 #define LLT_REQUIRES 360
216 #define LLT_RESULT 361
217 #define LLT_SIZEOF 362
219 #define LLT_TAGGEDUNION 364
222 #define LLT_TYPEDEF 367
223 #define LLT_UNCHANGED 368
226 #define LLT_CONST 371
227 #define LLT_DOUBLE 372
229 #define LLT_FLOAT 374
232 #define LLT_YIELD 377
234 #define LLT_SHORT 379
235 #define LLT_SIGNED 380
236 #define LLT_UNKNOWN 381
237 #define LLT_STRUCT 382
238 #define LLT_TELIPSIS 383
239 #define LLT_UNION 384
240 #define LLT_UNSIGNED 385
242 #define LLT_VOLATILE 387
243 #define LLT_PRINTFLIKE 388
244 #define LLT_SCANFLIKE 389
245 #define LLT_MESSAGELIKE 390
248 extern YYSTYPE yllval;