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