sig
type t
val pretty : Stdlib.Format.formatter -> Wp.CfgCompiler.Cfg.P.t -> unit
val create :
S.t Wp.CfgCompiler.Cfg.Node.Map.t ->
Wp.Lang.F.pred -> Wp.CfgCompiler.Cfg.P.t
val get : Wp.CfgCompiler.Cfg.P.t -> Wp.Lang.F.pred
val reads :
Wp.CfgCompiler.Cfg.P.t -> S.domain Wp.CfgCompiler.Cfg.Node.Map.t
val nodes : Wp.CfgCompiler.Cfg.P.t -> Wp.CfgCompiler.Cfg.Node.Set.t
val relocate :
S.t Wp.CfgCompiler.Cfg.Node.Map.t ->
Wp.CfgCompiler.Cfg.P.t -> Wp.CfgCompiler.Cfg.P.t
val to_condition :
Wp.CfgCompiler.Cfg.P.t ->
(Wp.CfgCompiler.Cfg.C.t * Wp.CfgCompiler.Cfg.Node.t option) option
end