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 tactical sub-goal | *) |
| |
PKCheck |
(* | internal check internal check | *) |
| |
PKProp |
(* | normal property normal property | *) |
| |
PKEstablished |
(* | computation related to a loop property before the loop. computation related to a loop property before the loop. | *) |
| |
PKPreserved |
(* | computation related to a loop property inside the loop. computation related to a loop property inside the loop. | *) |
| |
PKPropLoop |
(* | loop property used as hypothesis inside a loop. loop property used as hypothesis inside a loop. | *) |
| |
PKVarDecr |
(* | computation related to the decreasing of a variant in a loop computation related to the decreasing of a variant in a loop | *) |
| |
PKVarPos |
(* | computation related to a loop variant being positive computation related to a loop variant being positive | *) |
| |
PKAFctOut |
(* | computation related to the function assigns on normal termination computation related to the function assigns on normal termination | *) |
| |
PKAFctExit |
(* | computation related to the function assigns on exit termination computation related to the function assigns on exit termination | *) |
| |
PKPre of |
(* | 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 ! 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 : 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 : |
|
a_stmt : |
|
a_kind : |
|
a_assigns : |
val pp_assigns_desc : Stdlib.Format.formatter -> assigns_desc -> unit
type
effect_source =
| |
FromCode |
| |
FromCall |
| |
FromReturn |
typeassigns_info =
prop_id * assigns_desc
val assigns_info_id : assigns_info -> prop_id
type
assigns_full_info = private
| |
AssignsLocations of |
| |
AssignsAny of |
| |
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
typeaxiom_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
typepred_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
Quite don't understand what is going on here... what is it supposed to do ?
2011-07-07-Anne