sig
  val cluster : unit -> Definitions.cluster
  module type Model =
    sig
      module Chunk : Sigs.Chunk
      module Sigma :
        sig
          type chunk = Chunk.t
          module Chunk :
            sig
              type t = chunk
              type set
              type 'a map
              val hash : t -> int
              val equal : t -> t -> bool
              val compare : t -> t -> int
              module Map :
                sig
                  type key = t
                  type 'a t = 'a map
                  val empty : 'a t
                  val add : key -> '-> 'a t -> 'a t
                  val mem : key -> 'a t -> bool
                  val find : key -> 'a t -> 'a
                  val findk : key -> 'a t -> key * 'a
                  val size : 'a t -> int
                  val is_empty : 'a t -> bool
                  val insert :
                    (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
                  val change :
                    (key -> '-> 'a option -> 'a option) ->
                    key -> '-> 'a t -> 'a t
                  val map : ('-> 'b) -> 'a t -> 'b t
                  val mapi : (key -> '-> 'b) -> 'a t -> 'b t
                  val mapf : (key -> '-> 'b option) -> 'a t -> 'b t
                  val mapq : (key -> '-> 'a option) -> 'a t -> 'a t
                  val filter : (key -> '-> bool) -> 'a t -> 'a t
                  val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
                  val iter : (key -> '-> unit) -> 'a t -> unit
                  val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                  val iter_sorted : (key -> '-> unit) -> 'a t -> unit
                  val fold_sorted :
                    (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                  val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t
                  val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
                  val interf :
                    (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
                  val interq :
                    (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
                  val diffq :
                    (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
                  val subset :
                    (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
                  val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
                  val iterk :
                    (key -> '-> '-> unit) -> 'a t -> 'b t -> unit
                  val iter2 :
                    (key -> 'a option -> 'b option -> unit) ->
                    'a t -> 'b t -> unit
                  val merge :
                    (key -> 'a option -> 'b option -> 'c option) ->
                    'a t -> 'b t -> 'c t
                  type domain = set
                  val domain : 'a t -> domain
                end
              module Set :
                sig
                  type elt = t
                  type t = set
                  val empty : t
                  val add : elt -> t -> t
                  val singleton : elt -> t
                  val elements : t -> elt list
                  val is_empty : t -> bool
                  val mem : elt -> t -> bool
                  val iter : (elt -> unit) -> t -> unit
                  val fold : (elt -> '-> 'a) -> t -> '-> 'a
                  val filter : (elt -> bool) -> t -> t
                  val partition : (elt -> bool) -> t -> t * t
                  val for_all : (elt -> bool) -> t -> bool
                  val exists : (elt -> bool) -> t -> bool
                  val iter_sorted : (elt -> unit) -> t -> unit
                  val fold_sorted : (elt -> '-> 'a) -> t -> '-> 'a
                  val union : t -> t -> t
                  val inter : t -> t -> t
                  val diff : t -> t -> t
                  val subset : t -> t -> bool
                  val intersect : t -> t -> bool
                  val of_list : elt list -> t
                  type 'a mapping = 'a map
                  val mapping : (elt -> 'a) -> t -> 'a mapping
                end
            end
          type domain = Chunk.Set.t
          type t
          val pretty : Format.formatter -> t -> unit
          val create : unit -> t
          val mem : t -> chunk -> bool
          val get : t -> chunk -> Lang.F.var
          val value : t -> chunk -> Lang.F.term
          val copy : t -> t
          val join : t -> t -> Passive.t
          val assigned : pre:t -> post:t -> domain -> Lang.F.pred Bag.t
          val choose : t -> t -> t
          val merge : t -> t -> t * Passive.t * Passive.t
          val merge_list : t list -> t * Passive.t list
          val iter : (chunk -> Lang.F.var -> unit) -> t -> unit
          val iter2 :
            (chunk -> Lang.F.var option -> Lang.F.var option -> unit) ->
            t -> t -> unit
          val havoc_chunk : t -> chunk -> t
          val havoc : t -> domain -> t
          val havoc_any : call:bool -> t -> t
          val remove_chunks : t -> domain -> t
          val domain : t -> domain
          val union : domain -> domain -> domain
          val empty : domain
          val writes : t Sigs.sequence -> domain
        end
      val name : string
      type loc
      val sizeof : Ctypes.c_object -> int
      val field :
        MemLoader.Model.loc -> Cil_types.fieldinfo -> MemLoader.Model.loc
      val shift :
        MemLoader.Model.loc ->
        Ctypes.c_object -> Lang.F.term -> MemLoader.Model.loc
      val to_addr : MemLoader.Model.loc -> Lang.F.term
      val to_region_pointer : MemLoader.Model.loc -> int * Lang.F.term
      val of_region_pointer :
        int -> Ctypes.c_object -> Lang.F.term -> MemLoader.Model.loc
      val value_footprint :
        Ctypes.c_object ->
        MemLoader.Model.loc -> MemLoader.Model.Sigma.domain
      val init_footprint :
        Ctypes.c_object ->
        MemLoader.Model.loc -> MemLoader.Model.Sigma.domain
      val frames :
        Ctypes.c_object -> MemLoader.Model.loc -> Chunk.t -> Sigs.frame list
      val last :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_object -> MemLoader.Model.loc -> Lang.F.term
      val havoc :
        Ctypes.c_object ->
        MemLoader.Model.loc ->
        length:Lang.F.term ->
        Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.term
      val eqmem :
        Ctypes.c_object ->
        MemLoader.Model.loc ->
        Chunk.t -> Lang.F.term -> Lang.F.term -> Lang.F.pred
      val eqmem_forall :
        Ctypes.c_object ->
        MemLoader.Model.loc ->
        Chunk.t ->
        Lang.F.term ->
        Lang.F.term -> Lang.F.var list * Lang.F.pred * Lang.F.pred
      val load_int :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_int -> MemLoader.Model.loc -> Lang.F.term
      val load_float :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_float -> MemLoader.Model.loc -> Lang.F.term
      val load_pointer :
        MemLoader.Model.Sigma.t ->
        Cil_types.typ -> MemLoader.Model.loc -> MemLoader.Model.loc
      val store_int :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_int ->
        MemLoader.Model.loc -> Lang.F.term -> Chunk.t * Lang.F.term
      val store_float :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_float ->
        MemLoader.Model.loc -> Lang.F.term -> Chunk.t * Lang.F.term
      val store_pointer :
        MemLoader.Model.Sigma.t ->
        Cil_types.typ ->
        MemLoader.Model.loc -> Lang.F.term -> Chunk.t * Lang.F.term
      val is_init_atom :
        MemLoader.Model.Sigma.t -> MemLoader.Model.loc -> Lang.F.term
      val is_init_range :
        MemLoader.Model.Sigma.t ->
        Ctypes.c_object -> MemLoader.Model.loc -> Lang.F.term -> Lang.F.pred
      val set_init_atom :
        MemLoader.Model.Sigma.t ->
        MemLoader.Model.loc -> Lang.F.term -> Chunk.t * Lang.F.term
      val set_init :
        Ctypes.c_object ->
        MemLoader.Model.loc ->
        length:Lang.F.term -> Chunk.t -> current:Lang.F.term -> Lang.F.term
      val monotonic_init :
        MemLoader.Model.Sigma.t -> MemLoader.Model.Sigma.t -> Lang.F.pred
    end
  module Make :
    functor (M : Model->
      sig
        val domain : Ctypes.c_object -> M.loc -> M.Sigma.domain
        val load : M.Sigma.t -> Ctypes.c_object -> M.loc -> M.loc Sigs.value
        val loadvalue : M.Sigma.t -> Ctypes.c_object -> M.loc -> Lang.F.term
        val havoc :
          M.Sigma.t Sigs.sequence ->
          Ctypes.c_object -> M.loc -> Sigs.equation list
        val havoc_length :
          M.Sigma.t Sigs.sequence ->
          Ctypes.c_object -> M.loc -> Lang.F.term -> Sigs.equation list
        val stored :
          M.Sigma.t Sigs.sequence ->
          Ctypes.c_object -> M.loc -> Lang.F.term -> Sigs.equation list
        val copied :
          M.Sigma.t Sigs.sequence ->
          Ctypes.c_object -> M.loc -> M.loc -> Sigs.equation list
        val assigned :
          M.Sigma.t Sigs.sequence ->
          Ctypes.c_object -> M.loc Sigs.sloc -> Sigs.equation list
        val initialized : M.Sigma.t -> M.loc Sigs.rloc -> Lang.F.pred
      end
end