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