diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml index 30ff5840cb7ef7a7aadb6f21dad4faf2e7424a3e..473a678b004e30bbf22b9b84420ed2cc52b1bb4e 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 99ea8b43bc259d60739d361d8d0cdb9e8406b322..05488e25a7020525b67f8ac8c9f1e14d9364a19a 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