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   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 :     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 -> impl_assumes:bool -> 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 ->     Cil_types.logic_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 ->     Cil_types.logic_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 ->     Cil_types.logic_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.identified_term 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.identified_term 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_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 ->     bool ->     WpStrategy.strategy_kind -> WpStrategy.annots_tbl -> WpStrategy.strategy   val get_annots : WpStrategy.strategy -> Cil2cfg.edge -> WpStrategy.t_annots   val new_loop_computation : WpStrategy.strategy -> bool   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