diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index e39192b490684a67476a3993da30dbc8891f03ae..693f028f73a6392c115639f0086fae6cb5efacde 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 3fb10b206242fb7ebb8db899d5f1afc83f325ecb..9bc3b301edaa688add1e2ea3012fb778c3f81ba1 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" }