[ACSL] Accept ACSL keywords as C identifiers as volatile or logic reads zones

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:

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; */