sig
  type chunk
  type domain
  type t
  val create : unit -> Wp.Memory.Sigma.t
  val copy : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
  val merge :
    Wp.Memory.Sigma.t ->
    Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t * Wp.Passive.t * Wp.Passive.t
  val join : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> Wp.Passive.t
  val assigned :
    Wp.Memory.Sigma.t ->
    Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Lang.F.pred Bag.t
  val mem : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> bool
  val get : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.var
  val value : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Lang.F.term
  val iter :
    (Wp.Memory.Sigma.chunk -> Wp.Lang.F.var -> unit) ->
    Wp.Memory.Sigma.t -> unit
  val iter2 :
    (Wp.Memory.Sigma.chunk ->
     Wp.Lang.F.var option -> Wp.Lang.F.var option -> unit) ->
    Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t -> unit
  val havoc :
    Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain -> Wp.Memory.Sigma.t
  val havoc_chunk :
    Wp.Memory.Sigma.t -> Wp.Memory.Sigma.chunk -> Wp.Memory.Sigma.t
  val havoc_any : call:bool -> Wp.Memory.Sigma.t -> Wp.Memory.Sigma.t
  val domain : Wp.Memory.Sigma.t -> Wp.Memory.Sigma.domain
  val pretty : Format.formatter -> Wp.Memory.Sigma.t -> unit
end