]> andersk Git - splint.git/blame - src/llgrammar.y
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Initial revision
[splint.git] / src / llgrammar.y
CommitLineData
885824d3 1/*;-*-C-*-;
2** Copyright (c) Massachusetts Institute of Technology 1994-1998.
3** All Rights Reserved.
4** Unpublished rights reserved under the copyright laws of
5** the United States.
6**
7** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
8** OR IMPLIED. ANY USE IS AT YOUR OWN RISK.
9**
10** This code is distributed freely and may be used freely under the
11** following conditions:
12**
13** 1. This notice may not be removed or altered.
14**
15** 2. Works derived from this code are not distributed for
16** commercial gain without explicit permission from MIT
17** (for permission contact lclint-request@sds.lcs.mit.edu).
18*/
19/*
20** Copyright (c) Massachusetts Institute of Technology, 1993
21** All Rights Reserved. Unpublished rights reserved
22** under the copyright laws of the United States.
23**++
24** FACILITY: LSLC
25**
26** MODULE DESCRIPTION:
27**
28** FILENAME: llgramar.y
29**
30** PURPOSE: bison grammar for LCL language.
31**
32** AUTHORS:
33** Yang Meng Tan, Massachusetts Institute of Technology
34*/
35
36%{
37
38# include "lclintMacros.nf"
39# include "llbasic.h"
40# include "lclscan.h"
41# include "checking.h"
42# include "lslparse.h"
43# include "lh.h"
44# include "usymtab_interface.h"
45
46/*@-noparams@*/
47static /*@unused@*/ void yyprint ();
48/*@=noparams@*/
49
50/*@-redecl@*/
51void ylerror (char *) /*@modifies *g_msgstream@*/ ;
52/*@=redecl@*/
53
54bool g_inTypeDef = FALSE;
55
56/*@constant int YYDEBUG;@*/
57# define YYDEBUG 1
58
59/*@notfunction@*/
60# define YYPRINT(file, type, value) yyprint (file, type, value)
61
62/*
63** This is necessary, or else when the bison-generated code #include's malloc.h,
64** there will be a parse error.
65**
66** Unfortunately, it means the error checking on malloc, etc. is lost for allocations
67** in bison-generated files under Win32.
68*/
69
70# ifdef WIN32
71# undef malloc
72# undef calloc
73# undef realloc
74# endif
75
76%}
77
78%union
79{
80 ltoken ltok; /* a leaf is also an ltoken */
81 qual typequal;
82 unsigned int count;
83 /*@only@*/ ltokenList ltokenList;
84 /*@only@*/ abstDeclaratorNode abstDecl;
85 /*@only@*/ declaratorNode declare;
86 /*@only@*/ declaratorNodeList declarelist;
87 /*@only@*/ typeExpr typeexpr;
88 /*@only@*/ arrayQualNode array;
89 /*@only@*/ quantifierNode quantifier;
90 /*@only@*/ quantifierNodeList quantifiers;
91 /*@only@*/ varNode var;
92 /*@only@*/ varNodeList vars;
93 /*@only@*/ storeRefNode storeref;
94 /*@only@*/ storeRefNodeList storereflist;
95 /*@only@*/ termNode term;
96 /*@only@*/ termNodeList termlist;
97 /*@only@*/ programNode program;
98 /*@only@*/ stmtNode stmt;
99 /*@only@*/ claimNode claim;
100 /*@only@*/ typeNode type;
101 /*@only@*/ iterNode iter;
102 /*@only@*/ fcnNode fcn;
103 /*@only@*/ fcnNodeList fcns;
104 /*@only@*/ letDeclNode letdecl;
105 /*@only@*/ letDeclNodeList letdecls;
106 /*@only@*/ lclPredicateNode lclpredicate;
107 /*@only@*/ modifyNode modify;
108 /*@only@*/ paramNode param;
109 /*@only@*/ paramNodeList paramlist;
110 /*@only@*/ declaratorInvNodeList declaratorinvs;
111 /*@only@*/ declaratorInvNode declaratorinv;
112 /*@only@*/ abstBodyNode abstbody;
113 /*@only@*/ abstractNode abstract;
114 /*@only@*/ exposedNode exposed;
115 /* taggedUnionNode taggedunion; */
116 /*@only@*/ globalList globals;
117 /*@only@*/ constDeclarationNode constdeclaration;
118 /*@only@*/ varDeclarationNode vardeclaration;
119 /*@only@*/ varDeclarationNodeList vardeclarationlist;
120 /*@only@*/ initDeclNodeList initdecls;
121 /*@only@*/ initDeclNode initdecl;
122 /*@only@*/ stDeclNodeList structdecls;
123 /*@only@*/ stDeclNode structdecl;
124 /*@only@*/ strOrUnionNode structorunion;
125 /*@only@*/ enumSpecNode enumspec;
126 /*@only@*/ lclTypeSpecNode lcltypespec;
127 /*@only@*/ typeNameNode typname;
128 /*@only@*/ opFormNode opform;
129 /*@only@*/ sigNode signature;
130 /*@only@*/ nameNode name;
131 /*@only@*/ typeNameNodeList namelist;
132 /*@only@*/ replaceNode replace;
133 /*@only@*/ replaceNodeList replacelist;
134 /*@only@*/ renamingNode renaming;
135 /*@only@*/ traitRefNode traitref;
136 /*@only@*/ traitRefNodeList traitreflist;
137 /*@only@*/ importNode import;
138 /*@only@*/ importNodeList importlist;
139 /*@only@*/ interfaceNode iface;
140 /*@only@*/ interfaceNodeList interfacelist;
141 /*@only@*/ CTypesNode ctypes;
142}
143
144/* Order of precedence is increasing going down the list */
145
146%left simpleOp
147%right PREFIX_OP
148%left POSTFIX_OP
149%left LLT_MULOP
150 /* as arithmetic binary operator, or as iteration construct in claims */
151%left LLT_SEMI
152%left LLT_VERTICALBAR
153%nonassoc ITERATION_OP /* two * cannot follow each other */
154%left LLT_LPAR LLT_LBRACKET selectSym
155 /* to allow mixing if-then-else with other kinds of terms */
156%left LLT_IF_THEN_ELSE
157%left logicalOp
158
159/* Note: the grammar parses b = p /\ q as (b = p) /\ q, that is,
160 = has higher precedence than logicalOp.
161 Reminder: = > logicalOp >= if_then_else > == (present in LSL) */
162
163/* Precedence of claim operators: ( > * > | >; (| and; left-assoc) */
164
165/* These are not needed in the grammar,
166 but needed in init files and lclscanline.c */
167
168%token <ltok> eqSepSym /* \eqsep */
169%token <ltok> equationSym /* \equals or == */
170%token <ltok> commentSym /* \comment */
171%token <ltok> LLT_WHITESPACE
172%token <ltok> LLT_EOL /*@-varuse@*/ /* yacc declares yytranslate here */
173/* used to bypass parsing problems in C types */
174%token <ltok> LLT_TYPEDEF_NAME /*@=varuse@*/
175
176/* LSL reserved extension symbols */
177
178%token <ltok> quantifierSym /* \forall */
179%token <ltok> logicalOp /* \implies, \and, \not, \or */
180%token <ltok> selectSym /* \select */
181%token <ltok> openSym /* \( */
182%token <ltok> closeSym /* \) */
183%token <ltok> sepSym /* \, */
184
185%token <ltok> simpleId /* \: id-char +, Ordinary Identifier */
186%token <ltok> mapSym /* \arrow, -> */
187%token <ltok> markerSym /* \marker, __ */
188%token <ltok> preSym /* \pre */
189%token <ltok> postSym /* \post */
190%token <ltok> anySym /* \any */
191
192/* Generic LSL operators */
193
194%token <ltok> simpleOp /* opSym - reserved */
195
196/* Reserved special symbols */
197
198%token <ltok> LLT_COLON /* : */
199%token <ltok> LLT_COMMA /* , */
200%token <ltok> LLT_EQUALS /* = */
201%token <ltok> LLT_LBRACE /* { */
202%token <ltok> LLT_RBRACE /* } */
203%token <ltok> LLT_LBRACKET /* [ */
204%token <ltok> LLT_RBRACKET /* ] */
205%token <ltok> LLT_LPAR /* ( */
206%token <ltok> LLT_RPAR /* ) */
207%token <ltok> LLT_QUOTE /* ' */
208%token <ltok> LLT_SEMI /*; */
209%token <ltok> LLT_VERTICALBAR /* | */
210
211/* C operator tokens and Combined C/LSL operator tokens */
212
213%token <ltok> eqOp /* \eq, \neq, ==, != */
214%token <ltok> LLT_MULOP /* * */
215
216/* LCL C literal tokens */
217
218%token <ltok> LLT_CCHAR
219%token <ltok> LLT_CFLOAT
220%token <ltok> LLT_CINTEGER
221%token <ltok> LLT_LCSTRING
222
223/* LCL reserved words */
224
225%token <ltok> LLT_ALL
226%token <ltok> LLT_ANYTHING
227%token <ltok> LLT_BE
228%token <ltok> LLT_BODY
229%token <ltok> LLT_CLAIMS
230%token <ltok> LLT_CHECKS
231%token <ltok> LLT_CONSTANT
232%token <ltok> LLT_ELSE
233%token <ltok> LLT_ENSURES
234%token <ltok> LLT_FOR
235%token <ltok> LLT_FRESH
236%token <ltok> LLT_IF
237%token <ltok> LLT_IMMUTABLE
238%token <ltok> LLT_IMPORTS
239%token <ltok> LLT_CONSTRAINT /* was INVARIANT */
240%token <ltok> LLT_ISSUB
241%token <ltok> LLT_LET
242%token <ltok> LLT_MODIFIES
243%token <ltok> LLT_MUTABLE
244%token <ltok> LLT_NOTHING
245%token <ltok> LLT_INTERNAL
246%token <ltok> LLT_FILESYS
247%token <ltok> LLT_OBJ
248%token <ltok> LLT_OUT
249%token <ltok> LLT_SEF
250%token <ltok> LLT_ONLY LLT_PARTIAL LLT_OWNED LLT_DEPENDENT LLT_KEEP LLT_KEPT LLT_TEMP
251%token <ltok> LLT_SHARED LLT_UNIQUE LLT_UNUSED
252%token <ltok> LLT_EXITS LLT_MAYEXIT LLT_NEVEREXIT LLT_TRUEEXIT LLT_FALSEEXIT
253%token <ltok> LLT_UNDEF LLT_KILLED
254%token <ltok> LLT_CHECKMOD LLT_CHECKED LLT_UNCHECKED LLT_CHECKEDSTRICT
255%token <ltok> LLT_TRUENULL
256%token <ltok> LLT_FALSENULL
257%token <ltok> LLT_LNULL
258%token <ltok> LLT_LNOTNULL
259%token <ltok> LLT_RETURNED
260%token <ltok> LLT_OBSERVER
261%token <ltok> LLT_EXPOSED
262%token <ltok> LLT_REFCOUNTED
263%token <ltok> LLT_REFS
264%token <ltok> LLT_RELNULL
265%token <ltok> LLT_RELDEF
266%token <ltok> LLT_KILLREF
267%token <ltok> LLT_TEMPREF
268%token <ltok> LLT_NEWREF
269%token <ltok> LLT_PRIVATE
270%token <ltok> LLT_REQUIRES
271%token <ltok> LLT_RESULT
272%token <ltok> LLT_SIZEOF
273%token <ltok> LLT_SPEC
274%token <ltok> LLT_TAGGEDUNION /* keep it for other parts of LCL checker */
275%token <ltok> LLT_THEN
276%token <ltok> LLT_TYPE
277%token <ltok> LLT_TYPEDEF
278%token <ltok> LLT_UNCHANGED
279%token <ltok> LLT_USES
280
281/* LCL C keywords */
282
283%token <ltok> LLT_CHAR
284%token <ltok> LLT_CONST
285%token <ltok> LLT_DOUBLE
286%token <ltok> LLT_ENUM
287%token <ltok> LLT_FLOAT
288%token <ltok> LLT_INT
289%token <ltok> LLT_ITER
290%token <ltok> LLT_YIELD
291%token <ltok> LLT_LONG
292%token <ltok> LLT_SHORT
293%token <ltok> LLT_SIGNED
294%token <ltok> LLT_UNKNOWN
295%token <ltok> LLT_STRUCT
296%token <ltok> LLT_TELIPSIS
297%token <ltok> LLT_UNION
298%token <ltok> LLT_UNSIGNED
299%token <ltok> LLT_VOID
300%token <ltok> LLT_VOLATILE
301
302%token <ltok> LLT_PRINTFLIKE LLT_SCANFLIKE LLT_MESSAGELIKE
303
304%type <interfacelist> interface externals optDeclarations declarations
305%type <iface> external declaration imports uses export private private2
306%type <type> type
307%type <fcn> fcn
308%type <fcns> fcns
309%type <claim> claim
310%type <iter> iter
311%type <vardeclaration> varDeclaration globalDecl privateInit
312%type <globals> globals
313%type <ltokenList> interfaceNameList traitIdList domain sortList
314%type <import> importName
315%type <importlist> importNameList
316%type <traitreflist> traitRefNodeList
317%type <traitref> traitRef
318%type <renaming> renaming
319%type <namelist> nameList
320%type <name> name
321%type <replacelist> replaceNodeList
322%type <replace> replace
323%type <opform> opForm
324%type <signature> signature
325%type <typname> typeName
326%type <count> middle placeList pointers
327%type <abstDecl> optAbstDeclarator
328%type <lcltypespec> lclTypeSpec lclType sortSpec
329%type <ltokenList> enumeratorList postfixOps
330%type <ctypes> CTypes typeSpecifier
331%type <structorunion> structOrUnionSpec
332%type <enumspec> enumSpec
333%type <declare> declarator
334%type <typeexpr> notype_decl after_type_decl abstDeclarator parameter_decl
335%type <declarelist> declaratorList
336%type <structdecls> structDecls
337%type <structdecl> structDecl
338%type <constdeclaration> constDeclaration
339%type <initdecls> initDecls
340%type <initdecl> initDecl
341%type <vardeclarationlist> privateInits
342%type <abstract> abstract
343%type <exposed> exposed
344%type <declaratorinvs> declaratorInvs
345%type <declaratorinv> declaratorInv
346%type <abstbody> abstBody optExposedBody
347%type <lclpredicate> optClaim optEnsure optRequire optChecks lclPredicate
348%type <lclpredicate> optTypeInv typeInv
349%type <modify> optModify
350%type <letdecls> optLetDecl beDeclList
351%type <letdecl> beDecl
352%type <term> term constLclExpr initializer value equalityTerm
353%type <term> simpleOpTerm prefixOpTerm secondary primary lclPrimary
354%type <term> bracketed sqBracketed matched term0 cLiteral
355%type <termlist> args infixOpPart valueList termList
356%type <program> optBody callExpr
357%type <stmt> stmt
358%type <storereflist> storeRefList
359%type <storeref> storeRef
360%type <var> quantified
361%type <vars> quantifiedList
362%type <quantifier> quantifier
363%type <quantifiers> quantifiers
364%type <array> arrayQual
365%type <paramlist> optParamList paramList realParamList iterParamList realIterParamList
366%type <param> param iterParam
367%type <ltok> open close anyOp separator simpleOp2 stateFcn
368%type <ltok> interfaceName
369%type <ltok> varId fcnId tagId claimId sortId traitId opId CType optTagId
370%type <ltok> simpleIdOrTypedefName
371%type <typequal> specialQualifier special
372
373/*
374** Conventions in calling static semantic routines:
375** The inputs are in strict order (in AST) as well as in the position of
376** the call to the static semantic routine.
377*/
378
379%%
380
381interface
382 : externals { lhExternals ($1); } optDeclarations
383 { interfaceNodeList_free ($1); interfaceNodeList_free ($3); }
384
385externals
386 : /* empty */ { $$ = interfaceNodeList_new (); }
387 | externals external { $$ = interfaceNodeList_addh ($1, $2);}
388
389external
390 : imports
391 | uses
392
393optDeclarations
394 : /* empty */ { $$ = interfaceNodeList_new (); }
395 | export declarations { $$ = consInterfaceNode ($1, $2);}
396 | private declarations { $$ = consInterfaceNode ($1, $2);}
397
398declarations
399 : /* empty */ { $$ = interfaceNodeList_new (); }
400 | declarations declaration { $$ = interfaceNodeList_addh ($1, $2);}
401
402declaration
403 : export
404 | private
405 | uses
406
407imports
408 : LLT_IMPORTS importNameList LLT_SEMI
409 { $$ = makeInterfaceNodeImports ($2);
410 /* assume subspecs are already processed, symbol table info in external file */
411 }
412
413uses
414 : LLT_USES traitRefNodeList LLT_SEMI
415 { $$ = makeInterfaceNodeUses ($2); readlsignatures ($$);}
416
417export
418 : constDeclaration
419 { declareConstant ($1); $$ = interfaceNode_makeConst ($1); }
420 | varDeclaration
421 { declareVar ($1); $$ = interfaceNode_makeVar ($1); }
422 | type
423 { declareType ($1); $$ = interfaceNode_makeType ($1); }
424 | fcn
425 { declareFcn ($1, typeId_invalid); $$ = interfaceNode_makeFcn ($1); }
426 | claim
427 { $$ = interfaceNode_makeClaim ($1); }
428 | iter
429 { declareIter ($1); $$ = interfaceNode_makeIter ($1); }
430
431iter
432 : LLT_ITER varId LLT_LPAR iterParamList LLT_RPAR LLT_SEMI
433 { $$ = makeIterNode ($2, $4); }
434
435iterParamList
436 : /* empty */ { $$ = paramNodeList_new (); }
437 | realIterParamList { $$ = $1; }
438
439realIterParamList
440 : iterParam
441 { $$ = paramNodeList_add (paramNodeList_new (), $1); }
442 | realIterParamList LLT_COMMA iterParam
443 { $$ = paramNodeList_add ($1,$3); }
444
445iterParam
446 : LLT_YIELD param { $$ = markYieldParamNode ($2); }
447 | param { $$ = $1; }
448
449private
450 : LLT_SPEC { symtable_export (g_symtab, FALSE); } private2
451 { $$ = $3; symtable_export (g_symtab, TRUE); }
452
453private2
454 : constDeclaration
455 { declarePrivConstant ($1); $$ = interfaceNode_makePrivConst ($1); }
456 | varDeclaration
457 { declarePrivVar ($1); $$ = interfaceNode_makePrivVar ($1); }
458 | type
459 { declarePrivType ($1); $$ = interfaceNode_makePrivType ($1); }
460 | fcn
461 { declarePrivFcn ($1, typeId_invalid); $$ = interfaceNode_makePrivFcn ($1); }
462
463constDeclaration
464 : LLT_CONSTANT lclTypeSpec initDecls LLT_SEMI
465 { $$ = makeConstDeclarationNode ($2, $3); }
466
467varDeclaration
468 : lclTypeSpec initDecls LLT_SEMI
469 { $$ = makeVarDeclarationNode ($1, $2, FALSE, FALSE); $$->qualifier = QLF_NONE; }
470 | LLT_CONST lclTypeSpec initDecls LLT_SEMI
471 { $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_CONST; }
472 | LLT_VOLATILE lclTypeSpec initDecls LLT_SEMI
473 { $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_VOLATILE; }
474
475type
476 : abstract { $$ = makeAbstractTypeNode ($1); }
477 | exposed { $$ = makeExposedTypeNode ($1); }
478
479special
480 : LLT_PRINTFLIKE { $$ = qual_createPrintfLike (); }
481 | LLT_SCANFLIKE { $$ = qual_createScanfLike (); }
482 | LLT_MESSAGELIKE { $$ = qual_createMessageLike (); }
483
484fcn
485 : lclTypeSpec declarator globals { enteringFcnScope ($1, $2, $3); } LLT_LBRACE
486 privateInits optLetDecl optChecks optRequire optModify optEnsure optClaim LLT_RBRACE
487 { $$ = makeFcnNode (qual_createUnknown (), $1, $2, $3, $6, $7,
488 $8, $9, $10, $11, $12);
489 /* type, declarator, glovbls, privateinits,
490 lets, checks, requires, modifies, ensures, claims */
491 symtable_exitScope (g_symtab);
492 }
493 | special lclTypeSpec declarator globals { enteringFcnScope ($2, $3, $4); }
494 LLT_LBRACE
495 privateInits optLetDecl optChecks optRequire optModify optEnsure optClaim
496 LLT_RBRACE
497 { $$ = makeFcnNode ($1, $2, $3, $4, $7,
498 $8, $9, $10, $11, $12, $13);
499 /* type, declarator, glovbls, privateinits,
500 lets, checks, requires, modifies, ensures, claims */
501 symtable_exitScope (g_symtab);
502 }
503
504
505claim
506 : LLT_CLAIMS claimId LLT_LPAR optParamList LLT_RPAR globals
507 { enteringClaimScope ($4, $6); }
508 LLT_LBRACE optLetDecl optRequire optBody optEnsure LLT_RBRACE
509 { $$ = makeClaimNode ($2, $4, $6, $9, $10, $11, $12);
510 symtable_exitScope (g_symtab); }
511 | LLT_CLAIMS fcnId claimId LLT_SEMI
512 { $$ = (claimNode) 0; }
513
514abstract
515 : LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
516 { $$ = makeAbstractNode ($1, $4, TRUE, FALSE, $6); }
517 | LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_REFCOUNTED LLT_TYPE
518 LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
519 { $$ = makeAbstractNode ($1, $5, TRUE, TRUE, $7); }
520 | LLT_REFCOUNTED LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_TYPE
521 LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
522 { $$ = makeAbstractNode ($2, $5, TRUE, TRUE, $7); }
523 | LLT_IMMUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
524 { $$ = makeAbstractNode ($1, $4, FALSE, FALSE, $6); }
525
526exposed
527 : LLT_TYPEDEF lclTypeSpec { g_inTypeDef = TRUE; setExposedType ($2); } declaratorInvs
528 { g_inTypeDef = FALSE; } LLT_SEMI
529 { $$ = makeExposedNode ($1, $2, $4); /* to support mutually recursive types */ }
530 | structOrUnionSpec LLT_SEMI
531 { $$ = makeExposedNode ($2, makeLclTypeSpecNodeSU ($1), declaratorInvNodeList_new ()); }
532 | enumSpec LLT_SEMI
533 { $$ = makeExposedNode ($2, makeLclTypeSpecNodeEnum ($1), declaratorInvNodeList_new ()); }
534
535/* evs - 26 Feb 1995 (changed to be consistent with C grammar)
536 | STRUCT tagId LLT_SEMI
537 { (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy ($2));
538 lhForwardStruct ($2); $$ = (exposedNode)0;
539 }
540 | UNION tagId LLT_SEMI
541 { (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy ($2));
542 lhForwardUnion ($2);
543 $$ = (exposedNode)0;
544 }
545*/
546
547importNameList
548 : importName
549 { $$ = importNodeList_add (importNodeList_new (), $1); }
550 | importNameList LLT_COMMA importName
551 { $$ = importNodeList_add ($1, $3); }
552
553importName
554 : interfaceName { $$ = importNode_makePlain ($1); }
555 | simpleOp interfaceName simpleOp
556 { checkBrackets ($1, $3); $$ = importNode_makeBracketed ($2); }
557 | LLT_LCSTRING { $$ = importNode_makeQuoted ($1); }
558
559interfaceNameList
560 : interfaceName { $$ = ltokenList_singleton ($1); }
561 | interfaceNameList LLT_COMMA interfaceName { $$ = ltokenList_push ($1, $3); }
562
563interfaceName
564 : simpleIdOrTypedefName
565 /* to allow module names to be the same as LCL type names */
566
567traitRefNodeList
568 : traitRef
569 { $$ = traitRefNodeList_add (traitRefNodeList_new (), $1); }
570 | traitRefNodeList LLT_COMMA traitRef
571 { $$ = traitRefNodeList_add ($1, $3); }
572
573traitRef
574 : traitId
575 { $$ = makeTraitRefNode (ltokenList_singleton ($1), (renamingNode)0); }
576 | traitId LLT_LPAR renaming LLT_RPAR
577 { $$ = makeTraitRefNode (ltokenList_singleton ($1), $3); }
578 | LLT_LPAR traitIdList LLT_RPAR
579 { $$ = makeTraitRefNode ($2, (renamingNode)0); }
580 | LLT_LPAR traitIdList LLT_RPAR LLT_LPAR renaming LLT_RPAR
581 { $$ = makeTraitRefNode ($2, $5); }
582
583traitIdList
584 : traitId { $$ = ltokenList_singleton ($1); }
585 | traitIdList LLT_COMMA traitId { $$ = ltokenList_push ($1, $3); }
586
587renaming
588 : replaceNodeList
589 { $$ = makeRenamingNode (typeNameNodeList_new (), $1); }
590 | nameList
591 { $$ = makeRenamingNode ($1, replaceNodeList_new ()); }
592 | nameList LLT_COMMA replaceNodeList { $$ = makeRenamingNode ($1, $3); }
593
594nameList
595 : typeName
596 { $$ = typeNameNodeList_add (typeNameNodeList_new (), $1); }
597 | nameList LLT_COMMA typeName { $$ = typeNameNodeList_add ($1, $3); }
598
599replaceNodeList
600 : replace
601 { $$ = replaceNodeList_add (replaceNodeList_new (), $1); }
602 | replaceNodeList LLT_COMMA replace { $$ = replaceNodeList_add ($1, $3); }
603
604replace
605 : typeName LLT_FOR CType { $$ = makeReplaceNode ($2, $1, TRUE, $3, NULL, NULL); }
606 | typeName LLT_FOR name { $$ = makeReplaceNameNode ($2, $1, $3); }
607 | typeName LLT_FOR name signature { $$ = makeReplaceNode ($2, $1, FALSE, ltoken_undefined,
608 $3, $4); }
609
610name
611 : opId { $$ = makeNameNodeId ($1); }
612 | opForm { $$ = makeNameNodeForm ($1); }
613
614initializer : constLclExpr
615
616constLclExpr : term
617
618initDecls
619 : initDecl
620 { $$ = initDeclNodeList_add (initDeclNodeList_new (), $1); }
621 | initDecls LLT_COMMA initDecl
622 { $$ = initDeclNodeList_add ($1, $3); }
623
624initDecl
625 : declarator { $$ = makeInitDeclNode ($1, (termNode)0); }
626 | declarator LLT_EQUALS initializer { $$ = makeInitDeclNode ($1, $3); }
627
628globals
629 : /* empty */ /* has the same structure */
630 { $$ = varDeclarationNodeList_new (); }
631 | globals globalDecl
632 { varDeclarationNodeList_addh ($1, $2); $$ = $1; }
633
634globalDecl
635 : lclTypeSpec initDecls LLT_SEMI { $$ = makeVarDeclarationNode ($1, $2, TRUE, FALSE); }
636 | LLT_INTERNAL LLT_SEMI { $$ = makeInternalStateNode (); }
637 | LLT_FILESYS LLT_SEMI { $$ = makeFileSystemNode (); }
638
639privateInits
640 : /* empty */ { $$ = varDeclarationNodeList_new (); }
641 | privateInits privateInit { varDeclarationNodeList_addh ($1, $2); $$ = $1; }
642
643privateInit
644 : LLT_PRIVATE lclTypeSpec initDecls LLT_SEMI
645 { $$ = makeVarDeclarationNode ($2, $3, FALSE, TRUE); }
646
647optLetDecl
648 : /* empty */ { $$ = letDeclNodeList_new (); }
649 | LLT_LET beDeclList LLT_SEMI { $$ = $2; }
650
651beDeclList
652 : beDecl { $$ = letDeclNodeList_add (letDeclNodeList_new (), $1); }
653 | beDeclList LLT_COMMA beDecl { $$ = letDeclNodeList_add ($1, $3); }
654
655beDecl
656 : varId LLT_COLON sortSpec LLT_BE term { $$ = makeLetDeclNode ($1, $3, $5); }
657 | varId LLT_BE term { $$ = makeLetDeclNode ($1, (lclTypeSpecNode)0, $3); }
658
659sortSpec : lclTypeSpec
660
661optChecks
662 : /* empty */ { $$ = (lclPredicateNode)0; }
663 | LLT_CHECKS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeChecksNode ($1, $2); }
664
665optRequire
666 : /* empty */ { $$ = (lclPredicateNode)0; }
667 | LLT_REQUIRES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeRequiresNode ($1, $2);}
668
669optModify
670 : /* empty */ { $$ = (modifyNode)0; }
671 | LLT_MODIFIES LLT_NOTHING LLT_SEMI { $$ = makeModifyNodeSpecial ($1, TRUE); }
672 | LLT_MODIFIES LLT_ANYTHING LLT_SEMI { $$ = makeModifyNodeSpecial ($1, FALSE); }
673 | LLT_MODIFIES storeRefList LLT_SEMI { $$ = makeModifyNodeRef ($1, $2); }
674
675storeRefList
676 : storeRef { $$ = storeRefNodeList_add (storeRefNodeList_new (), $1); }
677 | storeRefList LLT_COMMA storeRef { $$ = storeRefNodeList_add ($1, $3); }
678
679storeRef
680 : term { $$ = makeStoreRefNodeTerm ($1); }
681 | lclType { $$ = makeStoreRefNodeType ($1, FALSE); }
682 | LLT_OBJ lclType { $$ = makeStoreRefNodeType ($2, TRUE); }
683 | LLT_INTERNAL { $$ = makeStoreRefNodeInternal (); }
684 | LLT_FILESYS { $$ = makeStoreRefNodeSystem (); }
685
686optEnsure
687 : /* empty */ { $$ = (lclPredicateNode)0; }
688 | LLT_ENSURES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeEnsuresNode ($1, $2);}
689
690optClaim
691 : /* empty */ { $$ = (lclPredicateNode)0; }
692 | LLT_CLAIMS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeIntraClaimNode ($1, $2);}
693
694optParamList
695 : /* empty */ { $$ = paramNodeList_new (); }
696 | realParamList { $$ = $1; }
697
698realParamList
699 : paramList
700 | LLT_TELIPSIS { $$ = paramNodeList_add (paramNodeList_new (), paramNode_elipsis ()); }
701 | paramList LLT_COMMA LLT_TELIPSIS { $$ = paramNodeList_add ($1, paramNode_elipsis ()); }
702
703paramList
704 : param { $$ = paramNodeList_single ($1); }
705 | paramList LLT_COMMA param { $$ = paramNodeList_add ($1, $3); }
706
707optBody
708 : /* empty */ { $$ = (programNode)0; }
709 | LLT_BODY LLT_LBRACE callExpr LLT_RBRACE { $$ = $3; }
710 | LLT_BODY LLT_LBRACE callExpr LLT_SEMI LLT_RBRACE { $$ = $3; }
711
712callExpr
713 : stmt { $$ = makeProgramNode ($1); }
714 | LLT_LPAR callExpr LLT_RPAR
715 /* may need to make a copy of $2 */
716 { $$ = $2; $$->wrapped = $$->wrapped + 1; }
717 | callExpr LLT_MULOP %prec ITERATION_OP
718 { programNodeList x = programNodeList_new ();
719 programNodeList_addh (x, $1);
720 $$ = makeProgramNodeAction (x, ACT_ITER);
721 }
722 | callExpr LLT_VERTICALBAR callExpr
723 { programNodeList x = programNodeList_new ();
724 programNodeList_addh (x, $1);
725 programNodeList_addh (x, $3);
726 $$ = makeProgramNodeAction (x, ACT_ALTERNATE);
727 }
728 | callExpr LLT_SEMI callExpr
729 { programNodeList x = programNodeList_new ();
730 programNodeList_addh (x, $1);
731 programNodeList_addh (x, $3);
732 $$ = makeProgramNodeAction (x, ACT_SEQUENCE);
733 }
734
735stmt
736 : fcnId LLT_LPAR valueList LLT_RPAR
737 { $$ = makeStmtNode (ltoken_undefined, $1, $3); }
738 | fcnId LLT_LPAR LLT_RPAR
739 { $$ = makeStmtNode (ltoken_undefined, $1, termNodeList_new ()); }
740 | varId LLT_EQUALS fcnId LLT_LPAR LLT_RPAR
741 { $$ = makeStmtNode ($1, $3, termNodeList_new ()); }
742 | varId LLT_EQUALS fcnId LLT_LPAR valueList LLT_RPAR
743 { $$ = makeStmtNode ($1, $3, $5); }
744
745valueList
746 : value { $$ = termNodeList_push (termNodeList_new (), $1); }
747 | valueList LLT_COMMA value { $$ = termNodeList_push ($1, $3); }
748
749value
750 : cLiteral
751 | varId { $$ = makeSimpleTermNode ($1); }
752 | simpleOp value %prec PREFIX_OP { $$ = makePrefixTermNode ($1, $2); }
753 | value simpleOp %prec POSTFIX_OP { $$ = makePostfixTermNode2 ($1, $2); }
754 | value simpleOp value /* infix */ { $$ = makeInfixTermNode ($1, $2, $3); }
755 | LLT_LPAR value LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
756 | fcnId LLT_LPAR LLT_RPAR
757 { $$ = makeOpCallTermNode ($1, $2, termNodeList_new (), $3); }
758 | fcnId LLT_LPAR valueList LLT_RPAR
759 { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
760
761abstBody
762 : LLT_SEMI { $$ = (abstBodyNode)0; }
763 | LLT_LBRACE fcns LLT_RBRACE { $$ = makeAbstBodyNode ($1, $2); }
764 | LLT_LBRACE interfaceNameList LLT_RBRACE LLT_SEMI { $$ = makeAbstBodyNode2 ($1, $2); }
765 | LLT_LBRACE LLT_RBRACE LLT_SEMI { $$ = (abstBodyNode)0; }
766
767fcns
768 : /* empty */ { $$ = fcnNodeList_new (); }
769 | fcns fcn { $$ = fcnNodeList_add ($1, $2); }
770
771optTypeInv
772 : /* empty */ { $$ = (lclPredicateNode)0; }
773 | typeInv
774
775typeInv
776 : LLT_CONSTRAINT { g_inTypeDef = FALSE; } quantifier LLT_LPAR lclPredicate LLT_RPAR
777 { $5->tok = $1; $5->kind = LPD_CONSTRAINT;
778 checkLclPredicate ($1, $5);
779 $$ = $5;
780 symtable_exitScope (g_symtab);
781 g_inTypeDef = TRUE;
782 }
783
784declaratorInvs
785 : declaratorInv { $$ = declaratorInvNodeList_add (declaratorInvNodeList_new (), $1); }
786 | declaratorInvs LLT_COMMA declaratorInv
787 { $$ = declaratorInvNodeList_add ($1, $3); }
788
789declaratorInv
790 : declarator { declareForwardType ($1); } optExposedBody
791 { $$ = makeDeclaratorInvNode ($1, $3); }
792
793optExposedBody
794 : /* empty */ { $$ = (abstBodyNode)0; }
795 | LLT_LBRACE optTypeInv LLT_RBRACE { $$ = makeExposedBodyNode ($1, $2); }
796
797CType
798 : LLT_VOID { $$ = $1; ltoken_setIntField ($$, fixBits (TS_VOID, 0)); }
799 | LLT_CHAR { $$ = $1; ltoken_setIntField ($$, fixBits (TS_CHAR, 0)); }
800 | LLT_DOUBLE { $$ = $1; ltoken_setIntField ($$, fixBits (TS_DOUBLE, 0)); }
801 | LLT_FLOAT { $$ = $1; ltoken_setIntField ($$, fixBits (TS_FLOAT, 0)); }
802 | LLT_INT { $$ = $1; ltoken_setIntField ($$, fixBits (TS_INT, 0)); }
803 | LLT_LONG { $$ = $1; ltoken_setIntField ($$, fixBits (TS_LONG, 0)); }
804 | LLT_SHORT { $$ = $1; ltoken_setIntField ($$, fixBits (TS_SHORT, 0)); }
805 | LLT_SIGNED { $$ = $1; ltoken_setIntField ($$, fixBits (TS_SIGNED, 0)); }
806 | LLT_UNSIGNED { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNSIGNED, 0)); }
807 | LLT_UNKNOWN { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNKNOWN, 0)); }
808
809/*
810** CTypes allow "unsigned short int" but we drop all C type qualifiers
811** and storage class except TYPEDEF
812*/
813
814CTypes
815 : CType { $$ = makeCTypesNode ((CTypesNode)0, $1); }
816 | CTypes CType { $$ = makeCTypesNode ($1, $2); }
817
818/* Add abstract type names and typedef names */
819
820typeSpecifier
821 : LLT_TYPEDEF_NAME
822 { $$ = makeTypeSpecifier ($1); }
823 | CTypes
824 { $$ = $1; $$->sort = sort_lookupName (lclctype_toSort ($1->intfield)); }
825
826/* Add struct and enum types */
827
828specialQualifier
829 : LLT_OUT { $$ = qual_createOut (); }
830 | LLT_UNUSED { $$ = qual_createUnused (); }
831 | LLT_SEF { $$ = qual_createSef (); }
832 | LLT_ONLY { $$ = qual_createOnly (); }
833 | LLT_OWNED { $$ = qual_createOwned (); }
834 | LLT_DEPENDENT { $$ = qual_createDependent (); }
835 | LLT_KEEP { $$ = qual_createKeep (); }
836 | LLT_KEPT { $$ = qual_createKept (); }
837 | LLT_OBSERVER { $$ = qual_createObserver (); }
838 | LLT_EXITS { $$ = qual_createExits (); }
839 | LLT_MAYEXIT { $$ = qual_createMayExit (); }
840 | LLT_TRUEEXIT { $$ = qual_createTrueExit (); }
841 | LLT_FALSEEXIT { $$ = qual_createFalseExit (); }
842 | LLT_NEVEREXIT { $$ = qual_createNeverExit (); }
843 | LLT_TEMP { $$ = qual_createOnly (); }
844 | LLT_SHARED { $$ = qual_createShared (); }
845 | LLT_UNIQUE { $$ = qual_createUnique (); }
846 | LLT_CHECKED { $$ = qual_createChecked (); }
847 | LLT_UNCHECKED { $$ = qual_createUnchecked (); }
848 | LLT_CHECKEDSTRICT { $$ = qual_createCheckedStrict (); }
849 | LLT_TRUENULL { $$ = qual_createTrueNull (); }
850 | LLT_FALSENULL { $$ = qual_createFalseNull (); }
851 | LLT_RELNULL { $$ = qual_createRelNull (); }
852 | LLT_RELDEF { $$ = qual_createRelDef (); }
853 | LLT_REFCOUNTED{ $$ = qual_createRefCounted (); }
854 | LLT_REFS { $$ = qual_createRefs (); }
855 | LLT_NEWREF { $$ = qual_createNewRef (); }
856 | LLT_KILLREF { $$ = qual_createKillRef (); }
857 | LLT_LNULL { $$ = qual_createNull (); }
858 | LLT_LNOTNULL { $$ = qual_createNotNull (); }
859 | LLT_RETURNED { $$ = qual_createReturned (); }
860 | LLT_EXPOSED { $$ = qual_createExposed (); }
861 | LLT_PARTIAL { $$ = qual_createPartial (); }
862 | LLT_UNDEF { $$ = qual_createUndef (); }
863 | LLT_KILLED { $$ = qual_createKilled (); }
864
865lclTypeSpec
866 : typeSpecifier
867 { $$ = makeLclTypeSpecNodeType ($1); } /* does not process CONST at all */
868 | structOrUnionSpec
869 { $$ = makeLclTypeSpecNodeSU ($1); }
870 | enumSpec
871 { $$ = makeLclTypeSpecNodeEnum ($1); }
872 | specialQualifier lclTypeSpec
873 { $$ = lclTypeSpecNode_addQual ($2, $1); }
874 | LLT_VERTICALBAR lclType LLT_COLON lclType LLT_VERTICALBAR
875 { $$ = makeLclTypeSpecNodeConj ($2, $4); }
876
877/*
878** Add pointers to the right, only used in StoreRef, maybe should throw
879** out and replace its use in StoreRef by CTypeName
880*/
881
882lclType
883 : lclTypeSpec
884 | lclTypeSpec pointers
885 { llassert (lclTypeSpecNode_isDefined ($1));
886 $1->pointers = $2; $$ = $1; }
887
888pointers
889 : LLT_MULOP { $$ = 1; }
890 | pointers LLT_MULOP { $$ = $1 + 1; }
891
892structOrUnionSpec
893 : LLT_STRUCT optTagId
894 { (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy ($2)); }
895 LLT_LBRACE structDecls LLT_RBRACE
896 { $$ = makestrOrUnionNode ($1, SU_STRUCT, $2, $5); }
897 | LLT_UNION optTagId
898 { (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy ($2)); }
899 LLT_LBRACE structDecls LLT_RBRACE
900 { $$ = makestrOrUnionNode ($1, SU_UNION, $2, $5); }
901 | LLT_STRUCT tagId
902 { $$ = makeForwardstrOrUnionNode ($1, SU_STRUCT, $2); }
903 | LLT_UNION tagId
904 { $$ = makeForwardstrOrUnionNode ($1, SU_UNION, $2); }
905
906optTagId
907 : /* empty */ { $$ = ltoken_undefined; }
908 | tagId
909
910structDecls
911 : structDecl { $$ = stDeclNodeList_add (stDeclNodeList_new (), $1); }
912 | structDecls structDecl { $$ = stDeclNodeList_add ($1, $2); }
913
914/* We don't allow specification of field size */
915
916structDecl
917 : lclTypeSpec declaratorList LLT_SEMI { $$ = makestDeclNode ($1, $2); }
918
919declaratorList
920 : declarator
921 { $$ = declaratorNodeList_add (declaratorNodeList_new (), $1); }
922 | declaratorList LLT_COMMA declarator
923 { $$ = declaratorNodeList_add ($1, $3); }
924
925optCOMMA
926 : /* empty */ { ; }
927 | LLT_COMMA { ; }
928
929enumSpec
930 : LLT_ENUM optTagId LLT_LBRACE enumeratorList optCOMMA LLT_RBRACE
931 { $$ = makeEnumSpecNode ($1, $2, $4); }
932 | LLT_ENUM tagId
933 { $$ = makeEnumSpecNode2 ($1, $2); }
934
935enumeratorList
936 : simpleId { $$ = ltokenList_singleton ($1); }
937 | enumeratorList LLT_COMMA simpleId { $$ = ltokenList_push ($1, $3); }
938
939/* This part of declarator rules is adapted from GCC (2.2.1)'s C grammar */
940
941/* An after_type_decl is a declarator that is allowed only after an explicit
942 typeSpecifier, an id can be typedef'd here.
943 A notype_decl is a declarator that may not have seen a typeSpecifier
944 preceding it; it cannot typedef'd an id. */
945
946declarator
947 : after_type_decl { $$ = makeDeclaratorNode ($1); }
948 | notype_decl { $$ = makeDeclaratorNode ($1); }
949
950notype_decl
951 : varId { $$ = makeTypeExpr ($1); }
952 | LLT_LPAR notype_decl LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
953 | LLT_MULOP notype_decl { $$ = makePointerNode ($1, $2); }
954 | notype_decl arrayQual { $$ = makeArrayNode ($1, $2); }
955 | notype_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
956 | notype_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
957
958after_type_decl
959 : LLT_TYPEDEF_NAME { $$ = makeTypeExpr ($1); }
960 | LLT_LPAR after_type_decl LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
961 | LLT_MULOP after_type_decl { $$ = makePointerNode ($1, $2); }
962 | after_type_decl arrayQual { $$ = makeArrayNode ($1, $2); }
963 | after_type_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
964 | after_type_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
965
966/* A parameter_decl is a decl that can appear in a parameter list.
967 We disallow the old C way of giving only the id names without types.
968 A parameter_decl is like an after_type_decl except that it does not
969 allow a TYPEDEF_NAME to appear in parens. It will conflict with a
970 a function with that typedef as an argument */
971
972parameter_decl
973 : LLT_TYPEDEF_NAME { $$ = makeTypeExpr ($1); }
974 | LLT_MULOP parameter_decl /* %prec UNARY */ { $$ = makePointerNode ($1, $2); }
975 | parameter_decl arrayQual { $$ = makeArrayNode ($1, $2); }
976 | parameter_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
977 | parameter_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
978
979/* param : the last production allows C types to be generated without the
980 parameter name */
981
982param
983 : lclTypeSpec parameter_decl { $$ = makeParamNode ($1, $2); }
984 | lclTypeSpec notype_decl { $$ = makeParamNode ($1, $2); }
985 | lclTypeSpec optAbstDeclarator { $$ = makeParamNode ($1, $2); }
986/*
987** | OUT lclTypeSpec parameter_decl { $$ = makeOutParamNode ($1, $2, $3); }
988** | OUT lclTypeSpec notype_decl { $$ = makeOutParamNode ($1, $2, $3); }
989** | OUT lclTypeSpec optAbstDeclarator { $$ = makeOutParamNode ($1, $2, $3); }
990*/
991
992/* typeName is only used in trait parameter renaming */
993
994typeName
995 : lclTypeSpec optAbstDeclarator { $$ = makeTypeNameNode (FALSE, $1, $2); }
996 | LLT_OBJ lclTypeSpec optAbstDeclarator { $$ = makeTypeNameNode (TRUE, $2, $3); }
997 | opForm { $$ = makeTypeNameNodeOp ($1); }
998
999/* Abstract declarator is like a declarator, but with no identifier */
1000
1001optAbstDeclarator
1002 : /* empty */ { $$ = (abstDeclaratorNode)0; }
1003 | abstDeclarator { $$ = (abstDeclaratorNode)$1; }
1004
1005abstDeclarator
1006 : LLT_LPAR abstDeclarator LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
1007 | LLT_MULOP abstDeclarator { $$ = makePointerNode ($1, $2); }
1008 | LLT_MULOP { $$ = makePointerNode ($1, (typeExpr)0); }
1009 | arrayQual { $$ = makeArrayNode ((typeExpr)0, $1); }
1010 | abstDeclarator arrayQual { $$ = makeArrayNode ($1, $2); }
1011 | abstDeclarator LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
1012 | LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ((typeExpr)0, $2); }
1013 | abstDeclarator LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
1014
1015arrayQual
1016 : LLT_LBRACKET LLT_RBRACKET { $$ = makeArrayQualNode ($1, (termNode)0); }
1017 | LLT_LBRACKET constLclExpr LLT_RBRACKET { $$ = makeArrayQualNode ($1, $2); }
1018
1019opForm
1020 : LLT_IF markerSym LLT_THEN markerSym LLT_ELSE markerSym
1021 { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); }
1022 | anyOp
1023 { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); }
1024 | markerSym anyOp
1025 { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); }
1026 | anyOp markerSym
1027 { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); }
1028 | markerSym anyOp markerSym
1029 { $$ = makeOpFormNode ($1, OPF_MANYOPM,
1030 opFormUnion_createAnyOp ($2), ltoken_undefined); }
1031 | open middle close
1032 { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); }
1033 | markerSym open middle close
1034 { $$ = makeOpFormNode ($1, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); }
1035 | open middle close markerSym
1036 { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); }
1037 | markerSym open middle close markerSym
1038 { $$ = makeOpFormNode ($2, OPF_MMIDDLEM, opFormUnion_createMiddle ($3), $4); }
1039 | LLT_LBRACKET middle LLT_RBRACKET
1040 { $$ = makeOpFormNode ($1, OPF_BMIDDLE, opFormUnion_createMiddle ($2), $3); }
1041 | LLT_LBRACKET middle LLT_RBRACKET markerSym
1042 { $$ = makeOpFormNode ($1, OPF_BMIDDLEM, opFormUnion_createMiddle ($2), $3); }
1043
1044 /* added the next 6 productions (wrt old checker) to complete LSL grammar
1045 ** LSL treats '[' and '{' as openSym but LCL treats them as LLT_LBRACKET and
1046 ** LLT_LBRACE, and hence the need for these separate productions
1047 */
1048
1049 | markerSym LLT_LBRACKET middle LLT_RBRACKET
1050 { $$ = makeOpFormNode ($2, OPF_BMMIDDLE, opFormUnion_createMiddle ($3), $4); }
1051 | markerSym LLT_LBRACKET middle LLT_RBRACKET markerSym
1052 { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM, opFormUnion_createMiddle ($3), $4); }
1053 | selectSym simpleIdOrTypedefName
1054 { $$ = makeOpFormNode ($1, OPF_SELECT,
1055 opFormUnion_createAnyOp ($2), ltoken_undefined); }
1056 | mapSym simpleIdOrTypedefName
1057 { $$ = makeOpFormNode ($1, OPF_MAP,
1058 opFormUnion_createAnyOp ($2), ltoken_undefined); }
1059 | markerSym selectSym simpleIdOrTypedefName
1060 { $$ = makeOpFormNode ($1, OPF_MSELECT,
1061 opFormUnion_createAnyOp ($3), ltoken_undefined); }
1062 | markerSym mapSym simpleIdOrTypedefName
1063 { $$ = makeOpFormNode ($1, OPF_MMAP,
1064 opFormUnion_createAnyOp ($3), ltoken_undefined); }
1065
1066open
1067 : openSym
1068 | LLT_LBRACE
1069
1070close
1071 : closeSym
1072 | LLT_RBRACE
1073
1074anyOp
1075 : simpleOp2
1076 | logicalOp
1077 | eqOp
1078
1079middle
1080 : /* empty */ { $$ = 0; }
1081 | placeList
1082
1083placeList
1084 : markerSym { $$ = 1; }
1085 | placeList separator markerSym { $$ = $1 + 1; }
1086
1087separator
1088 : LLT_COMMA
1089 | sepSym
1090
1091signature
1092 : LLT_COLON domain mapSym sortId { $$ = makesigNode ($1, $2, $4); }
1093
1094domain
1095 : /* empty */ { $$ = ltokenList_new (); }
1096 | sortList
1097
1098sortList
1099 : sortId { $$ = ltokenList_singleton ($1); }
1100 | sortList LLT_COMMA sortId { $$ = ltokenList_push ($1, $3); }
1101
1102lclPredicate
1103 : term { $$ = makeLclPredicateNode (ltoken_undefined, $1, LPD_PLAIN);}
1104
1105term
1106 : term0 { $$ = checkSort ($1); }
1107
1108/* When "if <term> then <term> else <term> . <logicalOp> <term>"
1109 shift instead of reduce */
1110
1111term0
1112 : LLT_IF term0 LLT_THEN term0 LLT_ELSE term0 %prec LLT_IF_THEN_ELSE
1113 { $$ = makeIfTermNode ($1,$2,$3,$4,$5,$6); }
1114 | equalityTerm
1115 | term0 logicalOp term0 { $$ = makeInfixTermNode ($1, $2, $3); }
1116
1117equalityTerm
1118 : simpleOpTerm /* was | quantifiers LLT_LPAR term LLT_RPAR */
1119 | quantifiers LLT_LPAR lclPredicate LLT_RPAR
1120 /* temp fix, should change interface in future, add lclPredicateKind too */
1121 { checkLclPredicate ($2, $3); $$ = makeQuantifiedTermNode ($1, $2, $3->predicate, $4);
1122 symtable_exitScope (g_symtab);
1123 }
1124 | simpleOpTerm eqOp simpleOpTerm
1125 { $$ = makeInfixTermNode ($1, $2, $3);}
1126 | simpleOpTerm LLT_EQUALS simpleOpTerm
1127 { $$ = makeInfixTermNode ($1, $2, $3);}
1128
1129simpleOpTerm
1130 : prefixOpTerm
1131 | secondary postfixOps { $$ = makePostfixTermNode ($1, $2); }
1132 | secondary infixOpPart { $$ = CollapseInfixTermNode ($1, $2); }
1133
1134simpleOp2
1135 : simpleOp
1136 | LLT_MULOP
1137
1138prefixOpTerm
1139 : secondary
1140 | simpleOp2 prefixOpTerm { $$ = makePrefixTermNode ($1, $2); }
1141
1142postfixOps
1143 : simpleOp2 { $$ = ltokenList_singleton ($1); }
1144 | postfixOps simpleOp2 { $$ = ltokenList_push ($1, $2); }
1145
1146infixOpPart
1147 : simpleOp2 secondary { $$ = pushInfixOpPartNode (termNodeList_new (), $1, $2); }
1148 | infixOpPart simpleOp2 secondary { $$ = pushInfixOpPartNode ($1, $2, $3); }
1149
1150secondary
1151 : primary
1152 | bracketed { $$ = computePossibleSorts ($1); }
1153 | bracketed primary { $$ = updateMatchedNode ((termNode)0, $1, $2); }
1154 | primary bracketed { $$ = updateMatchedNode ($1, $2, (termNode)0); }
1155 | primary bracketed primary { $$ = updateMatchedNode ($1, $2, $3); }
1156 | sqBracketed { $$ = computePossibleSorts ($1); }
1157 | sqBracketed primary { $$ = updateSqBracketedNode ((termNode)0, $1, $2); }
1158
1159bracketed
1160 : matched LLT_COLON sortId { $$ = $1; $$->sort = sort_lookupName (ltoken_getText ($3)); }
1161 | matched
1162
1163sqBracketed
1164 : LLT_LBRACKET args LLT_RBRACKET LLT_COLON sortId
1165 { $$ = makeSqBracketedNode ($1, $2, $3);
1166 $$->given = sort_lookupName (ltoken_getText ($5)); }
1167 | LLT_LBRACKET args LLT_RBRACKET
1168 { $$ = makeSqBracketedNode ($1, $2, $3); }
1169 | LLT_LBRACKET LLT_RBRACKET LLT_COLON sortId
1170 { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2);
1171 $$->given = sort_lookupName (ltoken_getText ($4));
1172 }
1173 | LLT_LBRACKET LLT_RBRACKET
1174 { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2); }
1175
1176matched
1177 : open args close { $$ = makeMatchedNode ($1, $2, $3); }
1178 | open close { $$ = makeMatchedNode ($1, termNodeList_new (), $2); }
1179
1180args
1181 : term { $$ = termNodeList_push (termNodeList_new (), $1); }
1182 | args separator term { $$ = termNodeList_push ($1, $3); }
1183
1184primary
1185 : LLT_LPAR term0 LLT_RPAR /* may need to make a copy of $2 */
1186 { $$ = $2; $$->wrapped = $$->wrapped + 1; }
1187 | varId
1188 { $$ = makeSimpleTermNode ($1); }
1189 | opId LLT_LPAR termList LLT_RPAR
1190 { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
1191 | lclPrimary
1192 | primary stateFcn
1193 { $$ = makePostfixTermNode2 ($1, $2); }
1194 | primary selectSym simpleIdOrTypedefName
1195 { ltoken_markOwned ($3); $$ = makeSelectTermNode ($1, $2, $3); }
1196 | primary mapSym simpleIdOrTypedefName
1197 { ltoken_markOwned ($3); $$ = makeMapTermNode ($1, $2, $3); }
1198 | primary LLT_LBRACKET LLT_RBRACKET
1199 { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, termNodeList_new (), $3),
1200 (termNode)0); }
1201 | primary LLT_LBRACKET termList LLT_RBRACKET
1202 { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, $3, $4), (termNode)0); }
1203 | primary LLT_COLON sortId
1204 { $$ = $1; $$->given = sort_lookupName (ltoken_getText ($3)); }
1205
1206termList
1207 : term0 { $$ = termNodeList_push (termNodeList_new (), $1); }
1208 | termList LLT_COMMA term0 { $$ = termNodeList_push ($1, $3); }
1209
1210stateFcn
1211 : preSym
1212 | postSym
1213 | anySym
1214 | LLT_QUOTE
1215
1216lclPrimary
1217 : cLiteral
1218 | LLT_RESULT { $$ = makeSimpleTermNode ($1); }
1219 | LLT_FRESH LLT_LPAR termList LLT_RPAR { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
1220 | LLT_UNCHANGED LLT_LPAR LLT_ALL LLT_RPAR { $$ = makeUnchangedTermNode1 ($1, $3); }
1221 | LLT_UNCHANGED LLT_LPAR storeRefList LLT_RPAR { $$ = makeUnchangedTermNode2 ($1, $3); }
1222 | LLT_SIZEOF LLT_LPAR term LLT_RPAR
1223 { termNodeList x = termNodeList_new ();
1224 termNodeList_addh (x, $3);
1225 $$ = makeOpCallTermNode ($1, $2, x, $4);
1226 }
1227 | LLT_ISSUB LLT_LPAR term LLT_COMMA term LLT_RPAR
1228 { termNodeList x = termNodeList_new ();
1229 termNodeList_addh (x, $3);
1230 termNodeList_addh (x, $5);
1231 $$ = makeOpCallTermNode ($1, $2, x, $6);
1232 }
1233 | LLT_SIZEOF LLT_LPAR lclTypeSpec LLT_RPAR { $$ = makeSizeofTermNode ($1, $3); }
1234
1235/* removed 94-Mar-25:
1236** | MODIFIES LLT_LPAR term LLT_RPAR
1237** {termNodeList x = termNodeList_new ();
1238** termNodeList_addh (x, $3);
1239** $$ = makeOpCallTermNode ($1, $2, x, $4); }
1240*/
1241
1242cLiteral
1243 : LLT_CINTEGER { $$ = makeLiteralTermNode ($1, sort_int); }
1244 | LLT_LCSTRING { $$ = makeLiteralTermNode ($1, sort_cstring); }
1245 | LLT_CCHAR { $$ = makeLiteralTermNode ($1, sort_char); }
1246 | LLT_CFLOAT { $$ = makeLiteralTermNode ($1, sort_double); }
1247
1248quantifiers
1249 : quantifier
1250 { $$ = quantifierNodeList_add (quantifierNodeList_new (), $1); }
1251 | quantifiers quantifier
1252 { $$ = quantifierNodeList_add ($1, $2); }
1253
1254quantifier
1255 : quantifierSym { scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
1256 si->kind = SPE_QUANT;
1257 symtable_enterScope (g_symtab, si); }
1258 quantifiedList
1259 { $$ = makeQuantifierNode ($3, $1); }
1260
1261quantifiedList
1262 : quantified { $$ = varNodeList_add (varNodeList_new (), $1); }
1263 | quantifiedList LLT_COMMA quantified { $$ = varNodeList_add ($1, $3); }
1264
1265quantified
1266 : varId LLT_COLON sortSpec { $$ = makeVarNode ($1, FALSE, $3); }
1267 | varId LLT_COLON LLT_OBJ sortSpec { $$ = makeVarNode ($1, TRUE, $4); }
1268
1269simpleIdOrTypedefName
1270 : simpleId
1271 | LLT_TYPEDEF_NAME
1272
1273/* a different name space from varId/fcnId/typeId */
1274fcnId : simpleId
1275varId : simpleId
1276tagId : simpleIdOrTypedefName
1277claimId : simpleIdOrTypedefName
1278sortId : simpleIdOrTypedefName
1279traitId : simpleIdOrTypedefName
1280opId : simpleIdOrTypedefName
1281
1282%%
1283
1284# include "bison.reset"
1285
1286/*
1287** yytext is set in lex scanner
1288** extern YYSTYPE yylval;
1289** yylval is defined by code generated by bison
1290*/
1291
1292void ylerror (char *s)
1293{
1294 /*
1295 ** This resetting of the left context is very important when multiple
1296 ** files are to be parsed. We do not want failures to propagate.
1297 ** Lex/Yacc does not reset the flags when the parsing goes bad.
1298 ** BEGIN 0;
1299 **/
1300
1301 /*@-mustfree@*/
1302 lclfatalerror (yllval.ltok,
1303 message ("%s: Token code: %s, Token String: %s",
1304 cstring_fromChars (s),
1305 ltoken_unparseCodeName (yllval.ltok),
1306 ltoken_getRawString (yllval.ltok)));
1307 /*@=mustfree@*/
1308}
1309
1310static void yyprint (FILE *f, int t, YYSTYPE value)
1311{
1312 fprintf (f, " type: %d (%s)", t,
1313 cstring_toCharsSafe (ltoken_getRawString (value.ltok)));
1314}
1315
1316
1317
1318
1319
1320
1321
git-cvsimport mirror of splint
This page took 0.223596 seconds and 5 git commands to generate.