From 88c1a72878baf89f9c27434a0345647cb89b82e8 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Fri, 10 Feb 2023 15:05:49 +0100
Subject: [PATCH] [alias] modificiation of print function
---
src/plugins/alias/abstract_state.ml | 31 ++++++++++++++++++++++++++++-
1 file changed, 30 insertions(+), 1 deletion(-)
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 494e8b07df7..f81bc42d470 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -104,8 +104,37 @@ let print_debug fmt (x:t) =
Format.fprintf fmt "cmpt: %d@." x.cmpt
let print_aliases fmt (x:t) =
+ let iter_vmap v set_lv =
+ if G.mem_vertex x.graph v then
+ let set_lv =
+ match G.succ x.graph v with
+ [] -> LSet.empty
+ | [_] -> set_lv
+ | _ -> failwith "this should not happen"
+ in
+ let set_pred = ref LSet.empty in
+ G.iter_pred
+ (fun v -> set_pred := LSet.union !set_pred (VMap.find v x.vmap))
+ x.graph
+ v;
+ if LSet.cardinal set_lv + LSet.cardinal !set_pred >= 2
+ then
+ Format.fprintf fmt "{%a%a} are aliased@."
+ (fun fmt s ->
+ LSet.iter
+ (fun lv -> Format.fprintf fmt "%a; " Lval.pretty lv)
+ s
+ )
+ set_lv
+ (fun fmt s ->
+ LSet.iter
+ (fun lv -> Format.fprintf fmt "*%a; " Lval.pretty lv)
+ s
+ )
+ !set_pred
+ in
Format.fprintf fmt "@[<hov 2><list of may-alias>@.";
- VMap.iter (fun _ set_lv -> if LSet.cardinal set_lv >= 2 then Format.fprintf fmt "%a are aliased@." LSet.pretty set_lv) x.vmap;
+ VMap.iter iter_vmap x.vmap;
Format.fprintf fmt "<end of list>@]@."
let pretty ?(debug=false) =
--
GitLab