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 ->
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