From aa988ed1c0adf31669119c648e4966e3d954b465 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 7 Oct 2024 18:03:41 +0200
Subject: [PATCH] [wp] mem-typed can not be used for MemRegion

---
 src/plugins/wp/MemTyped.ml  | 15 ---------------
 src/plugins/wp/MemTyped.mli |  4 ++--
 2 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 30ff5840cb7..473a678b004 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1265,18 +1265,3 @@ let updates seq domain =
   !pool
 
 (* -------------------------------------------------------------------------- *)
-
-let sizeof = MODEL.sizeof
-let last = MODEL.last
-let havoc = MODEL.havoc
-let eqmem_forall = MODEL.eqmem_forall
-let load_int = MODEL.load_int
-let load_float = MODEL.load_float
-let load_pointer = MODEL.load_pointer
-let store_int = MODEL.store_int
-let store_float = MODEL.store_float
-let store_pointer = MODEL.store_pointer
-let set_init_atom = MODEL.set_init_atom
-let set_init = MODEL.set_init
-let is_init_atom = MODEL.is_init_atom
-let is_init_range = MODEL.is_init_range
diff --git a/src/plugins/wp/MemTyped.mli b/src/plugins/wp/MemTyped.mli
index 99ea8b43bc2..05488e25a70 100644
--- a/src/plugins/wp/MemTyped.mli
+++ b/src/plugins/wp/MemTyped.mli
@@ -24,7 +24,7 @@
 (* --- Typed Memory Model                                                 --- *)
 (* -------------------------------------------------------------------------- *)
 
-include MemRegion.ModelWithLoader
-
 type pointer = NoCast | Fits | Unsafe
 val pointer : pointer Context.value
+
+include Sigs.Model
-- 
GitLab