X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/1ac6313d90a797f38280d75b2a63655579080ac6..7ac98eb7e62335f5bb191d2c399d7dae5c1e62ab:/src/Headers/cgrammar_tokens.h

diff --git a/src/Headers/cgrammar_tokens.h b/src/Headers/cgrammar_tokens.h
index fcaf9ec..a862ccb 100644
--- a/src/Headers/cgrammar_tokens.h
+++ b/src/Headers/cgrammar_tokens.h
@@ -41,212 +41,322 @@
 /*@-dependenttrans@*/
 /*@-unqualifiedtrans@*/
 /*@-nullassign@*/
+/*@-nullpass@*/
+/*@-nullptrarith*/
+/*@-usereleased@*/
+/*@-declundef@*/
+
+/*drl added 11/27/2001*/
+/*@-bounds@*/
+
+/*drl added 12/11/2002*/
+/*@-type@*/
 
 /* < end of bison.head > */
 
+#ifndef BISON_CGRAMMAR_TAB_H
+# define BISON_CGRAMMAR_TAB_H
+
+#ifndef cgrammar_YYSTYPE
 typedef union
 {
- lltok tok;
- int count;
- specialClauseKind sck;
- qual typequal;
- qualList tquallist;
- ctype ctyp;
- sRef sr;
- /*@only@*/ qtype qtyp;
- /*@only@*/ cstring cname;
- /*@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 alist;
- /*@only@*/ sRefSet srset; 
- /*@only@*/ cstringList cstringlist;
-} YYSTYPE;
-#define	BADTOK	258
-#define	SKIPTOK	259
-#define	CTOK_ELIPSIS	260
-#define	CASE	261
-#define	DEFAULT	262
-#define	CIF	263
-#define	CELSE	264
-#define	SWITCH	265
-#define	WHILE	266
-#define	DO	267
-#define	CFOR	268
-#define	GOTO	269
-#define	CONTINUE	270
-#define	BREAK	271
-#define	RETURN	272
-#define	TSEMI	273
-#define	TLBRACE	274
-#define	TRBRACE	275
-#define	TCOMMA	276
-#define	TCOLON	277
-#define	TASSIGN	278
-#define	TLPAREN	279
-#define	TRPAREN	280
-#define	TLSQBR	281
-#define	TRSQBR	282
-#define	TDOT	283
-#define	TAMPERSAND	284
-#define	TEXCL	285
-#define	TTILDE	286
-#define	TMINUS	287
-#define	TPLUS	288
-#define	TMULT	289
-#define	TDIV	290
-#define	TPERCENT	291
-#define	TLT	292
-#define	TGT	293
-#define	TCIRC	294
-#define	TBAR	295
-#define	TQUEST	296
-#define	CSIZEOF	297
-#define	CALIGNOF	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	QGLOBALS	327
-#define	QMODIFIES	328
-#define	QNOMODS	329
-#define	QCONSTANT	330
-#define	QFUNCTION	331
-#define	QITER	332
-#define	QDEFINES	333
-#define	QUSES	334
-#define	QALLOCATES	335
-#define	QSETS	336
-#define	QRELEASES	337
-#define	QPRECLAUSE	338
-#define	QPOSTCLAUSE	339
-#define	QALT	340
-#define	QUNDEF	341
-#define	QKILLED	342
-#define	QENDMACRO	343
-#define	LLMACRO	344
-#define	LLMACROITER	345
-#define	LLMACROEND	346
-#define	TENDMACRO	347
-#define	QSWITCHBREAK	348
-#define	QLOOPBREAK	349
-#define	QINNERBREAK	350
-#define	QSAFEBREAK	351
-#define	QINNERCONTINUE	352
-#define	QFALLTHROUGH	353
-#define	QLINTNOTREACHED	354
-#define	QLINTFALLTHROUGH	355
-#define	QLINTFALLTHRU	356
-#define	QARGSUSED	357
-#define	QPRINTFLIKE	358
-#define	QLINTPRINTFLIKE	359
-#define	QSCANFLIKE	360
-#define	QMESSAGELIKE	361
-#define	QNOTREACHED	362
-#define	QCONST	363
-#define	QVOLATILE	364
-#define	QINLINE	365
-#define	QEXTENSION	366
-#define	QEXTERN	367
-#define	QSTATIC	368
-#define	QAUTO	369
-#define	QREGISTER	370
-#define	QOUT	371
-#define	QIN	372
-#define	QYIELD	373
-#define	QONLY	374
-#define	QTEMP	375
-#define	QSHARED	376
-#define	QREF	377
-#define	QUNIQUE	378
-#define	QCHECKED	379
-#define	QUNCHECKED	380
-#define	QCHECKEDSTRICT	381
-#define	QCHECKMOD	382
-#define	QKEEP	383
-#define	QKEPT	384
-#define	QPARTIAL	385
-#define	QSPECIAL	386
-#define	QOWNED	387
-#define	QDEPENDENT	388
-#define	QRETURNED	389
-#define	QEXPOSED	390
-#define	QNULL	391
-#define	QOBSERVER	392
-#define	QISNULL	393
-#define	QEXITS	394
-#define	QMAYEXIT	395
-#define	QNEVEREXIT	396
-#define	QTRUEEXIT	397
-#define	QFALSEEXIT	398
-#define	QLONG	399
-#define	QSIGNED	400
-#define	QUNSIGNED	401
-#define	QSHORT	402
-#define	QUNUSED	403
-#define	QSEF	404
-#define	QNOTNULL	405
-#define	QRELNULL	406
-#define	QABSTRACT	407
-#define	QCONCRETE	408
-#define	QMUTABLE	409
-#define	QIMMUTABLE	410
-#define	QTRUENULL	411
-#define	QFALSENULL	412
-#define	QEXTERNAL	413
-#define	QREFCOUNTED	414
-#define	QREFS	415
-#define	QNEWREF	416
-#define	QTEMPREF	417
-#define	QKILLREF	418
-#define	QRELDEF	419
-#define	CGCHAR	420
-#define	CBOOL	421
-#define	CINT	422
-#define	CGFLOAT	423
-#define	CDOUBLE	424
-#define	CVOID	425
-#define	QANYTYPE	426
-#define	QINTEGRALTYPE	427
-#define	QUNSIGNEDINTEGRALTYPE	428
-#define	QSIGNEDINTEGRALTYPE	429
-#define	QNULLTERMINATED	430
-#define	IDENTIFIER	431
-#define	NEW_IDENTIFIER	432
-#define	TYPE_NAME_OR_ID	433
-#define	CCONSTANT	434
-#define	ITER_NAME	435
-#define	ITER_ENDNAME	436
-#define	TYPE_NAME	437
-
-
-extern YYSTYPE yylval;
+  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@*/ pointers pointers;
+  /*@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 cgrammar_YYSTYPE yystype
+# define cgrammar_YYSTYPE_IS_TRIVIAL 1
+#endif
+# 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	QDREVEALSTATE	350
+# define	QSWITCHBREAK	351
+# define	QLOOPBREAK	352
+# define	QINNERBREAK	353
+# define	QSAFEBREAK	354
+# define	QINNERCONTINUE	355
+# define	QFALLTHROUGH	356
+# define	QLINTNOTREACHED	357
+# define	QLINTFALLTHROUGH	358
+# define	QLINTFALLTHRU	359
+# define	QARGSUSED	360
+# define	QPRINTFLIKE	361
+# define	QLINTPRINTFLIKE	362
+# define	QSCANFLIKE	363
+# define	QMESSAGELIKE	364
+# define	QNOTREACHED	365
+# define	QCONST	366
+# define	QRESTRICT	367
+# define	QVOLATILE	368
+# define	QINLINE	369
+# define	QEXTENSION	370
+# define	QEXTERN	371
+# define	QSTATIC	372
+# define	QAUTO	373
+# define	QREGISTER	374
+# define	QOUT	375
+# define	QIN	376
+# define	QYIELD	377
+# define	QONLY	378
+# define	QTEMP	379
+# define	QSHARED	380
+# define	QREF	381
+# define	QUNIQUE	382
+# define	QCHECKED	383
+# define	QUNCHECKED	384
+# define	QCHECKEDSTRICT	385
+# define	QCHECKMOD	386
+# define	QKEEP	387
+# define	QKEPT	388
+# define	QPARTIAL	389
+# define	QSPECIAL	390
+# define	QOWNED	391
+# define	QDEPENDENT	392
+# define	QRETURNED	393
+# define	QEXPOSED	394
+# define	QNULL	395
+# define	QOBSERVER	396
+# define	QISNULL	397
+# define	QEXITS	398
+# define	QMAYEXIT	399
+# define	QNEVEREXIT	400
+# define	QTRUEEXIT	401
+# define	QFALSEEXIT	402
+# define	QLONG	403
+# define	QSIGNED	404
+# define	QUNSIGNED	405
+# define	QSHORT	406
+# define	QUNUSED	407
+# define	QSEF	408
+# define	QNOTNULL	409
+# define	QRELNULL	410
+# define	QABSTRACT	411
+# define	QNUMABSTRACT	412
+# define	QCONCRETE	413
+# define	QMUTABLE	414
+# define	QIMMUTABLE	415
+# define	QTRUENULL	416
+# define	QFALSENULL	417
+# define	QEXTERNAL	418
+# define	QREFCOUNTED	419
+# define	QREFS	420
+# define	QNEWREF	421
+# define	QTEMPREF	422
+# define	QKILLREF	423
+# define	QRELDEF	424
+# define	CGCHAR	425
+# define	CBOOL	426
+# define	CINT	427
+# define	CGFLOAT	428
+# define	CDOUBLE	429
+# define	CVOID	430
+# define	QANYTYPE	431
+# define	QINTEGRALTYPE	432
+# define	QUNSIGNEDINTEGRALTYPE	433
+# define	QSIGNEDINTEGRALTYPE	434
+# define	QNULLTERMINATED	435
+# define	QSETBUFFERSIZE	436
+# define	QSETSTRINGLENGTH	437
+# define	QMAXSET	438
+# define	QMAXREAD	439
+# define	QTESTINRANGE	440
+# define	TCAND	441
+# define	IDENTIFIER	442
+# define	NEW_IDENTIFIER	443
+# define	TYPE_NAME_OR_ID	444
+# define	CANNOTATION	445
+# define	CCONSTANT	446
+# define	ITER_NAME	447
+# define	ITER_ENDNAME	448
+# define	TYPE_NAME	449
+# define	METASTATE_NAME	450
+
+
+extern cgrammar_YYSTYPE yylval;
+
+#endif /* not BISON_CGRAMMAR_TAB_H */
+/*
+** 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@*/
+
+/*drl added 12/11/2002*/
+/*@=type@*/