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