--- /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
+{
+ 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;
+ /*@-redef@*/
+} YYSTYPE;
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 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@*/
+/*@=declundef@*/
+
+
+/*drl added 11/27/2001*/
+/*@=bounds@*/
andersk / splint.git / commitdiff
