diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 23362bc2b2c5b09f0fc486a7792dbe564e5b1a05..9f19ab4a33b1115f8392506b381534179d5d803d 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 67b6395ee7e5eed26c10d4996390440951e6fbcd..dc3ce4a0e103ed40d6f0b948b4aa5640063938cf 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 608fb2c0bbeafd937697e9f414647a871f337f45..f78d6e6eb2d71d3ccb8b6dc0f0aef72b193b5d94 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