diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml index 9017bdeb5e771beaff7f609cf5206724f37dafb5..f270318461d38c0ac74e75f9da97845690997cd9 100644 --- a/src/plugins/region/Region.ml +++ b/src/plugins/region/Region.ml @@ -60,3 +60,10 @@ let pointed_by (map:map) (region:region) : region list = let iter (map:map) (f:region -> unit) : unit = Memory.iter map.map f + + +let pp_region fmt region : unit = Memory.pp_region fmt region + + + +let accesses (map:map) (region:region) : Access.acs list = [] diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli index 67a7064825587afeaf3af4735b00ee0fa8f14fb7..ed48c4c8edd8bd981b26853b0151e94b408d4974 100644 --- a/src/plugins/region/Region.mli +++ b/src/plugins/region/Region.mli @@ -22,14 +22,13 @@ (** Interface for the Region plug-in. *) -open Cil_types +open Cil_types type region module R : Qed.Collection.S with type t = region - type map val get_map : kernel_function -> map @@ -44,3 +43,7 @@ val pointed_by : map -> region -> region list val iter : map -> (region -> unit) -> unit + +val pp_region : Format.formatter -> region -> unit + +val accesses : map -> region -> Access.acs list