diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml index 494e8b07df71de64e7b148baa200113b1e39d427..f81bc42d4708a93f382c5d4405271d897b5d12d0 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) =