Module Wp.WpPropId

module WpPropId: sig .. end


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 -> Property.t
returns the annotation which lead to the given PO. Dynamically exported.
val source_of_id : prop_id -> Lexing.position
module PropId: Datatype.S  with type t = prop_id
val compare_prop_id : prop_id -> prop_id -> int
val is_check : prop_id -> bool
val is_assigns : prop_id -> bool
val is_requires : Property.t -> bool
val is_loop_preservation : prop_id -> Cil_types.stmt option
val select_by_name : string list -> prop_id -> bool
test if the prop_id has to be selected for the asked name. Also returns a debug message to explain then answer.
val select_call_pre : Cil_types.stmt -> Property.t option -> prop_id -> bool
test if the prop_id has to be selected when we want to select the call precondition the the stmt call (None means all the call preconditions). Also returns a debug message to explain then answer.
val prop_id_keys : prop_id -> string list * string list
val get_propid : prop_id -> string
Unique identifier of prop_id
val pp_propid : Format.formatter -> prop_id -> unit
Print unique id of prop_id
type prop_kind = 
| PKCheck (*
internal check
*)
| PKProp (*
normal property
*)
| PKEstablished (*
computation related to a loop property before the loop.
*)
| PKPreserved (*
computation related to a loop property inside the loop.
*)
| PKPropLoop (*
loop property used as hypothesis inside a loop.
*)
| PKVarDecr (*
computation related to the decreasing of a variant in a loop
*)
| PKVarPos (*
computation related to a loop variant being positive
*)
| PKAFctOut (*
computation related to the function assigns on normal termination
*)
| PKAFctExit (*
computation related to the function assigns on exit termination
*)
| PKPre of Cil_types.kernel_function * Cil_types.stmt * Property.t (*
precondition for function at stmt, property of the require. Many information that should come from the p_prop part of the prop_id, but in the PKPre case, it seems that it is hiden in a IPBlob property !
*)
val pretty : Format.formatter -> prop_id -> unit
val pretty_context : Description.kf -> Format.formatter -> prop_id -> unit
val pretty_local : 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 : Cil_types.termination_kind -> string
TODO: should probably be somewhere else
val num_of_bhv_from : Cil_types.funbehavior -> Cil_types.identified_term Cil_types.from -> int
val mk_code_annot_ids : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id list
val mk_assert_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
val mk_establish_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
Invariant establishment
val mk_preserve_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
Invariant preservation
val mk_inv_hyp_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
Invariant used as hypothesis
val mk_var_decr_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
Variant decrease
val mk_var_pos_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
Variant positive
val mk_loop_from_id : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.identified_term Cil_types.from -> prop_id
\from property of loop assigns. Must not be FromAny
val mk_bhv_from_id : Cil_types.kernel_function ->
Cil_types.kinstr ->
string list ->
Cil_types.funbehavior ->
Cil_types.identified_term Cil_types.from -> prop_id
\from property of function or statement behavior assigns. Must not be FromAny
val mk_fct_from_id : Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.identified_term Cil_types.from -> prop_id
\from property of function behavior assigns. Must not be FromAny.
val mk_disj_bhv_id : Cil_types.kernel_function * 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 : Cil_types.kernel_function * Cil_types.kinstr * string list * string list ->
prop_id
complete behaviors property. See Property.ip_of_complete for more information
val mk_decrease_id : Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.term Cil_types.variant -> prop_id
val mk_lemma_id : Wp.LogicUsage.logic_lemma -> prop_id
axiom identification
val mk_stmt_assigns_id : Cil_types.kernel_function ->
Cil_types.stmt ->
string list ->
Cil_types.funbehavior ->
Cil_types.identified_term Cil_types.from list -> prop_id option
val mk_loop_assigns_id : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.identified_term Cil_types.from list -> prop_id option
val mk_fct_assigns_id : Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.identified_term Cil_types.from list -> prop_id option
function assigns
val mk_pre_id : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_predicate -> 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 ->
prop_id
val mk_fct_post_id : Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind * Cil_types.identified_predicate ->
prop_id
val mk_call_pre_id : Cil_types.kernel_function ->
Cil_types.stmt -> Property.t -> Property.t -> prop_id
mk_call_pre_id called_kf s_call called_pre
val mk_property : Property.t -> prop_id
val mk_check : Property.t -> prop_id
type a_kind = 
| LoopAssigns
| StmtAssigns
type assigns_desc = private {
   a_label : Cil_types.logic_label;
   a_stmt : Cil_types.stmt option;
   a_kind : a_kind;
   a_assigns : Cil_types.identified_term Cil_types.assigns;
}
val pp_assigns_desc : Format.formatter -> assigns_desc -> unit
type effect_source = 
| FromCode
| FromCall
| FromReturn
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 : Cil_types.stmt -> assigns_full_info
val mk_kf_any_assigns_info : unit -> assigns_full_info
val mk_loop_any_assigns_info : Cil_types.stmt -> assigns_full_info
val pp_assign_info : string -> Format.formatter -> assigns_full_info -> unit
val merge_assign_info : assigns_full_info ->
assigns_full_info -> assigns_full_info
val mk_loop_assigns_desc : Cil_types.stmt ->
Cil_types.identified_term Cil_types.from list -> assigns_desc
val mk_stmt_assigns_desc : Cil_types.stmt ->
Cil_types.identified_term Cil_types.from list -> assigns_desc
val mk_asm_assigns_desc : Cil_types.stmt -> assigns_desc
val mk_kf_assigns_desc : Cil_types.identified_term Cil_types.from list -> assigns_desc
val mk_init_assigns : assigns_desc
val is_call_assigns : assigns_desc -> bool
type axiom_info = prop_id * Wp.LogicUsage.logic_lemma 
val mk_axiom_info : Wp.LogicUsage.logic_lemma -> axiom_info
val pp_axiom_info : Format.formatter -> axiom_info -> unit
type pred_info = prop_id * Cil_types.predicate 
val mk_pred_info : prop_id -> Cil_types.predicate -> pred_info
val pred_info_id : pred_info -> prop_id
val pp_pred_of_pred_info : Format.formatter -> pred_info -> unit
val pp_pred_info : Format.formatter -> pred_info -> unit
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 kind_of_id : prop_id -> prop_kind
get the 'kind' information.
val parts_of_id : prop_id -> (int * int) option
get the 'part' infomation.
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 -> Cil_types.stmt option