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 -> Mcfg.Export.pred -> unit
      val export_decl : Stdlib.Format.formatter -> Mcfg.Export.decl -> unit
    end
  module type Splitter =
    sig
      type pred
      val simplify : Mcfg.Splitter.pred -> Mcfg.Splitter.pred
      val split : bool -> Mcfg.Splitter.pred -> Mcfg.Splitter.pred Bag.t
    end
  module type S =
    sig
      type t_env
      type t_prop
      val pretty : Stdlib.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_subgoal :
        Mcfg.S.t_env ->
        WpPropId.pred_info ->
        ?deps:Property.Set.t ->
        Cil_types.predicate ->
        Cil_types.stmt ->
        WpPropId.effect_source -> 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 ->
        WpPropId.prop_id option ->
        WpPropId.assigns_desc -> Mcfg.S.t_prop -> Mcfg.S.t_prop
      val label :
        Mcfg.S.t_env ->
        Cil_types.stmt option ->
        Clabels.c_label -> Mcfg.S.t_prop -> Mcfg.S.t_prop
      val init :
        Mcfg.S.t_env ->
        Cil_types.varinfo ->
        Cil_types.init option -> Mcfg.S.t_prop -> Mcfg.S.t_prop
      val const :
        Mcfg.S.t_env -> Cil_types.varinfo -> 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 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_terminates :
        Mcfg.S.t_env ->
        WpPropId.pred_info ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list ->
        callee_t:Cil_types.predicate -> 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.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
end