Wp.CfgAnnot
Normalization of Annotations.
Labels are renamed wrt NormAtLabels and reorganized for use/prove dispatching in CfgCalculus
.
type behavior = {
bhv_assumes : WpPropId.pred_info list; |
bhv_requires : WpPropId.pred_info list; |
bhv_smokes : WpPropId.pred_info list; |
bhv_ensures : WpPropId.pred_info list; |
bhv_exits : WpPropId.pred_info list; |
bhv_post_assigns : WpPropId.assigns_full_info; |
bhv_exit_assigns : WpPropId.assigns_full_info; |
}
val get_requires :
goal:bool ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.funbehavior ->
WpPropId.pred_info list
val get_preconditions :
goal:bool ->
Frama_c_kernel.Cil_types.kernel_function ->
WpPropId.pred_info list
val get_behavior_goals :
Frama_c_kernel.Cil_types.kernel_function ->
?smoking:bool ->
?exits:bool ->
Frama_c_kernel.Cil_types.funbehavior ->
behavior
val get_complete_behaviors :
Frama_c_kernel.Cil_types.kernel_function ->
WpPropId.pred_info list
val get_disjoint_behaviors :
Frama_c_kernel.Cil_types.kernel_function ->
WpPropId.pred_info list
val get_terminates_goal :
Frama_c_kernel.Cil_types.kernel_function ->
WpPropId.pred_info option
val get_decreases_goal :
Frama_c_kernel.Cil_types.kernel_function ->
WpPropId.variant_info option
type code_assertion = {
code_admitted : WpPropId.pred_info option; |
code_verified : WpPropId.pred_info option; |
}
val get_code_assertions :
?smoking:bool ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
code_assertion list
val get_unreachable :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
WpPropId.prop_id
val get_stmt_assigns :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
WpPropId.assigns_full_info list
type loop_invariant = {
loop_hyp : loop_hypothesis; |
loop_est : WpPropId.prop_id option; |
loop_ind : WpPropId.prop_id option; |
loop_pred : Frama_c_kernel.Cil_types.predicate; |
}
type loop_contract = {
loop_terminates : Frama_c_kernel.Cil_types.predicate option; | |
loop_invariants : loop_invariant list; | (* to be proved after loop invariants *) |
loop_smoke : WpPropId.pred_info list; | (* assigned by loop body *) |
loop_assigns : WpPropId.assigns_full_info list; |
}
val get_loop_contract :
?smoking:bool ->
?terminates:Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
loop_contract
val mk_variant_properties :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.code_annotation ->
Frama_c_kernel.Cil_types.term ->
WpPropId.pred_info * WpPropId.pred_info
type contract = {
contract_cond : WpPropId.pred_info list; |
contract_hpre : WpPropId.pred_info list; |
contract_post : WpPropId.pred_info list; |
contract_exit : WpPropId.pred_info list; |
contract_smoke : WpPropId.pred_info list; |
contract_assigns : Frama_c_kernel.Cil_types.assigns; |
contract_terminates : bool * Frama_c_kernel.Cil_types.predicate; |
contract_decreases : Frama_c_kernel.Cil_types.variant option; |
}
val get_call_contract :
?smoking:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.stmt ->
contract