From 336f28f6dbd506ccd000ebb82e7f1b0fc12194ec Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 5 Nov 2020 16:02:41 +0100
Subject: [PATCH] [parser] Merge assigns dependencies
---
src/kernel_internals/parsing/logic_parser.mly | 29 +++++++++++++------
tests/syntax/multiple_froms.i | 13 +++++++++
tests/syntax/oracle/multiple_froms.res.oracle | 18 ++++++++++++
3 files changed, 51 insertions(+), 9 deletions(-)
create mode 100644 tests/syntax/multiple_froms.i
create mode 100644 tests/syntax/oracle/multiple_froms.res.oracle
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 9b7cde38cfc..6b215c69952 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -109,32 +109,43 @@
let loc_ext d = { extended_node = d; extended_loc = loc () }
+ let concat_deps ds1 ds2 =
+ let fold ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
+ let ds = List.fold_left fold [] ds1 in
+ let ds = List.fold_left fold ds ds2 in
+ List.rev ds
+
+ let filter_from (l, d) =
+ match d with
+ | From ds -> l, From (concat_deps [] ds)
+ | _ -> l, d
+
let concat_froms a1 a2 =
- let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
+ let compare_pair (l1,_) (l2,_) = is_same_lexpr l1 l2 in
(* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
- let concat_one acc (_,f2 as p) =
+ let concat_one acc (l,d2 as f2) =
try
- let (_,f1) = List.find (compare_pair p) acc
+ let (_,d1) = List.find (compare_pair f2) acc
in
- match (f1, f2) with
+ match (d1, d2) with
| _,FromAny ->
(* the new fundeps does not give more information than the one
which is already present. Just ignore it.
*)
acc
- | FromAny, _ ->
+ | FromAny, From _ ->
(* the new fundeps is strictly more precise than the old one.
We replace the old dependency by the new one, but keep
the location at its old place in the list. This ensures
that we get the exact same clause if we try to
link the original contract with its pretty-printed version. *)
- Extlib.replace compare_pair p acc
- | From _, From _ ->
+ Extlib.replace compare_pair (filter_from f2) acc
+ | From ds1, From ds2 ->
(* we keep the two functional dependencies,
as they have to be proved separately. *)
- acc @ [p]
- with Not_found -> acc @ [p]
+ Extlib.replace compare_pair (l, From (concat_deps ds1 ds2)) acc
+ with Not_found -> acc @ [filter_from f2]
in List.fold_left concat_one a1 a2
let concat_allocation fa1 fa2 =
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
new file mode 100644
index 00000000000..9903819400f
--- /dev/null
+++ b/tests/syntax/multiple_froms.i
@@ -0,0 +1,13 @@
+int a, b, c, d, e;
+
+/*@ assigns a;
+ assigns a \from a, a, b, c, c;
+ assigns a \from c, b, d, e, a;
+ assigns a;
+ assigns b \from a, e, b, d, c;
+ assigns c \from c, c, c, c, c;
+ */
+void function(void)
+{
+ return;
+}
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
new file mode 100644
index 00000000000..ea197945fc7
--- /dev/null
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -0,0 +1,18 @@
+[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
+/* Generated by Frama-C */
+int a;
+int b;
+int c;
+int d;
+int e;
+/*@ assigns a, b, c;
+ assigns a \from a, b, c, d, e;
+ assigns b \from a, e, b, d, c;
+ assigns c \from c;
+ */
+void function(void)
+{
+ return;
+}
+
+
--
GitLab