sig
  module S : Sigs.Sigma
  module Node :
    sig
      type t
      module Map :
        sig
          type key = t
          type 'a t
          val is_empty : 'a t -> bool
          val empty : 'a t
          val add : key -> '-> 'a t -> 'a t
          val mem : key -> 'a t -> bool
          val find : key -> 'a t -> 'a
          val remove : key -> 'a t -> 'a t
          val compare : ('-> '-> int) -> 'a t -> 'a t -> int
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val map : (key -> '-> 'b) -> 'a t -> 'b t
          val mapf : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapq : (key -> '-> 'a option) -> 'a t -> 'a t
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val union : (key -> '-> '-> 'a) -> 'a t -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c) -> 'a t -> 'b t -> 'c t
          val interf : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val interq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
          val diffq : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val iter2 :
            (key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
          val subset : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val insert : (key -> '-> '-> 'a) -> key -> '-> 'a t -> 'a t
          val change :
            (key -> '-> 'a option -> 'a option) ->
            key -> '-> 'a t -> 'a t
        end
      module Set :
        sig
          type elt = t
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val find : elt -> t -> elt
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> '-> 'a) -> t -> '-> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val map : (elt -> elt) -> t -> t
          val mapf : (elt -> elt option) -> t -> t
          val intersect : t -> t -> bool
        end
      module Hashtbl :
        sig
          type key = t
          type !'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> '-> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_opt : 'a t -> key -> 'a option
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
          val to_seq : 'a t -> (key * 'a) Seq.t
          val to_seq_keys : 'a t -> key Seq.t
          val to_seq_values : 'a t -> 'Seq.t
          val add_seq : 'a t -> (key * 'a) Seq.t -> unit
          val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
          val of_seq : (key * 'a) Seq.t -> 'a t
        end
      val pp : Stdlib.Format.formatter -> Wp.CfgCompiler.Cfg.Node.t -> unit
      val create : unit -> Wp.CfgCompiler.Cfg.Node.t
      val equal :
        Wp.CfgCompiler.Cfg.Node.t -> Wp.CfgCompiler.Cfg.Node.t -> bool
    end
  type node = Wp.CfgCompiler.Cfg.Node.t
  val node : unit -> Wp.CfgCompiler.Cfg.node
  module C :
    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
  module P :
    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
  module T :
    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
  module E :
    sig
      type t
      val pretty : Stdlib.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
  type cfg
  val dump_env : name:string -> Wp.CfgCompiler.Cfg.cfg -> unit
  val output_dot :
    Stdlib.out_channel ->
    ?checks:Wp.CfgCompiler.Cfg.P.t Bag.t -> Wp.CfgCompiler.Cfg.cfg -> unit
  val nop : Wp.CfgCompiler.Cfg.cfg
  val add_tmpnode : Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val concat :
    Wp.CfgCompiler.Cfg.cfg ->
    Wp.CfgCompiler.Cfg.cfg -> Wp.CfgCompiler.Cfg.cfg
  val meta :
    ?stmt:Cil_types.stmt ->
    ?descr:string -> Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val goto :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val branch :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.C.t ->
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val guard :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.C.t ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val guard' :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.C.t ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val either :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.node list -> Wp.CfgCompiler.Cfg.cfg
  val implies :
    Wp.CfgCompiler.Cfg.node ->
    (Wp.CfgCompiler.Cfg.C.t * Wp.CfgCompiler.Cfg.node) list ->
    Wp.CfgCompiler.Cfg.cfg
  val effect :
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.E.t ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val assume : Wp.CfgCompiler.Cfg.P.t -> Wp.CfgCompiler.Cfg.cfg
  val havoc :
    Wp.CfgCompiler.Cfg.node ->
    effects:Wp.CfgCompiler.Cfg.node Wp.Sigs.sequence ->
    Wp.CfgCompiler.Cfg.node -> Wp.CfgCompiler.Cfg.cfg
  val compile :
    ?name:string ->
    ?mode:Wp.CfgCompiler.mode ->
    Wp.CfgCompiler.Cfg.node ->
    Wp.CfgCompiler.Cfg.Node.Set.t ->
    S.domain Wp.CfgCompiler.Cfg.Node.Map.t ->
    Wp.CfgCompiler.Cfg.cfg ->
    Wp.Lang.F.pred Wp.CfgCompiler.Cfg.Node.Map.t *
    S.t Wp.CfgCompiler.Cfg.Node.Map.t * Wp.Conditions.sequence
end