[parser] Narrow froms in case of inclusion

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

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)

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)

tests/syntax/multiple_froms.i

 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)
 {

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)
 {