From fe04c520feba4c68bcdd9813fa85dff11c5ab052 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 18 Jan 2019 11:37:01 +0100
Subject: [PATCH] [ACSL] Accept ACSL keywords as C identifiers as volatile or
logic reads zones
---
src/kernel_internals/parsing/logic_parser.mly | 8 ++++++--
tests/spec/kw.c | 11 +++++++++++
2 files changed, 17 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 86d705460a9..3fb10b20624 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -879,6 +879,10 @@ full_zones:
| enter_kw_c_mode zones exit_kw_c_mode { $2 }
;
+full_ne_zones:
+| enter_kw_c_mode zones exit_kw_c_mode { $2 }
+;
+
full_ne_lexpr_list:
enter_kw_c_mode ne_lexpr_list exit_kw_c_mode { $2 }
;
@@ -1476,7 +1480,7 @@ decl_list:
decl:
| GLOBAL INVARIANT any_identifier COLON full_lexpr SEMICOLON
{ LDinvariant ($3, $5) }
-| VOLATILE ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
+| VOLATILE full_ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
@@ -1652,7 +1656,7 @@ logic_decl_loc:
reads_clause:
| /* epsilon */ { None }
-| READS zones { Some $2 }
+| READS full_ne_zones { Some $2 }
;
typedef:
diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index 8ad24442c35..7b004bdb1c4 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -23,3 +23,14 @@ model{L}(l1,ll1) ==> model(Cons(0,l1),Cons(0,ll1));
} */
+/*@ axiomatic foo {
+ logic integer func(integer i) reads behavior;
+}
+*/
+
+volatile int assigns;
+
+int ensures(volatile int* a) { return *a; }
+void requires(volatile int*a, int v) { *a = v; }
+
+/*@ volatile assigns reads ensures writes requires; */
--
GitLab