sig
  val configure : unit -> Wp.WpContext.rollback
  val datatype : string
  module State : State
  type t
  type state = Wp.MemVal.State.t
  val null : Wp.MemVal.Value.t
  val literal : eid:int -> Wp.Cstring.cst -> int * Wp.MemVal.Value.t
  val cvar : Cil_types.varinfo -> Wp.MemVal.Value.t
  val field : Wp.MemVal.Value.t -> Cil_types.fieldinfo -> Wp.MemVal.Value.t
  val shift :
    Wp.MemVal.Value.t ->
    Wp.Ctypes.c_object -> Wp.Lang.F.term -> Wp.MemVal.Value.t
  val base_addr : Wp.MemVal.Value.t -> Wp.MemVal.Value.t
  val load :
    Wp.MemVal.Value.state ->
    Wp.MemVal.Value.t -> Wp.Ctypes.c_object -> Wp.MemVal.Value.t
  val domain : Wp.MemVal.Value.t -> Base.t list
  val offset : Wp.MemVal.Value.t -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val pretty : Stdlib.Format.formatter -> Wp.MemVal.Value.t -> unit
end