From ff48957bb6049ede336aa01e61077f53c3fb40d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Thu, 22 Aug 2024 16:30:09 +0200
Subject: [PATCH] [region] add some useful API calls

---
 src/plugins/region/Region.ml  | 35 +++++++++++++++++++++++++++++++++++
 src/plugins/region/Region.mli | 23 +++++++++++++++++++++++
 src/plugins/region/dune       |  2 +-
 src/plugins/region/memory.mli |  2 ++
 4 files changed, 61 insertions(+), 1 deletion(-)

diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index 2b8fce64aec..8d9d7f5ab5b 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -23,3 +23,38 @@
 (* -------------------------------------------------------------------------- *)
 (* --- Region Analysis API                                                --- *)
 (* -------------------------------------------------------------------------- *)
+
+
+open Cil_types
+
+type region = Memory.region
+
+module R : Qed.Collection.S with type t = region =
+  Qed.Collection.Make(struct
+    type t = region
+    let hash r = Memory.id r.Memory.node
+    let equal r1 r2 = (hash r1 == hash r2)
+    let compare r1 r2 = (hash r1) - (hash r2)
+  end)
+
+
+type map = Code.domain
+let get_map (f:kernel_function) : map = Code.domain f
+
+(** @raise Not_found *)
+let cvar (map:map) (var:varinfo) : region =
+  Memory.region map.map (Memory.lval map.map ((Var var), NoOffset))
+
+let field (map:map) (region:region) (field:fieldinfo) : region =
+  Memory.region map.map (Memory.offset map.map region.node (Field (field, NoOffset)))
+
+let index (_:map) (_:region) (_:typ) : region = (* TODO *) raise Not_found
+
+
+let points_to (map:map) (region:region) : region option =
+  Option.map (Memory.region map.map) @@ Memory.cpointed map.map region.Memory.node
+
+let pointed_by (_:map) (_:region) : region list = (* TODO *) []
+
+
+let iter (_:map) (_:region -> unit) : unit = (* TODO *) ()
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index d9615a6fffe..67a70648255 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -21,3 +21,26 @@
 (**************************************************************************)
 
 (** Interface for the Region plug-in. *)
+
+open Cil_types
+
+
+
+type region
+module R : Qed.Collection.S with type t = region
+
+
+type map
+val get_map : kernel_function -> map
+
+
+val cvar : map -> varinfo -> region
+val field : map -> region -> fieldinfo -> region
+val index : map -> region -> typ -> region
+
+
+val points_to : map -> region -> region option
+val pointed_by : map -> region -> region list
+
+
+val iter : map -> (region -> unit) -> unit
diff --git a/src/plugins/region/dune b/src/plugins/region/dune
index f4f00f77e3a..e091122472a 100644
--- a/src/plugins/region/dune
+++ b/src/plugins/region/dune
@@ -37,7 +37,7 @@
  (name Region)
  (public_name frama-c-region.core)
  (flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-server.core unionFind)
+ (libraries qed frama-c.kernel frama-c-server.core unionFind)
  (instrumentation (backend landmarks))
  (instrumentation (backend bisect_ppx)))
 
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 788ed51359d..4aab36af2c1 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -91,6 +91,8 @@ val merge_copy : map -> l:node -> r:node -> unit
 
 (** @raise Not_found *)
 val lval : map -> lval -> node
+val offset : map -> node -> offset -> node
+val cpointed : map -> node -> node option
 
 (** @raise Not_found *)
 val exp : map -> exp -> node option
-- 
GitLab