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_assigns :
    Mcfg.S.t_env -> WpPropId.assigns_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop
  val use_assigns :
    Mcfg.S.t_env ->
    Cil_types.stmt option ->
    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 :
    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