sig
  module type State =
    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
  module type Value =
    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
  module Make : functor (V : Value-> Sigs.Model
  module Eva : Value
end