2 ** Inserted at beginning of c files generated by bison
3 ** REMEMBER: Change bison.reset too.
42 /*@-unqualifiedtrans@*/
49 /*drl added 11/27/2001*/
51 /* < end of bison.head > */
55 ltoken ltok; /* a leaf is also an ltoken */
58 /*@only@*/ ltokenList ltokenList;
59 /*@only@*/ abstDeclaratorNode abstDecl;
60 /*@only@*/ declaratorNode declare;
61 /*@only@*/ declaratorNodeList declarelist;
62 /*@only@*/ typeExpr typeexpr;
63 /*@only@*/ arrayQualNode array;
64 /*@only@*/ quantifierNode quantifier;
65 /*@only@*/ quantifierNodeList quantifiers;
66 /*@only@*/ varNode var;
67 /*@only@*/ varNodeList vars;
68 /*@only@*/ storeRefNode storeref;
69 /*@only@*/ storeRefNodeList storereflist;
70 /*@only@*/ termNode term;
71 /*@only@*/ termNodeList termlist;
72 /*@only@*/ programNode program;
73 /*@only@*/ stmtNode stmt;
74 /*@only@*/ claimNode claim;
75 /*@only@*/ typeNode type;
76 /*@only@*/ iterNode iter;
77 /*@only@*/ fcnNode fcn;
78 /*@only@*/ fcnNodeList fcns;
79 /*@only@*/ letDeclNode letdecl;
80 /*@only@*/ letDeclNodeList letdecls;
81 /*@only@*/ lclPredicateNode lclpredicate;
82 /*@only@*/ modifyNode modify;
83 /*@only@*/ paramNode param;
84 /*@only@*/ paramNodeList paramlist;
85 /*@only@*/ declaratorInvNodeList declaratorinvs;
86 /*@only@*/ declaratorInvNode declaratorinv;
87 /*@only@*/ abstBodyNode abstbody;
88 /*@only@*/ abstractNode abstract;
89 /*@only@*/ exposedNode exposed;
90 /* taggedUnionNode taggedunion; */
91 /*@only@*/ globalList globals;
92 /*@only@*/ constDeclarationNode constdeclaration;
93 /*@only@*/ varDeclarationNode vardeclaration;
94 /*@only@*/ varDeclarationNodeList vardeclarationlist;
95 /*@only@*/ initDeclNodeList initdecls;
96 /*@only@*/ initDeclNode initdecl;
97 /*@only@*/ stDeclNodeList structdecls;
98 /*@only@*/ stDeclNode structdecl;
99 /*@only@*/ strOrUnionNode structorunion;
100 /*@only@*/ enumSpecNode enumspec;
101 /*@only@*/ lclTypeSpecNode lcltypespec;
102 /*@only@*/ typeNameNode typname;
103 /*@only@*/ opFormNode opform;
104 /*@only@*/ sigNode signature;
105 /*@only@*/ nameNode name;
106 /*@only@*/ typeNameNodeList namelist;
107 /*@only@*/ replaceNode replace;
108 /*@only@*/ replaceNodeList replacelist;
109 /*@only@*/ renamingNode renaming;
110 /*@only@*/ traitRefNode traitref;
111 /*@only@*/ traitRefNodeList traitreflist;
112 /*@only@*/ importNode import;
113 /*@only@*/ importNodeList importlist;
114 /*@only@*/ interfaceNode iface;
115 /*@only@*/ interfaceNodeList interfacelist;
116 /*@only@*/ CTypesNode ctypes;
120 #define PREFIX_OP 258
121 #define POSTFIX_OP 259
122 #define LLT_MULOP 260
124 #define LLT_VERTICALBAR 262
125 #define ITERATION_OP 263
127 #define LLT_LBRACKET 265
128 #define selectSym 266
129 #define LLT_IF_THEN_ELSE 267
130 #define logicalOp 268
132 #define equationSym 270
133 #define commentSym 271
134 #define LLT_WHITESPACE 272
136 #define LLT_TYPEDEF_NAME 274
137 #define quantifierSym 275
143 #define markerSym 281
147 #define LLT_COLON 285
148 #define LLT_COMMA 286
149 #define LLT_EQUALS 287
150 #define LLT_LBRACE 288
151 #define LLT_RBRACE 289
152 #define LLT_RBRACKET 290
154 #define LLT_QUOTE 292
156 #define LLT_CCHAR 294
157 #define LLT_CFLOAT 295
158 #define LLT_CINTEGER 296
159 #define LLT_LCSTRING 297
161 #define LLT_ANYTHING 299
164 #define LLT_CLAIMS 302
165 #define LLT_CHECKS 303
166 #define LLT_CONSTANT 304
168 #define LLT_ENSURES 306
170 #define LLT_FRESH 308
172 #define LLT_IMMUTABLE 310
173 #define LLT_IMPORTS 311
174 #define LLT_CONSTRAINT 312
175 #define LLT_ISSUB 313
177 #define LLT_MODIFIES 315
178 #define LLT_MUTABLE 316
179 #define LLT_NOTHING 317
180 #define LLT_INTERNAL 318
181 #define LLT_FILESYS 319
186 #define LLT_PARTIAL 324
187 #define LLT_OWNED 325
188 #define LLT_DEPENDENT 326
192 #define LLT_SHARED 330
193 #define LLT_UNIQUE 331
194 #define LLT_UNUSED 332
195 #define LLT_EXITS 333
196 #define LLT_MAYEXIT 334
197 #define LLT_NEVEREXIT 335
198 #define LLT_TRUEEXIT 336
199 #define LLT_FALSEEXIT 337
200 #define LLT_UNDEF 338
201 #define LLT_KILLED 339
202 #define LLT_CHECKMOD 340
203 #define LLT_CHECKED 341
204 #define LLT_UNCHECKED 342
205 #define LLT_CHECKEDSTRICT 343
206 #define LLT_TRUENULL 344
207 #define LLT_FALSENULL 345
208 #define LLT_LNULL 346
209 #define LLT_LNOTNULL 347
210 #define LLT_RETURNED 348
211 #define LLT_OBSERVER 349
212 #define LLT_EXPOSED 350
213 #define LLT_REFCOUNTED 351
215 #define LLT_RELNULL 353
216 #define LLT_RELDEF 354
217 #define LLT_KILLREF 355
218 #define LLT_NULLTERMINATED 356
219 #define LLT_TEMPREF 357
220 #define LLT_NEWREF 358
221 #define LLT_PRIVATE 359
222 #define LLT_REQUIRES 360
223 #define LLT_RESULT 361
224 #define LLT_SIZEOF 362
226 #define LLT_TAGGEDUNION 364
229 #define LLT_TYPEDEF 367
230 #define LLT_UNCHANGED 368
233 #define LLT_CONST 371
234 #define LLT_DOUBLE 372
236 #define LLT_FLOAT 374
239 #define LLT_YIELD 377
241 #define LLT_SHORT 379
242 #define LLT_SIGNED 380
243 #define LLT_UNKNOWN 381
244 #define LLT_STRUCT 382
245 #define LLT_TELIPSIS 383
246 #define LLT_UNION 384
247 #define LLT_UNSIGNED 385
249 #define LLT_VOLATILE 387
250 #define LLT_PRINTFLIKE 388
251 #define LLT_SCANFLIKE 389
252 #define LLT_MESSAGELIKE 390
255 extern YYSTYPE yllval;
257 ** Resets all flags in bison.head
279 /*@=evalorderuncon@*/
288 /*@=elseifcomplete@*/
296 /*@=dependenttrans@*/
297 /*@=unqualifiedtrans@*/
301 /*drl added 11/27/2001*/