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 : '-> int -> int -> int
  val empty : int
  val has_init : '-> bool
  type t_env = Kernel_function.t
  val new_env : ?lvars:'-> CfgDump.VC.t_env -> CfgDump.VC.t_env
  val add_axiom : '-> '-> unit
  val add_hyp : '-> WpPropId.prop_id * '-> int -> int
  val add_goal : '-> WpPropId.prop_id * '-> int -> int
  val add_assigns : '-> WpPropId.prop_id * '-> int -> int
  val use_assigns : '-> '-> WpPropId.prop_id option -> '-> int -> int
  val label : '-> Clabels.c_label -> int -> int
  val assign : '-> '-> Cil_types.lval -> Cil_types.exp -> int -> int
  val return : '-> '-> Cil_types.exp option -> int -> int
  val test : '-> '-> Cil_types.exp -> int -> int -> int
  val switch : '-> '-> Cil_types.exp -> ('c * int) list -> int -> int
  val init_value : '-> '-> '-> '-> '-> 'e
  val init_range : '-> '-> '-> '-> '-> '-> 'f
  val init_const : '-> '-> '-> 'c
  val tag : string -> int -> int
  val loop_entry : int -> int
  val loop_step : int -> int
  val call_dynamic :
    '-> '-> '-> Cil_types.exp -> ('d * int) list -> int
  val call_goal_precond :
    '-> '-> Kernel_function.t -> '-> pre:'-> int -> int
  val call :
    '->
    '->
    '->
    Kernel_function.t ->
    '->
    pre:'->
    post:'-> pexit:'-> assigns:'-> p_post:int -> p_exit:int -> int
  val pp_scope :
    Mcfg.scope -> Format.formatter -> Cil_types.varinfo list -> unit
  val scope : '-> Cil_types.varinfo list -> Mcfg.scope -> int -> int
  val close : Kernel_function.t -> int -> int
  val build_prop_of_from : '-> '-> '-> int
end