Skip to content
Snippets Groups Projects
Commit aa988ed1 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] mem-typed can not be used for MemRegion

parent 5b2642fc
No related branches found
No related tags found
No related merge requests found
...@@ -1265,18 +1265,3 @@ let updates seq domain = ...@@ -1265,18 +1265,3 @@ let updates seq domain =
!pool !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
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
(* --- Typed Memory Model --- *) (* --- Typed Memory Model --- *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
include MemRegion.ModelWithLoader
type pointer = NoCast | Fits | Unsafe type pointer = NoCast | Fits | Unsafe
val pointer : pointer Context.value val pointer : pointer Context.value
include Sigs.Model
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment