sig
  type t
  val pretty : Format.formatter -> Wp.CfgCompiler.Cfg.T.t -> unit
  val create :
    S.t Wp.CfgCompiler.Cfg.Node.Map.t ->
    Wp.Lang.F.term -> Wp.CfgCompiler.Cfg.T.t
  val get : Wp.CfgCompiler.Cfg.T.t -> Wp.Lang.F.term
  val reads :
    Wp.CfgCompiler.Cfg.T.t -> S.domain Wp.CfgCompiler.Cfg.Node.Map.t
  val relocate :
    S.t Wp.CfgCompiler.Cfg.Node.Map.t ->
    Wp.CfgCompiler.Cfg.T.t -> Wp.CfgCompiler.Cfg.T.t
  val init :
    Wp.CfgCompiler.Cfg.Node.Set.t ->
    (S.t Wp.CfgCompiler.Cfg.Node.Map.t -> Wp.Lang.F.term) ->
    Wp.CfgCompiler.Cfg.T.t
  val init' :
    Wp.CfgCompiler.Cfg.Node.t ->
    (S.t -> Wp.Lang.F.term) -> Wp.CfgCompiler.Cfg.T.t
end