X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ef2aa32aebac950c1784a2dd25f0fa299b8840da..f9264521e093e570a8831d5238ccc3bc20e01119:/src/Headers/cgrammar_tokens.h

diff --git a/src/Headers/cgrammar_tokens.h b/src/Headers/cgrammar_tokens.h
index ed3059a..569def2 100644
--- a/src/Headers/cgrammar_tokens.h
+++ b/src/Headers/cgrammar_tokens.h
@@ -41,73 +41,107 @@
 /*@-dependenttrans@*/
 /*@-unqualifiedtrans@*/
 /*@-nullassign@*/
+/*@-nullpass@*/
+/*@-nullptrarith*/
+/*@-usereleased@*/
+/*@-declundef@*/
 
+/*drl added 11/27/2001*/
+/*@-bounds@*/
 /* < end of bison.head > */
 
 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;
+  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	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	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
@@ -136,124 +170,175 @@ typedef union
 #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	QSETBUFFERSIZE	431
-#define	QBUFFERCONSTRAINT	432
-#define	QENSURESCONSTRAINT	433
-#define	QSETSTRINGLENGTH	434
-#define	QMAXSET	435
-#define	QMAXREAD	436
-#define	QTESTINRANGE	437
-#define	IDENTIFIER	438
-#define	NEW_IDENTIFIER	439
-#define	TYPE_NAME_OR_ID	440
-#define	CCONSTANT	441
-#define	ITER_NAME	442
-#define	ITER_ENDNAME	443
-#define	TYPE_NAME	444
+#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	QRESTRICT	366
+#define	QVOLATILE	367
+#define	QINLINE	368
+#define	QEXTENSION	369
+#define	QEXTERN	370
+#define	QSTATIC	371
+#define	QAUTO	372
+#define	QREGISTER	373
+#define	QOUT	374
+#define	QIN	375
+#define	QYIELD	376
+#define	QONLY	377
+#define	QTEMP	378
+#define	QSHARED	379
+#define	QREF	380
+#define	QUNIQUE	381
+#define	QCHECKED	382
+#define	QUNCHECKED	383
+#define	QCHECKEDSTRICT	384
+#define	QCHECKMOD	385
+#define	QKEEP	386
+#define	QKEPT	387
+#define	QPARTIAL	388
+#define	QSPECIAL	389
+#define	QOWNED	390
+#define	QDEPENDENT	391
+#define	QRETURNED	392
+#define	QEXPOSED	393
+#define	QNULL	394
+#define	QOBSERVER	395
+#define	QISNULL	396
+#define	QEXITS	397
+#define	QMAYEXIT	398
+#define	QNEVEREXIT	399
+#define	QTRUEEXIT	400
+#define	QFALSEEXIT	401
+#define	QLONG	402
+#define	QSIGNED	403
+#define	QUNSIGNED	404
+#define	QSHORT	405
+#define	QUNUSED	406
+#define	QSEF	407
+#define	QNOTNULL	408
+#define	QRELNULL	409
+#define	QABSTRACT	410
+#define	QCONCRETE	411
+#define	QMUTABLE	412
+#define	QIMMUTABLE	413
+#define	QTRUENULL	414
+#define	QFALSENULL	415
+#define	QEXTERNAL	416
+#define	QREFCOUNTED	417
+#define	QREFS	418
+#define	QNEWREF	419
+#define	QTEMPREF	420
+#define	QKILLREF	421
+#define	QRELDEF	422
+#define	CGCHAR	423
+#define	CBOOL	424
+#define	CINT	425
+#define	CGFLOAT	426
+#define	CDOUBLE	427
+#define	CVOID	428
+#define	QANYTYPE	429
+#define	QINTEGRALTYPE	430
+#define	QUNSIGNEDINTEGRALTYPE	431
+#define	QSIGNEDINTEGRALTYPE	432
+#define	QNULLTERMINATED	433
+#define	QSETBUFFERSIZE	434
+#define	QSETSTRINGLENGTH	435
+#define	QMAXSET	436
+#define	QMAXREAD	437
+#define	QTESTINRANGE	438
+#define	TCAND	439
+#define	IDENTIFIER	440
+#define	NEW_IDENTIFIER	441
+#define	TYPE_NAME_OR_ID	442
+#define	CANNOTATION	443
+#define	CCONSTANT	444
+#define	ITER_NAME	445
+#define	ITER_ENDNAME	446
+#define	TYPE_NAME	447
+#define	METASTATE_NAME	448
 
 
 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@*/