Module `Wp.WpPropId`Source

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)

Sourceval property_of_id : prop_id -> Frama_c_kernel.Property.t

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 source_of_id : prop_id -> Frama_c_kernel.Filepath.position

Sourcemodule PropId : Frama_c_kernel.Datatype.S with type t = prop_id

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.

Source

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.

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

Source

val user_pred_names : 
  Frama_c_kernel.Cil_types.toplevel_predicate ->
  string list

Sourceval user_bhv_names : Frama_c_kernel.Property.identified_property -> string list

Source

val 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

Source

val pretty_context : 
  Frama_c_kernel.Description.kf ->
  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

Source

val string_of_termination_kind : 
  Frama_c_kernel.Cil_types.termination_kind ->
  string

TODO: should probably be somewhere else

Source

val num_of_bhv_from : 
  Frama_c_kernel.Cil_types.funbehavior ->
  Frama_c_kernel.Cil_types.from ->
  int

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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.

Source

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

Source

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

Source

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

Sourceval mk_lemma_id : LogicUsage.logic_lemma -> prop_id

axiom identification

Source

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

Source

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

Source

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.

Source

val mk_pre_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.identified_predicate ->
  prop_id

Source

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

Source

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

Source

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

Source

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

Source

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

Sourceval mk_property : Frama_c_kernel.Property.t -> prop_id

Sourceval mk_check : Frama_c_kernel.Property.t -> prop_id

Sourcetype a_kind =

| LoopAssigns
| StmtAssigns

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

}

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

| AssignsLocations of assigns_info
| AssignsAny of assigns_desc
| NoAssignsInfo

Sourceval empty_assigns_info : assigns_full_info

Sourceval mk_assigns_info : prop_id -> assigns_desc -> assigns_full_info

Source

val mk_stmt_any_assigns_info : 
  Frama_c_kernel.Cil_types.stmt ->
  assigns_full_info

Sourceval mk_kf_any_assigns_info : unit -> assigns_full_info

Source

val 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

Source

val merge_assign_info : 
  assigns_full_info ->
  assigns_full_info ->
  assigns_full_info

Source

val mk_loop_assigns_desc : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.from list ->
  assigns_desc

Source

val mk_stmt_assigns_desc : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.from list ->
  assigns_desc

Sourceval mk_stmt_assigns_any_desc : Frama_c_kernel.Cil_types.stmt -> assigns_desc

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

Sourcetype axiom_info = prop_id * LogicUsage.logic_lemma

Sourceval mk_axiom_info : LogicUsage.logic_lemma -> axiom_info

Sourceval pp_axiom_info : Format.formatter -> axiom_info -> unit

Sourcetype pred_info = prop_id * Frama_c_kernel.Cil_types.predicate

Sourcetype variant_info = prop_id * Frama_c_kernel.Cil_types.variant

Sourceval mk_pred_info : prop_id -> Frama_c_kernel.Cil_types.predicate -> pred_info

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

Source

val 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 target : proof -> Frama_c_kernel.Property.t

Sourceval dependencies : proof -> Frama_c_kernel.Property.t list

Sourceval filter_status : prop_id -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/WpPropId/index.html

Module `Wp.WpPropId`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/WpPropId/index.html

Module Wp.WpPropIdSource

Module `Wp.WpPropId`Source