/*
** 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@*/

/* < end of bison.head > */

typedef union 
{
  ltoken ltok;  /* a leaf is also an ltoken */
  qual typequal;
  unsigned int count;
  /*@only@*/ ltokenList ltokenList;
  /*@only@*/ abstDeclaratorNode abstDecl; 
  /*@only@*/ declaratorNode declare;
  /*@only@*/ declaratorNodeList declarelist;
  /*@only@*/ typeExpr typeexpr;
  /*@only@*/ arrayQualNode array;
  /*@only@*/ quantifierNode quantifier;
  /*@only@*/ quantifierNodeList quantifiers;
  /*@only@*/ varNode var;
  /*@only@*/ varNodeList vars;
  /*@only@*/ storeRefNode storeref;
  /*@only@*/ storeRefNodeList storereflist;
  /*@only@*/ termNode term;
  /*@only@*/ termNodeList termlist;
  /*@only@*/ programNode program; 
  /*@only@*/ stmtNode stmt;
  /*@only@*/ claimNode claim;
  /*@only@*/ typeNode type;
  /*@only@*/ iterNode iter;
  /*@only@*/ fcnNode fcn;
  /*@only@*/ fcnNodeList fcns;
  /*@only@*/ letDeclNode letdecl;
  /*@only@*/ letDeclNodeList letdecls;
  /*@only@*/ lclPredicateNode lclpredicate;
  /*@only@*/ modifyNode modify;
  /*@only@*/ paramNode param;
  /*@only@*/ paramNodeList paramlist;
  /*@only@*/ declaratorInvNodeList declaratorinvs;	
  /*@only@*/ declaratorInvNode declaratorinv;	
  /*@only@*/ abstBodyNode abstbody;
  /*@only@*/ abstractNode abstract;
  /*@only@*/ exposedNode exposed;
  /*    taggedUnionNode taggedunion; */
  /*@only@*/ globalList globals;
  /*@only@*/ constDeclarationNode constdeclaration;
  /*@only@*/ varDeclarationNode vardeclaration;
  /*@only@*/ varDeclarationNodeList vardeclarationlist;
  /*@only@*/ initDeclNodeList initdecls;
  /*@only@*/ initDeclNode initdecl;
  /*@only@*/ stDeclNodeList structdecls;
  /*@only@*/ stDeclNode structdecl;
  /*@only@*/ strOrUnionNode structorunion;
  /*@only@*/ enumSpecNode enumspec; 
  /*@only@*/ lclTypeSpecNode lcltypespec;
  /*@only@*/ typeNameNode typname;
  /*@only@*/ opFormNode opform;
  /*@only@*/ sigNode signature;
  /*@only@*/ nameNode name;
  /*@only@*/ typeNameNodeList namelist;
  /*@only@*/ replaceNode replace;	
  /*@only@*/ replaceNodeList replacelist;
  /*@only@*/ renamingNode renaming;
  /*@only@*/ traitRefNode traitref;
  /*@only@*/ traitRefNodeList traitreflist;
  /*@only@*/ importNode import;
  /*@only@*/ importNodeList importlist;
  /*@only@*/ interfaceNode iface;
  /*@only@*/ interfaceNodeList interfacelist; 
  /*@only@*/ CTypesNode ctypes;
} YYSTYPE;
#define	simpleOp	258
#define	PREFIX_OP	259
#define	POSTFIX_OP	260
#define	LLT_MULOP	261
#define	LLT_SEMI	262
#define	LLT_VERTICALBAR	263
#define	ITERATION_OP	264
#define	LLT_LPAR	265
#define	LLT_LBRACKET	266
#define	selectSym	267
#define	LLT_IF_THEN_ELSE	268
#define	logicalOp	269
#define	eqSepSym	270
#define	equationSym	271
#define	commentSym	272
#define	LLT_WHITESPACE	273
#define	LLT_EOL	274
#define	LLT_TYPEDEF_NAME	275
#define	quantifierSym	276
#define	openSym	277
#define	closeSym	278
#define	sepSym	279
#define	simpleId	280
#define	mapSym	281
#define	markerSym	282
#define	preSym	283
#define	postSym	284
#define	anySym	285
#define	LLT_COLON	286
#define	LLT_COMMA	287
#define	LLT_EQUALS	288
#define	LLT_LBRACE	289
#define	LLT_RBRACE	290
#define	LLT_RBRACKET	291
#define	LLT_RPAR	292
#define	LLT_QUOTE	293
#define	eqOp	294
#define	LLT_CCHAR	295
#define	LLT_CFLOAT	296
#define	LLT_CINTEGER	297
#define	LLT_LCSTRING	298
#define	LLT_ALL	299
#define	LLT_ANYTHING	300
#define	LLT_BE	301
#define	LLT_BODY	302
#define	LLT_CLAIMS	303
#define	LLT_CHECKS	304
#define	LLT_CONSTANT	305
#define	LLT_ELSE	306
#define	LLT_ENSURES	307
#define	LLT_FOR	308
#define	LLT_FRESH	309
#define	LLT_IF	310
#define	LLT_IMMUTABLE	311
#define	LLT_IMPORTS	312
#define	LLT_CONSTRAINT	313
#define	LLT_ISSUB	314
#define	LLT_LET	315
#define	LLT_MODIFIES	316
#define	LLT_MUTABLE	317
#define	LLT_NOTHING	318
#define	LLT_INTERNAL	319
#define	LLT_FILESYS	320
#define	LLT_OBJ	321
#define	LLT_OUT	322
#define	LLT_SEF	323
#define	LLT_ONLY	324
#define	LLT_PARTIAL	325
#define	LLT_OWNED	326
#define	LLT_DEPENDENT	327
#define	LLT_KEEP	328
#define	LLT_KEPT	329
#define	LLT_TEMP	330
#define	LLT_SHARED	331
#define	LLT_UNIQUE	332
#define	LLT_UNUSED	333
#define	LLT_EXITS	334
#define	LLT_MAYEXIT	335
#define	LLT_NEVEREXIT	336
#define	LLT_TRUEEXIT	337
#define	LLT_FALSEEXIT	338
#define	LLT_UNDEF	339
#define	LLT_KILLED	340
#define	LLT_CHECKMOD	341
#define	LLT_CHECKED	342
#define	LLT_UNCHECKED	343
#define	LLT_CHECKEDSTRICT	344
#define	LLT_TRUENULL	345
#define	LLT_FALSENULL	346
#define	LLT_LNULL	347
#define	LLT_LNOTNULL	348
#define	LLT_RETURNED	349
#define	LLT_OBSERVER	350
#define	LLT_EXPOSED	351
#define	LLT_REFCOUNTED	352
#define	LLT_REFS	353
#define	LLT_RELNULL	354
#define	LLT_RELDEF	355
#define	LLT_KILLREF	356
#define	LLT_TEMPREF	357
#define	LLT_NEWREF	358
#define	LLT_PRIVATE	359
#define	LLT_REQUIRES	360
#define	LLT_RESULT	361
#define	LLT_SIZEOF	362
#define	LLT_SPEC	363
#define	LLT_TAGGEDUNION	364
#define	LLT_THEN	365
#define	LLT_TYPE	366
#define	LLT_TYPEDEF	367
#define	LLT_UNCHANGED	368
#define	LLT_USES	369
#define	LLT_CHAR	370
#define	LLT_CONST	371
#define	LLT_DOUBLE	372
#define	LLT_ENUM	373
#define	LLT_FLOAT	374
#define	LLT_INT	375
#define	LLT_ITER	376
#define	LLT_YIELD	377
#define	LLT_LONG	378
#define	LLT_SHORT	379
#define	LLT_SIGNED	380
#define	LLT_UNKNOWN	381
#define	LLT_STRUCT	382
#define	LLT_TELIPSIS	383
#define	LLT_UNION	384
#define	LLT_UNSIGNED	385
#define	LLT_VOID	386
#define	LLT_VOLATILE	387
#define	LLT_PRINTFLIKE	388
#define	LLT_SCANFLIKE	389
#define	LLT_MESSAGELIKE	390


extern YYSTYPE yllval;
/*
** 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@*/