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