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_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 |
(* |
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 : |
|
p_prop : |
|
p_part : |
val parts_of_id : prop_id -> (int * int) option
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
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
val mk_preserve_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
val mk_inv_hyp_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
val mk_var_decr_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
val mk_var_pos_id : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> prop_id
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
val mk_bhv_from_id : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_term Cil_types.from -> prop_id
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
val mk_compl_bhv_id : Cil_types.kernel_function * Cil_types.kinstr * string list ->
prop_id
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
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
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
typet =
WpPropId.prop_id
include Datatype.Undefinedval 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 : prop_id -> string
prop_id
val pp_propid : Format.formatter -> prop_id -> unit
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
val string_of_termination_kind : Cil_types.termination_kind -> string
val label_of_kind : prop_kind -> string
val label_of_prop_id : prop_id -> string
module Pretty:sig
..end
val pretty_local : Format.formatter -> prop_id -> unit
type
hints = {
|
mutable required : |
|
mutable hints : |
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
val select_call_pre : Cil_datatype.Stmt.t -> Property.t option -> prop_id -> bool
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 : |
|
a_stmt : |
|
a_kind : |
|
a_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_init_assigns : 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
typepred_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 ->
prop_id * Cil_types.predicate Cil_types.named -> unit
typeassigns_info =
prop_id * assigns_desc
val assigns_info_id : 'a * 'b -> 'a
type
assigns_full_info =
| |
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 -> Format.formatter -> assigns_full_info -> unit
val merge_assign_info : assigns_full_info ->
assigns_full_info -> assigns_full_info
typeaxiom_info =
prop_id * LogicUsage.logic_lemma
val mk_axiom_info : LogicUsage.logic_lemma -> prop_id * LogicUsage.logic_lemma
val pp_axiom_info : Format.formatter -> prop_id * LogicUsage.logic_lemma -> unit
val _split : (prop_id -> 'a -> unit) -> prop_id -> 'a Bag.t -> unit
val subproofs : prop_id -> int
val subproof_idx : prop_id -> int
val get_loop_stmt : Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt option
val get_induction : prop_id -> Cil_types.stmt option
2011-07-07-Anne