functor (V : VarUsage) (M : Memory.Model->
  sig
    val datatype : string
    val configure : Model.tuning
    type chunk =
        Var of Cil_types.varinfo
      | Alloc of Cil_types.varinfo
      | Mem of M.Chunk.t
    val is_framed_var : Cil_types.varinfo -> bool
    module VAR :
      sig
        type t = Cil_types.varinfo
        val self : string
        val hash : Cil_datatype.Varinfo.t -> int
        val equal : Cil_datatype.Varinfo.t -> Cil_datatype.Varinfo.t -> bool
        val compare : Cil_datatype.Varinfo.t -> Cil_datatype.Varinfo.t -> int
        val pretty : Format.formatter -> Cil_datatype.Varinfo.t -> unit
        val typ_of_param : Cil_types.varinfo -> Cil_types.typ
        val tau_of_chunk : Cil_types.varinfo -> Lang.tau
        val basename_of_chunk : Cil_types.varinfo -> string
        val is_framed : Cil_types.varinfo -> bool
        val is_pointer : Cil_types.varinfo -> bool
      end
    module VALLOC :
      sig
        type t = Cil_types.varinfo
        val self : string
        val hash : Cil_datatype.Varinfo.t -> int
        val compare : Cil_datatype.Varinfo.t -> Cil_datatype.Varinfo.t -> int
        val equal : Cil_datatype.Varinfo.t -> Cil_datatype.Varinfo.t -> bool
        val pretty : Format.formatter -> Cil_datatype.Varinfo.t -> unit
        val tau_of_chunk : '-> ('b, 'c) Qed.Logic.datatype
        val basename_of_chunk : Cil_types.varinfo -> string
        val is_framed : Cil_types.varinfo -> bool
      end
    module Chunk :
      sig
        type t = MemVar.Make.chunk
        val self : string
        val hash : MemVar.Make.chunk -> int
        val compare : MemVar.Make.chunk -> MemVar.Make.chunk -> int
        val equal : MemVar.Make.chunk -> MemVar.Make.chunk -> bool
        val pretty : Format.formatter -> MemVar.Make.chunk -> unit
        val tau_of_chunk : MemVar.Make.chunk -> Lang.tau
        val basename_of_chunk : MemVar.Make.chunk -> string
        val is_framed : MemVar.Make.chunk -> bool
      end
    module HEAP :
      sig
        type t = VAR.t
        type set = Qed.Collection.Make(VAR).set
        type 'a map = 'Qed.Collection.Make(VAR).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 subset : t -> t -> bool
            val intersect : t -> t -> bool
            type 'a mapping = 'a map
            val mapping : (elt -> 'a) -> t -> 'a mapping
          end
      end
    module TALLOC :
      sig
        type t = VALLOC.t
        type set = Qed.Collection.Make(VALLOC).set
        type 'a map = 'Qed.Collection.Make(VALLOC).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 subset : t -> t -> bool
            val intersect : t -> t -> bool
            type 'a mapping = 'a map
            val mapping : (elt -> 'a) -> t -> 'a mapping
          end
      end
    module SIGMA :
      sig
        type chunk = VAR.t
        type domain = HEAP.set
        type t = Sigma.Make(VAR)(HEAP).t
        val create : unit -> t
        val copy : t -> t
        val merge : t -> t -> t * Passive.t * Passive.t
        val join : t -> t -> Passive.t
        val assigned : t -> t -> domain -> Lang.F.pred Bag.t
        val mem : t -> chunk -> bool
        val get : t -> chunk -> Lang.F.var
        val value : t -> chunk -> Lang.F.term
        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 : t -> domain -> t
        val havoc_chunk : t -> chunk -> t
        val havoc_any : call:bool -> t -> t
        val domain : t -> domain
        val pretty : Format.formatter -> t -> unit
      end
    module ALLOC :
      sig
        type chunk = VALLOC.t
        type domain = TALLOC.set
        type t = Sigma.Make(VALLOC)(TALLOC).t
        val create : unit -> t
        val copy : t -> t
        val merge : t -> t -> t * Passive.t * Passive.t
        val join : t -> t -> Passive.t
        val assigned : t -> t -> domain -> Lang.F.pred Bag.t
        val mem : t -> chunk -> bool
        val get : t -> chunk -> Lang.F.var
        val value : t -> chunk -> Lang.F.term
        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 : t -> domain -> t
        val havoc_chunk : t -> chunk -> t
        val havoc_any : call:bool -> t -> t
        val domain : t -> domain
        val pretty : Format.formatter -> t -> unit
      end
    module Heap :
      sig
        type t = Chunk.t
        type set = Qed.Collection.Make(Chunk).set
        type 'a map = 'Qed.Collection.Make(Chunk).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 subset : t -> t -> bool
            val intersect : t -> t -> bool
            type 'a mapping = 'a map
            val mapping : (elt -> 'a) -> t -> 'a mapping
          end
      end
    type sigma = {
      mem : M.Sigma.t;
      vars : MemVar.Make.SIGMA.t;
      alloc : MemVar.Make.ALLOC.t;
    }
    module Sigma :
      sig
        type t = MemVar.Make.sigma
        type chunk = MemVar.Make.Chunk.t
        type domain = MemVar.Make.Heap.set
        val create : unit -> MemVar.Make.sigma
        val copy : MemVar.Make.sigma -> MemVar.Make.sigma
        val merge :
          MemVar.Make.sigma ->
          MemVar.Make.sigma -> MemVar.Make.sigma * Passive.t * Passive.t
        val join : MemVar.Make.sigma -> MemVar.Make.sigma -> Passive.t
        val get : MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> Lang.F.var
        val mem : MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> bool
        val value :
          MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> Lang.F.term
        val iter :
          (MemVar.Make.Sigma.chunk -> Lang.F.var -> unit) ->
          MemVar.Make.sigma -> unit
        val iter2 :
          (MemVar.Make.Sigma.chunk ->
           Lang.F.var option -> Lang.F.var option -> unit) ->
          MemVar.Make.sigma -> MemVar.Make.sigma -> unit
        val domain_partition :
          MemVar.Make.Heap.Set.t ->
          MemVar.Make.HEAP.Set.t * MemVar.Make.TALLOC.Set.t * M.Heap.Set.t
        val domain_var : MemVar.Make.HEAP.Set.t -> MemVar.Make.Heap.Set.t
        val domain_alloc : MemVar.Make.TALLOC.Set.t -> MemVar.Make.Heap.Set.t
        val domain_mem : M.Heap.Set.t -> MemVar.Make.Heap.Set.t
        val assigned :
          MemVar.Make.sigma ->
          MemVar.Make.sigma -> MemVar.Make.Heap.Set.t -> Lang.F.pred Bag.t
        val havoc :
          MemVar.Make.sigma -> MemVar.Make.Heap.Set.t -> MemVar.Make.sigma
        val havoc_chunk :
          MemVar.Make.sigma -> MemVar.Make.Sigma.chunk -> MemVar.Make.sigma
        val havoc_any : call:bool -> MemVar.Make.sigma -> MemVar.Make.sigma
        val domain : MemVar.Make.sigma -> MemVar.Make.Heap.Set.t
        val pretty : Format.formatter -> MemVar.Make.sigma -> unit
      end
    val get_var : MemVar.Make.sigma -> MemVar.Make.SIGMA.chunk -> Lang.F.var
    val get_term :
      MemVar.Make.sigma -> MemVar.Make.SIGMA.chunk -> Lang.F.term
    type loc =
        Mloc of M.loc
      | Fref of Cil_types.varinfo
      | Fval of Cil_types.varinfo * MemVar.Make.ofs list
      | Mval of Cil_types.varinfo * MemVar.Make.ofs list
    and ofs =
        Field of Cil_types.fieldinfo
      | Index of Ctypes.c_object * Lang.F.term
    type segment = MemVar.Make.loc Memory.rloc
    val pp_ofs : Format.formatter -> MemVar.Make.ofs list -> unit
    val pretty : Format.formatter -> MemVar.Make.loc -> unit
    val ofs_vars : Lang.F.Vars.t -> MemVar.Make.ofs list -> Lang.F.Vars.t
    val vars : MemVar.Make.loc -> Lang.F.Vars.t
    val ofs_occurs : Lang.F.Vars.elt -> MemVar.Make.ofs list -> bool
    val occurs : Lang.F.var -> MemVar.Make.loc -> bool
    val null : MemVar.Make.loc
    val literal : eid:int -> Cstring.cst -> MemVar.Make.loc
    val cvar : Cil_types.varinfo -> MemVar.Make.loc
    val mloc : Cil_types.varinfo -> MemVar.Make.ofs list -> M.loc
    val mloc_of_loc : MemVar.Make.loc -> M.loc
    val pointer_loc : Lang.F.term -> MemVar.Make.loc
    val pointer_val : MemVar.Make.loc -> Lang.F.term
    val field : MemVar.Make.loc -> Cil_types.fieldinfo -> MemVar.Make.loc
    val index :
      MemVar.Make.ofs list ->
      Ctypes.c_object -> Lang.F.term -> MemVar.Make.ofs list
    val shift :
      MemVar.Make.loc -> Ctypes.c_object -> Lang.F.term -> MemVar.Make.loc
    val base_addr : MemVar.Make.loc -> MemVar.Make.loc
    val block_length :
      MemVar.Make.sigma -> Ctypes.c_object -> MemVar.Make.loc -> Lang.F.term
    val cast :
      Ctypes.c_object Memory.sequence -> MemVar.Make.loc -> MemVar.Make.loc
    val loc_of_int : Ctypes.c_object -> Lang.F.term -> MemVar.Make.loc
    val int_of_loc : Ctypes.c_int -> MemVar.Make.loc -> Lang.F.term
    val access : Lang.F.term -> MemVar.Make.ofs list -> Lang.F.term
    val update :
      Lang.F.term -> MemVar.Make.ofs list -> Lang.F.term -> Lang.F.term
    val mload :
      MemVar.Make.sigma ->
      Ctypes.c_object -> M.loc -> MemVar.Make.loc Memory.value
    val load :
      MemVar.Make.sigma ->
      Ctypes.c_object -> MemVar.Make.loc -> MemVar.Make.loc Memory.value
    val mstored :
      MemVar.Make.sigma Memory.sequence ->
      Ctypes.c_object -> M.loc -> Lang.F.term -> Lang.F.pred list
    val stored :
      MemVar.Make.sigma Memory.sequence ->
      Ctypes.c_object -> MemVar.Make.loc -> Lang.F.term -> Lang.F.pred list
    val copied :
      MemVar.Make.sigma Memory.sequence ->
      Ctypes.c_object ->
      MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred list
    val is_null : MemVar.Make.loc -> Lang.F.pred
    val offset : MemVar.Make.ofs list -> Lang.F.term
    val loc_diff :
      Ctypes.c_object -> MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.term
    val loc_compare :
      (M.loc -> M.loc -> Lang.F.pred) ->
      (Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
      Lang.F.pred -> MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred
    val loc_eq : MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred
    val loc_lt : MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred
    val loc_leq : MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred
    val loc_neq : MemVar.Make.loc -> MemVar.Make.loc -> Lang.F.pred
    val size_of_array_type : Cil_types.typ -> Lang.F.term option
    val first_index : Lang.F.term option
    val range_offset : Cil_types.typ -> Lang.F.term -> Lang.F.pred
    val valid_offset : Cil_types.typ -> MemVar.Make.ofs list -> Lang.F.pred
    val valid_offsetrange :
      Cil_types.typ ->
      MemVar.Make.ofs list ->
      Lang.F.term option -> Lang.F.term option -> Lang.F.pred
    val valid_base :
      MemVar.Make.sigma ->
      Memory.acs -> MemVar.Make.ALLOC.chunk -> Lang.F.pred
    val valid_path :
      MemVar.Make.sigma ->
      Memory.acs ->
      MemVar.Make.ALLOC.chunk ->
      Cil_types.typ -> MemVar.Make.ofs list -> Lang.F.pred
    val valid_pathrange :
      MemVar.Make.sigma ->
      Memory.acs ->
      MemVar.Make.ALLOC.chunk ->
      Cil_types.typ ->
      MemVar.Make.ofs list ->
      Lang.F.term option -> Lang.F.term option -> Lang.F.pred
    val valid_loc :
      MemVar.Make.sigma ->
      Memory.acs -> Ctypes.c_object -> MemVar.Make.loc -> Lang.F.pred
    val valid_range :
      MemVar.Make.sigma ->
      Memory.acs ->
      MemVar.Make.loc ->
      Ctypes.c_object ->
      Lang.F.term option -> Lang.F.term option -> Lang.F.pred
    val valid_array :
      MemVar.Make.sigma ->
      Memory.acs -> MemVar.Make.loc -> Ctypes.c_object -> int -> Lang.F.pred
    val valid :
      MemVar.Make.sigma ->
      Memory.acs -> MemVar.Make.loc Memory.rloc -> Lang.F.pred
    val is_mem : Cil_types.varinfo -> bool
    val is_ref : Cil_types.varinfo -> bool
    val alloc_var :
      MemVar.Make.ALLOC.t ->
      MemVar.Make.TALLOC.Set.t -> Lang.F.term -> Lang.F.pred list
    val allocates :
      MemVar.Make.ALLOC.t ->
      MemVar.Make.TALLOC.Set.elt list ->
      bool -> MemVar.Make.ALLOC.t * Lang.F.pred list
    val framed : MemVar.Make.sigma -> Lang.F.pred list
    val scope_vars :
      MemVar.Make.sigma ->
      Mcfg.scope ->
      MemVar.Make.TALLOC.Set.elt list ->
      MemVar.Make.ALLOC.t * Lang.F.pred list
    val scope :
      MemVar.Make.sigma ->
      Mcfg.scope ->
      MemVar.Make.TALLOC.Set.elt list -> MemVar.Make.sigma * Lang.F.pred list
    val global : MemVar.Make.sigma -> Lang.F.term -> Lang.F.pred
    type seq =
        Rseg of Cil_types.varinfo
      | Fseg of Cil_types.varinfo * MemVar.Make.delta list
      | Mseg of M.loc Memory.rloc * Cil_types.varinfo *
          MemVar.Make.delta list
      | Lseg of M.loc Memory.rloc
    and delta =
        Dfield of Cil_types.fieldinfo
      | Drange of Lang.F.term option * Lang.F.term option
    val dofs : MemVar.Make.ofs -> MemVar.Make.delta
    val delta : MemVar.Make.ofs list -> MemVar.Make.delta list
    val range :
      MemVar.Make.ofs list ->
      Ctypes.c_object ->
      Lang.F.term option -> Lang.F.term option -> MemVar.Make.delta list
    val dsize : int -> MemVar.Make.delta
    val rsize : MemVar.Make.ofs list -> int -> MemVar.Make.delta list
    val locseg : MemVar.Make.loc Memory.rloc -> MemVar.Make.seq
    val included_delta :
      MemVar.Make.delta list -> MemVar.Make.delta list -> Lang.F.pred
    val included :
      MemVar.Make.loc Memory.rloc ->
      MemVar.Make.loc Memory.rloc -> Lang.F.pred
    val separated_delta :
      MemVar.Make.delta list -> MemVar.Make.delta list -> Lang.F.pred
    val separated :
      MemVar.Make.loc Memory.rloc ->
      MemVar.Make.loc Memory.rloc -> Lang.F.pred
    val sloc_descr :
      MemVar.Make.loc Memory.sloc ->
      Lang.F.var list * MemVar.Make.loc * Lang.F.pred
    val floc_path :
      MemVar.Make.loc -> Cil_types.varinfo * MemVar.Make.ofs list
    val assigned_path :
      Lang.F.pred list ->
      Lang.F.var list ->
      Lang.F.var list ->
      Lang.F.term -> Lang.F.term -> MemVar.Make.ofs list -> Lang.F.pred list
    val assigned :
      MemVar.Make.sigma Memory.sequence ->
      Ctypes.c_object -> MemVar.Make.loc Memory.sloc -> Lang.F.pred list
    val domain : Ctypes.c_object -> MemVar.Make.loc -> MemVar.Make.Heap.Set.t
  end