--- /dev/null
+/*
+** Inserted at beginning of c files generated by bison
+** REMEMBER: Change bison.reset too.
+*/
+
+/*@-allmacros@*/
+/*@+boolint@*/
+/*@+charint@*/
+/*@-macroparams@*/
+/*@-macroundef@*/
+/*@-unreachable@*/
+/*@-macrospec@*/
+/*@-varuse@*/
+/*@+ignorequals@*/
+/*@-macrostmt@*/
+/*@-noeffect@*/
+/*@-shadow@*/
+/*@-exitarg@*/
+/*@-macroredef@*/
+/*@-uniondef@*/
+/*@-compdef@*/
+/*@-matchfields@*/
+/*@-exportlocal@*/
+/*@-evalorderuncon@*/
+/*@-exportheader@*/
+/*@-typeuse@*/
+/*@-redecl@*/
+/*@-redef@*/
+/*@-noparams@*/
+/*@-ansireserved@*/
+/*@-fielduse@*/
+/*@-ifblock@*/
+/*@-elseifcomplete@*/
+/*@-whileblock@*/
+/*@-forblock@*/
+/*@-branchstate@*/
+/*@-readonlytrans@*/
+/*@-namechecks@*/
+/*@-usedef@*/
+/*@-systemunrecog@*/
+/*@-dependenttrans@*/
+/*@-unqualifiedtrans@*/
+/*@-nullassign@*/
+/*@-nullpass@*/
+/*@-nullptrarith*/
+/*@-usereleased@*/
+/*@-declundef@*/
+
+/*drl added 11/27/2001*/
+/*@-bounds@*/
+/* < end of bison.head > */
+
+typedef union
+{
+ lltok tok;
+ int count;
+ qual typequal;
+ qualList tquallist;
+ ctype ctyp;
+ /*@dependent@*/ sRef sr;
+ /*@only@*/ sRef osr;
+
+ /*@only@*/ functionClauseList funcclauselist;
+ /*@only@*/ functionClause funcclause;
+ /*@only@*/ flagSpec flagspec;
+ /*@only@*/ globalsClause globsclause;
+ /*@only@*/ modifiesClause modsclause;
+ /*@only@*/ warnClause warnclause;
+ /*@only@*/ stateClause stateclause;
+
+ /*@only@*/ functionConstraint fcnconstraint;
+
+ /*@only@*/ metaStateConstraint msconstraint;
+ /*@only@*/ metaStateSpecifier msspec;
+ /*@only@*/ metaStateExpression msexpr;
+ /*@observer@*/ metaStateInfo msinfo;
+
+ /*@only@*/ sRefList srlist;
+ /*@only@*/ globSet globset;
+ /*@only@*/ qtype qtyp;
+ /*@only@*/ cstring cname;
+ /*@observer@*/ annotationInfo annotation;
+ /*@only@*/ idDecl ntyp;
+ /*@only@*/ idDeclList ntyplist;
+ /*@only@*/ uentryList flist;
+ /*@owned@*/ uentryList entrylist;
+ /*@observer@*/ /*@dependent@*/ uentry entry;
+ /*@only@*/ uentry oentry;
+ /*@only@*/ exprNode expr;
+ /*@only@*/ enumNameList enumnamelist;
+ /*@only@*/ exprNodeList exprlist;
+ /*@only@*/ sRefSet srset;
+ /*@only@*/ cstringList cstringlist;
+
+ /*drl
+ added 1/19/2001
+ */
+ constraint con;
+ constraintList conL;
+ constraintExpr conE;
+ /* drl */
+} YYSTYPE;
+#define BADTOK 257
+#define SKIPTOK 258
+#define CTOK_ELIPSIS 259
+#define CASE 260
+#define DEFAULT 261
+#define CIF 262
+#define CELSE 263
+#define SWITCH 264
+#define WHILE 265
+#define DO 266
+#define CFOR 267
+#define GOTO 268
+#define CONTINUE 269
+#define BREAK 270
+#define RETURN 271
+#define TSEMI 272
+#define TLBRACE 273
+#define TRBRACE 274
+#define TCOMMA 275
+#define TCOLON 276
+#define TASSIGN 277
+#define TLPAREN 278
+#define TRPAREN 279
+#define TLSQBR 280
+#define TRSQBR 281
+#define TDOT 282
+#define TAMPERSAND 283
+#define TEXCL 284
+#define TTILDE 285
+#define TMINUS 286
+#define TPLUS 287
+#define TMULT 288
+#define TDIV 289
+#define TPERCENT 290
+#define TLT 291
+#define TGT 292
+#define TCIRC 293
+#define TBAR 294
+#define TQUEST 295
+#define CSIZEOF 296
+#define CALIGNOF 297
+#define CTYPEOF 298
+#define ARROW_OP 299
+#define CTYPEDEF 300
+#define COFFSETOF 301
+#define INC_OP 302
+#define DEC_OP 303
+#define LEFT_OP 304
+#define RIGHT_OP 305
+#define LE_OP 306
+#define GE_OP 307
+#define EQ_OP 308
+#define NE_OP 309
+#define AND_OP 310
+#define OR_OP 311
+#define MUL_ASSIGN 312
+#define DIV_ASSIGN 313
+#define MOD_ASSIGN 314
+#define ADD_ASSIGN 315
+#define SUB_ASSIGN 316
+#define LEFT_ASSIGN 317
+#define RIGHT_ASSIGN 318
+#define AND_ASSIGN 319
+#define XOR_ASSIGN 320
+#define OR_ASSIGN 321
+#define CSTRUCT 322
+#define CUNION 323
+#define CENUM 324
+#define VA_ARG 325
+#define VA_DCL 326
+#define QWARN 327
+#define QGLOBALS 328
+#define QMODIFIES 329
+#define QNOMODS 330
+#define QCONSTANT 331
+#define QFUNCTION 332
+#define QITER 333
+#define QDEFINES 334
+#define QUSES 335
+#define QALLOCATES 336
+#define QSETS 337
+#define QRELEASES 338
+#define QPRECLAUSE 339
+#define QPOSTCLAUSE 340
+#define QINVARIANT 341
+#define QALT 342
+#define QUNDEF 343
+#define QKILLED 344
+#define QENDMACRO 345
+#define LLMACRO 346
+#define LLMACROITER 347
+#define LLMACROEND 348
+#define TENDMACRO 349
+#define QSWITCHBREAK 350
+#define QLOOPBREAK 351
+#define QINNERBREAK 352
+#define QSAFEBREAK 353
+#define QINNERCONTINUE 354
+#define QFALLTHROUGH 355
+#define QLINTNOTREACHED 356
+#define QLINTFALLTHROUGH 357
+#define QLINTFALLTHRU 358
+#define QARGSUSED 359
+#define QPRINTFLIKE 360
+#define QLINTPRINTFLIKE 361
+#define QSCANFLIKE 362
+#define QMESSAGELIKE 363
+#define QNOTREACHED 364
+#define QCONST 365
+#define QVOLATILE 366
+#define QINLINE 367
+#define QEXTENSION 368
+#define QEXTERN 369
+#define QSTATIC 370
+#define QAUTO 371
+#define QREGISTER 372
+#define QOUT 373
+#define QIN 374
+#define QYIELD 375
+#define QONLY 376
+#define QTEMP 377
+#define QSHARED 378
+#define QREF 379
+#define QUNIQUE 380
+#define QCHECKED 381
+#define QUNCHECKED 382
+#define QCHECKEDSTRICT 383
+#define QCHECKMOD 384
+#define QKEEP 385
+#define QKEPT 386
+#define QPARTIAL 387
+#define QSPECIAL 388
+#define QOWNED 389
+#define QDEPENDENT 390
+#define QRETURNED 391
+#define QEXPOSED 392
+#define QNULL 393
+#define QOBSERVER 394
+#define QISNULL 395
+#define QEXITS 396
+#define QMAYEXIT 397
+#define QNEVEREXIT 398
+#define QTRUEEXIT 399
+#define QFALSEEXIT 400
+#define QLONG 401
+#define QSIGNED 402
+#define QUNSIGNED 403
+#define QSHORT 404
+#define QUNUSED 405
+#define QSEF 406
+#define QNOTNULL 407
+#define QRELNULL 408
+#define QABSTRACT 409
+#define QCONCRETE 410
+#define QMUTABLE 411
+#define QIMMUTABLE 412
+#define QTRUENULL 413
+#define QFALSENULL 414
+#define QEXTERNAL 415
+#define QREFCOUNTED 416
+#define QREFS 417
+#define QNEWREF 418
+#define QTEMPREF 419
+#define QKILLREF 420
+#define QRELDEF 421
+#define CGCHAR 422
+#define CBOOL 423
+#define CINT 424
+#define CGFLOAT 425
+#define CDOUBLE 426
+#define CVOID 427
+#define QANYTYPE 428
+#define QINTEGRALTYPE 429
+#define QUNSIGNEDINTEGRALTYPE 430
+#define QSIGNEDINTEGRALTYPE 431
+#define QNULLTERMINATED 432
+#define QSETBUFFERSIZE 433
+#define QSETSTRINGLENGTH 434
+#define QMAXSET 435
+#define QMAXREAD 436
+#define QTESTINRANGE 437
+#define TCAND 438
+#define IDENTIFIER 439
+#define NEW_IDENTIFIER 440
+#define TYPE_NAME_OR_ID 441
+#define CANNOTATION 442
+#define CCONSTANT 443
+#define ITER_NAME 444
+#define ITER_ENDNAME 445
+#define TYPE_NAME 446
+#define METASTATE_NAME 447
+
+
+extern YYSTYPE yylval;
+/*
+** Resets all flags in bison.head
+*/
+
+
+/*@=allmacros@*/
+/*@=boolint@*/
+/*@=charint@*/
+/*@=macroparams@*/
+/*@=macroundef@*/
+/*@=unreachable@*/
+/*@=macrospec@*/
+/*@=varuse@*/
+/*@=ignorequals@*/
+/*@=macrostmt@*/
+/*@=noeffect@*/
+/*@=shadow@*/
+/*@=exitarg@*/
+/*@=macroredef@*/
+/*@=uniondef@*/
+/*@=compdef@*/
+/*@=matchfields@*/
+/*@=exportlocal@*/
+/*@=evalorderuncon@*/
+/*@=exportheader@*/
+/*@=typeuse@*/
+/*@=redecl@*/
+/*@=redef@*/
+/*@=noparams@*/
+/*@=ansireserved@*/
+/*@=fielduse@*/
+/*@=ifblock@*/
+/*@=elseifcomplete@*/
+/*@=whileblock@*/
+/*@=forblock@*/
+/*@=branchstate@*/
+/*@=readonlytrans@*/
+/*@=namechecks@*/
+/*@=usedef@*/
+/*@=systemunrecog@*/
+/*@=dependenttrans@*/
+/*@=unqualifiedtrans@*/
+/*@=declundef@*/
+
+
+/*drl added 11/27/2001*/
+/*@=bounds@*/