diff --git a/src/plugins/wp/RegionDump.ml b/src/plugins/wp/RegionDump.ml
new file mode 100644
index 0000000000000000000000000000000000000000..500f578937befa044fc06b796043f2dfef2ff5bf
--- /dev/null
+++ b/src/plugins/wp/RegionDump.ml
@@ -0,0 +1,303 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+[@@@ warning "-32"]
+
+module Wp = Wp_parameters
+(*
+module G = Dotgraph
+module R = G.Node(Region.Map)
+*)
+let node_default = [`Attr("fontname","monospace")]
+let edge_default = [`Attr("fontname","monospace")]
+
+let attr_offset = [ `Filled ; `Color "grey" ; `Box ]
+let attr_write = [ `Label "W" ; `Fillcolor "green" ; `Filled ]
+let attr_read = [ `Label "R" ; `Fillcolor "green" ; `Filled ]
+let attr_alias = [ `Label "&" ; `Fillcolor "orange" ; `Filled ]
+let attr_merge = [ `Color "red" ; `Fillcolor "red" ; `Filled ]
+let attr_shift = [ `Label "[]" ]
+let attr_delta = [ `Filled ; `Color "lightblue" ; `Box ]
+let attr_deref = [ `ArrowHead "tee" ]
+let attr_cil = [ `Filled ; `Fillcolor "yellow" ]
+let attr_region = `Shape "tab" :: attr_cil
+let attr_var = `Shape "cds" :: attr_cil
+let attr_garbled = [`Fillcolor "red";`Filled]
+let attr_froms = [ `Color "blue" ; `Attr("dir","back") ]
+
+let attr_pointed = [
+ `Color "red"
+]
+
+let attr_pointed_deref = [
+ `Attr("taillabel","*");
+ `Attr("labelangle","+30");
+ `Color "red";
+]
+
+let attr_pointed_shift = [
+ `Attr("taillabel","[..]");
+ `Attr("labeldistance","1.7");
+ `Attr("labelangle","+40");
+ `Color "red";
+]
+
+let rid_key = Wp.register_category "rid"
+let dot_key = Wp.register_category "dot"
+let pdf_key = Wp.register_category "pdf"
+let deref_key = Wp.register_category "deref"
+let roots_key = Wp.register_category "roots"
+let froms_key = Wp.register_category "froms"
+let cluster_key = Wp.register_category "cluster"
+let chunk_key = Wp.register_category "chunk"
+let offset_key = Wp.register_category "offset"
+
+(*
+let sfprintf = Format.asprintf
+
+let dotpointed ~label r =
+ let attr =
+ if Region.is_shifted r
+ then attr_pointed_shift else attr_pointed_deref in
+ let target = G.port (R.get r) "w" in
+ `Port ("",["",attr,target],label)
+
+let dotvalue ?(prefix="") value : Dotgraph.record =
+ let open Layout in
+ match value with
+ | Int i -> `Label (sfprintf "%s%a" prefix Ctypes.pp_int i)
+ | Float f -> `Label (sfprintf "%s%a" prefix Ctypes.pp_float f)
+ | Pointer r -> dotpointed ~label:(prefix ^ "ptr") r
+
+let dotrange ?(prefix="") rg : Dotgraph.record =
+ let open Layout in
+ let pp_dim fmt = function
+ | Raw _ -> Format.pp_print_string fmt "raw"
+ | Dim(s,ds) -> Format.fprintf fmt "%d%a" s Matrix.pretty ds
+ in
+ let label = sfprintf "%d..%d: %s%a"
+ rg.ofs (rg.ofs + rg.len - 1)
+ prefix pp_dim rg.dim in
+ `Port("",["",[`Dotted],R.get rg.reg],label)
+
+let dotcluster cluster : Dotgraph.record =
+ let open Layout in
+ match cluster with
+ | Empty -> `Label "-"
+ | Garbled -> `Label "Garbled"
+ | Chunk v -> dotvalue v
+ | Layout { sizeof ; layout } ->
+ let label = Printf.sprintf "sizeof:%d" sizeof in
+ `Hbox (`Label label :: List.map dotrange layout)
+
+let dotchunk mem : Dotgraph.record =
+ let open Layout in
+ match mem with
+ | Mraw(_,None) -> `Label "Raw"
+ | Mraw(_,Some r) -> dotpointed ~label:"Raw" r
+ | Mref r -> dotpointed ~label:"Ref" r
+ | Mmem(rt,v) ->
+ let prefix = if Layout.Root.indexed rt then "Mem " else "Var " in
+ dotvalue ~prefix v
+ | Mcomp(_,ovl) ->
+ let range rg = dotrange
+ ~prefix:(if Overlay.once rg.reg ovl then "D" else "C") rg in
+ `Hbox (List.map range ovl)
+
+let dotregion dot map region node =
+ begin
+ let is_read = Region.is_read region in
+ let is_written = Region.is_written region in
+ let is_aliased = Region.is_aliased region in
+ let is_accessed = is_read || is_written || is_aliased in
+ let has_deref = Wp.has_dkey deref_key && Region.has_deref region in
+ let has_roots = Wp.has_dkey roots_key && Region.has_roots map region in
+ let has_index_infos = has_deref || has_roots in
+ let has_side_cluster =
+ is_accessed ||
+ has_index_infos ||
+ Region.has_names region ||
+ Wp.has_dkey offset_key ||
+ Wp.has_dkey rid_key ||
+ not (Wp.has_dkey cluster_key || Wp.has_dkey chunk_key) ||
+ not (Wp.Region_fixpoint.get ())
+ in
+ if has_side_cluster then
+ begin
+ let attr = G.decorate [ `Oval ] [
+ is_read , attr_read ;
+ Region.has_pointed region , [ `Label "D" ] ;
+ is_written , attr_write ;
+ Region.is_shifted region , attr_shift ;
+ is_aliased , attr_alias ;
+ Region.get_alias map region != region , attr_merge ;
+ Region.is_garbled region , attr_merge ;
+ ] in
+ G.node dot node attr ;
+ end ;
+ if Wp.has_dkey offset_key then
+ Region.iter_offset map
+ (fun offset target ->
+ let label = Pretty_utils.to_string Layout.Offset.pretty offset in
+ let delta = G.inode dot (`Label label :: attr_offset) in
+ G.link dot [node;delta;R.get target] [`Dotted]
+ ) region ;
+ if Wp.has_dkey offset_key then
+ Option.iter
+ (fun target ->
+ let label = if Region.is_shifted target then "[..]" else "*" in
+ let deref = G.inode dot (`Label label :: attr_offset) in
+ G.link dot [node;deref;R.get target] attr_pointed
+ ) (Region.get_pointed map region) ;
+ if has_index_infos then
+ begin
+ let derefs = ref [] in
+ let label s = derefs := s :: !derefs in
+ if has_roots then
+ label @@ sfprintf "roots:%a"
+ Layout.Root.pretty (Region.get_roots map region) ;
+ if has_deref then
+ Region.iter_deref
+ (fun deref ->
+ label @@ Pretty_utils.to_string Layout.Deref.pretty deref
+ ) region ;
+ if !derefs <> [] then
+ begin
+ let label = String.concat "\n" (List.rev !derefs) in
+ let delta = G.inode dot (`Label label :: attr_delta) in
+ G.rank dot [node;delta] ;
+ G.edge dot delta node attr_deref
+ end
+ end ;
+ if Wp.has_dkey cluster_key then
+ begin
+ let cluster = Region.cluster map region in
+ if not (has_side_cluster && Layout.Cluster.is_empty cluster) then
+ let record = dotcluster cluster in
+ let attr = if Region.is_garbled region then attr_garbled else [] in
+ if has_side_cluster then
+ let delta = G.irecord dot ~attr record in
+ G.edge dot node (G.port delta "w") attr_deref
+ else
+ G.record dot node ~attr record
+ end ;
+ if Wp.has_dkey chunk_key then
+ begin
+ let chunk = Region.chunk map region in
+ let record = dotchunk chunk in
+ let attr = if Region.is_garbled region then attr_garbled else [] in
+ if has_side_cluster then
+ let delta = G.irecord dot ~attr record in
+ G.edge dot node (G.port delta "w") attr_deref
+ else
+ G.record dot node ~attr record
+ end ;
+ if Wp.has_dkey froms_key then
+ begin
+ let open Layout in
+ List.iter
+ (function
+ | Fvar _ -> ()
+ | Farray r ->
+ G.edge dot (R.get r) node (`Label "[]"::attr_froms)
+ | Fderef r ->
+ G.edge dot (R.get r) node (`Label "*"::attr_froms)
+ | Findex r ->
+ G.edge dot (R.get r) node (`Label "+(..)"::attr_froms)
+ | Ffield(r,ofs) ->
+ let label = Printf.sprintf "+%d" ofs in
+ G.edge dot (R.get r) node (`Label label::attr_froms)
+ ) (Region.get_froms map region)
+ end ;
+ Region.iter_copies map
+ (fun target ->
+ G.edge dot node (R.get target) [`Color "green"]
+ ) region ;
+ Option.iter
+ (fun target ->
+ G.edge dot node (R.get target) [`Color "red"]
+ ) (Region.get_merged map region) ;
+ end
+
+let dotvar dot x r =
+ begin
+ let open Cil_types in
+ let xnode = G.inode dot ~prefix:"V" (`Label x.vname :: attr_var) in
+ G.edge dot (G.port xnode "e") (R.get r) [] ;
+ end
+
+let dotlabel dot a r =
+ begin
+ let anode = G.inode dot ~prefix:"R" (`Label a :: attr_region) in
+ let rnode = R.get r in
+ G.rank dot [ anode ; rnode ] ;
+ G.edge dot anode rnode []
+ end
+
+let dotrid dot r =
+ dotlabel dot (Pretty_utils.to_string Region.R.pretty r) r
+
+let dotstr dot r cst =
+ dotlabel dot (String.escaped cst) r
+
+let dotgraph dot map =
+ begin
+ G.node_default dot node_default ;
+ G.edge_default dot edge_default ;
+ R.clear () ;
+ R.define dot (dotregion dot map) ;
+ Region.iter_vars map (dotvar dot) ;
+ Region.iter_strings map (dotstr dot) ;
+ G.run dot ;
+ if Wp.has_dkey rid_key then Region.iter map (dotrid dot) ;
+ Region.iter_names map (dotlabel dot) ;
+ if Region.has_return map then
+ dotlabel dot "\\result" (Region.of_return map) ;
+ Region.iter_fusion map (fun i r ->
+ let rid = Region.id r in
+ if i <> rid then
+ dotlabel dot (Printf.sprintf "Fusion R%03d" i) r
+ else
+ dotlabel dot "Fusion (Self)" r
+ ) ;
+ G.run dot ;
+ end
+
+let dump_in_file ~file name map =
+ if Wp.has_dkey dot_key || Wp.has_dkey pdf_key then
+ begin
+ let file = Pretty_utils.to_string Datatype.Filepath.pretty file in
+ let dot = Dotgraph.open_dot ~attr:[`LR] ~name ~file () in
+ dotgraph dot map ;
+ Dotgraph.close dot ;
+ let outcome =
+ if Wp.has_dkey pdf_key
+ then Dotgraph.layout dot
+ else file in
+ Wp.result "Region Graph: %s" outcome
+ end
+
+let dump_in_dir ~dir name map =
+ let file = Datatype.Filepath.concat dir (name ^ ".dot") in
+ dump_in_file ~file name map
+
+*)
diff --git a/src/plugins/wp/RegionDump.mli b/src/plugins/wp/RegionDump.mli
new file mode 100644
index 0000000000000000000000000000000000000000..44ac5d848f5ef3f0c9c7c25b9e27e67bbc8eb3e5
--- /dev/null
+++ b/src/plugins/wp/RegionDump.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Dump region graphs to dir according to -wp options.
+ By default, does nothing. *)
+(*
+val dump_in_dir : dir:Datatype.Filepath.t -> string -> Region.map -> unit
+
+val dump_in_file : file:Datatype.Filepath.t -> string -> Region.map -> unit
+*)