From 6fcf509c8a9936cce46d5fc1eac16121e723bb6e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 27 Jul 2022 20:36:13 +0200
Subject: [PATCH] [parsing] add missing cases in wildcard rules of ACSL parser
---
src/kernel_internals/parsing/logic_parser.mly | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index fb91e861657..d2bd2fcccbc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1145,7 +1145,13 @@ contract:
// use that to detect potentially missing ';' at end of clause
clause_kw:
| ADMIT_REQUIRES { "admit requires" }
+| ADMIT_INVARIANT { "admit invariant" }
+| ADMIT_LEMMA { "admit lemma" }
+| ADMIT_LOOP { "admit loop" }
| CHECK_REQUIRES { "check requires" }
+| CHECK_INVARIANT { "check invariant" }
+| CHECK_LEMMA { "check lemma" }
+| CHECK_LOOP { "check loop" }
| REQUIRES { "requires" }
| ASSUMES {"assumes"}
| ASSIGNS { "assigns" }
@@ -1495,6 +1501,8 @@ beg_pragma_or_code_annotation:
| INVARIANT {}
| CHECK_INVARIANT {}
| ADMIT_INVARIANT {}
+| CHECK_LOOP {}
+| ADMIT_LOOP {}
| EXT_CODE_ANNOT {}
;
@@ -1871,7 +1879,7 @@ identifier_or_typename: /* allowed as C field names */
| is_acsl_typename { $1 }
| TYPENAME { $1 } /* followed by the same list than 'identifier' */
| IDENTIFIER { $1 }
-/* token list used inside ascl clauses: */
+/* token list used inside acsl clauses: */
| BEHAVIORS { "behaviors" }
| LABEL { "label" }
| READS { "reads" }
@@ -1880,7 +1888,7 @@ identifier_or_typename: /* allowed as C field names */
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
| IDENTIFIER { $1 }
-/* token list used inside ascl clauses: */
+/* token list used inside acsl clauses: */
| BEHAVIORS { "behaviors" }
| LABEL { "label" }
| READS { "reads" }
@@ -1975,8 +1983,14 @@ is_acsl_decl_or_code_annot:
| IMPACT { "impact" }
| INDUCTIVE { "inductive" }
| INVARIANT { "invariant" }
+| ADMIT_INVARIANT { "admit invariant" }
+| CHECK_INVARIANT { "check invariant" }
| LEMMA { "lemma" }
+| ADMIT_LEMMA { "admit lemma" }
+| CHECK_LEMMA { "check lemma" }
| LOOP { "loop" }
+| ADMIT_LOOP { "admit loop" }
+| CHECK_LOOP { "check loop" }
| PRAGMA { "pragma" }
| PREDICATE { "predicate" }
| SLICE { "slice" }
--
GitLab