sig
  val fc : (Pervasives.out_channel * string) option Pervasives.ref
  val out : Format.formatter Pervasives.ref
  val knode : int Pervasives.ref
  val node : unit -> int
  val init : Kernel_function.t -> string option -> unit
  val flush : unit -> unit
  type t_prop = int
  val pretty : Format.formatter -> int -> unit
  val link : int -> int -> unit
  val merge : 'a -> int -> int -> int
  val empty : int
  type t_env = Kernel_function.t
  val new_env : ?lvars:'a -> CfgDump.VC.t_env -> CfgDump.VC.t_env
  val add_axiom : 'a -> 'b -> unit
  val add_hyp : 'a -> WpPropId.prop_id * 'b -> int -> int
  val add_goal : 'a -> WpPropId.prop_id * 'b -> int -> int
  val add_assigns : 'a -> WpPropId.prop_id * 'b -> int -> int
  val use_assigns : 'a -> 'b -> WpPropId.prop_id option -> 'c -> int -> int
  val label : 'a -> Clabels.c_label -> int -> int
  val assign : 'a -> 'b -> Cil_types.lval -> Cil_types.exp -> int -> int
  val return : 'a -> 'b -> Cil_types.exp option -> int -> int
  val test : 'a -> 'b -> Cil_types.exp -> int -> int -> int
  val switch : 'a -> 'b -> Cil_types.exp -> ('c * int) list -> int -> int
  val init_value : 'a -> 'b -> 'c -> 'd -> 'e -> 'e
  val init_range : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'f
  val tag : string -> int -> int
  val loop_entry : int -> int
  val loop_step : int -> int
  val call_dynamic :
    'a -> 'b -> 'c -> Cil_types.exp -> ('d * int) list -> int
  val call_goal_precond :
    'a -> 'b -> Kernel_function.t -> 'c -> pre:'d -> int -> int
  val call :
    'a ->
    'b ->
    'c ->
    Kernel_function.t ->
    'd ->
    pre:'e ->
    post:'f -> pexit:'g -> assigns:'h -> p_post:int -> p_exit:int -> int
  val pp_scope :
    Mcfg.scope -> Format.formatter -> Cil_types.varinfo list -> unit
  val scope : 'a -> Cil_types.varinfo list -> Mcfg.scope -> int -> int
  val close : Kernel_function.t -> int -> int
  val build_prop_of_from : 'a -> 'b -> 'c -> int
end