diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index e5efe57447e06eca9c6d6a6bb409346c9dcb7372..7d800ea9fe6be22f57a17c8ecab9b301efba66b1 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -721,8 +721,8 @@ cv:
 
 type_spec_cv:
      type_spec { $1 }
-|    cv type_spec { LTattribute ($2, $1) }
-|    type_spec cv { LTattribute ($1, $2) }
+|    cv type_spec_cv { LTattribute ($2, $1) }
+|    type_spec_cv cv { LTattribute ($1, $2) }
 
 cast_logic_type:
  | type_spec_cv abs_spec_cv_option { $2 $1 }
diff --git a/tests/spec/oracle/rm_qualifiers.res.oracle b/tests/spec/oracle/rm_qualifiers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c1fcfb54dce01b8338946cf06f02e27845482c67
--- /dev/null
+++ b/tests/spec/oracle/rm_qualifiers.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/spec/rm_qualifiers.i (no preprocessing)
+[kernel] Parsing tests/spec/result/rm_qualifiers_res.i (no preprocessing)
+/* Generated by Frama-C */
+extern void G(void const *p);
+
+void *ptr;
+/*@ ensures ptr ≡ (void *)((int const volatile *)*(\old(ftab) + 1)); */
+void F(int const volatile (*ftab)[3], unsigned int const id)
+{
+  G((void const *)(*(ftab + 1)));
+  return;
+}
+
+
diff --git a/tests/spec/rm_qualifiers.i b/tests/spec/rm_qualifiers.i
new file mode 100644
index 0000000000000000000000000000000000000000..66d6d336519ad00ab153d800784078580d692d82
--- /dev/null
+++ b/tests/spec/rm_qualifiers.i
@@ -0,0 +1,11 @@
+/* run.config
+OPT: @PTEST_FILE@ -ocode @PTEST_DIR@/result/@PTEST_NAME@_res.i -print -then @PTEST_DIR@/result/@PTEST_NAME@_res.i -ocode="" -print
+*/
+extern void G(const void* p);
+typedef volatile int ARR[42][3];
+void* ptr;
+
+//@ ensures ptr == (void *)ftab[1];
+void F(const ARR ftab, const unsigned id) {
+  G((void *)ftab[1]);
+}