functor (W : Mcfg.S->
  sig
    val dkey : Log.category
    val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
    val do_labels : W.t_env -> Cil2cfg.edge -> W.t_prop -> W.t_prop
    val add_hyp : W.t_env -> W.t_prop -> WpPropId.pred_info -> W.t_prop
    val open_scope :
      W.t_env -> Cil_types.varinfo list -> Cil_types.block list -> W.t_prop
    val add_goal : W.t_env -> W.t_prop -> WpPropId.pred_info -> W.t_prop
    val add_assigns_goal :
      W.t_env -> W.t_prop -> WpPropId.assigns_full_info -> W.t_prop
    val add_assigns_hyp :
      W.t_env ->
      W.t_prop ->
      WpPropId.assigns_full_info -> Clabels.c_label option * W.t_prop
    exception Stop of Cil2cfg.edge
    val test_edge_loop_ok :
      Cil2cfg.t -> WpStrategy.strategy option -> Cil2cfg.Eset.elt -> bool
    module R :
      sig
        type t
        val empty : Cil2cfg.t -> Calculus.Cfg.??.t
        val is_pass1 : Calculus.Cfg.??.-> bool
        val change_mode_if_needed : Calculus.Cfg.??.-> unit
        val find : Calculus.Cfg.??.-> Cil2cfg.edge -> W.t_prop
        val set :
          WpStrategy.strategy ->
          W.t_env ->
          Calculus.Cfg.??.-> Cil2cfg.edge -> W.t_prop -> W.t_prop
        val add_oblig :
          Calculus.Cfg.??.-> Clabels.c_label -> W.t_prop -> unit
        val add_memo : Calculus.Cfg.??.-> Cil2cfg.edge -> W.t_prop -> unit
      end
    val use_loop_assigns :
      WpStrategy.strategy -> W.t_env -> Cil2cfg.edge -> W.t_prop -> W.t_prop
    val loop_with_cut :
      Cil2cfg.t -> WpStrategy.strategy -> Cil2cfg.node -> bool
    val wp_loop :
      'a * Cil2cfg.t * WpStrategy.strategy * 'b * W.t_env ->
      Calculus.Cfg.R.t ->
      Cil2cfg.node -> Cil2cfg.edge -> (Cil2cfg.node -> W.t_prop) -> W.t_prop
    type callenv = {
      pre_annots : WpStrategy.t_annots;
      post_annots : WpStrategy.t_annots;
      exit_annots : WpStrategy.t_annots;
    }
    val callenv :
      Cil2cfg.t ->
      WpStrategy.strategy -> Cil2cfg.node -> Calculus.Cfg.callenv
    val wp_call_any :
      W.t_env ->
      Calculus.Cfg.callenv -> p_post:W.t_prop -> p_exit:W.t_prop -> W.t_prop
    val wp_call_kf :
      W.t_env ->
      Calculus.Cfg.callenv ->
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil_types.kernel_function ->
      Cil_types.exp list ->
      bool -> p_post:W.t_prop -> p_exit:W.t_prop -> W.t_prop
    val wp_calls :
      Cil_types.kernel_function * Cil2cfg.t * WpStrategy.strategy * 'a *
      W.t_env ->
      Calculus.Cfg.R.t ->
      Cil2cfg.node ->
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil2cfg.call_type ->
      Cil_types.exp list -> W.t_prop -> W.t_prop -> W.t_prop
    val wp_stmt : W.t_env -> Cil_types.stmt -> W.t_prop -> W.t_prop
    val wp_scope :
      W.t_env -> Cil_types.varinfo list -> Mcfg.scope -> W.t_prop -> W.t_prop
    val get_wp_edge :
      Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
      Calculus.Cfg.R.t * W.t_env -> Cil2cfg.Eset.elt -> W.t_prop
    val get_only_succ :
      Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
      Calculus.Cfg.R.t * W.t_env -> Cil2cfg.t -> Cil2cfg.node -> W.t_prop
    val compute_wp_edge :
      Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
      Calculus.Cfg.R.t * W.t_env -> Cil2cfg.Eset.elt -> W.t_prop
    val init_global_variable :
      W.t_env -> Cil_types.lval -> Cil_types.init -> W.t_prop -> W.t_prop
    val process_global_init :
      W.t_env -> Cil_types.kernel_function -> W.t_prop -> W.t_prop
    val get_weakest_precondition :
      Cil2cfg.t ->
      Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
      Calculus.Cfg.R.t * W.t_env -> W.t_prop
    val compute :
      Cil2cfg.t ->
      WpStrategy.strategy ->
      W.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)
  end