sig
  type initialization = SurelyInitialized | MaybeUninitialized
  type bit =
      Uninitialized
    | Zero of Abstract_memory.initialization
    | Any of Base.SetLattice.t * Abstract_memory.initialization
  module Bit :
    sig
      type t = Abstract_memory.bit
      val uninitialized : Abstract_memory.Bit.t
      val zero : Abstract_memory.Bit.t
      val numerical : Abstract_memory.Bit.t
      val top : Abstract_memory.Bit.t
      val is_any : Abstract_memory.Bit.t -> bool
      val initialization :
        Abstract_memory.Bit.t -> Abstract_memory.initialization
      val pretty : Stdlib.Format.formatter -> Abstract_memory.Bit.t -> unit
      val hash : Abstract_memory.Bit.t -> int
      val equal : Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> bool
      val compare : Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> int
      val is_included :
        Abstract_memory.Bit.t -> Abstract_memory.Bit.t -> bool
      val join :
        Abstract_memory.Bit.t ->
        Abstract_memory.Bit.t -> Abstract_memory.Bit.t
    end
  type size = Integer.t
  type side = Left | Right
  type oracle = Cil_types.exp -> Int_val.t
  type bioracle = Abstract_memory.side -> Abstract_memory.oracle
  module type ProtoMemory =
    sig
      type t
      type value
      val pretty :
        Stdlib.Format.formatter -> Abstract_memory.ProtoMemory.t -> unit
      val pretty_root :
        Stdlib.Format.formatter -> Abstract_memory.ProtoMemory.t -> unit
      val hash : Abstract_memory.ProtoMemory.t -> int
      val equal :
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t -> bool
      val compare :
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t -> int
      val of_raw : Abstract_memory.bit -> Abstract_memory.ProtoMemory.t
      val raw : Abstract_memory.ProtoMemory.t -> Abstract_memory.bit
      val of_value :
        Cil_types.typ ->
        Abstract_memory.ProtoMemory.value -> Abstract_memory.ProtoMemory.t
      val to_value :
        Cil_types.typ ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.value
      val to_singleton_int :
        Abstract_memory.ProtoMemory.t -> Integer.t option
      val weak_erase :
        Abstract_memory.bit ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
      val is_included :
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t -> bool
      val unify :
        oracle:Abstract_memory.bioracle ->
        (size:Abstract_memory.size ->
         Abstract_memory.ProtoMemory.value ->
         Abstract_memory.ProtoMemory.value ->
         Abstract_memory.ProtoMemory.value) ->
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
      val join :
        oracle:Abstract_memory.bioracle ->
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
      val smash :
        oracle:Abstract_memory.oracle ->
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
      val read :
        oracle:Abstract_memory.oracle ->
        (Cil_types.typ -> Abstract_memory.ProtoMemory.t -> 'a) ->
        ('-> '-> 'a) ->
        Abstract_offset.t -> Abstract_memory.ProtoMemory.t -> 'a
      val update :
        oracle:Abstract_memory.oracle ->
        (weak:bool ->
         Cil_types.typ ->
         Abstract_memory.ProtoMemory.t ->
         Abstract_memory.ProtoMemory.t Lattice_bounds.or_bottom) ->
        weak:bool ->
        Abstract_offset.t ->
        Abstract_memory.ProtoMemory.t ->
        Abstract_memory.ProtoMemory.t Lattice_bounds.or_bottom
      val incr_bound :
        oracle:Abstract_memory.oracle ->
        Cil_types.varinfo ->
        Integer.t option ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
      val add_segmentation_bounds :
        oracle:Abstract_memory.oracle ->
        typ:Cil_types.typ ->
        Cil_types.exp list ->
        Abstract_memory.ProtoMemory.t -> Abstract_memory.ProtoMemory.t
    end
end