From 676b1078fd0e50664a8967caf5882d4b366036a4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 18 Jan 2019 14:57:01 +0100
Subject: [PATCH] [ACSL] fixes acceptance of identifier with ACSL keyword in
volatile clauses
---
src/kernel_internals/parsing/logic_lexer.mll | 6 ++++--
src/kernel_internals/parsing/logic_parser.mly | 6 ++++--
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index e39192b4906..693f028f73a 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -127,7 +127,8 @@
"module", MODULE, false;(* ACSL extension for external spec file *)
"pragma", PRAGMA, false;
"predicate", PREDICATE, false;
- "reads", READS, false;
+ "reads", READS, true; (* treated specifically in the parser to
+ avoid issue in volatile clause. *)
"requires", REQUIRES, false;
"returns", RETURNS, false;
"short", SHORT, true;
@@ -142,7 +143,8 @@
"variant", VARIANT, false;
"void", VOID, true;
"volatile", VOLATILE, true;
- "writes", WRITES, false;
+ "writes", WRITES, true; (* treated specifically in the parser to
+ avoid issue in volatile clause. *)
];
List.iter (fun (x, y) -> Hashtbl.add type_kw x y)
["integer", INTEGER; "real", REAL; "boolean", BOOLEAN; ];
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 3fb10b20624..9bc3b301eda 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -880,7 +880,7 @@ full_zones:
;
full_ne_zones:
-| enter_kw_c_mode zones exit_kw_c_mode { $2 }
+| enter_kw_c_mode ne_zones exit_kw_c_mode { $2 }
;
full_ne_lexpr_list:
@@ -1758,6 +1758,8 @@ identifier_or_typename:
identifier:
| IDENTIFIER { $1 }
+| READS { "reads" }
+| WRITES { "writes" }
;
bounded_var:
@@ -1798,7 +1800,7 @@ acsl_c_keyword:
;
post_cond:
-| ENSURES { Normal, "normal" }
+| ENSURES { Normal, "ensures" }
| EXITS { Exits, "exits" }
| BREAKS { Breaks, "breaks" }
| CONTINUES { Continues, "continues" }
--
GitLab