functor (V : VarUsage->
  functor (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
        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 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 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 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 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 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 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 -> MemVar.Make.ALLOC.chunk -> Lang.F.pred
      val valid_path :
        MemVar.Make.sigma ->
        MemVar.Make.ALLOC.chunk ->
        Cil_types.typ -> MemVar.Make.ofs list -> Lang.F.pred
      val valid_pathrange :
        MemVar.Make.sigma ->
        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 scope_vars :
        MemVar.Make.ALLOC.t ->
        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
      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