sig
  type t_annots
  val empty_acc : WpStrategy.t_annots
  type annot_kind =
      Ahyp
    | Agoal
    | Aboth of bool
    | AcutB of bool
    | AcallHyp of Cil_types.kernel_function
    | AcallPre of bool * Cil_types.kernel_function
    | AcallPost of Cil_types.kernel_function
  val normalize :
    WpPropId.prop_id ->
    ?assumes:Cil_types.predicate ->
    NormAtLabels.label_mapping ->
    Cil_types.predicate -> Cil_types.predicate option
  val add_prop :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    WpPropId.prop_id -> Cil_types.predicate option -> WpStrategy.t_annots
  val add_prop_fct_pre_bhv :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function -> Cil_types.funbehavior -> WpStrategy.t_annots
  val add_prop_fct_pre :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    assumes:Cil_types.predicate option ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_fct_bhv_pre :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function -> Cil_types.funbehavior -> WpStrategy.t_annots
  val add_prop_fct_smoke :
    WpStrategy.t_annots ->
    Cil_types.kernel_function -> Cil_types.funbehavior -> WpStrategy.t_annots
  val add_prop_dead_loop :
    WpStrategy.t_annots ->
    Cil_types.kernel_function -> Cil_types.stmt -> WpStrategy.t_annots
  val add_prop_dead_code :
    WpStrategy.t_annots ->
    Cil_types.kernel_function -> Cil_types.stmt -> WpStrategy.t_annots
  val add_prop_dead_call :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    WpStrategy.t_annots ->
    WpStrategy.t_annots -> WpStrategy.t_annots * WpStrategy.t_annots
  val add_prop_fct_post :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_stmt_pre :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.funbehavior ->
    assumes:Cil_types.predicate option ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_stmt_post :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind ->
    Clabels.c_label option ->
    assumes:Cil_types.predicate option ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_stmt_bhv_requires :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.funbehavior -> with_assumes:bool -> WpStrategy.t_annots
  val add_prop_stmt_spec_pre :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.funspec -> WpStrategy.t_annots
  val add_prop_call_pre :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    WpPropId.prop_id ->
    assumes:Cil_types.predicate ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_call_post :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.funbehavior ->
    Cil_types.termination_kind ->
    assumes:Cil_types.predicate ->
    Cil_types.identified_predicate -> WpStrategy.t_annots
  val add_prop_assert :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation -> Cil_types.predicate -> WpStrategy.t_annots
  val add_prop_loop_inv :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    Cil_types.stmt ->
    WpPropId.prop_id -> Cil_types.predicate -> WpStrategy.t_annots
  val add_assigns :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    WpPropId.prop_id -> WpPropId.assigns_desc -> WpStrategy.t_annots
  val add_assigns_any :
    WpStrategy.t_annots ->
    WpStrategy.annot_kind ->
    WpPropId.assigns_full_info -> WpStrategy.t_annots
  val add_stmt_spec_assigns_hyp :
    WpStrategy.t_annots ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Clabels.c_label option -> Cil_types.funspec -> WpStrategy.t_annots
  val add_call_assigns_any :
    WpStrategy.t_annots -> Cil_types.stmt -> WpStrategy.t_annots
  val add_call_assigns_hyp :
    WpStrategy.t_annots ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    called_kf:Cil_types.kernel_function ->
    Clabels.c_label option -> Cil_types.funspec option -> WpStrategy.t_annots
  val add_loop_assigns_hyp :
    WpStrategy.t_annots ->
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    (Cil_types.code_annotation * Cil_types.from list) option ->
    WpStrategy.t_annots
  val add_fct_bhv_assigns_hyp :
    WpStrategy.t_annots ->
    Cil_types.kernel_function ->
    Cil_types.termination_kind ->
    Cil_types.funbehavior -> WpStrategy.t_annots
  val assigns_upper_bound :
    Cil_types.funspec -> (Cil_types.funbehavior * Cil_types.from list) option
  val get_hyp_only : WpStrategy.t_annots -> WpPropId.pred_info list
  val get_goal_only : WpStrategy.t_annots -> WpPropId.pred_info list
  val get_both_hyp_goals :
    WpStrategy.t_annots -> WpPropId.pred_info list * WpPropId.pred_info list
  val get_cut : WpStrategy.t_annots -> (bool * WpPropId.pred_info) list
  val get_call_hyp :
    WpStrategy.t_annots ->
    Cil_types.kernel_function -> WpPropId.pred_info list
  val get_call_pre :
    WpStrategy.t_annots ->
    Cil_types.kernel_function ->
    WpPropId.pred_info list * WpPropId.pred_info list
  val get_call_post :
    WpStrategy.t_annots ->
    Cil_types.kernel_function -> WpPropId.pred_info list
  val get_call_asgn :
    WpStrategy.t_annots ->
    Cil_types.kernel_function option -> WpPropId.assigns_full_info
  val get_asgn_hyp : WpStrategy.t_annots -> WpPropId.assigns_full_info
  val get_asgn_goal : WpStrategy.t_annots -> WpPropId.assigns_full_info
  val pp_annots : Format.formatter -> WpStrategy.t_annots -> unit
  type annots_tbl
  val create_tbl : unit -> WpStrategy.annots_tbl
  val add_on_edges :
    WpStrategy.annots_tbl -> WpStrategy.t_annots -> Cil2cfg.edge list -> unit
  val add_node_annots :
    WpStrategy.annots_tbl ->
    Cil2cfg.t ->
    Cil2cfg.node ->
    WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots) -> unit
  val add_loop_annots :
    WpStrategy.annots_tbl ->
    Cil2cfg.t ->
    Cil2cfg.node ->
    entry:WpStrategy.t_annots ->
    back:WpStrategy.t_annots -> core:WpStrategy.t_annots -> unit
  val add_axiom : WpStrategy.annots_tbl -> LogicUsage.logic_lemma -> unit
  val add_all_axioms : WpStrategy.annots_tbl -> unit
  type strategy
  type strategy_for_froms = {
    get_pre : unit -> WpStrategy.t_annots;
    more_vars : Cil_types.logic_var list;
  }
  type strategy_kind = SKannots | SKfroms of WpStrategy.strategy_for_froms
  val mk_strategy :
    string ->
    Cil2cfg.t ->
    string option ->
    WpStrategy.strategy_kind -> WpStrategy.annots_tbl -> WpStrategy.strategy
  val get_annots : WpStrategy.strategy -> Cil2cfg.edge -> WpStrategy.t_annots
  val strategy_has_asgn_goal : WpStrategy.strategy -> bool
  val strategy_has_prop_goal : WpStrategy.strategy -> bool
  val strategy_kind : WpStrategy.strategy -> WpStrategy.strategy_kind
  val global_axioms : WpStrategy.strategy -> WpPropId.axiom_info list
  val behavior_name_of_strategy : WpStrategy.strategy -> string option
  val is_default_behavior : WpStrategy.strategy -> bool
  val cfg_of_strategy : WpStrategy.strategy -> Cil2cfg.t
  val get_kf : WpStrategy.strategy -> Cil_types.kernel_function
  val get_bhv : WpStrategy.strategy -> string option
  val pp_info_of_strategy : Format.formatter -> WpStrategy.strategy -> unit
  val is_main_init : Cil_types.kernel_function -> bool
  val isInitConst : unit -> bool
  val isGlobalInitConst : Cil_types.varinfo -> bool
  val fold_bhv_post_cond :
    warn:bool ->
    ('n_acc -> Cil_types.identified_predicate -> 'n_acc) ->
    ('e_acc -> Cil_types.identified_predicate -> 'e_acc) ->
    'n_acc * 'e_acc -> Cil_types.funbehavior -> 'n_acc * 'e_acc
  val mk_variant_properties :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    Cil_types.term ->
    (WpPropId.prop_id * Cil_types.predicate) *
    (WpPropId.prop_id * Cil_types.predicate)
end