Module Wp.CfgAnnotSource

Normalization of Annotations.

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

Sourcetype 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;
}
Sourceval get_preconditions : goal:bool -> Frama_c_kernel.Cil_types.kernel_function -> WpPropId.pred_info list
Sourceval get_behavior_goals : Frama_c_kernel.Cil_types.kernel_function -> ?smoking:bool -> ?exits:bool -> Frama_c_kernel.Cil_types.funbehavior -> behavior
Sourcetype code_assertion = {
  1. code_admitted : WpPropId.pred_info option;
  2. code_verified : WpPropId.pred_info option;
}
Sourcetype loop_hypothesis =
  1. | NoHyp
  2. | Check of WpPropId.prop_id
  3. | Always of WpPropId.prop_id
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourceval clear : unit -> unit