Module Wp.MemTyped

module MemTyped: sig .. end

include Wp.Sigs.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 p_included : Wp.Lang.lfun
val p_valid_rd : Wp.Lang.lfun
val p_valid_rw : Wp.Lang.lfun
val p_invalid : 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