diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 121ad96facc0f37bf6de65c4c7f03e57953649fb..8a41fe69f4f24827622a3d4d6c56ed638821d3eb 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/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
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6567141ad0a51d2dbd1cff12ccae4751edb12368..cbe560e6038c0caf1e5f5507bc9c9530c3637b7d 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/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 -> ()
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 0ddeab5c75a42c32227c2d5099582104a5a112c4..27e2b1cd3fe12941cac241bd352aad73593f1e89 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index f62ba3b05e3b0e7eaae81d3e521ffc219007cccf..c6ffe271274d0566b44115791d6a158d672cc056 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/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
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1c7f3e7c9488445e723a1e84af235443d579c607..ea25b25f657c75f8ceeeaed060cf712e5c7268bb 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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 ..)));
diff --git a/tests/rte/oracle/assign4.res.oracle b/tests/rte/oracle/assign4.res.oracle
index e835835a444036c29505eac0bde563c5fcc12dce..143f1a6b3fcb116c94c4f1f3e00b27372d1e075d 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/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)
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index 7240925afa98a9cc66e358cbd24e22615203e5b6..52d1def1f07ac9c260c9f52025366357dfa448a3 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -1,14 +1,16 @@
[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)
diff --git a/tests/syntax/multiple_assigns.i b/tests/syntax/multiple_assigns.i
new file mode 100644
index 0000000000000000000000000000000000000000..d20a1dfcda46f0720ce70523677b4472dd709f80
--- /dev/null
+++ b/tests/syntax/multiple_assigns.i
@@ -0,0 +1,10 @@
+int z;
+
+/*@ assigns z, z;
+ assigns z \from z;
+ assigns z, z;
+ */
+void function(void)
+{
+ return;
+}
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
new file mode 100644
index 0000000000000000000000000000000000000000..6a0a25687f9e2960e533cbec4ac5dbc0dc21e286
--- /dev/null
+++ b/tests/syntax/multiple_froms.i
@@ -0,0 +1,17 @@
+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;
+}
diff --git a/tests/syntax/oracle/multiple_assigns.res.oracle b/tests/syntax/oracle/multiple_assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0cda603d543618256b3d8bc527983157bf1538ed
--- /dev/null
+++ b/tests/syntax/oracle/multiple_assigns.res.oracle
@@ -0,0 +1,11 @@
+[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;
+}
+
+
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b90f4dc55f6e2c31b6f7656f8f8cc0ecfa6cf03d
--- /dev/null
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -0,0 +1,23 @@
+[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;
+}
+
+