Merge branch 'fix/virgile/filter-qualifier-logic' into 'master'

[logic] fix qualifier parsing

See merge request frama-c/frama-c!2404

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 }

tests/spec/oracle/rm_qualifiers.res.oracle

+[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;
+}
+
+

tests/spec/rm_qualifiers.i

+/* 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]);
+}