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 -> Filepath.position
module PropId: Datatype.S  with type t = prop_id
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 : Property.t -> bool
val is_loop_preservation : prop_id -> Cil_types.stmt option
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 name. Also returns a debug message to explain then answer. Includes a test for no_wp:.

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 get_legacy : prop_id -> string

Unique legacy identifier of prop_id

val pp_propid : Stdlib.Format.formatter -> prop_id -> unit

Print unique id of prop_id

type prop_kind = 
| PKTactic (*

tactical sub-goal

*)
| 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 hidden in a IPBlob property !

*)
val pretty : Stdlib.Format.formatter -> prop_id -> unit
val pretty_context : 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 : Cil_types.termination_kind -> string

TODO: should probably be somewhere else

val num_of_bhv_from : Cil_types.funbehavior -> 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_loop_inv_id : Cil_types.kernel_function ->
Cil_types.stmt ->
established:bool -> Cil_types.code_annotation -> prop_id

Invariant establishment and 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.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.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.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.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.from list -> prop_id option
val mk_loop_assigns_id : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
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.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 : Wp.Clabels.c_label;
   a_stmt : Cil_types.stmt option;
   a_kind : a_kind;
   a_assigns : Cil_types.assigns;
}
val pp_assigns_desc : Stdlib.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 -> 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 : Cil_types.stmt -> Cil_types.from list -> assigns_desc
val mk_stmt_assigns_desc : Cil_types.stmt -> Cil_types.from list -> assigns_desc
val mk_asm_assigns_desc : Cil_types.stmt -> assigns_desc
val mk_kf_assigns_desc : 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 : Stdlib.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 : Stdlib.Format.formatter -> pred_info -> unit
val pp_pred_info : Stdlib.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' 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 -> Cil_types.stmt option