sig   type scope =       SC_Global     | SC_Function_in     | SC_Function_frame     | SC_Function_out     | SC_Block_in     | SC_Block_out   module type Export =     sig       type pred       type decl       val export_section : Format.formatter -> string -> unit       val export_goal :         Format.formatter -> string -> Wp.Mcfg.Export.pred -> unit       val export_decl : Format.formatter -> Wp.Mcfg.Export.decl -> unit     end   module type Splitter =     sig       type pred       val simplify : Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred       val split :         bool -> Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred Bag.t     end   module type S =     sig       type t_env       type t_prop       val pretty : Format.formatter -> Wp.Mcfg.S.t_prop -> unit       val merge :         Wp.Mcfg.S.t_env ->         Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val empty : Wp.Mcfg.S.t_prop       val new_env :         ?lvars:Cil_types.logic_var list ->         Cil_types.kernel_function -> Wp.Mcfg.S.t_env       val add_axiom :         Wp.WpPropId.prop_id -> Wp.LogicUsage.logic_lemma -> unit       val add_hyp :         Wp.Mcfg.S.t_env ->         Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val add_goal :         Wp.Mcfg.S.t_env ->         Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val add_assigns :         Wp.Mcfg.S.t_env ->         Wp.WpPropId.assigns_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val use_assigns :         Wp.Mcfg.S.t_env ->         Cil_types.stmt option ->         Wp.WpPropId.prop_id option ->         Wp.WpPropId.assigns_desc -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val label :         Wp.Mcfg.S.t_env ->         Wp.Clabels.c_label -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val assign :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.lval ->         Cil_types.exp -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val return :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val test :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.exp ->         Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val switch :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.exp ->         (Cil_types.exp list * Wp.Mcfg.S.t_prop) list ->         Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val has_init : Wp.Mcfg.S.t_env -> bool       val init_value :         Wp.Mcfg.S.t_env ->         Cil_types.lval ->         Cil_types.typ ->         Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val init_range :         Wp.Mcfg.S.t_env ->         Cil_types.lval ->         Cil_types.typ ->         Integer.t ->         Integer.t ->         Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val init_const :         Wp.Mcfg.S.t_env ->         Cil_types.varinfo -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val loop_entry : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val loop_step : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val call_dynamic :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Wp.WpPropId.prop_id ->         Cil_types.exp ->         (Cil_types.kernel_function * Wp.Mcfg.S.t_prop) list ->         Wp.Mcfg.S.t_prop       val call_goal_precond :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.kernel_function ->         Cil_types.exp list ->         pre:Wp.WpPropId.pred_info list ->         Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val call :         Wp.Mcfg.S.t_env ->         Cil_types.stmt ->         Cil_types.lval option ->         Cil_types.kernel_function ->         Cil_types.exp list ->         pre:Wp.WpPropId.pred_info list ->         post:Wp.WpPropId.pred_info list ->         pexit:Wp.WpPropId.pred_info list ->         assigns:Cil_types.identified_term Cil_types.assigns ->         p_post:Wp.Mcfg.S.t_prop ->         p_exit:Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val scope :         Wp.Mcfg.S.t_env ->         Cil_types.varinfo list ->         Wp.Mcfg.scope -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val close : Wp.Mcfg.S.t_env -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop       val build_prop_of_from :         Wp.Mcfg.S.t_env ->         Wp.WpPropId.pred_info list -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop     end end