diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml index f270318461d38c0ac74e75f9da97845690997cd9..5e712c5d7767987e21d4d57cd20529d9c121fbdb 100644 --- a/src/plugins/region/Region.ml +++ b/src/plugins/region/Region.ml @@ -66,4 +66,21 @@ let pp_region fmt region : unit = Memory.pp_region fmt region -let accesses (map:map) (region:region) : Access.acs list = [] + +type acs = { + acs_read : typ list; + acs_write : typ list; + acs_shift : typ list; +} +let empty_acs = { + acs_read = []; + acs_write = []; + acs_shift = []; +} + +let accesses (region:region) : acs = + { + acs_read = List.map Access.typeof region.Memory.reads ; + acs_write = List.map Access.typeof region.Memory.writes ; + acs_shift = List.map Access.typeof region.Memory.shifts ; + } diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli index ed48c4c8edd8bd981b26853b0151e94b408d4974..de03ecc23a0125456bdf6dc6d113eb52c1859f68 100644 --- a/src/plugins/region/Region.mli +++ b/src/plugins/region/Region.mli @@ -26,24 +26,35 @@ open Cil_types +(* General type *) type region module R : Qed.Collection.S with type t = region - type map -val get_map : kernel_function -> map +(* API GETTERS *) +val get_map : kernel_function -> map val cvar : map -> varinfo -> region val field : map -> region -> fieldinfo -> region val index : map -> region -> typ -> region - +(* API POINTERS *) val points_to : map -> region -> region option val pointed_by : map -> region -> region list - +(* API ITERATOR *) val iter : map -> (region -> unit) -> unit + +(* API PRINTER *) val pp_region : Format.formatter -> region -> unit -val accesses : map -> region -> Access.acs list + +(* API ACCESS *) +type acs = { + acs_read : typ list; + acs_write : typ list; + acs_shift : typ list; +} +val empty_acs : acs +val accesses : region -> acs