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

main
Last change on this file was f7b746f, checked in by Alex Wilton <awilton@…>, 8 months ago

Added initial implementation of a focus "ordered" annotation. Also cleaned up a lot of warnings.

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