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

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.



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_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 !*)
type prop_id = {
   p_kind : prop_kind;
   p_prop : Property.t;
   p_part : (int * int) option;
}
Property.t information and kind of PO (establishment, preservation, etc)
val parts_of_id : prop_id -> (int * int) option
get the 'part' infomation.
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 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
exception Found of int
val num_of_bhv_from : ('a, Cil_types.identified_term) Cil_types.behavior ->
Cil_types.identified_term * 'b -> int
val mk_prop : prop_kind -> Property.t -> prop_id
val mk_check : Property.t -> prop_id
val mk_property : Property.t -> prop_id
val mk_annot_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> Property.identified_property
val mk_annot_ids : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation -> Property.identified_property list
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
val mk_bhv_from_id : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_term Cil_types.from -> prop_id
\from property of function or statement behavior assigns
val get_kind_for_tk : Kernel_function.t -> Cil_types.termination_kind -> prop_kind
val mk_fct_from_id : Kernel_function.t ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.identified_term Cil_types.from -> prop_id
val mk_disj_bhv_id : Cil_types.kernel_function * Cil_types.kinstr * string list ->
prop_id
disjoint behaviors property.
val mk_compl_bhv_id : Cil_types.kernel_function * Cil_types.kinstr * string list ->
prop_id
complete behaviors property.
val mk_decrease_id : Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.term Cil_types.variant -> prop_id
val mk_lemma_id : LogicUsage.logic_lemma -> prop_id
axiom identification
val mk_stmt_assigns_id : Cil_types.kernel_function ->
Cil_types.stmt ->
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 : Kernel_function.t ->
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 kind_order : prop_kind -> int
val compare_kind : prop_kind -> prop_kind -> int
val compare_prop_id : prop_id -> prop_id -> int
module PropId: Datatype.Make_with_collections(sig
type t = WpPropId.prop_id 
include Datatype.Undefined
val name : string
val reprs : WpPropId.prop_id list
val hash : WpPropId.prop_id -> int
val compare : WpPropId.prop_id -> WpPropId.prop_id -> int
val equal : WpPropId.prop_id -> WpPropId.prop_id -> bool
val copy : 'a -> 'b
val rehash : 'a -> 'a
val internal_pretty_code : 'a -> 'b
val pretty : 'a -> 'b
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
val varname : 'a -> 'b
end)
module Names: sig .. end
val get_propid : Names.IndexTbl.key -> Names.IndexTbl.data
Unique identifier of prop_id

Name related to a property PO
val pp_propid : Format.formatter -> Names.IndexTbl.key -> unit
Print unique id of prop_id
val pp_names : Format.formatter -> string list -> unit
val ident_names : string list -> string list
val code_annot_names : Cil_types.code_annotation -> string list
val user_prop_names : Property.identified_property -> string list
This is used to give the name of the property that the user can give to select it from the command line (-wp-prop option)
val string_of_termination_kind : Cil_types.termination_kind -> string
TODO: should probably be somewhere else
val label_of_kind : prop_kind -> string
val label_of_prop_id : prop_id -> string
Short description of the kind of PO
module Pretty: sig .. end
val pretty_local : Format.formatter -> prop_id -> unit
type hints = {
   mutable required : string list;
   mutable hints : string list;
}
val add_hint : hints -> string -> unit
val add_required : hints -> string -> unit
val stmt_hints : hints -> Cil_types.stmt -> unit
val kinstr_hints : hints -> Cil_types.kinstr -> unit
val propid_hints : hints -> prop_id -> unit
val term_hints : hints -> Cil_types.term -> unit
val lval_hints : hints -> Cil_types.term_lhost -> unit
val assigns_hints : hints -> (Cil_types.identified_term * 'a) list -> unit
val annot_hints : hints ->
('a, 'b Cil_types.named, 'c, Cil_types.identified_term) Cil_types.code_annot ->
unit
val property_hints : hints -> Property.identified_property -> unit
val prop_id_keys : prop_id -> String.t list * String.t list
val pp_goal_kind : Format.formatter -> prop_kind -> unit
val pp_goal_part : Format.formatter -> (int * int) option -> unit
val pretty : Format.formatter -> prop_id -> unit
val pretty_context : Description.kf -> Format.formatter -> prop_id -> unit
val is_check : prop_id -> bool
val is_assigns : prop_id -> bool
val is_requires : Property.identified_property -> 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_datatype.Stmt.t -> 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.
type a_kind = 
| LoopAssigns
| StmtAssigns
type effect_source = 
| FromCode
| FromCall
| FromReturn
type assigns_desc = {
   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 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_kf_assigns_desc : Cil_types.identified_term Cil_types.from list -> assigns_desc
val is_call_assigns : assigns_desc -> bool
val pp_assigns_desc : Format.formatter -> assigns_desc -> unit

2 kinds of annotations can be found : predicates and assigns. because assigns properties can only be translated into predicates by the memory model.
type pred_info = prop_id * Cil_types.predicate Cil_types.named 
val mk_pred_info : 'a -> 'b -> 'a * 'b
val pred_info_id : 'a * 'b -> 'a
val pp_pred_of_pred_info : Format.formatter -> 'a * Cil_types.predicate Cil_types.named -> unit
val pp_pred_info : Format.formatter ->
Names.IndexTbl.key * Cil_types.predicate Cil_types.named -> unit
type assigns_info = prop_id * assigns_desc 
val assigns_info_id : 'a * 'b -> 'a
type assigns_full_info = 
| 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
type axiom_info = prop_id * LogicUsage.logic_lemma 
val mk_axiom_info : LogicUsage.logic_lemma -> prop_id * LogicUsage.logic_lemma
val pp_axiom_info : Format.formatter ->
Names.IndexTbl.key * LogicUsage.logic_lemma -> unit
val _split : (prop_id -> 'a -> unit) -> prop_id -> 'a Bag.t -> unit

About proofs
val subproofs : prop_id -> int
How many subproofs
val subproof_idx : prop_id -> int
subproof index of this propr_id
val get_loop_stmt : Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt option
find the outer loop in which the stmt is.
val get_induction : prop_id -> Cil_types.stmt option
Quite don't understand what is going on here... what is it supposed to do ? 2011-07-07-Anne