sig
  type env
  type label
  type value =
      Term
    | Addr of Wp.Sigs.s_lval
    | Lval of Wp.Sigs.s_lval * Wp.Pcfg.label
    | Chunk of string * Wp.Pcfg.label
  val create : unit -> Wp.Pcfg.env
  val register : Wp.Conditions.sequence -> Wp.Pcfg.env
  val at : Wp.Pcfg.env -> id:int -> Wp.Pcfg.label
  val find : Wp.Pcfg.env -> Wp.Lang.F.term -> Wp.Pcfg.value
  val updates :
    Wp.Pcfg.env ->
    Wp.Pcfg.label Wp.Sigs.sequence ->
    Wp.Lang.F.Vars.t -> Wp.Sigs.update Bag.t
  val visible : Wp.Pcfg.label -> bool
  val subterms :
    Wp.Pcfg.env -> (Wp.Lang.F.term -> unit) -> Wp.Lang.F.term -> bool
  val prev : Wp.Pcfg.label -> Wp.Pcfg.label list
  val next : Wp.Pcfg.label -> Wp.Pcfg.label list
  val iter :
    (Wp.Sigs.mval -> Wp.Lang.F.term -> unit) -> Wp.Pcfg.label -> unit
  val branching : Wp.Pcfg.label -> bool
  class virtual engine :
    object
      method is_atomic_lv : Wp.Sigs.s_lval -> bool
      method pp_addr : Stdlib.Format.formatter -> Wp.Sigs.s_lval -> unit
      method virtual pp_atom :
        Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
      method pp_chunk : Stdlib.Format.formatter -> string -> unit
      method virtual pp_flow :
        Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
      method pp_host : Stdlib.Format.formatter -> Wp.Sigs.s_host -> unit
      method pp_label : Stdlib.Format.formatter -> Wp.Pcfg.label -> unit
      method pp_lval : Stdlib.Format.formatter -> Wp.Sigs.s_lval -> unit
      method pp_offset :
        Stdlib.Format.formatter -> Wp.Sigs.s_offset list -> unit
      method pp_ofs : Stdlib.Format.formatter -> Wp.Sigs.s_offset -> unit
    end
end