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 /*@only@*/ pointers pointers;
91 /* taggedUnionNode taggedunion; */
92 /*@only@*/ globalList globals;
93 /*@only@*/ constDeclarationNode constdeclaration;
94 /*@only@*/ varDeclarationNode vardeclaration;
95 /*@only@*/ varDeclarationNodeList vardeclarationlist;
96 /*@only@*/ initDeclNodeList initdecls;
97 /*@only@*/ initDeclNode initdecl;
98 /*@only@*/ stDeclNodeList structdecls;
99 /*@only@*/ stDeclNode structdecl;
100 /*@only@*/ strOrUnionNode structorunion;
101 /*@only@*/ enumSpecNode enumspec;
102 /*@only@*/ lclTypeSpecNode lcltypespec;
103 /*@only@*/ typeNameNode typname;
104 /*@only@*/ opFormNode opform;
105 /*@only@*/ sigNode signature;
106 /*@only@*/ nameNode name;
107 /*@only@*/ typeNameNodeList namelist;
108 /*@only@*/ replaceNode replace;
109 /*@only@*/ replaceNodeList replacelist;
110 /*@only@*/ renamingNode renaming;
111 /*@only@*/ traitRefNode traitref;
112 /*@only@*/ traitRefNodeList traitreflist;
113 /*@only@*/ importNode import;
114 /*@only@*/ importNodeList importlist;
115 /*@only@*/ interfaceNode iface;
116 /*@only@*/ interfaceNodeList interfacelist;
117 /*@only@*/ CTypesNode ctypes;
121 #define PREFIX_OP 258
122 #define POSTFIX_OP 259
123 #define LLT_MULOP 260
125 #define LLT_VERTICALBAR 262
126 #define ITERATION_OP 263
128 #define LLT_LBRACKET 265
129 #define selectSym 266
130 #define LLT_IF_THEN_ELSE 267
131 #define logicalOp 268
133 #define equationSym 270
134 #define commentSym 271
135 #define LLT_WHITESPACE 272
137 #define LLT_TYPEDEF_NAME 274
138 #define quantifierSym 275
144 #define markerSym 281
148 #define LLT_COLON 285
149 #define LLT_COMMA 286
150 #define LLT_EQUALS 287
151 #define LLT_LBRACE 288
152 #define LLT_RBRACE 289
153 #define LLT_RBRACKET 290
155 #define LLT_QUOTE 292
157 #define LLT_CCHAR 294
158 #define LLT_CFLOAT 295
159 #define LLT_CINTEGER 296
160 #define LLT_LCSTRING 297
162 #define LLT_ANYTHING 299
165 #define LLT_CLAIMS 302
166 #define LLT_CHECKS 303
167 #define LLT_CONSTANT 304
169 #define LLT_ENSURES 306
171 #define LLT_FRESH 308
173 #define LLT_IMMUTABLE 310
174 #define LLT_IMPORTS 311
175 #define LLT_CONSTRAINT 312
176 #define LLT_ISSUB 313
178 #define LLT_MODIFIES 315
179 #define LLT_MUTABLE 316
180 #define LLT_NOTHING 317
181 #define LLT_INTERNAL 318
182 #define LLT_FILESYS 319
187 #define LLT_PARTIAL 324
188 #define LLT_OWNED 325
189 #define LLT_DEPENDENT 326
193 #define LLT_SHARED 330
194 #define LLT_UNIQUE 331
195 #define LLT_UNUSED 332
196 #define LLT_EXITS 333
197 #define LLT_MAYEXIT 334
198 #define LLT_NEVEREXIT 335
199 #define LLT_TRUEEXIT 336
200 #define LLT_FALSEEXIT 337
201 #define LLT_UNDEF 338
202 #define LLT_KILLED 339
203 #define LLT_CHECKMOD 340
204 #define LLT_CHECKED 341
205 #define LLT_UNCHECKED 342
206 #define LLT_CHECKEDSTRICT 343
207 #define LLT_TRUENULL 344
208 #define LLT_FALSENULL 345
209 #define LLT_LNULL 346
210 #define LLT_LNOTNULL 347
211 #define LLT_RETURNED 348
212 #define LLT_OBSERVER 349
213 #define LLT_EXPOSED 350
214 #define LLT_REFCOUNTED 351
216 #define LLT_RELNULL 353
217 #define LLT_RELDEF 354
218 #define LLT_KILLREF 355
219 #define LLT_NULLTERMINATED 356
220 #define LLT_TEMPREF 357
221 #define LLT_NEWREF 358
222 #define LLT_PRIVATE 359
223 #define LLT_REQUIRES 360
224 #define LLT_RESULT 361
225 #define LLT_SIZEOF 362
227 #define LLT_TAGGEDUNION 364
230 #define LLT_TYPEDEF 367
231 #define LLT_UNCHANGED 368
234 #define LLT_CONST 371
235 #define LLT_DOUBLE 372
237 #define LLT_FLOAT 374
240 #define LLT_YIELD 377
242 #define LLT_SHORT 379
243 #define LLT_SIGNED 380
244 #define LLT_UNKNOWN 381
245 #define LLT_STRUCT 382
246 #define LLT_TELIPSIS 383
247 #define LLT_UNION 384
248 #define LLT_UNSIGNED 385
250 #define LLT_VOLATILE 387
251 #define LLT_PRINTFLIKE 388
252 #define LLT_SCANFLIKE 389
253 #define LLT_MESSAGELIKE 390
256 extern YYSTYPE yllval;
258 ** Resets all flags in bison.head
280 /*@=evalorderuncon@*/
289 /*@=elseifcomplete@*/
297 /*@=dependenttrans@*/
298 /*@=unqualifiedtrans@*/
302 /*drl added 11/27/2001*/