From 3ce322ba3a4637634dd4dd66b0097b8a9e12e978 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 5 Nov 2020 14:41:10 +0100
Subject: [PATCH] [parser] Merge "assigns x, x, ..."
---
src/kernel_internals/parsing/logic_parser.mly | 2 +-
tests/syntax/multiple_assigns.i | 10 ++++++++++
tests/syntax/oracle/multiple_assigns.res.oracle | 11 +++++++++++
3 files changed, 22 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/multiple_assigns.i
create mode 100644 tests/syntax/oracle/multiple_assigns.res.oracle
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 121ad96facc..9b7cde38cfc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -151,7 +151,7 @@
| Writes [], _ | Writes _, [] ->
raise (
Not_well_formed (loc(),"Mixing \\nothing and a real location"))
- | Writes a1, a2 -> Writes (concat_froms a2 a1)
+ | Writes a1, a2 -> Writes (concat_froms (concat_froms [] a2) a1)
let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
(* NB: this is supposed to merge assigns related to named behaviors, in
diff --git a/tests/syntax/multiple_assigns.i b/tests/syntax/multiple_assigns.i
new file mode 100644
index 00000000000..d20a1dfcda4
--- /dev/null
+++ b/tests/syntax/multiple_assigns.i
@@ -0,0 +1,10 @@
+int z;
+
+/*@ assigns z, z;
+ assigns z \from z;
+ assigns z, z;
+ */
+void function(void)
+{
+ return;
+}
diff --git a/tests/syntax/oracle/multiple_assigns.res.oracle b/tests/syntax/oracle/multiple_assigns.res.oracle
new file mode 100644
index 00000000000..0cda603d543
--- /dev/null
+++ b/tests/syntax/oracle/multiple_assigns.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/multiple_assigns.i (no preprocessing)
+/* Generated by Frama-C */
+int z;
+/*@ assigns z;
+ assigns z \from z; */
+void function(void)
+{
+ return;
+}
+
+
--
GitLab