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