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