sig
  type behavior = {
    bhv_assumes : WpPropId.pred_info list;
    bhv_requires : WpPropId.pred_info list;
    bhv_smokes : WpPropId.pred_info list;
    bhv_ensures : WpPropId.pred_info list;
    bhv_exits : WpPropId.pred_info list;
    bhv_post_assigns : WpPropId.assigns_full_info;
    bhv_exit_assigns : WpPropId.assigns_full_info;
  }
  val get_requires :
    goal:bool ->
    Cil_types.kernel_function ->
    Cil_types.funbehavior -> WpPropId.pred_info list
  val get_preconditions :
    goal:bool -> Cil_types.kernel_function -> WpPropId.pred_info list
  val get_behavior_goals :
    Cil_types.kernel_function ->
    ?smoking:bool ->
    ?exits:bool -> Cil_types.funbehavior -> CfgAnnot.behavior
  val get_complete_behaviors :
    Cil_types.kernel_function -> WpPropId.pred_info list
  val get_disjoint_behaviors :
    Cil_types.kernel_function -> WpPropId.pred_info list
  val get_terminates_goal :
    Cil_types.kernel_function -> WpPropId.pred_info option
  val get_decreases_goal :
    Cil_types.kernel_function -> WpPropId.variant_info option
  type code_assertion = {
    code_admitted : WpPropId.pred_info option;
    code_verified : WpPropId.pred_info option;
  }
  val get_code_assertions :
    ?smoking:bool ->
    Cil_types.kernel_function ->
    Cil_types.stmt -> CfgAnnot.code_assertion list
  val get_unreachable :
    Cil_types.kernel_function -> Cil_types.stmt -> WpPropId.prop_id
  val get_stmt_assigns :
    Cil_types.kernel_function ->
    Cil_types.stmt -> WpPropId.assigns_full_info list
  type loop_hypothesis =
      NoHyp
    | Check of WpPropId.prop_id
    | Always of WpPropId.prop_id
  type loop_invariant = {
    loop_hyp : CfgAnnot.loop_hypothesis;
    loop_est : WpPropId.prop_id option;
    loop_ind : WpPropId.prop_id option;
    loop_pred : Cil_types.predicate;
  }
  type loop_contract = {
    loop_terminates : Cil_types.predicate option;
    loop_invariants : CfgAnnot.loop_invariant list;
    loop_smoke : WpPropId.pred_info list;
    loop_assigns : WpPropId.assigns_full_info list;
  }
  val get_loop_contract :
    ?smoking:bool ->
    ?terminates:Cil_types.predicate ->
    Cil_types.kernel_function -> Cil_types.stmt -> CfgAnnot.loop_contract
  val mk_variant_properties :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    Cil_types.term -> WpPropId.pred_info * WpPropId.pred_info
  type contract = {
    contract_cond : WpPropId.pred_info list;
    contract_hpre : WpPropId.pred_info list;
    contract_post : WpPropId.pred_info list;
    contract_exit : WpPropId.pred_info list;
    contract_smoke : WpPropId.pred_info list;
    contract_assigns : Cil_types.assigns;
    contract_terminates : bool * Cil_types.predicate;
    contract_decreases : Cil_types.variant option;
  }
  val get_call_contract :
    ?smoking:Cil_types.stmt ->
    Cil_types.kernel_function -> Cil_types.stmt -> CfgAnnot.contract
  val clear : unit -> unit
end