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