From 273c39d62e09600b7cf5aac977bb2ec5acf941b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Mon, 26 Aug 2024 10:59:30 +0200
Subject: [PATCH] [wp] API access
---
src/plugins/region/Region.ml | 19 ++++++++++++++++++-
src/plugins/region/Region.mli | 21 ++++++++++++++++-----
2 files changed, 34 insertions(+), 6 deletions(-)
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index f270318461d..5e712c5d776 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 ed48c4c8edd..de03ecc23a0 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
--
GitLab