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