sig
  type t_env
  type t_prop
  val pretty : 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 :
    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_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 ->
    Cil_types.stmt option ->
    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 :
    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