Frama-C:
Plug-ins:
Libraries:

Frama-C API - CfgAnnot

Normalization of Annotations.

Labels are renamed wrt NormAtLabels and reorganized for use/prove dispatching in CfgCalculus.

type behavior = {
  1. bhv_assumes : WpPropId.pred_info list;
  2. bhv_requires : WpPropId.pred_info list;
  3. bhv_smokes : WpPropId.pred_info list;
  4. bhv_ensures : WpPropId.pred_info list;
  5. bhv_exits : WpPropId.pred_info list;
  6. bhv_post_assigns : WpPropId.assigns_full_info;
  7. bhv_exit_assigns : WpPropId.assigns_full_info;
}
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
type code_assertion = {
  1. code_admitted : WpPropId.pred_info option;
  2. 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
type loop_hypothesis =
  1. | NoHyp
  2. | Check of WpPropId.prop_id
  3. | Always of WpPropId.prop_id
type loop_invariant = {
  1. loop_hyp : loop_hypothesis;
  2. loop_est : WpPropId.prop_id option;
  3. loop_ind : WpPropId.prop_id option;
  4. loop_pred : Frama_c_kernel.Cil_types.predicate;
}
type loop_contract = {
  1. loop_terminates : Frama_c_kernel.Cil_types.predicate option;
  2. loop_invariants : loop_invariant list;
    (*

    to be proved after loop invariants

    *)
  3. loop_smoke : WpPropId.pred_info list;
    (*

    assigned by loop body

    *)
  4. loop_assigns : WpPropId.assigns_full_info list;
}
type contract = {
  1. contract_cond : WpPropId.pred_info list;
  2. contract_hpre : WpPropId.pred_info list;
  3. contract_post : WpPropId.pred_info list;
  4. contract_exit : WpPropId.pred_info list;
  5. contract_smoke : WpPropId.pred_info list;
  6. contract_assigns : Frama_c_kernel.Cil_types.assigns;
  7. contract_terminates : bool * Frama_c_kernel.Cil_types.predicate;
  8. contract_decreases : Frama_c_kernel.Cil_types.variant option;
}
val clear : unit -> unit