sig
  type scope =
      SC_Global
    | SC_Frame_in
    | SC_Frame_out
    | SC_Block_in
    | SC_Block_out
  module type Export =
    sig
      type pred
      type decl
      val export_section : Stdlib.Format.formatter -> string -> unit
      val export_goal :
        Stdlib.Format.formatter -> string -> Wp.Mcfg.Export.pred -> unit
      val export_decl :
        Stdlib.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 : Stdlib.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 :
        ?for_pid:Wp.WpPropId.prop_id ->
        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_subgoal :
        Wp.Mcfg.S.t_env ->
        Wp.WpPropId.prop_id * '->
        ?deps:Property.Set.t ->
        Cil_types.predicate ->
        Cil_types.stmt ->
        Wp.WpPropId.effect_source -> 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 ->
        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 ->
        Cil_types.stmt option ->
        Wp.Clabels.c_label -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
      val init :
        Wp.Mcfg.S.t_env ->
        Cil_types.varinfo ->
        Cil_types.init option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
      val const :
        Wp.Mcfg.S.t_env ->
        Cil_types.varinfo -> 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 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_terminates :
        Wp.Mcfg.S.t_env ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list ->
        Wp.WpPropId.pred_info ->
        ?callee_t:Cil_types.predicate -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
      val call_decreases :
        Wp.Mcfg.S.t_env ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list ->
        Wp.WpPropId.variant_info ->
        ?caller_t:Cil_types.predicate ->
        ?callee_d:Cil_types.variant -> 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.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