sig
type t
val bottom : Wp.MemVal.State.t
val join : Wp.MemVal.State.t -> Wp.MemVal.State.t -> Wp.MemVal.State.t
val of_kinstr : Cil_types.kinstr -> Wp.MemVal.State.t
val of_stmt : Cil_types.stmt -> Wp.MemVal.State.t
val of_kf : Cil_types.kernel_function -> Wp.MemVal.State.t
val pretty : Stdlib.Format.formatter -> Wp.MemVal.State.t -> unit
end