module E:sig
..end
type
t
val pretty : Format.formatter -> t -> unit
val create : S.t Wp.Sigs.sequence -> Wp.Lang.F.pred -> t
val get : t -> Wp.Lang.F.pred
val reads : t -> S.domain
val writes : t -> S.domain
val relocate : S.t Wp.Sigs.sequence -> t -> t