Wp.WpPropId
Beside the property identification, it can be found in different contexts * depending on which part of the computation is involved. * For instance, properties on loops are split in 2 parts : establishment and * preservation.
val property_of_id : prop_id -> Frama_c_kernel.Property.t
returns the annotation which lead to the given PO.
val doomed_if_valid : prop_id -> Frama_c_kernel.Property.t list
Properties that are False-if-unreachable in case the PO is valid.
val unreachable_if_valid : prop_id -> Frama_c_kernel.Property.other_loc
Stmt that is unreachable in case the PO is valid.
val source_of_id : prop_id -> Frama_c_kernel.Filepath.position
module PropId : Frama_c_kernel.Datatype.S with type t = prop_id
val tactical : gid:string -> prop_id
val is_check : prop_id -> bool
val is_tactic : prop_id -> bool
val is_assigns : prop_id -> bool
val is_requires : Frama_c_kernel.Property.t -> bool
val is_loop_preservation : prop_id -> Frama_c_kernel.Cil_types.stmt option
val is_smoke_test : prop_id -> bool
val select_default : prop_id -> bool
test if the prop_id does not have a no_wp:
in its name(s).
val select_by_name : string list -> prop_id -> bool
test if the prop_id has to be selected for the asked names.
val select_for_behaviors : string list -> prop_id -> bool
test if the prop_id has to be selected for the asked behavior names.
val select_call_pre :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Property.t option ->
prop_id ->
bool
test if the prop_id has to be selected when we want to select the call.
From a list of names (of an identified terms), returns usable names.
val prop_id_keys : prop_id -> string list * string list
val get_propid : prop_id -> string
Unique identifier of prop_id
val pp_propid : Stdlib.Format.formatter -> prop_id -> unit
Print unique id of prop_id
val user_pred_names :
Frama_c_kernel.Cil_types.toplevel_predicate ->
string list
val user_bhv_names : Frama_c_kernel.Property.identified_property -> string list
val user_prop_names :
Frama_c_kernel.Property.identified_property ->
string list
are_selected_names asked names
checks if names
of a property are selected according to asked
names.
val pretty : Stdlib.Format.formatter -> prop_id -> unit
val pretty_context :
Frama_c_kernel.Description.kf ->
Stdlib.Format.formatter ->
prop_id ->
unit
val pretty_local : Stdlib.Format.formatter -> prop_id -> unit
val label_of_prop_id : prop_id -> string
Short description of the kind of PO
val string_of_termination_kind :
Frama_c_kernel.Cil_types.termination_kind ->
string
TODO: should probably be somewhere else
val num_of_bhv_from :
Frama_c_kernel.Cil_types.funbehavior ->
Frama_c_kernel.Cil_types.from ->
int
val mk_smoke :
Frama_c_kernel.Cil_types.kernel_function ->
id:string ->
?doomed:Frama_c_kernel.Property.t list ->
?unreachable:Frama_c_kernel.Cil_types.stmt ->
unit ->
prop_id
val mk_code_annot_ids :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id list
val mk_assert_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
val mk_loop_inv_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
established:bool ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
Invariant establishment and preservation
val mk_loop_inv :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id * prop_id
Invariant establishment and preservation, in this order
val mk_inv_hyp_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
Invariant used as hypothesis
val mk_var_decr_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
Variant decrease
val mk_var_pos_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
Variant positive
val mk_var_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
prop_id
Variant for
val mk_loop_from_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
Frama_c_kernel.Cil_types.from ->
prop_id
\from property of loop assigns. Must not be FromAny
val mk_bhv_from_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.kinstr ->
string list ->
Frama_c_kernel.Cil_types.funbehavior ->
Frama_c_kernel.Cil_types.from ->
prop_id
\from property of function or statement behavior assigns. Must not be FromAny
val mk_fct_from_id :
Frama_c_kernel.Cil_types.kernel_function ->
bool ->
Frama_c_kernel.Cil_types.funbehavior ->
Frama_c_kernel.Cil_types.termination_kind ->
Frama_c_kernel.Cil_types.from ->
prop_id
\from property of function behavior assigns. Must not be FromAny
. The boolean indicate whether the function has exit node or not.
val mk_disj_bhv_id :
(Frama_c_kernel.Cil_types.kernel_function
* Frama_c_kernel.Cil_types.kinstr
* string list
* string list) ->
prop_id
disjoint behaviors property. See Property
.ip_of_disjoint for more information
val mk_compl_bhv_id :
(Frama_c_kernel.Cil_types.kernel_function
* Frama_c_kernel.Cil_types.kinstr
* string list
* string list) ->
prop_id
complete behaviors property. See Property
.ip_of_complete for more information
val mk_decrease_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.kinstr ->
Frama_c_kernel.Cil_types.variant ->
prop_id
val mk_lemma_id : LogicUsage.logic_lemma -> prop_id
axiom identification
val mk_stmt_assigns_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
string list ->
Frama_c_kernel.Cil_types.funbehavior ->
Frama_c_kernel.Cil_types.from list ->
prop_id option
val mk_loop_assigns_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
Frama_c_kernel.Cil_types.from list ->
prop_id option
val mk_fct_assigns_id :
Frama_c_kernel.Cil_types.kernel_function ->
bool ->
Frama_c_kernel.Cil_types.funbehavior ->
Frama_c_kernel.Cil_types.termination_kind ->
Frama_c_kernel.Cil_types.from list ->
prop_id option
function assigns The boolean indicate whether the function has exit node or not.
val mk_terminates_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.kinstr ->
Frama_c_kernel.Cil_types.identified_predicate ->
prop_id
val mk_call_pre_id :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Property.t ->
Frama_c_kernel.Property.t ->
prop_id
mk_call_pre_id called_kf s_call called_pre
val mk_property : Frama_c_kernel.Property.t -> prop_id
val mk_check : Frama_c_kernel.Property.t -> prop_id
type assigns_desc = private {
a_label : Clabels.c_label;
a_stmt : Frama_c_kernel.Cil_types.stmt option;
a_kind : a_kind;
a_assigns : Frama_c_kernel.Cil_types.assigns;
}
val pp_assigns_desc : Stdlib.Format.formatter -> assigns_desc -> unit
type assigns_info = prop_id * assigns_desc
val assigns_info_id : assigns_info -> prop_id
type assigns_full_info = private
| AssignsLocations of assigns_info
| AssignsAny of assigns_desc
| NoAssignsInfo
val empty_assigns_info : assigns_full_info
val mk_assigns_info : prop_id -> assigns_desc -> assigns_full_info
val mk_stmt_any_assigns_info :
Frama_c_kernel.Cil_types.stmt ->
assigns_full_info
val mk_kf_any_assigns_info : unit -> assigns_full_info
val mk_loop_any_assigns_info :
Frama_c_kernel.Cil_types.stmt ->
assigns_full_info
val pp_assign_info :
string ->
Stdlib.Format.formatter ->
assigns_full_info ->
unit
val merge_assign_info :
assigns_full_info ->
assigns_full_info ->
assigns_full_info
val mk_loop_assigns_desc :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.from list ->
assigns_desc
val mk_stmt_assigns_desc :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.from list ->
assigns_desc
val mk_stmt_assigns_any_desc : Frama_c_kernel.Cil_types.stmt -> assigns_desc
val mk_asm_assigns_desc : Frama_c_kernel.Cil_types.stmt -> assigns_desc
val mk_kf_assigns_desc : Frama_c_kernel.Cil_types.from list -> assigns_desc
val mk_init_assigns : assigns_desc
val is_call_assigns : assigns_desc -> bool
type axiom_info = prop_id * LogicUsage.logic_lemma
val mk_axiom_info : LogicUsage.logic_lemma -> axiom_info
val pp_axiom_info : Stdlib.Format.formatter -> axiom_info -> unit
type pred_info = prop_id * Frama_c_kernel.Cil_types.predicate
type variant_info = prop_id * Frama_c_kernel.Cil_types.variant
val mk_pred_info : prop_id -> Frama_c_kernel.Cil_types.predicate -> pred_info
val pp_pred_of_pred_info : Stdlib.Format.formatter -> pred_info -> unit
val pp_pred_info : Stdlib.Format.formatter -> pred_info -> unit
val split_bag :
(prop_id -> 'a -> unit) ->
prop_id ->
'a Frama_c_kernel.Bag.t ->
unit
mk_part pid (k, n)
build the identification for the k/n
part of pid
.
val parts_of_id : prop_id -> (int * int) option
get the 'part' information.
val subproofs : prop_id -> int
How many subproofs
val subproof_idx : prop_id -> int
subproof index of this propr_id
val get_induction : prop_id -> Frama_c_kernel.Cil_types.stmt option
val add_proof : proof -> prop_id -> Frama_c_kernel.Property.t list -> unit
accumulate in the proof the partial proof for this prop_id
val add_invalid_proof : proof -> unit
add an invalid proof result ; can not revert a complete proof
val is_composed : proof -> bool
whether a proof needs several lemma to be complete
val is_proved : proof -> bool
whether all partial proofs have been accumulated or not
val is_invalid : proof -> bool
whether an invalid proof result has been registered or not
val target : proof -> Frama_c_kernel.Property.t
val dependencies : proof -> Frama_c_kernel.Property.t list
val filter_status : prop_id -> bool