sig   type t_env   type t_prop   val pretty : Format.formatter -> Mcfg.S.t_prop -> unit   val merge : Mcfg.S.t_env -> Mcfg.S.t_prop -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val empty : Mcfg.S.t_prop   val new_env :     ?lvars:Cil_types.logic_var list ->     Cil_types.kernel_function -> Mcfg.S.t_env   val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit   val add_hyp :     Mcfg.S.t_env -> WpPropId.pred_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val add_goal :     Mcfg.S.t_env -> WpPropId.pred_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val add_assigns :     Mcfg.S.t_env -> WpPropId.assigns_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val use_assigns :     Mcfg.S.t_env ->     Cil_types.stmt option ->     WpPropId.prop_id option ->     WpPropId.assigns_desc -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val label :     Mcfg.S.t_env -> Clabels.c_label -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val assign :     Mcfg.S.t_env ->     Cil_types.stmt ->     Cil_types.lval -> Cil_types.exp -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val return :     Mcfg.S.t_env ->     Cil_types.stmt -> Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val test :     Mcfg.S.t_env ->     Cil_types.stmt ->     Cil_types.exp -> Mcfg.S.t_prop -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val switch :     Mcfg.S.t_env ->     Cil_types.stmt ->     Cil_types.exp ->     (Cil_types.exp list * Mcfg.S.t_prop) list ->     Mcfg.S.t_prop -> Mcfg.S.t_prop   val has_init : Mcfg.S.t_env -> bool   val init_value :     Mcfg.S.t_env ->     Cil_types.lval ->     Cil_types.typ -> Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val init_range :     Mcfg.S.t_env ->     Cil_types.lval ->     Cil_types.typ ->     Integer.t ->     Integer.t -> Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val init_const :     Mcfg.S.t_env -> Cil_types.varinfo -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val loop_entry : Mcfg.S.t_prop -> Mcfg.S.t_prop   val loop_step : Mcfg.S.t_prop -> Mcfg.S.t_prop   val call_dynamic :     Mcfg.S.t_env ->     Cil_types.stmt ->     WpPropId.prop_id ->     Cil_types.exp ->     (Cil_types.kernel_function * Mcfg.S.t_prop) list -> Mcfg.S.t_prop   val call_goal_precond :     Mcfg.S.t_env ->     Cil_types.stmt ->     Cil_types.kernel_function ->     Cil_types.exp list ->     pre:WpPropId.pred_info list -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val call :     Mcfg.S.t_env ->     Cil_types.stmt ->     Cil_types.lval option ->     Cil_types.kernel_function ->     Cil_types.exp list ->     pre:WpPropId.pred_info list ->     post:WpPropId.pred_info list ->     pexit:WpPropId.pred_info list ->     assigns:Cil_types.identified_term Cil_types.assigns ->     p_post:Mcfg.S.t_prop -> p_exit:Mcfg.S.t_prop -> Mcfg.S.t_prop   val scope :     Mcfg.S.t_env ->     Cil_types.varinfo list -> Mcfg.scope -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val close : Mcfg.S.t_env -> Mcfg.S.t_prop -> Mcfg.S.t_prop   val build_prop_of_from :     Mcfg.S.t_env -> WpPropId.pred_info list -> Mcfg.S.t_prop -> Mcfg.S.t_prop end