Module Wp.WpPropIdSource

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.

Sourcetype prop_id

Property.t information and kind of PO (establishment, preservation, etc)

returns the annotation which lead to the given PO.

Sourceval doomed_if_valid : prop_id -> Frama_c_kernel.Property.t list

Properties that are False-if-unreachable in case the PO is valid.

Sourceval unreachable_if_valid : prop_id -> Frama_c_kernel.Property.other_loc

Stmt that is unreachable in case the PO is valid.

Sourceval compare_prop_id : prop_id -> prop_id -> int
Sourceval tactical : gid:string -> prop_id
Sourceval is_check : prop_id -> bool
Sourceval is_tactic : prop_id -> bool
Sourceval is_assigns : prop_id -> bool
Sourceval is_requires : Frama_c_kernel.Property.t -> bool
Sourceval is_loop_preservation : prop_id -> Frama_c_kernel.Cil_types.stmt option
Sourceval is_smoke_test : prop_id -> bool
Sourceval select_default : prop_id -> bool

test if the prop_id does not have a no_wp: in its name(s).

Sourceval select_by_name : string list -> prop_id -> bool

test if the prop_id has to be selected for the asked names.

Sourceval select_for_behaviors : string list -> prop_id -> bool

test if the prop_id has to be selected for the asked behavior names.

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

Sourceval ident_names : string list -> string list

From a list of names (of an identified terms), returns usable names.

Sourceval prop_id_keys : prop_id -> string list * string list
Sourceval get_propid : prop_id -> string

Unique identifier of prop_id

Sourceval pp_propid : Format.formatter -> prop_id -> unit

Print unique id of prop_id

Sourceval user_pred_names : Frama_c_kernel.Cil_types.toplevel_predicate -> string list
Sourceval user_bhv_names : Frama_c_kernel.Property.identified_property -> string list
Sourceval user_prop_names : Frama_c_kernel.Property.identified_property -> string list
Sourceval are_selected_names : string list -> string list -> bool

are_selected_names asked names checks if names of a property are selected according to asked names.

Sourceval pretty : Format.formatter -> prop_id -> unit
Sourceval pretty_local : Format.formatter -> prop_id -> unit
Sourceval label_of_prop_id : prop_id -> string

Short description of the kind of PO

Sourceval string_of_termination_kind : Frama_c_kernel.Cil_types.termination_kind -> string

TODO: should probably be somewhere else

Sourceval 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

Invariant establishment and preservation

Invariant establishment and preservation, in this order

Invariant used as hypothesis

Variant decrease

Variant positive

Variant for

\from property of loop assigns. Must not be FromAny

\from property of function or statement behavior assigns. Must not be FromAny

\from property of function behavior assigns. Must not be FromAny. The boolean indicate whether the function has exit node or not.

Sourceval 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

Sourceval 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

axiom identification

function assigns The boolean indicate whether the function has exit node or not.

Sourceval mk_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id
Sourceval mk_stmt_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id
Sourceval mk_fct_post_id : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.funbehavior -> (Frama_c_kernel.Cil_types.termination_kind * Frama_c_kernel.Cil_types.identified_predicate) -> prop_id

mk_call_pre_id called_kf s_call called_pre

Sourcetype a_kind =
  1. | LoopAssigns
  2. | StmtAssigns
Sourcetype assigns_desc = private {
  1. a_label : Clabels.c_label;
  2. a_stmt : Frama_c_kernel.Cil_types.stmt option;
  3. a_kind : a_kind;
  4. a_assigns : Frama_c_kernel.Cil_types.assigns;
}
Sourceval pp_assigns_desc : Format.formatter -> assigns_desc -> unit
Sourcetype assigns_info = prop_id * assigns_desc
Sourceval assigns_info_id : assigns_info -> prop_id
Sourcetype assigns_full_info = private
  1. | AssignsLocations of assigns_info
  2. | AssignsAny of assigns_desc
  3. | NoAssignsInfo
Sourceval empty_assigns_info : assigns_full_info
Sourceval mk_assigns_info : prop_id -> assigns_desc -> assigns_full_info
Sourceval mk_stmt_any_assigns_info : Frama_c_kernel.Cil_types.stmt -> assigns_full_info
Sourceval mk_kf_any_assigns_info : unit -> assigns_full_info
Sourceval mk_loop_any_assigns_info : Frama_c_kernel.Cil_types.stmt -> assigns_full_info
Sourceval pp_assign_info : string -> Format.formatter -> assigns_full_info -> unit
Sourceval mk_stmt_assigns_any_desc : Frama_c_kernel.Cil_types.stmt -> assigns_desc
Sourceval mk_kf_assigns_desc : Frama_c_kernel.Cil_types.from list -> assigns_desc
Sourceval mk_init_assigns : assigns_desc
Sourceval is_call_assigns : assigns_desc -> bool
Sourceval pp_axiom_info : Format.formatter -> axiom_info -> unit
Sourceval pred_info_id : pred_info -> prop_id
Sourceval pp_pred_of_pred_info : Format.formatter -> pred_info -> unit
Sourceval pp_pred_info : Format.formatter -> pred_info -> unit
Sourceval split_bag : (prop_id -> 'a -> unit) -> prop_id -> 'a Frama_c_kernel.Bag.t -> unit
Sourceval split_map : (prop_id -> 'a -> 'b) -> prop_id -> 'a list -> 'b list
Sourceval mk_part : prop_id -> (int * int) -> prop_id

mk_part pid (k, n) build the identification for the k/n part of pid.

Sourceval parts_of_id : prop_id -> (int * int) option

get the 'part' information.

Sourceval subproofs : prop_id -> int

How many subproofs

Sourceval subproof_idx : prop_id -> int

subproof index of this propr_id

Sourceval get_induction : prop_id -> Frama_c_kernel.Cil_types.stmt option
Sourcetype proof

A proof accumulator for a set of related prop_id

Sourceval create_proof : prop_id -> proof

to be used only once for one of the related prop_id

Sourceval add_proof : proof -> prop_id -> Frama_c_kernel.Property.t list -> unit

accumulate in the proof the partial proof for this prop_id

Sourceval add_invalid_proof : proof -> unit

add an invalid proof result ; can not revert a complete proof

Sourceval is_composed : proof -> bool

whether a proof needs several lemma to be complete

Sourceval is_proved : proof -> bool

whether all partial proofs have been accumulated or not

Sourceval is_invalid : proof -> bool

whether an invalid proof result has been registered or not

Sourceval dependencies : proof -> Frama_c_kernel.Property.t list
Sourceval filter_status : prop_id -> bool