From 637af0a0c20bef6227da180bd299cae5fdd37b6e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 5 Nov 2020 18:02:25 +0100
Subject: [PATCH] [kernel] Clean from but do not merge them
---
src/kernel_internals/parsing/logic_parser.mly | 14 ++++++++------
src/kernel_services/ast_printing/cil_printer.ml | 15 +++++++++++++--
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
tests/rte/oracle/assign4.res.oracle | 6 +++---
tests/rte/oracle/assign5.res.oracle | 4 ++--
tests/syntax/oracle/multiple_froms.res.oracle | 3 ++-
6 files changed, 29 insertions(+), 15 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 936ce77df49..282b60b5bfc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/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 =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6567141ad0a..b2f6b77a20f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/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 -> ()
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1c7f3e7c948..ea25b25f657 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 e835835a444..4ce28ed1aba 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/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);
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index 7240925afa9..c72860ec208 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -1,12 +1,12 @@
[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);
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
index ea197945fc7..eac436bb15e 100644
--- a/tests/syntax/oracle/multiple_froms.res.oracle
+++ b/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;
*/
--
GitLab