From f8f9cd0ff1c9890b41440e5241e7d5bdd80cfe5d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 6 Nov 2020 10:59:25 +0100
Subject: [PATCH] [parser] Narrow froms in case of inclusion
---
src/kernel_internals/parsing/logic_parser.mly | 25 +++++++++++--------
tests/rte/oracle/assign4.res.oracle | 4 +--
tests/rte/oracle/assign5.res.oracle | 4 +--
tests/syntax/multiple_froms.i | 10 +++++---
tests/syntax/oracle/multiple_froms.res.oracle | 4 +--
5 files changed, 25 insertions(+), 22 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index d96ad86c4f7..66cc4871b21 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -116,16 +116,16 @@
let f ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
l, From(List.(rev (fold_left f [] ds)))
- let concat_froms a1 a2 =
- let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
+ let concat_froms cura newa =
+ let compare_pair (curb,_) (newb,_) = is_same_lexpr curb newb in
(* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
- let concat_one acc (l, f2) =
- let (_, f2) as p = filter_from l f2 in
+ let concat_one acc (l, newf) =
+ let (_, newf) as p = filter_from l newf in
try
- let (_,f1) = List.find (compare_pair p) acc
+ let (_,curf) = List.find (compare_pair p) acc
in
- match (f1, f2) with
+ match (curf, newf) with
| _,FromAny ->
(* the new fundeps does not give more information than the one
which is already present. Just ignore it.
@@ -138,12 +138,15 @@
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 _ ->
- (* we keep the two functional dependencies,
- as they have to be proved separately. *)
- acc @ [p]
+ | From curl, From newl ->
+ let incl l lin =
+ List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
+ in
+ if incl curl newl then acc
+ else if incl newl curl then Extlib.replace compare_pair p acc
+ else acc @ [p]
with Not_found -> acc @ [p]
- in List.fold_left concat_one a1 a2
+ in List.fold_left concat_one cura newa
let concat_allocation fa1 fa2 =
match fa1,fa2 with
diff --git a/tests/rte/oracle/assign4.res.oracle b/tests/rte/oracle/assign4.res.oracle
index 4ce28ed1aba..143f1a6b3fc 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/tests/rte/oracle/assign4.res.oracle
@@ -6,9 +6,7 @@
int choose1(int min, int max);
/*@ assigns \result;
- assigns \result \from min, max;
- assigns \result \from min, max;
- */
+ assigns \result \from min, max; */
int choose2(int min, int max);
int main(void)
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index c72860ec208..b8dd6f9a540 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -2,13 +2,11 @@
[rte] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
- assigns *p \from x;
assigns *p \from \nothing; */
int f(int *p, int x);
/*@ assigns *p;
- assigns *p \from \nothing;
- assigns *p \from x; */
+ assigns *p \from \nothing; */
int g(int *p, int x);
int main(void)
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
index 9903819400f..6a0a25687f9 100644
--- a/tests/syntax/multiple_froms.i
+++ b/tests/syntax/multiple_froms.i
@@ -1,11 +1,15 @@
int a, b, c, d, e;
+// Reminder: assigns are visited in reverse
+
/*@ assigns a;
- assigns a \from a, a, b, c, c;
+ assigns a \from a, a, b, c, c; // more precise so replace the next one
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;
+ assigns b \from a, e, b, d, c; // is ignored because the next one is more precise
+ assigns b \from a, e;
+ assigns c \from c, c, c, c, c; // both are kept (no inclusion)
+ assigns c \from d;
*/
void function(void)
{
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
index eac436bb15e..421f9c3f94d 100644
--- a/tests/syntax/oracle/multiple_froms.res.oracle
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -7,9 +7,9 @@ int d;
int e;
/*@ assigns a, b, c;
assigns a \from a, b, c;
- assigns a \from c, b, d, e, a;
- assigns b \from a, e, b, d, c;
+ assigns b \from a, e;
assigns c \from c;
+ assigns c \from d;
*/
void function(void)
{
--
GitLab