[kernel] Clean from but do not merge them

src/kernel_internals/parsing/logic_parser.mly

@@ -124,7 +124,8 @@
     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 (l,d2 as f2)  =
+    let concat_one acc (_,d2 as f2)  =
+      let f2 = filter_from f2 in
       try
         let (_,d1) = List.find (compare_pair f2) acc
         in
@@ -140,11 +141,12 @@
                  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 (filter_from f2) acc
-          | From ds1, From ds2 ->
-            (* we merge the two functional dependencies. *)
-              Extlib.replace compare_pair (l, From (concat_deps ds1 ds2)) acc
-      with Not_found -> acc @ [filter_from f2]
+              Extlib.replace compare_pair f2 acc
+          | From _, From _ ->
+            (* we keep the two functional dependencies,
+               as they have to be proved separately. *)
+            acc @ [f2]
+      with Not_found -> acc @ [f2]
     in List.fold_left concat_one a1 a2
 
   let concat_allocation fa1 fa2 =

src/kernel_services/ast_printing/cil_printer.ml

@@ -2912,12 +2912,23 @@ class cil_printer () = object (self)
           (function (a,_) -> not (Logic_const.is_exit_status a.it_content))
           l
       in
+      let remove_duplicates l =
+        let same t1 t2 = Cil_datatype.Term.equal t1.it_content t2.it_content in
+        let rec aux l acc =
+          match l with
+          | [] -> acc
+          | (x,_) :: l when List.exists (same x) acc -> aux l acc
+          | (x,_) :: l -> aux l (x :: acc)
+        in
+        List.rev (aux l [])
+      in
+      let l = remove_duplicates without_result in
       fprintf fmt "@[<h>%t%a@]"
         (fun fmt -> if without_result <> [] then
             Format.fprintf fmt "%a " self#pp_acsl_keyword kw)
         (Pretty_utils.pp_list ~sep:",@ " ~suf:";@]"
-           (fun fmt (t, _) -> self#identified_term fmt t))
-        without_result
+           (fun fmt t -> self#identified_term fmt t))
+        l
 
   method private assigns_deps kw fmt = function
     | WritesAny -> ()

tests/libc/oracle/fc_libc.1.res.oracle

@@ -3994,7 +3994,7 @@ extern size_t strcspn(char const *s, char const *reject);
 /*@ requires valid_string_s: valid_read_string(s);
     requires valid_string_accept: valid_read_string(accept);
     ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
-    assigns \result, \result;
+    assigns \result;
     assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
     assigns \result
       \from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));

tests/rte/oracle/assign4.res.oracle

@@ -5,9 +5,9 @@
     assigns \result \from min, max; */
 int choose1(int min, int max);
 
-/*@ assigns \result, \result;
-    assigns \result \from min, max, min, max;
-    assigns \result \from min, max, min, max;
+/*@ assigns \result;
+    assigns \result \from min, max;
+    assigns \result \from min, max;
  */
 int choose2(int min, int max);
 

tests/rte/oracle/assign5.res.oracle

 [kernel] Parsing tests/rte/assign5.c (with preprocessing)
 [rte] annotating function main
 /* Generated by Frama-C */
-/*@ assigns *p, *p;
+/*@ assigns *p;
     assigns *p \from x;
     assigns *p \from \nothing; */
 int f(int *p, int x);
 
-/*@ assigns *p, *p;
+/*@ assigns *p;
     assigns *p \from \nothing;
     assigns *p \from x; */
 int g(int *p, int x);

tests/syntax/oracle/multiple_froms.res.oracle

@@ -6,7 +6,8 @@ int c;
 int d;
 int e;
 /*@ assigns a, b, c;
-    assigns a \from a, b, c, d, e;
+    assigns a \from a, b, c;
+    assigns a \from c, b, d, e, a;
     assigns b \from a, e, b, d, c;
     assigns c \from c;
  */