sig
  module type VCgen =
    sig
      type t_env
      type t_prop
      val pretty : Format.formatter -> t_prop -> unit
      val merge : t_env -> t_prop -> t_prop -> t_prop
      val empty : t_prop
      val new_env :
        ?lvars:Cil_types.logic_var list -> Cil_types.kernel_function -> t_env
      val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
      val add_hyp :
        ?for_pid:WpPropId.prop_id ->
        t_env -> WpPropId.pred_info -> t_prop -> t_prop
      val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
      val add_subgoal :
        t_env ->
        WpPropId.prop_id * '->
        ?deps:Property.Set.t ->
        Cil_types.predicate ->
        Cil_types.stmt -> WpPropId.effect_source -> t_prop -> t_prop
      val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
      val use_assigns :
        t_env ->
        WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_prop
      val label :
        t_env -> Cil_types.stmt option -> Clabels.c_label -> t_prop -> t_prop
      val init :
        t_env ->
        Cil_types.varinfo -> Cil_types.init option -> t_prop -> t_prop
      val const : t_env -> Cil_types.varinfo -> t_prop -> t_prop
      val assign :
        t_env ->
        Cil_types.stmt -> Cil_types.lval -> Cil_types.exp -> t_prop -> t_prop
      val return :
        t_env -> Cil_types.stmt -> Cil_types.exp option -> t_prop -> t_prop
      val test :
        t_env ->
        Cil_types.stmt -> Cil_types.exp -> t_prop -> t_prop -> t_prop
      val switch :
        t_env ->
        Cil_types.stmt ->
        Cil_types.exp ->
        (Cil_types.exp list * t_prop) list -> t_prop -> t_prop
      val has_init : t_env -> bool
      val loop_entry : t_prop -> t_prop
      val loop_step : t_prop -> t_prop
      val call_dynamic :
        t_env ->
        Cil_types.stmt ->
        WpPropId.prop_id ->
        Cil_types.exp -> (Cil_types.kernel_function * t_prop) list -> t_prop
      val call_goal_precond :
        t_env ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list -> pre:WpPropId.pred_info list -> t_prop -> t_prop
      val call_terminates :
        t_env ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list ->
        WpPropId.pred_info ->
        ?callee_t:Cil_types.predicate -> t_prop -> t_prop
      val call_decreases :
        t_env ->
        Cil_types.stmt ->
        Cil_types.kernel_function ->
        Cil_types.exp list ->
        WpPropId.variant_info ->
        ?caller_t:Cil_types.predicate ->
        ?callee_d:Cil_types.variant -> t_prop -> t_prop
      val call :
        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:t_prop -> p_exit:t_prop -> t_prop
      val scope :
        t_env -> Cil_types.varinfo list -> Mcfg.scope -> t_prop -> t_prop
      val close : t_env -> t_prop -> t_prop
      val build_prop_of_from :
        t_env -> WpPropId.pred_info list -> t_prop -> t_prop
      val register_lemma : LogicUsage.logic_lemma -> unit
      val compile_lemma : LogicUsage.logic_lemma -> Wpo.t
      val compile_wp : Wpo.index -> t_prop -> Wpo.t Bag.t
    end
  val vcgen : Factory.setup -> Factory.driver -> (module CfgWP.VCgen)
end