From c228279d6b44726d0d386ebeec68aae20b9c9599 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Thu, 7 Nov 2024 13:57:21 +0100
Subject: [PATCH] [wp] +region footprint

---
 src/plugins/wp/MemRegion.ml      | 1 +
 src/plugins/wp/MemRegion.mli     | 1 +
 src/plugins/wp/RegionAnalysis.ml | 2 ++
 3 files changed, 4 insertions(+)

diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 23362bc2b2c..9f19ab4a33b 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -67,6 +67,7 @@ sig
   val literal : eid:int -> Cstring.cst -> region option
   val separated : region -> region -> bool
   val included : region -> region -> bool
+  val footprint : region -> region list
 end
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 67b6395ee7e..dc3ce4a0e10 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -48,6 +48,7 @@ sig
   val literal : eid:int -> Cstring.cst -> region option
   val separated : region -> region -> bool
   val included : region -> region -> bool
+  val footprint : region -> region list
 end
 
 module type ModelWithLoader =
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 608fb2c0bbe..f78d6e6eb2d 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -102,3 +102,5 @@ let shift r obj =
   with Not_found -> None
 
 let literal ~eid _ = ignore eid ; None
+
+let footprint r = Region.footprint (get_map ()) r
-- 
GitLab