source: CIVL/mods/dev.civl.abc/grammar/c/AcslParser.g@ c2b37db

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since c2b37db was c2b37db, checked in by Alex Wilton <awilton@…>, 11 months ago

Merged focus branch into trunk.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5988 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 34.6 KB
Line 
1parser grammar AcslParser;
2
3/*
4 * Grammar for ACSL: an ANSI/ISO C Specification Language,
5 * with additional CIVL-C extensions.
6 * Based on ACSL 1.12.
7 * https://frama-c.com/acsl.html
8 *
9 * Author: Manchun Zheng, University of Delaware
10 * Author: Stephen F. Siegel, University of Delaware
11 * Last changed: May 2018
12 */
13
14options
15{
16 language=Java;
17 tokenVocab=PreprocessorParser;
18 output=AST;
19 backtrack = true; // TODO: get rid of this
20}
21
22tokens{
23 ABSENT;
24 ABSENT_EVENT_SENDTO;
25 ABSENT_EVENT_SENDFROM;
26 ABSENT_EVENT_ENTER;
27 ABSENT_EVENT_EXIT;
28 ABSTRACT_DECLARATOR;
29 ACCESS_ACSL;
30 ALLOC;
31 ANYACT;
32 ARGUMENT_LIST;
33 ARRAY_SUFFIX;
34 ASSUMES_ACSL;
35 ASSIGNS_ACSL;
36 ASSERT_ACSL;
37 BEHAVIOR;
38 BEHAVIOR_BODY;
39 BEHAVIOR_COMPLETE;
40 BEHAVIOR_DISJOINT;
41 BEQUIV_ACSL;
42 BIMPLIES_ACSL;
43 BINDER;
44 BINDER_LIST;
45 BOOLEAN;
46 BOTH;
47 C_TYPE;
48 CALL_ACSL;
49 CAST;
50 CLAUSE_NORMAL;
51 CLAUSE_BEHAVIOR;
52 CLAUSE_COMPLETE;
53 COL;
54 CONTRACT;
55 DEPENDSON;
56 DIRECT_ABSTRACT_DECLARATOR;
57 ENSURES_ACSL;
58 EVENT_BASE;
59 EVENT_PLUS;
60 EVENT_SUB;
61 EVENT_INTS;
62 EVENT_LIST;
63 EVENT_PARENTHESIZED;
64 EXECUTES_WHEN;
65 EXISTS_ACSL;
66 FALSE_ACSL;
67 FOCUS_ASSERT;
68 FOCUS_LOOP;
69 FORALL_ACSL;
70 FREES;
71 FUNC_CALL;
72 FUNC_CONTRACT;
73 FUNC_CONTRACT_BLOCK;
74 ID_LIST;
75 INDEX;
76 INTEGER;
77 INTER;
78 LAMBDA_ACSL;
79 LOGIC_FUNCTIONS;
80 LOGIC_FUNCTION_CLAUSE;
81 LOGIC_TYPE;
82 LOOP_ALLOC;
83 LOOP_ASSIGNS;
84 LOOP_BEHAVIOR;
85 LOOP_CLAUSE;
86 LOOP_CONTRACT;
87 LOOP_CONTRACT_BLOCK;
88 LOOP_FREE;
89 LOOP_INVARIANT;
90 LOOP_VARIANT;
91 MAX;
92 MIN;
93 MPI_AGREE;
94 MPI_COLLECTIVE;
95 MPI_COMM_RANK;
96 MPI_COMM_SIZE;
97 MPI_CONSTANT;
98 MPI_EMPTY_IN;
99 MPI_EMPTY_OUT;
100 MPI_EQUALS;
101 MPI_EXPRESSION;
102 MPI_EXTENT;
103 MPI_OFFSET;
104 MPI_VALID;
105 MPI_REGION;
106 MPI_REDUCE;
107 MPI_ABSENT;
108 NOTHING;
109 NULL_ACSL;
110 NUMOF;
111 OBJECT_OF;
112 OLD;
113 OPERATOR;
114 P2P;
115 POINTER;
116 PROD;
117 PURE;
118 PREDICATE_CLAUSE;
119 LOGIC_FUNCTION_BODY; /* shared by both predicate and logic function */
120 QUANTIFIED;
121 QUANTIFIED_EXT;
122 READ_ACSL;
123 READS_ACSL;
124 REAL_ACSL;
125 RELCHAIN; // a chain of relational expressions
126 RESULT_ACSL;
127 REMOTE_ACCESS;
128 REQUIRES_ACSL;
129 SET_BINDERS;
130 SET_SIMPLE;
131 SIZEOF_EXPR;
132 SIZEOF_TYPE;
133 SPECIFIER_QUALIFIER_LIST;
134 SUM;
135 TERM_PARENTHESIZED;
136 TERMINATES;
137 TRANSFORM;
138 TRANSFORM_CONTRACT;
139 TRANSFORM_CONTRACT_BLOCK;
140 TRUE_ACSL;
141 TYPE_BUILTIN;
142 TYPE_ID;
143 UNION_ACSL;
144 VALID;
145 VAR_ID;
146 VAR_ID_BASE;
147 VAR_ID_SQUARE;
148 VAR_ID_STAR;
149 WAITSFOR;
150 WRITE_ACSL;
151}
152
153@header
154{
155package dev.civl.abc.front.c.parse;
156}
157
158contract
159 : loop_contract
160 | function_contract
161 | logic_function_contract
162 | assert_contract
163 | transform_contract
164 ;
165
166/* Section 2.4.2 Loop Annotations */
167loop_contract
168 : loop_contract_block
169 ->^(LOOP_CONTRACT loop_contract_block)
170 ;
171
172loop_contract_block
173 : lc+=loop_clause* lb+=loop_behavior* lv=loop_variant?
174 ->^(LOOP_CONTRACT_BLOCK $lc* $lb* $lv?)
175 ;
176
177loop_clause
178 : loop_invariant SEMI
179 ->^(LOOP_CLAUSE loop_invariant)
180 | loop_assigns SEMI
181 ->^(LOOP_CLAUSE loop_assigns)
182 | loop_allocation SEMI
183 ->^(LOOP_CLAUSE loop_allocation)
184 ;
185
186loop_invariant
187 : loop_key invariant_key term
188 ->^(LOOP_INVARIANT term)
189 ;
190
191loop_assigns
192 : loop_key assigns_key argumentExpressionList
193 ->^(LOOP_ASSIGNS assigns_key argumentExpressionList)
194 ;
195
196loop_allocation
197 : loop_key alloc_key argumentExpressionList (COMMA term)?
198 ->^(LOOP_ALLOC argumentExpressionList term?)
199 | loop_key frees_key argumentExpressionList
200 ->^(LOOP_FREE argumentExpressionList)
201 ;
202
203loop_behavior
204 : FOR ilist=id_list COLON lc+=loop_clause*
205 ->^(LOOP_BEHAVIOR $ilist $lc*)
206 ;
207
208loop_variant
209 : loop_key variant_key term
210 ->^(LOOP_VARIANT term)
211 | loop_key variant_key term FOR IDENTIFIER
212 ->^(LOOP_VARIANT term IDENTIFIER)
213 ;
214
215transform_contract
216 : transform_contract_block
217 ->^(TRANSFORM_CONTRACT transform_contract_block)
218 ;
219
220transform_contract_block
221 : trs+=transform* ->^(TRANSFORM_CONTRACT_BLOCK $trs*)
222 ;
223
224transform
225 : transform_spec SEMI ->^(TRANSFORM transform_spec)
226 ;
227
228transform_spec
229 : focus_spec
230 ;
231
232focus_spec
233 : focus_assert_spec | focus_loop_spec
234 ;
235
236focus_assert_spec
237 : focus_key IDENTIFIER+ ->^(FOCUS_ASSERT IDENTIFIER+)
238 ;
239
240focus_loop_spec
241 : focus_key IDENTIFIER BITOR argumentExpressionList ->^(FOCUS_LOOP IDENTIFIER argumentExpressionList)
242 ;
243
244/* sec. 2.3 Function contracts */
245function_contract
246 : pure_function? full_contract_block
247 -> ^(FUNC_CONTRACT full_contract_block pure_function?)
248 ;
249
250/* sec. 2.6.1 Predicate and (Logic) Function
251 * definitions. Semantically, predicates are logic functions as
252 * well. */
253logic_function_contract
254 : (a+=logic_function_clause*) -> ^(LOGIC_FUNCTIONS $a*)
255 ;
256
257logic_function_clause
258 : logic_specifier_key type_expr a=IDENTIFIER b=logic_function_body SEMI
259 -> ^(LOGIC_FUNCTION_CLAUSE type_expr $a $b)
260 | predicate_key a=IDENTIFIER b=logic_function_body SEMI
261 -> ^(PREDICATE_CLAUSE $a $b)
262 ;
263
264/* simple ACSL assertion */
265assert_contract
266 : assert_key term SEMI -> ^(ASSERT_ACSL term)
267 ;
268
269/* ACSL logic function (predicate) declaration, either binder is
270 * absent or body is absent. They cannot be both absent. */
271/* binders (optional) = function-body */
272logic_function_body
273 : LPAREN binders RPAREN ASSIGN term
274 -> ^(LOGIC_FUNCTION_BODY binders term)
275 | LPAREN binders RPAREN
276 -> ^(LOGIC_FUNCTION_BODY binders ABSENT)
277 | ASSIGN term
278 -> ^(LOGIC_FUNCTION_BODY ABSENT term)
279 ;
280
281pure_function
282 : pure_key SEMI
283 ;
284
285/* a full contract block non-terminal represents an ACSL contract
286 * block for a function */
287full_contract_block
288 : (f+=function_clause)* (m+=contract_block)*
289 (c+=completeness_clause_block)*
290 -> ^(FUNC_CONTRACT_BLOCK $f* $m* $c*)
291 ;
292
293/* a partial contract block non-terminal represents an ACSL contract
294 * block inside an MPI collective block. There is no nested MPI
295 * collective block allowed */
296partial_contract_block
297 : (f+=function_clause)* (b+=named_behavior_block)*
298 (c+=completeness_clause_block)*
299 -> ^(FUNC_CONTRACT_BLOCK $f* $b* $c*)
300 ;
301
302/* a block in contracts, either an mpi collective block or a behavior
303* block. Behavior blocks are allowed to be inside an mpi collective
304* block while an mpi collective block will not belong to a behavior
305* block. An mpi collective block appears after a behavior block marks
306* the end of the behavior block. */
307contract_block
308 : mpi_collective_block
309 | named_behavior_block completeness_clause_block?
310 ;
311
312function_clause
313 : requires_clause SEMI-> ^(CLAUSE_NORMAL requires_clause)
314 | terminates_clause SEMI-> ^(CLAUSE_NORMAL terminates_clause)
315 | simple_clause SEMI -> ^(CLAUSE_NORMAL simple_clause)
316 ;
317
318named_behavior_block
319 : named_behavior -> ^(CLAUSE_BEHAVIOR named_behavior)
320 ;
321
322completeness_clause_block
323 : completeness_clause SEMI -> ^(CLAUSE_COMPLETE completeness_clause)
324 ;
325
326requires_clause
327 : requires_key term -> ^(REQUIRES_ACSL requires_key term)
328 ;
329
330terminates_clause
331 : terminates_key term -> ^(TERMINATES terminates_key term)
332 ;
333
334binders
335 : binder (COMMA binder)*
336 ->^(BINDER_LIST binder+)
337 ;
338
339binder
340 : type_expr variable_ident (COMMA variable_ident)*
341 ->^(BINDER type_expr variable_ident+)
342 ;
343
344type_expr
345 : logic_type_expr ->^(LOGIC_TYPE logic_type_expr)
346 | specifierQualifierList abstractDeclarator
347 -> ^(C_TYPE specifierQualifierList abstractDeclarator)
348 ;
349
350/* Start of C-like type name syntax */
351specifierQualifierList
352 : c_basic_type+
353 -> ^(SPECIFIER_QUALIFIER_LIST c_basic_type+)
354 ;
355
356abstractDeclarator
357 : pointer
358 -> ^(ABSTRACT_DECLARATOR pointer ABSENT)
359 | directAbstractDeclarator
360 -> ^(ABSTRACT_DECLARATOR ABSENT directAbstractDeclarator)
361 | pointer directAbstractDeclarator
362 -> ^(ABSTRACT_DECLARATOR pointer directAbstractDeclarator)
363 | -> ABSENT
364 ;
365
366directAbstractDeclarator
367 : LPAREN abstractDeclarator RPAREN directAbstractDeclaratorSuffix*
368 -> ^(DIRECT_ABSTRACT_DECLARATOR abstractDeclarator
369 directAbstractDeclaratorSuffix*)
370 | directAbstractDeclaratorSuffix+
371 -> ^(DIRECT_ABSTRACT_DECLARATOR ABSENT directAbstractDeclaratorSuffix+)
372 ;
373
374pointer
375 : STAR+ -> ^(POINTER STAR+)
376 ;
377
378directAbstractDeclaratorSuffix
379 : LSQUARE assignmentExpression_opt RSQUARE
380 -> ^(ARRAY_SUFFIX LSQUARE
381 assignmentExpression_opt RSQUARE)
382 ;
383/* End of C-like type name syntax */
384
385
386logic_type_expr
387 : built_in_logic_type ->^(TYPE_BUILTIN built_in_logic_type)
388 ;
389
390c_basic_type
391 : CHAR | DOUBLE | FLOAT | INT | LONG | SHORT | VOID
392 ;
393
394built_in_logic_type
395 : boolean_type | integer_type | real_type
396 ;
397
398variable_ident
399 : STAR variable_ident_base
400 ->^(VAR_ID_STAR variable_ident_base)
401 | variable_ident_base LSQUARE RSQUARE
402 ->^(VAR_ID_SQUARE variable_ident_base)
403 | variable_ident_base
404 ->^(VAR_ID variable_ident_base)
405 ;
406
407variable_ident_base
408 : IDENTIFIER
409 ->^(IDENTIFIER)
410 | LPAREN variable_ident RPAREN
411 ->^(VAR_ID_BASE variable_ident)
412 ;
413
414guards_clause
415 : executeswhen_key term ->^(EXECUTES_WHEN executeswhen_key term)
416 ;
417
418simple_clause
419 : assigns_clause
420 | ensures_clause
421 | allocation_clause
422 | reads_clause
423 | depends_clause
424 | guards_clause
425 | waitsfor_clause
426 ;
427
428assigns_clause
429 : assigns_key argumentExpressionList ->^(ASSIGNS_ACSL assigns_key argumentExpressionList)
430 ;
431
432ensures_clause
433 : ensures_key term ->^(ENSURES_ACSL ensures_key term)
434 ;
435
436allocation_clause
437 : alloc_key argumentExpressionList ->^(ALLOC alloc_key argumentExpressionList)
438 | frees_key argumentExpressionList ->^(FREES frees_key argumentExpressionList)
439 ;
440
441reads_clause
442 : reads_key argumentExpressionList ->^(READS_ACSL reads_key argumentExpressionList)
443 ;
444
445waitsfor_clause
446 : waitsfor_key argumentExpressionList -> ^(WAITSFOR waitsfor_key argumentExpressionList)
447 ;
448
449depends_clause
450 : dependson_key event_list ->^(DEPENDSON dependson_key event_list)
451 ;
452
453event_list
454 : event (COMMA event)* -> ^(EVENT_LIST event+)
455 ;
456
457event
458 : event_base PLUS event_base
459 -> ^(EVENT_PLUS event_base event_base)
460 | event_base SUB event_base
461 -> ^(EVENT_SUB event_base event_base)
462 | event_base AMPERSAND event_base
463 -> ^(EVENT_INTS event_base event_base)
464 | event_base
465 -> ^(EVENT_BASE event_base)
466 ;
467
468event_base
469 : read_key LPAREN argumentExpressionList RPAREN
470 -> ^(READ_ACSL read_key argumentExpressionList)
471 | write_key LPAREN argumentExpressionList RPAREN
472 -> ^(WRITE_ACSL write_key argumentExpressionList)
473 | access_key LPAREN argumentExpressionList RPAREN
474 -> ^(ACCESS_ACSL access_key argumentExpressionList)
475 | call_key LPAREN IDENTIFIER (COMMA argumentExpressionList)? RPAREN
476 -> ^(CALL_ACSL call_key IDENTIFIER argumentExpressionList?)
477 | nothing_key
478 | anyact_key
479 | LPAREN event RPAREN
480 -> ^(EVENT_PARENTHESIZED event)
481 ;
482
483/* ACSL-MPI extensions: constructors */
484mpi_collective_block
485 : mpicollective_key LPAREN IDENTIFIER COMMA kind=mpi_collective_kind RPAREN COLON
486 c=partial_contract_block -> ^(MPI_COLLECTIVE mpicollective_key IDENTIFIER $kind $c)
487 ;
488
489
490
491/* sec. 2.3.3 contracts with named behaviors */
492named_behavior
493 : behavior_key IDENTIFIER COLON behavior_body
494 -> ^(BEHAVIOR behavior_key IDENTIFIER behavior_body)
495 ;
496
497behavior_body
498 : (b+=behavior_clause SEMI)+ -> ^(BEHAVIOR_BODY $b+)
499 ;
500
501behavior_clause
502 : assumes_clause
503 | requires_clause
504 | simple_clause
505 ;
506
507assumes_clause
508 : assumes_key term ->^(ASSUMES_ACSL assumes_key term)
509 ;
510
511completeness_clause
512 : completes_key behaviors_key id_list
513 -> ^(BEHAVIOR_COMPLETE completes_key behaviors_key id_list)
514 | disjoint_key behaviors_key id_list
515 -> ^(BEHAVIOR_DISJOINT disjoint_key behaviors_key id_list)
516 ;
517
518id_list
519 :
520 | IDENTIFIER (COMMA IDENTIFIER)* -> ^(ID_LIST IDENTIFIER+)
521 ;
522
523/* C11 section 6.5 Expressions: Grammar here is organized with a
524 * backwards order against the order of sub-sections in C11 standard,
525 * because it's a more viewful way to illustrate how expressions will
526 * be derived
527 */
528
529 /* ****************************** Expressions ******************************* */
530
531// SFS: why is this called a "term"? Why not "formula"?
532term
533 : quantifierExpression | assignmentExpression
534 ;
535
536quantifierExpression
537 : forall_key binders SEMI term
538 -> ^(QUANTIFIED forall_key binders term)
539 | exists_key binders SEMI term
540 -> ^(QUANTIFIED exists_key binders term)
541 | lambda_key binders SEMI term
542 -> ^(LAMBDA_ACSL lambda_key binders term)
543 ;
544
545/* SFS: Does ACSL have an assignment expression?
546 * 6.5.16
547 * assignment-expression
548 * conditional-expression
549 * unary-expression assignment-operator assignment-expression
550 * Tree:
551 * Root: OPERATOR
552 * Child 0: ASSIGN, in ACSL other side-effective assign operators
553 * are not allowed
554 * Child 1: ARGUMENT_LIST
555 * Child 1.0: unaryExpression
556 * Child 1.1: assignmentExpression
557 */
558assignmentExpression
559 : (unaryExpression ASSIGN)=> unaryExpression ASSIGN assignmentExpression
560 -> ^(OPERATOR ASSIGN
561 ^(ARGUMENT_LIST unaryExpression assignmentExpression))
562 | conditionalExpression
563 ;
564
565assignmentExpression_opt
566 : -> ABSENT
567 | assignmentExpression
568 ;
569
570/* 6.5.15
571 * In C11 it is
572 * conditional-expression:
573 * logical-OR-expression
574 * logical-OR-expression ? expression : conditional-expression
575 *
576 * Note: "a?b:c?d:e". Is it (1) "(a?b:c)?d:e" or (2) "a?b:(c?d:e)".
577 * Answer is (2), it is "right associative".
578 *
579 * Note: the order matters in the two alternatives below.
580 * The alternatives are tried in order from first to last.
581 * Therefore it is necessary for the non-empty to appear first.
582 * Else the empty will always be matched.
583 */
584conditionalExpression
585 : a=logicalEquivExpression
586 ( QMARK b=conditionalExpression COLON
587 (c=quantifierExpression | c=conditionalExpression)
588 -> ^(OPERATOR QMARK ^(ARGUMENT_LIST $a $b $c))
589 | -> $a
590 )
591 ;
592
593/* ACSL Logical equivalence: a<==>b.
594 * Left associative: a<==>b<==>c means (a<==>b)<==>c.
595 */
596logicalEquivExpression
597 : (a=logicalImpliesExpression -> $a)
598 ( EQUIV_ACSL (b=quantifierExpression | b=logicalImpliesExpression)
599 -> ^(OPERATOR EQUIV_ACSL ^(ARGUMENT_LIST $logicalEquivExpression $b))
600 )*
601 ;
602
603/* ACSL logical implies expression: a==>b.
604 * NOTE: *RIGHT* associative: a==>b==>c is a==>(b==>c).
605 */
606logicalImpliesExpression
607 : a=logicalOrExpression
608 ( op=(IMPLIES|IMPLIES_ACSL) (b=quantifierExpression | b=logicalImpliesExpression)
609 -> ^(OPERATOR $op ^(ARGUMENT_LIST $a $b))
610 | -> $a
611 )
612 ;
613
614/* logical-OR-expression: a||b.
615 * Left associative: a||b||c is (a||b)||c.
616 */
617logicalOrExpression
618 : (a=logicalXorExpression -> $a)
619 ( OR (b=quantifierExpression | b=logicalXorExpression)
620 -> ^(OPERATOR OR ^(ARGUMENT_LIST $logicalOrExpression $b))
621 )*
622 ;
623
624/* ACSL logical exclusive or: a^^b.
625 * Left associative.
626 */
627logicalXorExpression
628 : (a=logicalAndExpression -> $a)
629 ( XOR_ACSL (b=quantifierExpression | b=logicalAndExpression)
630 -> ^(OPERATOR XOR_ACSL ^(ARGUMENT_LIST $logicalXorExpression $b))
631 )*
632 ;
633
634/* 6.5.13, logical and: a && b.
635 * Left associative.
636 */
637logicalAndExpression
638 : (a=bitwiseEquivExpression -> $a)
639 ( AND (b=quantifierExpression | b=bitwiseEquivExpression)
640 -> ^(OPERATOR AND ^(ARGUMENT_LIST $logicalAndExpression $b))
641 )*
642 ;
643
644/* ACSL bitwise equivalence: a <--> b.
645 * Left associative.
646 */
647bitwiseEquivExpression
648 : (a=bitwiseImpliesExpression -> $a)
649 ( bitequiv_op b=bitwiseImpliesExpression
650 -> ^(OPERATOR BEQUIV_ACSL ^(ARGUMENT_LIST $bitwiseEquivExpression $b))
651 )*
652 ;
653
654/* ACSL bitwise implies: a-->b.
655 * RIGHT associative
656 */
657bitwiseImpliesExpression
658 : a=inclusiveOrExpression
659 ( op=bitimplies_op b=bitwiseImpliesExpression
660 -> ^(OPERATOR BIMPLIES_ACSL ^(ARGUMENT_LIST $a $b))
661 | -> $a
662 )
663 ;
664
665// TODO: SFS: look at this, it doesn't make sense...
666/* 6.5.12 *
667 * Bitwise inclusive OR
668 * inclusive-OR-expression:
669 * exclusive-OR-expression
670 * inclusive-OR-expression | exclusive-OR-expression
671 *
672 * Note: the syntatic predicate before BITOR is to solve the ambiguity with
673 * set expressions because ACSL type names are parsed as IDENTIFIER tokens.
674 * For example, {a|integer | integer a; a<10}.
675 * The first | is a bitor operator and the first "integer" is some variable name.
676 * Without the predicate, the grammar would consider the second | as an bitor operator
677 * and crashes, because "integer" is an IDENTIFIER token and it thinkgs that the second
678 * "integer" is an identifier expression.
679 */
680inclusiveOrExpression
681 : ( exclusiveOrExpression -> exclusiveOrExpression )
682 ( {!(input.LA(2)==IDENTIFIER && input.LA(3)==IDENTIFIER)}?BITOR y=exclusiveOrExpression
683 -> ^(OPERATOR BITOR ^(ARGUMENT_LIST $inclusiveOrExpression $y))
684 )*
685 ;
686
687/* 6.5.11 *
688 * Bitwise exclusive OR
689 * exclusive-OR-expression:
690 * AND-expression
691 * exclusive-OR-expression ^ AND-expression
692 */
693exclusiveOrExpression
694 : ( andExpression -> andExpression )
695 ( BITXOR y=andExpression
696 -> ^(OPERATOR BITXOR ^(ARGUMENT_LIST $exclusiveOrExpression $y))
697 )*
698 ;
699
700/* 6.5.10 *
701 * Bitwise AND
702 * AND-expression
703 * equality-expression
704 * AND-expression & equality-expression
705 */
706andExpression
707 : ( relationalExpression -> relationalExpression )
708 ( AMPERSAND y=relationalExpression
709 -> ^(OPERATOR AMPERSAND ^(ARGUMENT_LIST $andExpression $y))
710 )*
711 ;
712
713
714/*
715 Note on ACSL relational expressions, from the ACSL manual:
716 The construct t1 relop1 t2 relop2 t3 · · · tk
717 with several consecutive comparison operators is a shortcut
718 (t1 relop1 t2) && (t2 relop2 t3) && ···.
719 It is required that the relopi operators must be in the same “direction”,
720 i.e. they must all belong either to {<, <=, ==} or to {>,>=,==}.
721 Expressions such as x < y > z or x != y != z are not allowed.
722
723 Also, <,<=,>=,> have higher precedence than == and !=. Though
724 not sure what that means, so ignoring it.
725
726 "a<b==c" means "a<b && b==c".
727
728 a<b<c<d : (and (a<b) (and (b<c) (c<d)))
729
730 Grammar: The following works but doesn't check for illegal expressions.
731 Better: create a new node RELCHAIN
732 args: a < b <= c < d, in order, then check and assemble in Java code.
733
734relationalExpression
735 : x=shiftExpression
736 ( r=relChain[(Tree)$x.tree] -> $r
737 | -> $x
738 )
739 ;
740
741// t is the tree of a single shiftExpression, t < y (< ...)
742relChain[Tree t]
743 : r=relOp y=shiftExpression
744 ( z=relChain[(Tree)$y.tree]
745 -> ^(OPERATOR AND ^(ARGUMENT_LIST
746 ^(OPERATOR $r ^(ARGUMENT_LIST {$t} $y))
747 $z))
748 | -> ^(OPERATOR $r ^(ARGUMENT_LIST {$t} $y))
749 )
750 ;
751*/
752
753/* A relational operator */
754relOp: EQUALS | NEQ | LT | LTE | GT | GTE ;
755
756/* A relational expression or chain of such expressions.
757 * Returns a tree with root RELCHAIN and then the sequence
758 * that alternates shiftExpression, relational operator,
759 * and begins and ends with a shiftExpression.
760 */
761relationalExpression
762 : x=shiftExpression
763 ( (s+=relOp s+=shiftExpression)+ -> ^(RELCHAIN $x $s*)
764 | -> $x
765 )
766 ;
767
768
769/* 6.5.7 *
770 * In C11:
771 * shift-expression:
772 * additive-expression
773 * shift-expression <</>> additive-expression
774 *
775 * CIVL-C extends C11 with a range-expression. see range-expression
776 * shift-expression:
777 * range-expression:
778 * shift-expression <</>> range-expression
779 */
780shiftExpression
781 : (rangeExpression -> rangeExpression)
782 ( SHIFTLEFT y=rangeExpression
783 -> ^(OPERATOR SHIFTLEFT ^(ARGUMENT_LIST $shiftExpression $y))
784 | SHIFTRIGHT y=rangeExpression
785 -> ^(OPERATOR SHIFTRIGHT ^(ARGUMENT_LIST $shiftExpression $y))
786 )*
787 ;
788
789/* 6.5.6.5 *
790 *
791 * CIVL-C range expression "lo .. hi" or "lo .. hi # step"
792 * a + b .. c + d is equivalent to (a + b) .. (c + d)
793 * (*,/,%) > (+,-) > range > shift > ...
794 */
795rangeExpression
796 : x=additiveExpression
797 ( DOTDOT s=rangeSuffix -> ^(DOTDOT $x $s)
798 | -> $x
799 )
800 ;
801
802rangeSuffix
803 : additiveExpression (HASH! additiveExpression)?
804 ;
805
806/* 6.5.6 *
807 * additive-expression:
808 * multiplicative-expression
809 * additive-expression +/- multiplicative-expression
810 */
811additiveExpression
812 : (multiplicativeExpression -> multiplicativeExpression)
813 ( PLUS y=multiplicativeExpression
814 -> ^(OPERATOR PLUS ^(ARGUMENT_LIST $additiveExpression $y))
815 | SUB y=multiplicativeExpression
816 -> ^(OPERATOR SUB ^(ARGUMENT_LIST $additiveExpression $y))
817 )*
818 ;
819
820/* 6.5.5 *
821 * In C11:
822 * multiplicative-expression:
823 * cast-expression
824 * multiplicative-expression STAR/DIV/MOD cast-expression
825 */
826multiplicativeExpression
827 : (castExpression -> castExpression)
828 ( STAR y=castExpression
829 -> ^(OPERATOR STAR ^(ARGUMENT_LIST $multiplicativeExpression $y))
830 | DIV y=castExpression
831 -> ^(OPERATOR DIV ^(ARGUMENT_LIST $multiplicativeExpression $y))
832 | MOD y=castExpression
833 -> ^(OPERATOR MOD ^(ARGUMENT_LIST $multiplicativeExpression $y))
834 )*
835 ;
836
837/* 6.5.4 *
838 * cast-expression:
839 * unary-expression
840 * (type-name) cast-expression
841 *
842 */
843// ambiguity 1: (expr) is a unary expression and looks like (typeName).
844// ambiguity 2: (typeName){...} is a compound literal and looks like cast
845castExpression
846 : (LPAREN type_expr RPAREN)=> l=LPAREN type_expr RPAREN castExpression
847 -> ^(CAST type_expr castExpression)
848 | unaryExpression
849 ;
850
851/* 6.5.3 *
852 * unary-expression:
853 * postfix-expression
854 * ++/--/sizeof unary-expression
855 * unary-operator cast-expression
856 * sizeof (type-name)
857 */
858unaryExpression
859 : postfixExpression
860 | unary_op (b=castExpression | b=quantifierExpression)
861 -> ^(OPERATOR unary_op ^(ARGUMENT_LIST $b))
862 | (SIZEOF LPAREN type_expr)=> SIZEOF LPAREN type_expr RPAREN
863 -> ^(SIZEOF_TYPE type_expr)
864 | SIZEOF unaryExpression
865 -> ^(SIZEOF_EXPR unaryExpression)
866 | union_key LPAREN argumentExpressionList RPAREN
867 -> ^(UNION_ACSL union_key argumentExpressionList RPAREN)
868 | inter_key LPAREN argumentExpressionList RPAREN
869 -> ^(INTER inter_key argumentExpressionList RPAREN)
870 | valid_key LPAREN term RPAREN
871 -> ^(VALID valid_key term RPAREN)
872 | extendedQuantification ->^(QUANTIFIED_EXT extendedQuantification)
873 | object_of_key LPAREN term RPAREN -> ^(OBJECT_OF object_of_key LPAREN term RPAREN)
874 | mpi_expression -> ^(MPI_EXPRESSION mpi_expression)
875 | old_key LPAREN term RPAREN
876 -> ^(OLD old_key term RPAREN)
877 ;
878
879extendedQuantification
880 : sum_key LPAREN term COMMA term COMMA term RPAREN
881 -> ^(SUM sum_key term+)
882 | max_key LPAREN term COMMA term COMMA term RPAREN
883 -> ^(MAX max_key term+)
884 | min_key LPAREN term COMMA term COMMA term RPAREN
885 -> ^(MIN min_key term+)
886 | product_key LPAREN term COMMA term COMMA term RPAREN
887 -> ^(PROD product_key term+)
888 | numof_key LPAREN term COMMA term COMMA term RPAREN
889 -> ^(NUMOF numof_key term+)
890 ;
891
892/* 6.5.2 *
893 * postfix-expression:
894 * primary-expression
895 * postfix-expression [expression]
896 * postfix-expression (argument-expression-list)
897 * postfix-expression . identifier
898 * postfix-expression -> identifier
899 * postfix-expression ++
900 * postfix-expression --
901 * (type-name) {initializer-list}
902 * (type-name) {initializer-list, }
903 */
904postfixExpression
905 : (primaryExpression -> primaryExpression)
906 // array index operator:
907 ( l=LSQUARE term RSQUARE
908 -> ^(OPERATOR
909 INDEX[$l]
910 ^(ARGUMENT_LIST $postfixExpression term)
911 RSQUARE)
912 | // function call:
913 LPAREN argumentExpressionList RPAREN
914 -> ^(FUNC_CALL $postfixExpression argumentExpressionList
915 )
916 | DOT IDENTIFIER
917 -> ^(DOT $postfixExpression IDENTIFIER)
918 | ARROW IDENTIFIER
919 -> ^(ARROW $postfixExpression IDENTIFIER)
920 )*
921 ;
922
923/* 6.5.2 */
924argumentExpressionList
925 : -> ^(ARGUMENT_LIST)
926 | assignmentExpression (COMMA assignmentExpression)*
927 -> ^(ARGUMENT_LIST assignmentExpression+)
928 ;
929
930/* 6.5.1 */
931primaryExpression
932 : constant
933 | IDENTIFIER
934 | STRING_LITERAL
935 | LCURLY term BITOR binders (SEMI term)? RCURLY
936 ->^(SET_BINDERS term binders term?)
937 | LCURLY term RCURLY
938 ->^(SET_SIMPLE term)
939 | LPAREN term RPAREN
940 -> ^(TERM_PARENTHESIZED term)
941 | remoteExpression
942 ;
943
944
945/* 6.5.0.1 *
946 * remote-expression:
947 * REMOTE_ACCESS ( identifier , shiftExpression ).
948 * A remote-expression should be used in the same way as a variable
949 * identifier.
950 */
951remoteExpression
952 : remote_key LPAREN a=shiftExpression COMMA b=term RPAREN
953 -> ^(REMOTE_ACCESS remote_key $a $b)
954 ;
955
956/* 6.6 */
957constantExpression
958 : conditionalExpression
959 ;
960
961constant
962 : INTEGER_CONSTANT
963 | FLOATING_CONSTANT
964 | CHARACTER_CONSTANT
965 | true_key | false_key | result_key | nothing_key | ELLIPSIS
966 | SELF | null_key
967 | mpi_constant -> ^(MPI_CONSTANT mpi_constant)
968 ;
969
970/* ACSL-MPI extensions Expressions and Constants */
971mpi_expression
972 : mpiemptyin_key LPAREN term RPAREN
973 -> ^(MPI_EMPTY_IN mpiemptyin_key term)
974 | mpiemptyout_key LPAREN term RPAREN
975 -> ^(MPI_EMPTY_OUT mpiemptyout_key term)
976 | mpiagree_key LPAREN a=term RPAREN
977 -> ^(MPI_AGREE mpiagree_key $a)
978 | mpiregion_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
979 -> ^(MPI_REGION mpiregion_key $a $b $c)
980 | mpireduce_key LPAREN a=term COMMA b=term COMMA c=term COMMA d=term RPAREN
981 -> ^(MPI_REDUCE mpireduce_key $a $b $c $d)
982 | mpiequals_key LPAREN a=term COMMA b=term RPAREN
983 -> ^(MPI_EQUALS mpiequals_key $a $b)
984 | mpiextent_key LPAREN a=primaryExpression RPAREN
985 -> ^(MPI_EXTENT mpiextent_key $a)
986 | mpioffset_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
987 -> ^(MPI_OFFSET mpioffset_key $a $b $c)
988 | mpivalid_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
989 -> ^(MPI_VALID mpivalid_key $a $b $c)
990 | absent_key a=absent_event after_key b=absent_event until_key c=absent_event
991 -> ^(MPI_ABSENT $a $b $c)
992 ;
993
994absent_event
995: absent_event_sendto_key LPAREN a=term COMMA b=term RPAREN
996 -> ^(ABSENT_EVENT_SENDTO $a $b)
997 | absent_event_sendfrom_key LPAREN a=term COMMA b=term RPAREN
998 -> ^(ABSENT_EVENT_SENDFROM $a $b)
999 | absent_event_enter_key a=absent_event_optional_argument
1000 -> ^(ABSENT_EVENT_ENTER $a)
1001 | absent_event_exit_key a=absent_event_optional_argument
1002 -> ^(ABSENT_EVENT_EXIT $a)
1003;
1004
1005absent_event_optional_argument
1006 : LPAREN term RPAREN
1007 -> ^(TERM_PARENTHESIZED term)
1008 | -> ABSENT
1009 ;
1010
1011mpi_constant
1012 : mpicommrank_key | mpicommsize_key
1013 ;
1014
1015mpi_collective_kind
1016 : col_key | p2p_key | both_key
1017 ;
1018
1019bitimplies_op
1020 : MINUSMINUS GT
1021 ;
1022
1023bitequiv_op
1024 : LT MINUSMINUS GT
1025 ;
1026
1027unary_op
1028 : PLUS | SUB | NOT | TILDE | STAR | AMPERSAND
1029 ;
1030
1031/* rules for ACSL types */
1032boolean_type
1033 : {input.LT(1).getText().equals("boolean")}? IDENTIFIER
1034 -> ^(BOOLEAN IDENTIFIER)
1035 ;
1036
1037integer_type
1038 : {input.LT(1).getText().equals("integer")}? IDENTIFIER
1039 -> ^(INTEGER IDENTIFIER)
1040 ;
1041
1042real_type
1043 : {input.LT(1).getText().equals("real")}? IDENTIFIER
1044 -> ^(REAL_ACSL IDENTIFIER)
1045 ;
1046
1047/* rules for ACSL contract clause keywords */
1048
1049alloc_key
1050 : {input.LT(1).getText().equals("allocates")}? IDENTIFIER
1051 ;
1052
1053assigns_key
1054 : {input.LT(1).getText().equals("assigns")}? IDENTIFIER
1055 ;
1056
1057assumes_key
1058 : {input.LT(1).getText().equals("assumes")}? IDENTIFIER
1059 ;
1060
1061assert_key
1062 : {input.LT(1).getText().equals("assert")}? IDENTIFIER
1063 ;
1064
1065behaviors_key
1066 : {input.LT(1).getText().equals("behaviors")}? IDENTIFIER
1067 ;
1068
1069behavior_key
1070 : {input.LT(1).getText().equals("behavior")}? IDENTIFIER
1071 ;
1072
1073completes_key
1074 : {input.LT(1).getText().equals("complete")}? IDENTIFIER
1075 ;
1076
1077decreases_key
1078 : {input.LT(1).getText().equals("decreases")}? IDENTIFIER
1079 ;
1080
1081disjoint_key
1082 : {input.LT(1).getText().equals("disjoint")}? IDENTIFIER
1083 ;
1084
1085ensures_key
1086 : {input.LT(1).getText().equals("ensures")}? IDENTIFIER
1087 ;
1088
1089frees_key
1090 : {input.LT(1).getText().equals("frees")}? IDENTIFIER
1091 ;
1092
1093focus_key
1094 : {input.LT(1).getText().equals("focus")}? IDENTIFIER
1095 ;
1096
1097invariant_key
1098 : {input.LT(1).getText().equals("invariant")}? IDENTIFIER
1099 ;
1100
1101loop_key
1102 : {input.LT(1).getText().equals("loop")}? IDENTIFIER
1103 ;
1104
1105requires_key
1106 : {input.LT(1).getText().equals("requires")}? IDENTIFIER
1107 ;
1108
1109terminates_key
1110 : {input.LT(1).getText().equals("terminates")}? IDENTIFIER
1111 ;
1112
1113variant_key
1114 : {input.LT(1).getText().equals("variant")}? IDENTIFIER
1115 ;
1116
1117waitsfor_key
1118 : {input.LT(1).getText().equals("waitsfor")}? IDENTIFIER
1119 ;
1120
1121predicate_key
1122 : {input.LT(1).getText().equals("predicate")}? IDENTIFIER
1123 ;
1124
1125logic_specifier_key
1126 : {input.LT(1).getText().equals("logic")}? IDENTIFIER
1127 ;
1128
1129/* ACSL terms keywords */
1130/* keywords of terms */
1131empty_key
1132 : {input.LT(1).getText().equals("\\empty")}? EXTENDED_IDENTIFIER
1133 ;
1134
1135exists_key
1136 : {input.LT(1).getText().equals("\\exists")}? EXTENDED_IDENTIFIER
1137 -> ^(EXISTS_ACSL EXTENDED_IDENTIFIER)
1138 ;
1139
1140false_key
1141 : {input.LT(1).getText().equals("\\false")}? EXTENDED_IDENTIFIER
1142 -> ^(FALSE_ACSL EXTENDED_IDENTIFIER)
1143 ;
1144
1145forall_key
1146 : {input.LT(1).getText().equals("\\forall")}? EXTENDED_IDENTIFIER
1147 -> ^(FORALL_ACSL EXTENDED_IDENTIFIER)
1148 ;
1149
1150inter_key
1151 : {input.LT(1).getText().equals("\\inter")}? EXTENDED_IDENTIFIER
1152 ;
1153
1154let_key
1155 : {input.LT(1).getText().equals("\\let")}? EXTENDED_IDENTIFIER
1156 ;
1157
1158nothing_key
1159 : {input.LT(1).getText().equals("\\nothing")}? EXTENDED_IDENTIFIER
1160 -> ^(NOTHING EXTENDED_IDENTIFIER)
1161 ;
1162
1163null_key
1164 : {input.LT(1).getText().equals("\\null")}? EXTENDED_IDENTIFIER
1165 -> ^(NULL_ACSL EXTENDED_IDENTIFIER)
1166 ;
1167
1168old_key
1169 : {input.LT(1).getText().equals("\\old")}? EXTENDED_IDENTIFIER
1170 ;
1171
1172result_key
1173 : {input.LT(1).getText().equals("\\result")}? EXTENDED_IDENTIFIER
1174 -> ^(RESULT_ACSL EXTENDED_IDENTIFIER)
1175 ;
1176
1177true_key
1178 : {input.LT(1).getText().equals("\\true")}? EXTENDED_IDENTIFIER
1179 -> ^(TRUE_ACSL EXTENDED_IDENTIFIER)
1180 ;
1181
1182union_key
1183 : {input.LT(1).getText().equals("\\union")}? EXTENDED_IDENTIFIER
1184 ;
1185
1186valid_key
1187 : {input.LT(1).getText().equals("\\valid")}? EXTENDED_IDENTIFIER
1188 ;
1189
1190with_key
1191 : {input.LT(1).getText().equals("\\with")}? EXTENDED_IDENTIFIER
1192 ;
1193
1194/* ACSL CIVL extension */
1195executeswhen_key
1196 : {input.LT(1).getText().equals("executes_when")}? IDENTIFIER
1197 ;
1198
1199pure_key
1200 : {input.LT(1).getText().equals("pure")}? IDENTIFIER
1201 -> ^(PURE IDENTIFIER)
1202 ;
1203
1204reads_key
1205 : {input.LT(1).getText().equals("reads")}? IDENTIFIER
1206 ;
1207
1208remote_key
1209 : {input.LT(1).getText().equals("\\on")}? EXTENDED_IDENTIFIER
1210 ;
1211
1212/* ACSL dependence-specification extension */
1213
1214access_key
1215 : {input.LT(1).getText().equals("\\access")}? EXTENDED_IDENTIFIER
1216// -> ^(ACCESS_ACSL EXTENDED_IDENTIFIER)
1217 ;
1218
1219anyact_key
1220 : {input.LT(1).getText().equals("\\anyact")}? EXTENDED_IDENTIFIER
1221 -> ^(ANYACT EXTENDED_IDENTIFIER)
1222 ;
1223
1224
1225call_key
1226 : {input.LT(1).getText().equals("\\call")}? EXTENDED_IDENTIFIER
1227 ;
1228
1229dependson_key
1230 : {input.LT(1).getText().equals("depends_on")}? IDENTIFIER
1231 ;
1232
1233object_of_key
1234 : {input.LT(1).getText().equals("\\object_of")}? EXTENDED_IDENTIFIER
1235 ;
1236
1237read_key
1238 : {input.LT(1).getText().equals("\\read")}? EXTENDED_IDENTIFIER
1239// -> ^(READ_ACSL EXTENDED_IDENTIFIER)
1240 ;
1241
1242region_of_key
1243 : {input.LT(1).getText().equals("\\region_of")}? EXTENDED_IDENTIFIER
1244 ;
1245
1246write_key
1247 : {input.LT(1).getText().equals("\\write")}? EXTENDED_IDENTIFIER
1248// -> ^(WRITE_ACSL EXTENDED_IDENTIFIER)
1249 ;
1250
1251/* ACSL MPI-extension keywords */
1252
1253both_key
1254 : {input.LT(1).getText().equals("BOTH")}? IDENTIFIER
1255 -> ^(BOTH IDENTIFIER)
1256 ;
1257
1258col_key
1259 : {input.LT(1).getText().equals("COL")}? IDENTIFIER
1260 -> ^(COL IDENTIFIER)
1261 ;
1262
1263p2p_key
1264 : {input.LT(1).getText().equals("P2P")}? IDENTIFIER
1265 -> ^(P2P IDENTIFIER)
1266 ;
1267
1268mpiagree_key
1269 : {input.LT(1).getText().equals("\\mpi_agree")}? EXTENDED_IDENTIFIER
1270// -> ^(MPI_AGREE EXTENDED_IDENTIFIER)
1271 ;
1272
1273mpicollective_key
1274 : {input.LT(1).getText().equals("\\mpi_collective")}? EXTENDED_IDENTIFIER
1275// -> ^(MPI_COLLECTIVE EXTENDED_IDENTIFIER)
1276 ;
1277
1278mpicommsize_key
1279 : {input.LT(1).getText().equals("\\mpi_comm_size")}? EXTENDED_IDENTIFIER
1280 -> ^(MPI_COMM_SIZE EXTENDED_IDENTIFIER)
1281 ;
1282
1283mpicommrank_key
1284 : {input.LT(1).getText().equals("\\mpi_comm_rank")}? EXTENDED_IDENTIFIER
1285 -> ^(MPI_COMM_RANK EXTENDED_IDENTIFIER)
1286 ;
1287
1288mpiemptyin_key
1289 : {input.LT(1).getText().equals("\\mpi_empty_in")}? EXTENDED_IDENTIFIER
1290// -> ^(MPI_EMPTY_IN EXTENDED_IDENTIFIER)
1291 ;
1292
1293mpiemptyout_key
1294 : {input.LT(1).getText().equals("\\mpi_empty_out")}? EXTENDED_IDENTIFIER
1295// -> ^(MPI_EMPTY_OUT EXTENDED_IDENTIFIER)
1296 ;
1297
1298mpiequals_key
1299 : {input.LT(1).getText().equals("\\mpi_equals")}? EXTENDED_IDENTIFIER
1300// -> ^(MPI_EQUALS EXTENDED_IDENTIFIER)
1301 ;
1302
1303mpiextent_key
1304 : {input.LT(1).getText().equals("\\mpi_extent")}? EXTENDED_IDENTIFIER
1305// -> ^(MPI_EXTENT EXTENDED_IDENTIFIER)
1306 ;
1307
1308mpioffset_key
1309 : {input.LT(1).getText().equals("\\mpi_offset")}? EXTENDED_IDENTIFIER
1310// -> ^(MPI_OFFSET EXTENDED_IDENTIFIER)
1311 ;
1312
1313mpivalid_key
1314 : {input.LT(1).getText().equals("\\mpi_valid")}? EXTENDED_IDENTIFIER
1315 ;
1316
1317mpiregion_key
1318 : {input.LT(1).getText().equals("\\mpi_region")}? EXTENDED_IDENTIFIER
1319 ;
1320
1321mpireduce_key
1322 : {input.LT(1).getText().equals("\\mpi_reduce")}? EXTENDED_IDENTIFIER
1323 ;
1324
1325absent_key
1326 : {input.LT(1).getText().equals("\\absentof")}? EXTENDED_IDENTIFIER
1327 ;
1328
1329after_key
1330 : {input.LT(1).getText().equals("\\after")}? EXTENDED_IDENTIFIER
1331 ;
1332
1333until_key
1334 : {input.LT(1).getText().equals("\\until")}? EXTENDED_IDENTIFIER
1335 ;
1336
1337absent_event_sendto_key
1338 : {input.LT(1).getText().equals("\\sendto")}? EXTENDED_IDENTIFIER
1339 ;
1340
1341absent_event_sendfrom_key
1342 : {input.LT(1).getText().equals("\\sendfrom")}? EXTENDED_IDENTIFIER
1343 ;
1344
1345absent_event_enter_key
1346 : {input.LT(1).getText().equals("\\enter")}? EXTENDED_IDENTIFIER
1347 ;
1348
1349absent_event_exit_key
1350 : {input.LT(1).getText().equals("\\exit")}? EXTENDED_IDENTIFIER
1351 ;
1352
1353/** ACSL higher-order keywords */
1354lambda_key
1355 : {input.LT(1).getText().equals("\\lambda")}? EXTENDED_IDENTIFIER
1356 ;
1357
1358sum_key
1359 : {input.LT(1).getText().equals("\\sum")}? EXTENDED_IDENTIFIER
1360 ;
1361
1362max_key
1363 : {input.LT(1).getText().equals("\\max")}? EXTENDED_IDENTIFIER
1364 ;
1365
1366min_key
1367 : {input.LT(1).getText().equals("\\min")}? EXTENDED_IDENTIFIER
1368 ;
1369
1370product_key
1371 : {input.LT(1).getText().equals("\\product")}? EXTENDED_IDENTIFIER
1372 ;
1373
1374numof_key
1375 : {input.LT(1).getText().equals("\\numof")}? EXTENDED_IDENTIFIER
1376 ;
Note: See TracBrowser for help on using the repository browser.