]>
Commit | Line | Data |
---|---|---|
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" |
b73d1009 | 30 | # include "basic.h" |
885824d3 | 31 | # include "lclscan.h" |
32 | # include "checking.h" | |
33 | # include "lslparse.h" | |
34 | # include "lh.h" | |
35 | # include "usymtab_interface.h" | |
36 | ||
37 | /*@-noparams@*/ | |
38 | static /*@unused@*/ void yyprint (); | |
39 | /*@=noparams@*/ | |
40 | ||
41 | /*@-redecl@*/ | |
80489f0a | 42 | void ylerror (char *) /*@modifies *g_warningstream@*/ ; |
885824d3 | 43 | /*@=redecl@*/ |
44 | ||
45 | bool 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 | ||
381 | interface | |
382 | : externals { lhExternals ($1); } optDeclarations | |
383 | { interfaceNodeList_free ($1); interfaceNodeList_free ($3); } | |
2f2892c2 | 384 | ; |
885824d3 | 385 | |
386 | externals | |
387 | : /* empty */ { $$ = interfaceNodeList_new (); } | |
388 | | externals external { $$ = interfaceNodeList_addh ($1, $2);} | |
2f2892c2 | 389 | ; |
885824d3 | 390 | |
391 | external | |
392 | : imports | |
393 | | uses | |
2f2892c2 | 394 | ; |
885824d3 | 395 | |
396 | optDeclarations | |
397 | : /* empty */ { $$ = interfaceNodeList_new (); } | |
398 | | export declarations { $$ = consInterfaceNode ($1, $2);} | |
399 | | private declarations { $$ = consInterfaceNode ($1, $2);} | |
2f2892c2 | 400 | ; |
885824d3 | 401 | |
402 | declarations | |
403 | : /* empty */ { $$ = interfaceNodeList_new (); } | |
404 | | declarations declaration { $$ = interfaceNodeList_addh ($1, $2);} | |
2f2892c2 | 405 | ; |
885824d3 | 406 | |
407 | declaration | |
408 | : export | |
409 | | private | |
410 | | uses | |
2f2892c2 | 411 | ; |
885824d3 | 412 | |
413 | imports | |
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 | |
420 | uses | |
421 | : LLT_USES traitRefNodeList LLT_SEMI | |
422 | { $$ = makeInterfaceNodeUses ($2); readlsignatures ($$);} | |
2f2892c2 | 423 | ; |
885824d3 | 424 | |
425 | export | |
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 | |
440 | iter | |
441 | : LLT_ITER varId LLT_LPAR iterParamList LLT_RPAR LLT_SEMI | |
442 | { $$ = makeIterNode ($2, $4); } | |
2f2892c2 | 443 | ; |
885824d3 | 444 | |
445 | iterParamList | |
446 | : /* empty */ { $$ = paramNodeList_new (); } | |
447 | | realIterParamList { $$ = $1; } | |
2f2892c2 | 448 | ; |
885824d3 | 449 | |
450 | realIterParamList | |
451 | : iterParam | |
dfd82dce | 452 | { $$ = paramNodeList_add (paramNodeList_new (), $1); } |
885824d3 | 453 | | realIterParamList LLT_COMMA iterParam |
454 | { $$ = paramNodeList_add ($1,$3); } | |
2f2892c2 | 455 | ; |
456 | ||
885824d3 | 457 | iterParam |
458 | : LLT_YIELD param { $$ = markYieldParamNode ($2); } | |
459 | | param { $$ = $1; } | |
2f2892c2 | 460 | ; |
885824d3 | 461 | |
462 | private | |
463 | : LLT_SPEC { symtable_export (g_symtab, FALSE); } private2 | |
464 | { $$ = $3; symtable_export (g_symtab, TRUE); } | |
2f2892c2 | 465 | ; |
885824d3 | 466 | |
467 | private2 | |
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 | |
478 | constDeclaration | |
479 | : LLT_CONSTANT lclTypeSpec initDecls LLT_SEMI | |
480 | { $$ = makeConstDeclarationNode ($2, $3); } | |
2f2892c2 | 481 | ; |
885824d3 | 482 | |
483 | varDeclaration | |
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 | |
492 | type | |
493 | : abstract { $$ = makeAbstractTypeNode ($1); } | |
494 | | exposed { $$ = makeExposedTypeNode ($1); } | |
2f2892c2 | 495 | ; |
885824d3 | 496 | |
497 | special | |
498 | : LLT_PRINTFLIKE { $$ = qual_createPrintfLike (); } | |
499 | | LLT_SCANFLIKE { $$ = qual_createScanfLike (); } | |
500 | | LLT_MESSAGELIKE { $$ = qual_createMessageLike (); } | |
2f2892c2 | 501 | ; |
885824d3 | 502 | |
503 | fcn | |
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 | |
524 | claim | |
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 | |
534 | abstract | |
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 | |
547 | exposed | |
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 | |
569 | importNameList | |
570 | : importName | |
dfd82dce | 571 | { $$ = importNodeList_add (importNodeList_new (), $1); } |
885824d3 | 572 | | importNameList LLT_COMMA importName |
573 | { $$ = importNodeList_add ($1, $3); } | |
2f2892c2 | 574 | ; |
885824d3 | 575 | |
576 | importName | |
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 | |
583 | interfaceNameList | |
584 | : interfaceName { $$ = ltokenList_singleton ($1); } | |
585 | | interfaceNameList LLT_COMMA interfaceName { $$ = ltokenList_push ($1, $3); } | |
2f2892c2 | 586 | ; |
885824d3 | 587 | |
588 | interfaceName | |
589 | : simpleIdOrTypedefName | |
590 | /* to allow module names to be the same as LCL type names */ | |
2f2892c2 | 591 | ; |
885824d3 | 592 | |
593 | traitRefNodeList | |
594 | : traitRef | |
dfd82dce | 595 | { $$ = traitRefNodeList_add (traitRefNodeList_new (), $1); } |
885824d3 | 596 | | traitRefNodeList LLT_COMMA traitRef |
597 | { $$ = traitRefNodeList_add ($1, $3); } | |
2f2892c2 | 598 | ; |
885824d3 | 599 | |
600 | traitRef | |
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 | |
611 | traitIdList | |
612 | : traitId { $$ = ltokenList_singleton ($1); } | |
613 | | traitIdList LLT_COMMA traitId { $$ = ltokenList_push ($1, $3); } | |
2f2892c2 | 614 | ; |
885824d3 | 615 | |
616 | renaming | |
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 | |
624 | nameList | |
625 | : typeName | |
dfd82dce | 626 | { $$ = typeNameNodeList_add (typeNameNodeList_new (), $1); } |
885824d3 | 627 | | nameList LLT_COMMA typeName { $$ = typeNameNodeList_add ($1, $3); } |
2f2892c2 | 628 | ; |
885824d3 | 629 | |
630 | replaceNodeList | |
631 | : replace | |
dfd82dce | 632 | { $$ = replaceNodeList_add (replaceNodeList_new (), $1); } |
885824d3 | 633 | | replaceNodeList LLT_COMMA replace { $$ = replaceNodeList_add ($1, $3); } |
2f2892c2 | 634 | ; |
885824d3 | 635 | |
636 | replace | |
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 | |
643 | name | |
644 | : opId { $$ = makeNameNodeId ($1); } | |
645 | | opForm { $$ = makeNameNodeForm ($1); } | |
2f2892c2 | 646 | ; |
885824d3 | 647 | |
648 | initializer : constLclExpr | |
2f2892c2 | 649 | ; |
885824d3 | 650 | |
651 | constLclExpr : term | |
2f2892c2 | 652 | ; |
885824d3 | 653 | |
654 | initDecls | |
655 | : initDecl | |
dfd82dce | 656 | { $$ = initDeclNodeList_add (initDeclNodeList_new (), $1); } |
885824d3 | 657 | | initDecls LLT_COMMA initDecl |
658 | { $$ = initDeclNodeList_add ($1, $3); } | |
2f2892c2 | 659 | ; |
885824d3 | 660 | |
661 | initDecl | |
662 | : declarator { $$ = makeInitDeclNode ($1, (termNode)0); } | |
663 | | declarator LLT_EQUALS initializer { $$ = makeInitDeclNode ($1, $3); } | |
2f2892c2 | 664 | ; |
885824d3 | 665 | |
666 | globals | |
667 | : /* empty */ /* has the same structure */ | |
668 | { $$ = varDeclarationNodeList_new (); } | |
669 | | globals globalDecl | |
670 | { varDeclarationNodeList_addh ($1, $2); $$ = $1; } | |
2f2892c2 | 671 | ; |
885824d3 | 672 | |
673 | globalDecl | |
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 | |
679 | privateInits | |
680 | : /* empty */ { $$ = varDeclarationNodeList_new (); } | |
681 | | privateInits privateInit { varDeclarationNodeList_addh ($1, $2); $$ = $1; } | |
2f2892c2 | 682 | ; |
885824d3 | 683 | |
684 | privateInit | |
685 | : LLT_PRIVATE lclTypeSpec initDecls LLT_SEMI | |
686 | { $$ = makeVarDeclarationNode ($2, $3, FALSE, TRUE); } | |
2f2892c2 | 687 | ; |
885824d3 | 688 | |
689 | optLetDecl | |
690 | : /* empty */ { $$ = letDeclNodeList_new (); } | |
691 | | LLT_LET beDeclList LLT_SEMI { $$ = $2; } | |
2f2892c2 | 692 | ; |
885824d3 | 693 | |
694 | beDeclList | |
dfd82dce | 695 | : beDecl { $$ = letDeclNodeList_add (letDeclNodeList_new (), $1); } |
885824d3 | 696 | | beDeclList LLT_COMMA beDecl { $$ = letDeclNodeList_add ($1, $3); } |
2f2892c2 | 697 | ; |
885824d3 | 698 | |
699 | beDecl | |
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 | |
704 | sortSpec : lclTypeSpec | |
2f2892c2 | 705 | ; |
885824d3 | 706 | |
707 | optChecks | |
708 | : /* empty */ { $$ = (lclPredicateNode)0; } | |
709 | | LLT_CHECKS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeChecksNode ($1, $2); } | |
2f2892c2 | 710 | ; |
885824d3 | 711 | |
712 | optRequire | |
713 | : /* empty */ { $$ = (lclPredicateNode)0; } | |
714 | | LLT_REQUIRES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeRequiresNode ($1, $2);} | |
2f2892c2 | 715 | ; |
885824d3 | 716 | |
717 | optModify | |
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 | |
724 | storeRefList | |
dfd82dce | 725 | : storeRef { $$ = storeRefNodeList_add (storeRefNodeList_new (), $1); } |
885824d3 | 726 | | storeRefList LLT_COMMA storeRef { $$ = storeRefNodeList_add ($1, $3); } |
2f2892c2 | 727 | ; |
885824d3 | 728 | |
729 | storeRef | |
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 | |
737 | optEnsure | |
738 | : /* empty */ { $$ = (lclPredicateNode)0; } | |
739 | | LLT_ENSURES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeEnsuresNode ($1, $2);} | |
2f2892c2 | 740 | ; |
885824d3 | 741 | |
742 | optClaim | |
743 | : /* empty */ { $$ = (lclPredicateNode)0; } | |
744 | | LLT_CLAIMS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeIntraClaimNode ($1, $2);} | |
2f2892c2 | 745 | ; |
885824d3 | 746 | |
747 | optParamList | |
748 | : /* empty */ { $$ = paramNodeList_new (); } | |
749 | | realParamList { $$ = $1; } | |
2f2892c2 | 750 | ; |
885824d3 | 751 | |
752 | realParamList | |
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 | |
758 | paramList | |
759 | : param { $$ = paramNodeList_single ($1); } | |
760 | | paramList LLT_COMMA param { $$ = paramNodeList_add ($1, $3); } | |
2f2892c2 | 761 | ; |
885824d3 | 762 | |
763 | optBody | |
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 | |
769 | callExpr | |
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 | |
793 | stmt | |
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 | |
804 | valueList | |
dfd82dce | 805 | : value { $$ = termNodeList_push (termNodeList_new (), $1); } |
885824d3 | 806 | | valueList LLT_COMMA value { $$ = termNodeList_push ($1, $3); } |
2f2892c2 | 807 | ; |
885824d3 | 808 | |
809 | value | |
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 | |
822 | abstBody | |
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 | |
829 | fcns | |
830 | : /* empty */ { $$ = fcnNodeList_new (); } | |
831 | | fcns fcn { $$ = fcnNodeList_add ($1, $2); } | |
2f2892c2 | 832 | ; |
885824d3 | 833 | |
834 | optTypeInv | |
835 | : /* empty */ { $$ = (lclPredicateNode)0; } | |
836 | | typeInv | |
2f2892c2 | 837 | ; |
885824d3 | 838 | |
839 | typeInv | |
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 | |
849 | declaratorInvs | |
dfd82dce | 850 | : declaratorInv { $$ = declaratorInvNodeList_add (declaratorInvNodeList_new (), $1); } |
885824d3 | 851 | | declaratorInvs LLT_COMMA declaratorInv |
852 | { $$ = declaratorInvNodeList_add ($1, $3); } | |
2f2892c2 | 853 | ; |
885824d3 | 854 | |
855 | declaratorInv | |
856 | : declarator { declareForwardType ($1); } optExposedBody | |
857 | { $$ = makeDeclaratorInvNode ($1, $3); } | |
2f2892c2 | 858 | ; |
885824d3 | 859 | |
860 | optExposedBody | |
861 | : /* empty */ { $$ = (abstBodyNode)0; } | |
862 | | LLT_LBRACE optTypeInv LLT_RBRACE { $$ = makeExposedBodyNode ($1, $2); } | |
2f2892c2 | 863 | ; |
885824d3 | 864 | |
865 | CType | |
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 | ||
883 | CTypes | |
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 | ||
890 | typeSpecifier | |
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 | ||
899 | specialQualifier | |
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 | |
938 | lclTypeSpec | |
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 | ||
956 | lclType | |
957 | : lclTypeSpec | |
958 | | lclTypeSpec pointers | |
959 | { llassert (lclTypeSpecNode_isDefined ($1)); | |
960 | $1->pointers = $2; $$ = $1; } | |
2f2892c2 | 961 | ; |
885824d3 | 962 | |
963 | pointers | |
f9264521 | 964 | : LLT_MULOP { $$ = pointers_createLt ($1); } |
965 | | pointers LLT_MULOP { $$ = pointers_extend ($1, pointers_createLt ($2)); } | |
2f2892c2 | 966 | ; |
885824d3 | 967 | |
968 | structOrUnionSpec | |
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 | |
983 | optTagId | |
984 | : /* empty */ { $$ = ltoken_undefined; } | |
985 | | tagId | |
2f2892c2 | 986 | ; |
885824d3 | 987 | |
988 | structDecls | |
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 | ||
995 | structDecl | |
996 | : lclTypeSpec declaratorList LLT_SEMI { $$ = makestDeclNode ($1, $2); } | |
2f2892c2 | 997 | ; |
885824d3 | 998 | |
999 | declaratorList | |
1000 | : declarator | |
dfd82dce | 1001 | { $$ = declaratorNodeList_add (declaratorNodeList_new (), $1); } |
885824d3 | 1002 | | declaratorList LLT_COMMA declarator |
1003 | { $$ = declaratorNodeList_add ($1, $3); } | |
2f2892c2 | 1004 | ; |
885824d3 | 1005 | |
1006 | optCOMMA | |
1007 | : /* empty */ { ; } | |
1008 | | LLT_COMMA { ; } | |
2f2892c2 | 1009 | ; |
885824d3 | 1010 | |
1011 | enumSpec | |
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 | |
1018 | enumeratorList | |
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 | ||
1030 | declarator | |
1031 | : after_type_decl { $$ = makeDeclaratorNode ($1); } | |
1032 | | notype_decl { $$ = makeDeclaratorNode ($1); } | |
2f2892c2 | 1033 | ; |
885824d3 | 1034 | |
1035 | notype_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 | |
1044 | after_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 | ||
1059 | parameter_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 | ||
1070 | param | |
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 | ||
1083 | typeName | |
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 | ||
1091 | optAbstDeclarator | |
1092 | : /* empty */ { $$ = (abstDeclaratorNode)0; } | |
1093 | | abstDeclarator { $$ = (abstDeclaratorNode)$1; } | |
2f2892c2 | 1094 | ; |
885824d3 | 1095 | |
1096 | abstDeclarator | |
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 | |
1107 | arrayQual | |
1108 | : LLT_LBRACKET LLT_RBRACKET { $$ = makeArrayQualNode ($1, (termNode)0); } | |
1109 | | LLT_LBRACKET constLclExpr LLT_RBRACKET { $$ = makeArrayQualNode ($1, $2); } | |
2f2892c2 | 1110 | ; |
885824d3 | 1111 | |
1112 | opForm | |
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 | |
1160 | open | |
1161 | : openSym | |
1162 | | LLT_LBRACE | |
2f2892c2 | 1163 | ; |
885824d3 | 1164 | |
1165 | close | |
1166 | : closeSym | |
1167 | | LLT_RBRACE | |
2f2892c2 | 1168 | ; |
885824d3 | 1169 | |
1170 | anyOp | |
1171 | : simpleOp2 | |
1172 | | logicalOp | |
1173 | | eqOp | |
2f2892c2 | 1174 | ; |
885824d3 | 1175 | |
1176 | middle | |
1177 | : /* empty */ { $$ = 0; } | |
1178 | | placeList | |
2f2892c2 | 1179 | ; |
885824d3 | 1180 | |
1181 | placeList | |
1182 | : markerSym { $$ = 1; } | |
1183 | | placeList separator markerSym { $$ = $1 + 1; } | |
2f2892c2 | 1184 | ; |
885824d3 | 1185 | |
1186 | separator | |
1187 | : LLT_COMMA | |
1188 | | sepSym | |
2f2892c2 | 1189 | ; |
885824d3 | 1190 | |
1191 | signature | |
1192 | : LLT_COLON domain mapSym sortId { $$ = makesigNode ($1, $2, $4); } | |
2f2892c2 | 1193 | ; |
885824d3 | 1194 | |
1195 | domain | |
1196 | : /* empty */ { $$ = ltokenList_new (); } | |
1197 | | sortList | |
2f2892c2 | 1198 | ; |
885824d3 | 1199 | |
1200 | sortList | |
1201 | : sortId { $$ = ltokenList_singleton ($1); } | |
1202 | | sortList LLT_COMMA sortId { $$ = ltokenList_push ($1, $3); } | |
2f2892c2 | 1203 | ; |
885824d3 | 1204 | |
1205 | lclPredicate | |
1206 | : term { $$ = makeLclPredicateNode (ltoken_undefined, $1, LPD_PLAIN);} | |
2f2892c2 | 1207 | ; |
885824d3 | 1208 | |
1209 | term | |
1210 | : term0 { $$ = checkSort ($1); } | |
2f2892c2 | 1211 | ; |
885824d3 | 1212 | |
1213 | /* When "if <term> then <term> else <term> . <logicalOp> <term>" | |
1214 | shift instead of reduce */ | |
1215 | ||
1216 | term0 | |
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 | |
1223 | equalityTerm | |
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 | |
1236 | simpleOpTerm | |
1237 | : prefixOpTerm | |
1238 | | secondary postfixOps { $$ = makePostfixTermNode ($1, $2); } | |
1239 | | secondary infixOpPart { $$ = CollapseInfixTermNode ($1, $2); } | |
2f2892c2 | 1240 | ; |
885824d3 | 1241 | |
1242 | simpleOp2 | |
1243 | : simpleOp | |
1244 | | LLT_MULOP | |
2f2892c2 | 1245 | ; |
885824d3 | 1246 | |
1247 | prefixOpTerm | |
1248 | : secondary | |
1249 | | simpleOp2 prefixOpTerm { $$ = makePrefixTermNode ($1, $2); } | |
2f2892c2 | 1250 | ; |
885824d3 | 1251 | |
1252 | postfixOps | |
1253 | : simpleOp2 { $$ = ltokenList_singleton ($1); } | |
1254 | | postfixOps simpleOp2 { $$ = ltokenList_push ($1, $2); } | |
2f2892c2 | 1255 | ; |
885824d3 | 1256 | |
1257 | infixOpPart | |
dfd82dce | 1258 | : simpleOp2 secondary { $$ = pushInfixOpPartNode (termNodeList_new (), $1, $2); } |
885824d3 | 1259 | | infixOpPart simpleOp2 secondary { $$ = pushInfixOpPartNode ($1, $2, $3); } |
2f2892c2 | 1260 | ; |
885824d3 | 1261 | |
1262 | secondary | |
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 | |
1272 | bracketed | |
1273 | : matched LLT_COLON sortId { $$ = $1; $$->sort = sort_lookupName (ltoken_getText ($3)); } | |
1274 | | matched | |
2f2892c2 | 1275 | ; |
885824d3 | 1276 | |
1277 | sqBracketed | |
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 | |
1291 | matched | |
1292 | : open args close { $$ = makeMatchedNode ($1, $2, $3); } | |
dfd82dce | 1293 | | open close { $$ = makeMatchedNode ($1, termNodeList_new (), $2); } |
2f2892c2 | 1294 | ; |
885824d3 | 1295 | |
1296 | args | |
dfd82dce | 1297 | : term { $$ = termNodeList_push (termNodeList_new (), $1); } |
885824d3 | 1298 | | args separator term { $$ = termNodeList_push ($1, $3); } |
2f2892c2 | 1299 | ; |
885824d3 | 1300 | |
1301 | primary | |
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 | |
1324 | termList | |
dfd82dce | 1325 | : term0 { $$ = termNodeList_push (termNodeList_new (), $1); } |
885824d3 | 1326 | | termList LLT_COMMA term0 { $$ = termNodeList_push ($1, $3); } |
2f2892c2 | 1327 | ; |
885824d3 | 1328 | |
1329 | stateFcn | |
1330 | : preSym | |
1331 | | postSym | |
1332 | | anySym | |
1333 | | LLT_QUOTE | |
2f2892c2 | 1334 | ; |
885824d3 | 1335 | |
1336 | lclPrimary | |
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 | ||
1363 | cLiteral | |
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 | |
1370 | quantifiers | |
1371 | : quantifier | |
dfd82dce | 1372 | { $$ = quantifierNodeList_add (quantifierNodeList_new (), $1); } |
885824d3 | 1373 | | quantifiers quantifier |
1374 | { $$ = quantifierNodeList_add ($1, $2); } | |
2f2892c2 | 1375 | ; |
885824d3 | 1376 | |
1377 | quantifier | |
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 | |
1385 | quantifiedList | |
dfd82dce | 1386 | : quantified { $$ = varNodeList_add (varNodeList_new (), $1); } |
885824d3 | 1387 | | quantifiedList LLT_COMMA quantified { $$ = varNodeList_add ($1, $3); } |
2f2892c2 | 1388 | ; |
885824d3 | 1389 | |
1390 | quantified | |
1391 | : varId LLT_COLON sortSpec { $$ = makeVarNode ($1, FALSE, $3); } | |
1392 | | varId LLT_COLON LLT_OBJ sortSpec { $$ = makeVarNode ($1, TRUE, $4); } | |
2f2892c2 | 1393 | ; |
885824d3 | 1394 | |
1395 | simpleIdOrTypedefName | |
1396 | : simpleId | |
1397 | | LLT_TYPEDEF_NAME | |
2f2892c2 | 1398 | ; |
885824d3 | 1399 | |
1400 | /* a different name space from varId/fcnId/typeId */ | |
2f2892c2 | 1401 | fcnId : simpleId ; |
1402 | varId : simpleId ; | |
1403 | tagId : simpleIdOrTypedefName ; | |
1404 | claimId : simpleIdOrTypedefName ; | |
1405 | sortId : simpleIdOrTypedefName ; | |
1406 | traitId : simpleIdOrTypedefName ; | |
1407 | opId : 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 | ||
1419 | void 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 | ||
1437 | static 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 |