Frama-C API - 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