Merge remote-tracking branch 'origin/stable/titanium' into...

Merge remote-tracking branch 'origin/stable/titanium' into feature/blanchard/wp/warn-unsupported-from

src/kernel_internals/parsing/logic_parser.mly

@@ -109,15 +109,23 @@
 
   let loc_ext d = { extended_node = d; extended_loc = loc () }
 
-  let concat_froms a1 a2 =
-    let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
+  let filter_from l = function
+    | FromAny ->
+      l, FromAny
+    | From ds ->
+      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 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 (_,f2 as p)  =
+    let concat_one acc (newloc, newf)  =
+      let (newloc, newf) as p = filter_from newloc newf in
       try
-        let (_,f1) = List.find (compare_pair p) acc
+        let (curloc,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.
@@ -130,12 +138,28 @@
                  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
+            let drop d k =
+              Kernel.warning ~current:false ~wkey:Kernel.wkey_multi_from
+                "Drop '%a' \\from at %a for more precise one at %a"
+                Logic_print.print_lexpr curloc
+                Cil_datatype.Location.pretty d.lexpr_loc
+                Cil_datatype.Location.pretty k.lexpr_loc
+            in
+            if incl curl newl then begin
+              if not (incl newl curl) then drop newloc curloc;
+              acc
+            end
+            else if incl newl curl then begin
+              drop curloc newloc;
+              Extlib.replace compare_pair p acc
+            end
+            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
@@ -151,7 +175,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

src/kernel_services/ast_printing/cil_printer.ml

@@ -2912,12 +2912,17 @@ class cil_printer () = object (self)
           (function (a,_) -> not (Logic_const.is_exit_status a.it_content))
           l
       in
+      let unique_assigned_locs =
+        let same t1 t2 = Cil_datatype.Term.equal t1.it_content t2.it_content in
+        let f l (a,_) = if List.exists (same a) l then l else a :: l in
+        List.rev (List.fold_left f [] 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))
+        unique_assigned_locs
 
   method private assigns_deps kw fmt = function
     | WritesAny -> ()

src/kernel_services/plugin_entry_points/kernel.ml

@@ -185,6 +185,8 @@ let wkey_no_proto = register_warn_category "typing:no-proto"
 
 let wkey_missing_spec = register_warn_category "annot:missing-spec"
 
+let wkey_multi_from = register_warn_category "annot:multi-from"
+
 let wkey_decimal_float = register_warn_category "parser:decimal-float"
 let () = set_warn_status wkey_decimal_float Log.Wonce
 

src/kernel_services/plugin_entry_points/kernel.mli

@@ -175,6 +175,8 @@ val wkey_no_proto: warn_category
 
 val wkey_missing_spec: warn_category
 
+val wkey_multi_from: warn_category
+
 val wkey_decimal_float: warn_category
 
 val wkey_acsl_extension: warn_category

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,10 +5,8 @@
     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; */
 int choose2(int min, int max);
 
 int main(void)

tests/rte/oracle/assign5.res.oracle

 [kernel] Parsing tests/rte/assign5.c (with preprocessing)
+[kernel:annot:multi-from] Warning: 
+  Drop '*p' \from at tests/rte/assign5.c:9 for more precise one at tests/rte/assign5.c:10
+[kernel:annot:multi-from] Warning: 
+  Drop '*p' \from at tests/rte/assign5.c:19 for more precise one at tests/rte/assign5.c:18
 [rte] annotating function main
 /* Generated by Frama-C */
-/*@ assigns *p, *p;
-    assigns *p \from x;
+/*@ assigns *p;
     assigns *p \from \nothing; */
 int f(int *p, int x);
 
-/*@ assigns *p, *p;
-    assigns *p \from \nothing;
-    assigns *p \from x; */
+/*@ assigns *p;
+    assigns *p \from \nothing; */
 int g(int *p, int x);
 
 int main(void)

tests/syntax/multiple_assigns.i

+int z;
+
+/*@ assigns z, z;
+    assigns z \from z;
+    assigns z, z;
+ */
+void function(void)
+{
+  return;
+}

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; // 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; // 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)
+{
+  return;
+}

tests/syntax/oracle/multiple_assigns.res.oracle

+[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;
+}
+
+

tests/syntax/oracle/multiple_froms.res.oracle

+[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
+[kernel:annot:multi-from] Warning: 
+  Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
+[kernel:annot:multi-from] Warning: 
+  Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
+/* Generated by Frama-C */
+int a;
+int b;
+int c;
+int d;
+int e;
+/*@ assigns a, b, c;
+    assigns a \from a, b, c;
+    assigns b \from a, e;
+    assigns c \from c;
+    assigns c \from d;
+ */
+void function(void)
+{
+  return;
+}
+
+