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

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

Added ability to loop focus with an offset or over a contiguous window of values.

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