module MemTyped:sig
..end
include Sigs.Model
type
pointer =
| |
NoCast |
| |
Fits |
| |
Unsafe |
val pointer : pointer Context.value
val f_havoc : Lang.lfun
val p_separated : Lang.lfun
val p_included : Lang.lfun
val p_valid_rd : Lang.lfun
val p_valid_rw : Lang.lfun
val p_invalid : Lang.lfun
val a_base : Lang.F.term -> Lang.F.term
val a_offset : Lang.F.term -> Lang.F.term