sig
type t
val pretty : Stdlib.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