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