sig
  type t
  val equal : Wp.CfgCompiler.Cfg.C.t -> Wp.CfgCompiler.Cfg.C.t -> bool
  val create : S.t -> Wp.Lang.F.pred -> Wp.CfgCompiler.Cfg.C.t
  val get : Wp.CfgCompiler.Cfg.C.t -> Wp.Lang.F.pred
  val reads : Wp.CfgCompiler.Cfg.C.t -> S.domain
  val relocate : S.t -> Wp.CfgCompiler.Cfg.C.t -> Wp.CfgCompiler.Cfg.C.t
end