Module Wp.CfgCompiler.Cfg.E

module E: sig .. end
Relocatable effect (a predicate that depend on two states).

type t 
val pretty : Format.formatter -> t -> unit
val create : S.t Wp.Sigs.sequence -> Wp.Lang.F.pred -> t
Bundle an equation with the sigma sequence that created it
val get : t -> Wp.Lang.F.pred
val reads : t -> S.domain
val writes : t -> S.domain
as defined by S.writes
val relocate : S.t Wp.Sigs.sequence -> t -> t