From b9a1eb430b05c3deb87a00d856f96be5dc147d5f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 3 Oct 2019 16:03:50 +0200
Subject: [PATCH] [logic] fix qualifier parsing
---
src/kernel_internals/parsing/logic_parser.mly | 4 ++--
tests/spec/oracle/rm_qualifiers.res.oracle | 14 ++++++++++++++
tests/spec/rm_qualifiers.i | 11 +++++++++++
3 files changed, 27 insertions(+), 2 deletions(-)
create mode 100644 tests/spec/oracle/rm_qualifiers.res.oracle
create mode 100644 tests/spec/rm_qualifiers.i
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index e5efe57447e..7d800ea9fe6 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 00000000000..c1fcfb54dce
--- /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 00000000000..66d6d336519
--- /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]);
+}
--
GitLab