Module Wp.MemTyped

module MemTyped: sig .. end

include Wp.Memory.Model
type pointer = 
| NoCast
| Fits
| Unsafe
val pointer : pointer Wp.Context.value
val p_havoc : Wp.Lang.lfun
val p_separated : Wp.Lang.lfun
val a_base : Wp.Lang.F.term -> Wp.Lang.F.term
val a_offset : Wp.Lang.F.term -> Wp.Lang.F.term