sig
type prop_id
val property_of_id : Wp.WpPropId.prop_id -> Property.t
val doomed_if_valid : Wp.WpPropId.prop_id -> Property.t list
val unreachable_if_valid : Wp.WpPropId.prop_id -> Property.other_loc
val source_of_id : Wp.WpPropId.prop_id -> Filepath.position
module PropId :
sig
type t = prop_id
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
val compare_prop_id : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_id -> int
val tactical : gid:string -> Wp.WpPropId.prop_id
val is_check : Wp.WpPropId.prop_id -> bool
val is_tactic : Wp.WpPropId.prop_id -> bool
val is_assigns : Wp.WpPropId.prop_id -> bool
val is_requires : Property.t -> bool
val is_loop_preservation : Wp.WpPropId.prop_id -> Cil_types.stmt option
val is_smoke_test : Wp.WpPropId.prop_id -> bool
val select_default : Wp.WpPropId.prop_id -> bool
val select_by_name : string list -> Wp.WpPropId.prop_id -> bool
val select_call_pre :
Cil_types.stmt -> Property.t option -> Wp.WpPropId.prop_id -> bool
val prop_id_keys : Wp.WpPropId.prop_id -> string list * string list
val get_propid : Wp.WpPropId.prop_id -> string
val get_legacy : Wp.WpPropId.prop_id -> string
val pp_propid : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
val user_bhv_names : Property.identified_property -> string list
val user_prop_names : Property.identified_property -> string list
val are_selected_names : string list -> string list -> bool
type prop_kind =
PKTactic
| PKCheck
| PKProp
| PKEstablished
| PKPreserved
| PKPropLoop
| PKVarDecr
| PKVarPos
| PKAFctOut
| PKAFctExit
| PKSmoke
| PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t
val pretty : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
val pretty_context :
Description.kf -> Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
val pretty_local : Stdlib.Format.formatter -> Wp.WpPropId.prop_id -> unit
val label_of_prop_id : Wp.WpPropId.prop_id -> string
val string_of_termination_kind : Cil_types.termination_kind -> string
val num_of_bhv_from : Cil_types.funbehavior -> Cil_types.from -> int
val mk_smoke :
Cil_types.kernel_function ->
id:string ->
?doomed:Property.t list ->
?unreachable:Cil_types.stmt -> unit -> Wp.WpPropId.prop_id
val mk_code_annot_ids :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id list
val mk_assert_id :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
val mk_loop_inv_id :
Cil_types.kernel_function ->
Cil_types.stmt ->
established:bool -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
val mk_inv_hyp_id :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
val mk_var_decr_id :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
val mk_var_pos_id :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Wp.WpPropId.prop_id
val mk_loop_from_id :
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation -> Cil_types.from -> Wp.WpPropId.prop_id
val mk_bhv_from_id :
Cil_types.kernel_function ->
Cil_types.kinstr ->
string list ->
Cil_types.funbehavior -> Cil_types.from -> Wp.WpPropId.prop_id
val mk_fct_from_id :
Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind -> Cil_types.from -> Wp.WpPropId.prop_id
val mk_disj_bhv_id :
Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
Wp.WpPropId.prop_id
val mk_compl_bhv_id :
Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
Wp.WpPropId.prop_id
val mk_decrease_id :
Cil_types.kernel_function * Cil_types.kinstr * Cil_types.variant ->
Wp.WpPropId.prop_id
val mk_lemma_id : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.prop_id
val mk_stmt_assigns_id :
Cil_types.kernel_function ->
Cil_types.stmt ->
string list ->
Cil_types.funbehavior ->
Cil_types.from list -> Wp.WpPropId.prop_id option
val mk_loop_assigns_id :
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.from list -> Wp.WpPropId.prop_id option
val mk_fct_assigns_id :
Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.from list -> Wp.WpPropId.prop_id option
val mk_pre_id :
Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_predicate -> Wp.WpPropId.prop_id
val mk_stmt_post_id :
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.funbehavior ->
Cil_types.termination_kind * Cil_types.identified_predicate ->
Wp.WpPropId.prop_id
val mk_fct_post_id :
Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind * Cil_types.identified_predicate ->
Wp.WpPropId.prop_id
val mk_call_pre_id :
Cil_types.kernel_function ->
Cil_types.stmt -> Property.t -> Property.t -> Wp.WpPropId.prop_id
val mk_property : Property.t -> Wp.WpPropId.prop_id
val mk_check : Property.t -> Wp.WpPropId.prop_id
type a_kind = LoopAssigns | StmtAssigns
type assigns_desc = private {
a_label : Wp.Clabels.c_label;
a_stmt : Cil_types.stmt option;
a_kind : Wp.WpPropId.a_kind;
a_assigns : Cil_types.assigns;
}
val pp_assigns_desc :
Stdlib.Format.formatter -> Wp.WpPropId.assigns_desc -> unit
type effect_source = FromCode | FromCall | FromReturn
type assigns_info = Wp.WpPropId.prop_id * Wp.WpPropId.assigns_desc
val assigns_info_id : Wp.WpPropId.assigns_info -> Wp.WpPropId.prop_id
type assigns_full_info = private
AssignsLocations of Wp.WpPropId.assigns_info
| AssignsAny of Wp.WpPropId.assigns_desc
| NoAssignsInfo
val empty_assigns_info : Wp.WpPropId.assigns_full_info
val mk_assigns_info :
Wp.WpPropId.prop_id ->
Wp.WpPropId.assigns_desc -> Wp.WpPropId.assigns_full_info
val mk_stmt_any_assigns_info :
Cil_types.stmt -> Wp.WpPropId.assigns_full_info
val mk_kf_any_assigns_info : unit -> Wp.WpPropId.assigns_full_info
val mk_loop_any_assigns_info :
Cil_types.stmt -> Wp.WpPropId.assigns_full_info
val pp_assign_info :
string ->
Stdlib.Format.formatter -> Wp.WpPropId.assigns_full_info -> unit
val merge_assign_info :
Wp.WpPropId.assigns_full_info ->
Wp.WpPropId.assigns_full_info -> Wp.WpPropId.assigns_full_info
val mk_loop_assigns_desc :
Cil_types.stmt -> Cil_types.from list -> Wp.WpPropId.assigns_desc
val mk_stmt_assigns_desc :
Cil_types.stmt -> Cil_types.from list -> Wp.WpPropId.assigns_desc
val mk_asm_assigns_desc : Cil_types.stmt -> Wp.WpPropId.assigns_desc
val mk_kf_assigns_desc : Cil_types.from list -> Wp.WpPropId.assigns_desc
val mk_init_assigns : Wp.WpPropId.assigns_desc
val is_call_assigns : Wp.WpPropId.assigns_desc -> bool
type axiom_info = Wp.WpPropId.prop_id * Wp.LogicUsage.logic_lemma
val mk_axiom_info : Wp.LogicUsage.logic_lemma -> Wp.WpPropId.axiom_info
val pp_axiom_info :
Stdlib.Format.formatter -> Wp.WpPropId.axiom_info -> unit
type pred_info = Wp.WpPropId.prop_id * Cil_types.predicate
val mk_pred_info :
Wp.WpPropId.prop_id -> Cil_types.predicate -> Wp.WpPropId.pred_info
val pred_info_id : Wp.WpPropId.pred_info -> Wp.WpPropId.prop_id
val pp_pred_of_pred_info :
Stdlib.Format.formatter -> Wp.WpPropId.pred_info -> unit
val pp_pred_info : Stdlib.Format.formatter -> Wp.WpPropId.pred_info -> unit
val split_bag :
(Wp.WpPropId.prop_id -> 'a -> unit) ->
Wp.WpPropId.prop_id -> 'a Bag.t -> unit
val split_map :
(Wp.WpPropId.prop_id -> 'a -> 'b) ->
Wp.WpPropId.prop_id -> 'a list -> 'b list
val mk_part : Wp.WpPropId.prop_id -> int * int -> Wp.WpPropId.prop_id
val kind_of_id : Wp.WpPropId.prop_id -> Wp.WpPropId.prop_kind
val parts_of_id : Wp.WpPropId.prop_id -> (int * int) option
val subproofs : Wp.WpPropId.prop_id -> int
val subproof_idx : Wp.WpPropId.prop_id -> int
val get_induction : Wp.WpPropId.prop_id -> Cil_types.stmt option
end