sig
  module type Config = sig val slice_limit : unit -> int end
  module Bound :
    sig
      type t
      exception UnsupportedBoundExpression
      val of_exp : Cil_types.exp -> Segmentation.Bound.t
      val of_integer : Integer.t -> Segmentation.Bound.t
      val succ : Segmentation.Bound.t -> Segmentation.Bound.t
    end
  module type Segmentation =
    sig
      type bound = Segmentation.Bound.t
      type submemory
      type t
      val pretty :
        Stdlib.Format.formatter -> Segmentation.Segmentation.t -> unit
      val hash : Segmentation.Segmentation.t -> int
      val equal :
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> bool
      val compare :
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> int
      val hull :
        oracle:Abstract_memory.oracle ->
        Segmentation.Segmentation.t ->
        (Segmentation.Segmentation.bound * Segmentation.Segmentation.bound)
        Lattice_bounds.or_top
      val raw : Segmentation.Segmentation.t -> Abstract_memory.Bit.t
      val weak_erase :
        Abstract_memory.Bit.t ->
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t
      val is_included :
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t -> bool
      val unify :
        oracle:Abstract_memory.bioracle ->
        (Segmentation.Segmentation.submemory ->
         Segmentation.Segmentation.submemory ->
         Segmentation.Segmentation.submemory) ->
        Segmentation.Segmentation.t ->
        Segmentation.Segmentation.t ->
        Segmentation.Segmentation.t Lattice_bounds.or_top
      val single :
        Abstract_memory.bit ->
        Segmentation.Segmentation.bound ->
        Segmentation.Segmentation.bound ->
        Segmentation.Segmentation.submemory -> Segmentation.Segmentation.t
      val read :
        oracle:Abstract_memory.oracle ->
        (Segmentation.Segmentation.submemory -> 'a) ->
        ('-> '-> 'a) ->
        Segmentation.Segmentation.t ->
        Segmentation.Segmentation.bound ->
        Segmentation.Segmentation.bound -> 'a
      val update :
        oracle:Abstract_memory.oracle ->
        (Segmentation.Segmentation.submemory ->
         Segmentation.Segmentation.submemory Lattice_bounds.or_bottom) ->
        Segmentation.Segmentation.t ->
        Segmentation.Segmentation.bound ->
        Segmentation.Segmentation.bound ->
        Segmentation.Segmentation.t Lattice_bounds.or_top_bottom
      val incr_bound :
        oracle:Abstract_memory.oracle ->
        Cil_types.varinfo ->
        Integer.t option ->
        Segmentation.Segmentation.t ->
        Segmentation.Segmentation.t Lattice_bounds.or_top
      val map :
        (Segmentation.Segmentation.submemory ->
         Segmentation.Segmentation.submemory) ->
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t
      val fold :
        (Segmentation.Segmentation.submemory -> '-> 'a) ->
        (Abstract_memory.bit -> '-> 'a) ->
        Segmentation.Segmentation.t -> '-> 'a
      val add_segmentation_bounds :
        oracle:Abstract_memory.oracle ->
        Segmentation.Segmentation.bound list ->
        Segmentation.Segmentation.t -> Segmentation.Segmentation.t
    end
  module Make :
    functor (Config : Config) (M : Abstract_memory.ProtoMemory->
      sig
        type bound = Bound.t
        type submemory = M.t
        type t
        val pretty : Format.formatter -> t -> unit
        val hash : t -> int
        val equal : t -> t -> bool
        val compare : t -> t -> int
        val hull :
          oracle:Abstract_memory.oracle ->
          t -> (bound * bound) Lattice_bounds.or_top
        val raw : t -> Abstract_memory.Bit.t
        val weak_erase : Abstract_memory.Bit.t -> t -> t
        val is_included : t -> t -> bool
        val unify :
          oracle:Abstract_memory.bioracle ->
          (submemory -> submemory -> submemory) ->
          t -> t -> t Lattice_bounds.or_top
        val single : Abstract_memory.bit -> bound -> bound -> submemory -> t
        val read :
          oracle:Abstract_memory.oracle ->
          (submemory -> 'a) -> ('-> '-> 'a) -> t -> bound -> bound -> 'a
        val update :
          oracle:Abstract_memory.oracle ->
          (submemory -> submemory Lattice_bounds.or_bottom) ->
          t -> bound -> bound -> t Lattice_bounds.or_top_bottom
        val incr_bound :
          oracle:Abstract_memory.oracle ->
          Cil_types.varinfo ->
          Integer.t option -> t -> t Lattice_bounds.or_top
        val map : (submemory -> submemory) -> t -> t
        val fold :
          (submemory -> '-> 'a) ->
          (Abstract_memory.bit -> '-> 'a) -> t -> '-> 'a
        val add_segmentation_bounds :
          oracle:Abstract_memory.oracle -> bound list -> t -> t
      end
end