Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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.

type prop_id

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

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 compare_prop_id : prop_id -> prop_id -> int
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.

val ident_names : string list -> string list

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

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

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_lemma_id : LogicUsage.logic_lemma -> prop_id

axiom identification

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

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

val mk_property : Frama_c_kernel.Property.t -> prop_id
type a_kind =
  1. | LoopAssigns
  2. | StmtAssigns
type 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;
}
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
  1. | AssignsLocations of assigns_info
  2. | AssignsAny of assigns_desc
  3. | 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 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
val pred_info_id : pred_info -> prop_id
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
val split_map : (prop_id -> 'a -> 'b) -> prop_id -> 'a list -> 'b list
val mk_part : prop_id -> (int * int) -> prop_id

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

A proof accumulator for a set of related prop_id

val create_proof : prop_id -> proof

to be used only once for one of the related prop_id

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 dependencies : proof -> Frama_c_kernel.Property.t list
val filter_status : prop_id -> bool